From b72a3c69b67daec88a9160a8a96f1e4ad20c5eef Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 24 Nov 2020 14:58:45 -0800 Subject: [PATCH] fix: ambiguity at `induction/cases` See efc3a320fe --- doc/tactics.md | 4 ++-- lean4-mode/lean4-syntax.el | 2 +- src/Init/Classical.lean | 2 +- src/Init/Data/Array/Basic.lean | 6 ++--- src/Init/Data/List/Basic.lean | 8 +++---- src/Init/Data/Nat/Basic.lean | 6 ++--- src/Init/Notation.lean | 2 +- src/Init/WF.lean | 36 ++++++++++++++--------------- src/Lean/Elab/Tactic/Induction.lean | 5 +--- tests/lean/hygienicIntro.lean | 4 ++-- tests/lean/inductionErrors.lean | 22 +++++++++--------- tests/lean/run/casesUsing.lean | 26 ++++++++++----------- tests/lean/run/concatElim.lean | 2 +- tests/lean/run/induction1.lean | 28 +++++++++++----------- tests/lean/run/inj2.lean | 4 ++-- tests/lean/run/tacticTests.lean | 24 +++++++++---------- tests/lean/run/where1.lean | 2 +- tests/lean/unsolvedIndCases.lean | 10 ++++---- 18 files changed, 95 insertions(+), 98 deletions(-) diff --git a/doc/tactics.md b/doc/tactics.md index e288365a43..a7d4fa45c8 100644 --- a/doc/tactics.md +++ b/doc/tactics.md @@ -31,7 +31,7 @@ The tactic `assumption` tries to fill a hole by searching the local context for ```lean theorem ex1 : p ∨ q → q ∨ p := by intro h - cases h + cases h with | inl h1 => apply Or.inr exact h1 @@ -172,7 +172,7 @@ theorem Nat.mod.inductionOn -/ theorem ex (x : Nat) {y : Nat} (h : y > 0) : x % y < y := by - induction x, y using Nat.mod.inductionOn generalizing h + induction x, y using Nat.mod.inductionOn generalizing h with | ind x y h₁ ih => rw [Nat.modEqSubMod h₁.2] exact ih h diff --git a/lean4-mode/lean4-syntax.el b/lean4-mode/lean4-syntax.el index a2d3a90018..c284152e39 100644 --- a/lean4-mode/lean4-syntax.el +++ b/lean4-mode/lean4-syntax.el @@ -20,7 +20,7 @@ "try" "catch" "finally" "where" "rec" "mut" "forall" "fun" "exists" "if" "then" "else" "from" "init_quot" "return" "mutual" "def" "run_cmd" "declare_syntax_cat" "syntax" "macro_rules" "macro" - "initialize" "builtin_initialize") + "initialize" "builtin_initialize" "induction" "cases" "generalizing") "lean keywords ending with 'word' (not symbol)") (defconst lean4-keywords1-regexp (eval `(rx word-start (or ,@lean4-keywords1) word-end))) diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean index ae3801a2b0..4ffe96d675 100644 --- a/src/Init/Classical.lean +++ b/src/Init/Classical.lean @@ -114,7 +114,7 @@ theorem skolem {α : Sort u} {b : α → Sort v} {p : ∀ x, b x → Prop} : ( ⟨axiomOfChoice, fun ⟨f, hw⟩ (x) => ⟨f x, hw x⟩⟩ theorem propComplete (a : Prop) : a = True ∨ a = False := by - cases em a + cases em a with | inl _ => apply Or.inl; apply propext; apply Iff.intro; { intros; apply True.intro }; { intro; assumption } | inr hn => apply Or.inr; apply propext; apply Iff.intro; { intro h; exact hn h }; { intro h; apply False.elim h } diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 895a744038..b053277356 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -570,13 +570,13 @@ theorem ext (a b : Array α) (h₁ : a.length = b.length) (h₂ : (i : Nat) → (hi₁ : i < a.length) → (hi₂ : i < b.length) → a.get i hi₁ = b.get i hi₂) : a = b := by - induction a generalizing b + induction a generalizing b with | nil => - cases b + cases b with | nil => rfl | cons b bs => rw [List.lengthConsEq] at h₁; injection h₁ | cons a as ih => - cases b + cases b with | nil => rw [List.lengthConsEq] at h₁; injection h₁ | cons b bs => have hz₁ : 0 < (a::as).length by rw [List.lengthConsEq]; apply Nat.zeroLtSucc diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index 2983648c5d..453b3dd72d 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -336,7 +336,7 @@ def dropLast {α} : List α → List α def lengthReplicateEq {α} (n : Nat) (a : α) : (replicate n a).length = n := let rec aux (n : Nat) (as : List α) : (replicate.loop a n as).length = n + as.length := by - induction n generalizing as + induction n generalizing as with | zero => rw [Nat.zeroAdd]; rfl | succ n ih => show length (replicate.loop a n (a::as)) = Nat.succ n + length as @@ -345,7 +345,7 @@ def lengthReplicateEq {α} (n : Nat) (a : α) : (replicate n a).length = n := aux n [] def lengthConcatEq {α} (as : List α) (a : α) : (concat as a).length = as.length + 1 := by - induction as + induction as with | nil => rfl | cons x xs ih => show length (x :: concat xs a) = length (x :: xs) + 1 @@ -353,10 +353,10 @@ def lengthConcatEq {α} (as : List α) (a : α) : (concat as a).length = as.leng rfl def lengthSetEq {α} (as : List α) (i : Nat) (a : α) : (as.set i a).length = as.length := by - induction as generalizing i + induction as generalizing i with | nil => rfl | cons x xs ih => - cases i + cases i with | zero => rfl | succ i => show length (x :: set xs i a) = length (x :: xs) diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean index 5ddf01a653..46a336452e 100644 --- a/src/Init/Data/Nat/Basic.lean +++ b/src/Init/Data/Nat/Basic.lean @@ -164,12 +164,12 @@ protected theorem subZero (n : Nat) : n - 0 = n := rfl theorem succSubSuccEqSub (n m : Nat) : succ n - succ m = n - m := by - induction m + induction m with | zero => exact rfl | succ m ih => apply congrArg pred ih theorem notSuccLeSelf (n : Nat) : ¬succ n ≤ n := by - induction n + induction n with | zero => intro h; apply notSuccLeZero 0 h | succ n ih => intro h; exact ih (leOfSuccLeSucc h) @@ -185,7 +185,7 @@ theorem predLt : ∀ {n : Nat}, n ≠ 0 → pred n < n | succ n, h => ltSuccOfLe (Nat.leRefl _) theorem subLe (n m : Nat) : n - m ≤ n := by - induction m + induction m with | zero => exact Nat.leRefl (n - 0) | succ m ih => apply Nat.leTrans (predLe (n - m)) ih diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index 07c16ce7fb..b92d29c879 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -165,7 +165,7 @@ syntax[«let!»] "let! " letDecl : tactic syntax[letrec] withPosition(atomic(group("let " &"rec ")) letRecDecls) : tactic syntax inductionAlt := (ident <|> "_") (ident <|> "_")* " => " (hole <|> syntheticHole <|> tacticSeq) -syntax inductionAlts := withPosition("| " sepBy1(inductionAlt, colGe "| ")) +syntax inductionAlts := "with " withPosition("| " sepBy1(inductionAlt, colGe "| ")) syntax[induction] "induction " sepBy1(term, ", ") (" using " ident)? ("generalizing " ident+)? (inductionAlts)? : tactic syntax casesTarget := atomic(ident " : ")? term syntax[cases] "cases " sepBy1(casesTarget, ", ") (" using " ident)? (inductionAlts)? : tactic diff --git a/src/Init/WF.lean b/src/Init/WF.lean index 8fd7a49c9d..fd815d8aaf 100644 --- a/src/Init/WF.lean +++ b/src/Init/WF.lean @@ -50,7 +50,7 @@ section variables {α : Sort u} {r : α → α → Prop} (hwf : WellFounded r) theorem recursion {C : α → Sort v} (a : α) (h : ∀ x, (∀ y, r y x → C y) → C x) : C a := by - induction (apply hwf a) + induction (apply hwf a) with | intro x₁ ac₁ ih => exact h x₁ ih theorem induction {C : α → Prop} (a : α) (h : ∀ x, (∀ y, r y x → C y) → C x) : C a := @@ -60,11 +60,11 @@ variable {C : α → Sort v} variable (F : ∀ x, (∀ y, r y x → C y) → C x) def fixF (x : α) (a : Acc r x) : C x := by - induction a + induction a with | intro x₁ ac₁ ih => exact F x₁ ih def fixFEq (x : α) (acx : Acc r x) : fixF F x acx = F x (fun (y : α) (p : r y x) => fixF F y (Acc.inv acx p)) := by - induction acx + induction acx with | intro x r ih => exact rfl end @@ -96,7 +96,7 @@ namespace Subrelation variables {α : Sort u} {r q : α → α → Prop} def accessible {a : α} (h₁ : Subrelation q r) (ac : Acc r a) : Acc q a := by - induction ac + induction ac with | intro x ax ih => apply Acc.intro intro y h @@ -111,7 +111,7 @@ namespace InvImage variables {α : Sort u} {β : Sort v} {r : β → β → Prop} private def accAux (f : α → β) {b : β} (ac : Acc r b) : (x : α) → f x = b → Acc (InvImage r f) x := by - induction ac + induction ac with | intro x acx ih => intro z e apply Acc.intro @@ -131,11 +131,11 @@ namespace TC variables {α : Sort u} {r : α → α → Prop} def accessible {z : α} (ac : Acc r z) : Acc (TC r) z := by - induction ac + induction ac with | intro x acx ih => apply Acc.intro x intro y rel - induction rel generalizing acx ih + induction rel generalizing acx ih with | base a b rab => exact ih a rab | trans a b c rab rbc ih₁ ih₂ => apply Acc.inv (ih₂ acx ih) rab @@ -147,7 +147,7 @@ end TC def Nat.ltWf : WellFounded Nat.lt := by apply WellFounded.intro intro n - induction n + induction n with | zero => apply Acc.intro 0 intro _ h @@ -201,13 +201,13 @@ variables {α : Type u} {β : Type v} variables {ra : α → α → Prop} {rb : β → β → Prop} def lexAccessible (aca : (a : α) → Acc ra a) (acb : (b : β) → Acc rb b) (a : α) (b : β) : Acc (Lex ra rb) (a, b) := by - induction (aca a) generalizing b + induction (aca a) generalizing b with | intro xa aca iha => - induction (acb b) + induction (acb b) with | intro xb acb ihb => apply Acc.intro (xa, xb) intro p lt - cases lt + cases lt with | left a₁ b₁ a₂ b₂ h => apply iha a₁ h | right a b₁ b₂ h => apply ihb b₁ h @@ -217,7 +217,7 @@ def lexWf (ha : WellFounded ra) (hb : WellFounded rb) : WellFounded (Lex ra rb) -- relational product is a Subrelation of the Lex def rprodSubLex (a : α × β) (b : α × β) (h : Rprod ra rb a b) : Lex ra rb a b := by - cases h + cases h with | intro a₁ b₁ a₂ b₂ h₁ h₂ => exact Lex.left b₁ b₂ h₁ -- The relational product of well founded relations is well-founded @@ -252,13 +252,13 @@ variables {α : Sort u} {β : α → Sort v} variables {r : α → α → Prop} {s : ∀ (a : α), β a → β a → Prop} def lexAccessible {a} (aca : Acc r a) (acb : (a : α) → WellFounded (s a)) (b : β a) : Acc (Lex r s) ⟨a, b⟩ := by - induction aca generalizing b + induction aca generalizing b with | intro xa aca iha => - induction (WellFounded.apply (acb xa) b) + induction (WellFounded.apply (acb xa) b) with | intro xb acb ihb => apply Acc.intro intro p lt - cases lt + cases lt with | left => apply iha; assumption | right => apply ihb; assumption @@ -292,14 +292,14 @@ variables {α : Sort u} {β : Sort v} variables {r : α → α → Prop} {s : β → β → Prop} def revLexAccessible {b} (acb : Acc s b) (aca : (a : α) → Acc r a): (a : α) → Acc (RevLex r s) ⟨a, b⟩ := by - induction acb + induction acb with | intro xb acb ihb => intro a - induction (aca a) + induction (aca a) with | intro xa aca iha => apply Acc.intro intro p lt - cases lt + cases lt with | left => apply iha; assumption | right => apply ihb; assumption diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index 9b883ad6fe..5042dbe78e 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/src/Lean/Elab/Tactic/Induction.lean @@ -240,10 +240,7 @@ private def generalizeVars (stx : Syntax) (targets : Array Expr) : TacticM Nat : pure (fvarIds.size, [mvarId']) private def getAltsOfInductionAlts (inductionAlts : Syntax) : Array Syntax := - if inductionAlts.getNumArgs == 2 then - inductionAlts[1].getSepArgs -- TODO remove - else - inductionAlts[2].getSepArgs + inductionAlts[2].getSepArgs private def getAltsOfOptInductionAlts (optInductionAlts : Syntax) : Array Syntax := if optInductionAlts.isNone then #[] else getAltsOfInductionAlts optInductionAlts[0] diff --git a/tests/lean/hygienicIntro.lean b/tests/lean/hygienicIntro.lean index 48c2337501..9a92cdda03 100644 --- a/tests/lean/hygienicIntro.lean +++ b/tests/lean/hygienicIntro.lean @@ -1,4 +1,4 @@ - +-- set_option hygienicIntro false in theorem ex1 {a p q r : Prop} : p → (p → q) → (q → r) → r := by @@ -32,7 +32,7 @@ exact h -- Hygienic versions example {p q : Prop} (h₁ : p → q) (h₂ : p ∨ q) : q := by -cases h₂ +cases h₂ with | inl h => apply h₁; exact h | inr h => exact h diff --git a/tests/lean/inductionErrors.lean b/tests/lean/inductionErrors.lean index 32b3038cb7..b75b155422 100644 --- a/tests/lean/inductionErrors.lean +++ b/tests/lean/inductionErrors.lean @@ -7,25 +7,25 @@ axiom elimEx (motive : Nat → Nat → Sort u) (x y : Nat) : motive y x theorem ex1 (p q : Nat) : p ≤ q ∨ p > q := by - cases p, q using elimEx + cases p, q using elimEx with | lower d => apply Or.inl -- Error | upper d => apply Or.inr -- Error | diag => apply Or.inl; apply Nat.leRefl theorem ex2 (p q : Nat) : p ≤ q ∨ p > q := by - cases p, q using elimEx2 -- Error + cases p, q using elimEx2 with -- Error | lower d => apply Or.inl | upper d => apply Or.inr | diag => apply Or.inl; apply Nat.leRefl theorem ex3 (p q : Nat) : p ≤ q ∨ p > q := by - cases p /- Error -/ using elimEx + cases p /- Error -/ using elimEx with | lower d => apply Or.inl | upper d => apply Or.inr | diag => apply Or.inl; apply Nat.leRefl theorem ex4 (p q : Nat) : p ≤ q ∨ p > q := by - cases p using Nat.add -- Error + cases p using Nat.add with -- Error | lower d => apply Or.inl | upper d => apply Or.inr | diag => apply Or.inl; apply Nat.leRefl @@ -36,7 +36,7 @@ theorem ex5 (x : Nat) : 0 + x = x := by | y+1 => done -- Error theorem ex5b (x : Nat) : 0 + x = x := by - cases x + cases x with | zero => done -- Error | succ y => done -- Error @@ -45,36 +45,36 @@ inductive Vec : Nat → Type | cons : Bool → {n : Nat} → Vec n → Vec (n+1) theorem ex6 (x : Vec 0) : x = Vec.nil := by - cases x using Vec.casesOn + cases x using Vec.casesOn with | nil => rfl | cons => done -- Error theorem ex7 (x : Vec 0) : x = Vec.nil := by - cases x -- Error: TODO: improve error location + cases x with -- Error: TODO: improve error location | nil => rfl | cons => done theorem ex8 (p q : Nat) : p ≤ q ∨ p > q := by - cases p, q using elimEx + cases p, q using elimEx with | lower d => apply Or.inl; admit | upper2 /- Error -/ d => apply Or.inr | diag => apply Or.inl; apply Nat.leRefl theorem ex9 (p q : Nat) : p ≤ q ∨ p > q := by - cases p, q using elimEx + cases p, q using elimEx with | lower d => apply Or.inl; admit | _ => apply Or.inr; admit | diag => apply Or.inl; apply Nat.leRefl theorem ex10 (p q : Nat) : p ≤ q ∨ p > q := by - cases p, q using elimEx + cases p, q using elimEx with | lower d => apply Or.inl; admit | upper d => apply Or.inr; admit | diag => apply Or.inl; apply Nat.leRefl | _ /- error unused -/ => admit theorem ex11 (p q : Nat) : p ≤ q ∨ p > q := by - cases p, q using elimEx + cases p, q using elimEx with | lower d => apply Or.inl; admit | upper d => apply Or.inr; admit | lower d /- error unused -/ => apply Or.inl; admit diff --git a/tests/lean/run/casesUsing.lean b/tests/lean/run/casesUsing.lean index ee49770b8d..b7f2786e9c 100644 --- a/tests/lean/run/casesUsing.lean +++ b/tests/lean/run/casesUsing.lean @@ -12,7 +12,7 @@ axiom elimEx (motive : Nat → Nat → Sort u) (x y : Nat) : motive y x theorem ex1 (p q : Nat) : p ≤ q ∨ p > q := by - cases p, q using elimEx + cases p, q using elimEx with | diag => apply Or.inl; apply Nat.leRefl | lower d => apply Or.inl; show p ≤ p + d.succ; admit | upper d => apply Or.inr; show q + d.succ > q; admit @@ -36,7 +36,7 @@ theorem time2Eq (n : Nat) : 2*n = n + n := by rfl theorem ex3 (n : Nat) : Exists (fun m => n = m + m ∨ n = m + m + 1) := by - cases n using parityElim + cases n using parityElim with | even i => apply Exists.intro i apply Or.inl @@ -49,12 +49,12 @@ theorem ex3 (n : Nat) : Exists (fun m => n = m + m ∨ n = m + m + 1) := by rfl def ex4 {α} (xs : List α) (h : xs = [] → False) : α := by - cases he:xs + cases he:xs with | nil => apply False.elim; exact h he; done | cons x _ => exact x def ex5 {α} (xs : List α) (h : xs = [] → False) : α := by - cases he:xs using List.casesOn + cases he:xs using List.casesOn with | nil => apply False.elim; exact h he; done | cons x _ => exact x @@ -64,22 +64,22 @@ theorem ex6 {α} (f : List α → Bool) (h₁ : {xs : List α} → f xs = true | false => rfl theorem ex7 {α} (f : List α → Bool) (h₁ : {xs : List α} → f xs = true → xs = []) (xs : List α) (h₂ : xs ≠ []) : f xs = false := by - cases he:f xs + cases he:f xs with | true => exact False.elim (h₂ (h₁ he)) | false => rfl theorem ex8 {α} (f : List α → Bool) (h₁ : {xs : List α} → f xs = true → xs = []) (xs : List α) (h₂ : xs ≠ []) : f xs = false := by - cases he:f xs using Bool.casesOn + cases he:f xs using Bool.casesOn with | true => exact False.elim (h₂ (h₁ he)) | false => rfl theorem ex9 {α} (xs : List α) (h : xs = [] → False) : Nonempty α := by - cases xs using List.rec + cases xs using List.rec with | nil => apply False.elim; apply h; rfl | cons x _ => apply Nonempty.intro; assumption theorem modLt (x : Nat) {y : Nat} (h : y > 0) : x % y < y := by - induction x, y using Nat.mod.inductionOn generalizing h + induction x, y using Nat.mod.inductionOn generalizing h with | ind x y h₁ ih => rw [Nat.modEqSubMod h₁.2] exact ih h @@ -93,21 +93,21 @@ theorem modLt (x : Nat) {y : Nat} (h : y > 0) : x % y < y := by assumption theorem ex11 {p q : Prop } (h : p ∨ q) : q ∨ p := by - induction h using Or.casesOn + induction h using Or.casesOn with | inr h => ?myright | inl h => ?myleft case myleft => exact Or.inr h case myright => exact Or.inl h theorem ex12 {p q : Prop } (h : p ∨ q) : q ∨ p := by - cases h using Or.casesOn + cases h using Or.casesOn with | inr h => ?myright | inl h => ?myleft case myleft => exact Or.inr h case myright => exact Or.inl h theorem ex13 (p q : Nat) : p ≤ q ∨ p > q := by - cases p, q using elimEx + cases p, q using elimEx with | diag => ?hdiag | lower d => ?hlower | upper d => ?hupper @@ -116,7 +116,7 @@ theorem ex13 (p q : Nat) : p ≤ q ∨ p > q := by case hupper => apply Or.inr; show q + d.succ > q; admit theorem ex14 (p q : Nat) : p ≤ q ∨ p > q := by - cases p, q using elimEx + cases p, q using elimEx with | diag => ?hdiag | lower d => _ | upper d => ?hupper @@ -125,7 +125,7 @@ theorem ex14 (p q : Nat) : p ≤ q ∨ p > q := by case hupper => apply Or.inr; show q + d.succ > q; admit theorem ex15 (p q : Nat) : p ≤ q ∨ p > q := by - cases p, q using elimEx + cases p, q using elimEx with | diag => ?hdiag | lower d => _ | upper d => ?hupper diff --git a/tests/lean/run/concatElim.lean b/tests/lean/run/concatElim.lean index 0879a6bf6f..c1f719a8cf 100644 --- a/tests/lean/run/concatElim.lean +++ b/tests/lean/run/concatElim.lean @@ -51,7 +51,7 @@ theorem dropLastLen {α} (xs : List α) : (n : Nat) → xs.length = n+1 → (dro rfl | x₁::x₂::xs => intro n h - cases n + cases n with | zero => rw [lengthCons, lengthCons] at h injection h with h diff --git a/tests/lean/run/induction1.lean b/tests/lean/run/induction1.lean index 362aa757f8..3fd38124fe 100644 --- a/tests/lean/run/induction1.lean +++ b/tests/lean/run/induction1.lean @@ -21,34 +21,34 @@ focus assumption theorem tst1 {p q : Prop } (h : p ∨ q) : q ∨ p := by -induction h +induction h with | inr h2 => exact Or.inl h2 | inl h1 => exact Or.inr h1 theorem tst2 {p q : Prop } (h : p ∨ q) : q ∨ p := by -induction h using elim2 +induction h using elim2 with | left _ => apply Or.inr; assumption | right _ => apply Or.inl; assumption theorem tst2b {p q : Prop } (h : p ∨ q) : q ∨ p := by -induction h using elim2 +induction h using elim2 with | left => apply Or.inr; assumption | _ => apply Or.inl; assumption theorem tst3 {p q : Prop } (h : p ∨ q) : q ∨ p := by -induction h using elim2 +induction h using elim2 with | right h => exact Or.inl h | left h => exact Or.inr h theorem tst4 {p q : Prop } (h : p ∨ q) : q ∨ p := by -induction h using elim2 +induction h using elim2 with | right h => ?myright | left h => ?myleft case myleft => exact Or.inr h case myright => exact Or.inl h theorem tst5 {p q : Prop } (h : p ∨ q) : q ∨ p := by -induction h using elim2 +induction h using elim2 with | right h => _ | left h => refine Or.inr ?_ @@ -57,14 +57,14 @@ case right => exact Or.inl h theorem tst6 {p q : Prop } (h : p ∨ q) : q ∨ p := by { - cases h + cases h with | inr h2 => exact Or.inl h2 | inl h1 => exact Or.inr h1 } theorem tst7 {α : Type} (xs : List α) (h : (a : α) → (as : List α) → xs ≠ a :: as) : xs = [] := by { - induction xs + induction xs with | nil => exact rfl | cons z zs ih => exact absurd rfl (h z zs) } @@ -76,23 +76,23 @@ theorem tst8 {α : Type} (xs : List α) (h : (a : α) → (as : List α) → xs } theorem tst9 {α : Type} (xs : List α) (h : (a : α) → (as : List α) → xs ≠ a :: as) : xs = [] := by - cases xs + cases xs with | nil => exact rfl | cons z zs => exact absurd rfl (h z zs) theorem tst10 {p q : Prop } (h₁ : p ↔ q) (h₂ : p) : q := by - induction h₁ + induction h₁ with | intro h _ => exact h h₂ def Iff2 (m p q : Prop) := p ↔ q theorem tst11 {p q r : Prop } (h₁ : Iff2 r p q) (h₂ : p) : q := by - induction h₁ using Iff.rec + induction h₁ using Iff.rec with | intro h _ => exact h h₂ theorem tst12 {p q : Prop } (h₁ : p ∨ q) (h₂ : p ↔ q) (h₃ : p) : q := by failIfSuccess induction h₁ using Iff.casesOn - induction h₂ using Iff.casesOn + induction h₂ using Iff.casesOn with | intro h _ => exact h h₃ @@ -106,12 +106,12 @@ def Tree.isLeaf₁ : Tree → Bool | _ => false theorem tst13 (x : Tree) (h : x = Tree.leaf₁) : x.isLeaf₁ = true := by - cases x + cases x with | leaf₁ => rfl | _ => injection h theorem tst14 (x : Tree) (h : x = Tree.leaf₁) : x.isLeaf₁ = true := by - induction x + induction x with | leaf₁ => rfl | _ => injection h diff --git a/tests/lean/run/inj2.lean b/tests/lean/run/inj2.lean index c20d5c1f64..7492d928cf 100644 --- a/tests/lean/run/inj2.lean +++ b/tests/lean/run/inj2.lean @@ -30,9 +30,9 @@ theorem test4 {α} (v : Fin2 0) : α := by cases v def test5 {α β} {n} (v : Vec2 α β (n+1)) : α := by - cases v + cases v with | cons h1 h2 n tail => exact h1 def test6 {α β} {n} (v : Vec2 α β (n+2)) : α := by - cases v + cases v with | cons h1 h2 n tail => exact h1 diff --git a/tests/lean/run/tacticTests.lean b/tests/lean/run/tacticTests.lean index f760b78bb1..be035acb77 100644 --- a/tests/lean/run/tacticTests.lean +++ b/tests/lean/run/tacticTests.lean @@ -9,14 +9,14 @@ theorem ex1 (m : Nat) : Le m 0 → m = 0 := by theorem ex2 (m n : Nat) : Le m n → Le m.succ n.succ := by intro h - induction h + induction h with | base n => apply Le.base | succ n m ih => apply Le.succ apply ih theorem ex3 (m : Nat) : Le 0 m := by - induction m + induction m with | zero => apply Le.base | succ m ih => apply Le.succ @@ -28,22 +28,22 @@ theorem ex4 (m : Nat) : ¬ Le m.succ 0 := by theorem ex5 {m n : Nat} : Le m n.succ → m = n.succ ∨ Le m n := by intro h - cases h + cases h with | base => apply Or.inl; rfl | succ => apply Or.inr; assumption theorem ex6 {m n : Nat} : Le m.succ n.succ → Le m n := by revert m - induction n + induction n with | zero => intros m h; - cases h + cases h with | base => apply Le.base | succ n h => exact absurd h (ex4 _) | succ n ih => intros m h have aux := ih (m := m) - cases ex5 h + cases ex5 h with | inl h => injection h with h subst h @@ -54,7 +54,7 @@ theorem ex6 {m n : Nat} : Le m.succ n.succ → Le m n := by theorem ex7 {m n o : Nat} : Le m n → Le n o → Le m o := by intro h - induction h + induction h with | base => intros; assumption | succ n s ih => intro h₂ @@ -71,7 +71,7 @@ theorem ex8 {m n : Nat} : Le m.succ n → Le m n := by theorem ex9 {m n : Nat} : Le m n → m = n ∨ Le m.succ n := by intro h - cases h + cases h with | base => apply Or.inl; rfl | succ n s => apply Or.inr @@ -86,12 +86,12 @@ theorem ex10 (n : Nat) : ¬ Le n.succ n := by -/ theorem ex10 (n : Nat) : n.succ ≠ n := by - induction n + induction n with | zero => intro h; injection h; done | succ n ih => intro h; injection h with h; apply ih h theorem ex11 (n : Nat) : ¬ Le n.succ n := by - induction n + induction n with | zero => intro h; cases h; done | succ n ih => intro h @@ -101,12 +101,12 @@ theorem ex11 (n : Nat) : ¬ Le n.succ n := by theorem ex12 (m n : Nat) : Le m n → Le n m → m = n := by revert m - induction n + induction n with | zero => intro m h1 h2; apply ex1; assumption; done | succ n ih => intro m h1 h2 have ih := ih m - cases ex5 h1 + cases ex5 h1 with | inl h => assumption | inr h => have ih := ih h diff --git a/tests/lean/run/where1.lean b/tests/lean/run/where1.lean index 54214815ce..9b41b3ca60 100644 --- a/tests/lean/run/where1.lean +++ b/tests/lean/run/where1.lean @@ -19,7 +19,7 @@ theorem lengthReverse (as : List α) : (reverse as).length = as.length := revLoop as [] where revLoop (as bs : List α) : (reverse.loop as bs).length = as.length + bs.length := by - induction as generalizing bs + induction as generalizing bs with | nil => rw [Nat.zeroAdd]; rfl | cons a as ih => show (reverse.loop as (a::bs)).length = (a :: as).length + bs.length diff --git a/tests/lean/unsolvedIndCases.lean b/tests/lean/unsolvedIndCases.lean index 40c4a7c1c2..c0e55ce21e 100644 --- a/tests/lean/unsolvedIndCases.lean +++ b/tests/lean/unsolvedIndCases.lean @@ -1,24 +1,24 @@ theorem ex1 (x : Nat) : 0 + x = x := by - cases x + cases x with | zero => skip -- Error: unsolved goals | succ y => skip -- Error: unsolved goals theorem ex2 (x : Nat) : 0 + x = x := by - induction x + induction x with | zero => skip -- Error: unsolved goals | succ y ih => skip -- Error: unsolved goals theorem ex3 (x : Nat) : 0 + x = x := by - cases x + cases x with | zero => rfl | succ y => skip -- Error: unsolved goals theorem ex4 (x : Nat) {y : Nat} (h : y > 0) : x % y < y := by - induction x, y using Nat.mod.inductionOn generalizing h + induction x, y using Nat.mod.inductionOn generalizing h with | ind x y h₁ ih => skip -- Error: unsolved goals | base x y h₁ => skip -- Error: unsolved goals theorem ex5 (x : Nat) {y : Nat} (h : y > 0) : x % y < y := by - cases x, y using Nat.mod.inductionOn + cases x, y using Nat.mod.inductionOn with | ind x y h₁ ih => skip -- Error: unsolved goals | base x y h₁ => skip -- Error: unsolved goals