max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: adapt stdlib & tests

Browse source
This commit is contained in:
Sebastian Ullrich 2021-05-20 17:42:24 +02:00 • committed by Leonardo de Moura
parent 6ede77abbd
commit a02c6fd3eb
52 changed files with 175 additions and 182 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
doc/tactics.md
View file

@ -176,11 +176,11 @@ theorem ex (x : Nat) {y : Nat} (h : y > 0) : x % y < y := by
rw [Nat.mod_eq_sub_mod h₁.2]
exact ih h
| base x y h₁ =>
have ¬ 0 < y ∨ ¬ y ≤ x from Iff.mp (Decidable.notAndIffOrNot ..) h₁
have : ¬ 0 < y ∨ ¬ y ≤ x := Iff.mp (Decidable.notAndIffOrNot ..) h₁
match this with
| Or.inl h₁ => exact absurd h h₁
| Or.inr h₁ =>
have hgt : y > x from Nat.gtOfNotLe h₁
have hgt : y > x := Nat.gtOfNotLe h₁
rw [← Nat.mod_eq_of_lt hgt] at hgt
assumption
```

22
src/Init/Classical.lean
View file

@ -28,30 +28,30 @@ theorem chooseSpec {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (choose
theorem em (p : Prop) : p ∨ ¬p :=
let U (x : Prop) : Prop := x = True ∨ p;
let V (x : Prop) : Prop := x = False ∨ p;
have exU : ∃ x, U x from ⟨True, Or.inl rfl⟩;
have exV : ∃ x, V x from ⟨False, Or.inl rfl⟩;
have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩;
have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩;
let u : Prop := choose exU;
let v : Prop := choose exV;
have uDef : U u from chooseSpec exU;
have vDef : V v from chooseSpec exV;
have notUvOrP : u ≠ v ∨ p from
have uDef : U u := chooseSpec exU;
have vDef : V v := chooseSpec exV;
have notUvOrP : u ≠ v ∨ p :=
match uDef, vDef with
| Or.inr h, _ => Or.inr h
| _, Or.inr h => Or.inr h
| Or.inl hut, Or.inl hvf =>
have hne : u ≠ v from hvf.symm ▸ hut.symm ▸ trueNeFalse
have hne : u ≠ v := hvf.symm ▸ hut.symm ▸ trueNeFalse
Or.inl hne
have pImpliesUv : p → u = v from
have pImpliesUv : p → u = v :=
fun hp =>
have hpred : U = V from
have hpred : U = V :=
funext fun x =>
have hl : (x = True ∨ p) → (x = False ∨ p) from
have hl : (x = True ∨ p) → (x = False ∨ p) :=
fun a => Or.inr hp;
have hr : (x = False ∨ p) → (x = True ∨ p) from
have hr : (x = False ∨ p) → (x = True ∨ p) :=
fun a => Or.inr hp;
show (x = True ∨ p) = (x = False ∨ p) from
propext (Iff.intro hl hr);
have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV from
have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV :=
hpred ▸ fun exU exV => rfl;
show u = v from h₀ ..;
match notUvOrP with

2
src/Init/Control/Lawful.lean
View file

@ -75,7 +75,7 @@ theorem bind_congr [Bind m] {x : m α} {f g : α → m β} (h : ∀ a, f a = g a
simp [funext h]
@[simp] theorem bind_pure_unit [Monad m] [LawfulMonad m] {x : m PUnit} : (x >>= fun _ => pure ⟨⟩) = x := by
have (x >>= fun _ => pure ⟨⟩) = (x >>= pure) by
have : (x >>= fun _ => pure ⟨⟩) = (x >>= pure) := by
apply bind_congr; intro u
cases u; simp
rw [bind_pure] at this

2
src/Init/Core.lean
View file

@ -222,7 +222,7 @@ theorem neFalseOfSelf : p → p ≠ False :=
theorem neTrueOfNot : ¬p → p ≠ True :=
fun (hnp : ¬p) (h : p = True) =>
have ¬True from h ▸ hnp
have : ¬True := h ▸ hnp
this trivial
theorem trueNeFalse : ¬True = False :=

42
src/Init/Data/Array/Basic.lean
View file

@ -90,7 +90,7 @@ def swapAt! (a : Array α) (i : Nat) (v : α) : α × Array α :=
if h : i < a.size then
swapAt a ⟨i, h⟩ v
else
have Inhabited α from ⟨v⟩
have : Inhabited α := ⟨v⟩
panic! ("index " ++ toString i ++ " out of bounds")
@[extern "lean_array_pop"]
@ -143,7 +143,7 @@ def modifyOp [Inhabited α] (self : Array α) (idx : Nat) (f : α → α) : Arra
private theorem zeroLtOfLt : {a b : Nat} → a < b → 0 < b
| 0, _, h => h
| a+1, b, h =>
have a < b from Nat.ltTrans (Nat.ltSuccSelf _) h
have : a < b := Nat.ltTrans (Nat.ltSuccSelf _) h
zeroLtOfLt this
/- Reference implementation for `forIn` -/
@ -153,9 +153,9 @@ protected def forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m
match i, h with
| 0, _ => pure b
| i+1, h =>
have h' : i < as.size from Nat.ltOfLtOfLe (Nat.ltSuccSelf i) h
have as.size - 1 < as.size from Nat.subLt (zeroLtOfLt h') (by decide)
have as.size - 1 - i < as.size from Nat.ltOfLeOfLt (Nat.subLe (as.size - 1) i) this
have h' : i < as.size := Nat.ltOfLtOfLe (Nat.ltSuccSelf i) h
have : as.size - 1 < as.size := Nat.subLt (zeroLtOfLt h') (by decide)
have : as.size - 1 - i < as.size := Nat.ltOfLeOfLt (Nat.subLe (as.size - 1) i) this
match (← f (as.get ⟨as.size - 1 - i, this⟩) b) with
| ForInStep.done b => pure b
| ForInStep.yield b => loop i (Nat.leOfLt h') b
@ -225,7 +225,7 @@ def foldrM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
else match i, h with
| 0, _ => pure b
| i+1, h =>
have i < as.size from Nat.ltOfLtOfLe (Nat.ltSuccSelf _) h
have : i < as.size := Nat.ltOfLtOfLe (Nat.ltSuccSelf _) h
fold i (Nat.leOfLt this) (← f (as.get ⟨i, this⟩) b)
if h : start ≤ as.size then
if stop < start then
@ -262,9 +262,9 @@ def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as :
match i, inv with
| 0, _ => pure bs
| i+1, inv =>
have j < as.size by rw [← inv, Nat.add_assoc, Nat.add_comm 1 j, Nat.add_left_comm]; apply Nat.leAddRight
have : j < as.size := by rw [← inv, Nat.add_assoc, Nat.add_comm 1 j, Nat.add_left_comm]; apply Nat.leAddRight
let idx : Fin as.size := ⟨j, this⟩
have i + (j + 1) = as.size by rw [← inv, Nat.add_comm j 1, Nat.add_assoc]
have : i + (j + 1) = as.size := by rw [← inv, Nat.add_comm j 1, Nat.add_assoc]
map i (j+1) this (bs.push (← f idx (as.get idx)))
map as.size 0 rfl (mkEmpty as.size)
@ -339,12 +339,12 @@ def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
let rec @[specialize] find : (i : Nat) → i ≤ as.size → m (Option β)
| 0, h => pure none
| i+1, h => do
have i < as.size from Nat.ltOfLtOfLe (Nat.ltSuccSelf _) h
have : i < as.size := Nat.ltOfLtOfLe (Nat.ltSuccSelf _) h
let r ← f (as.get ⟨i, this⟩)
match r with
| some v => pure r
| none =>
have i ≤ as.size from Nat.leOfLt this
have : i ≤ as.size := Nat.leOfLt this
find i this
find as.size (Nat.leRefl _)
@ -412,7 +412,7 @@ def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
if p (as.get ⟨j, hlt⟩) then
some j
else
have i + (j+1) = as.size by
have : i + (j+1) = as.size := by
rw [← inv, Nat.add_comm j 1, Nat.add_assoc]
loop i (j+1) this
else
@ -576,17 +576,17 @@ theorem ext (a b : Array α)
cases b with
| nil => rw [List.length_cons] at h₁; injection h₁
| cons b bs =>
have hz₁ : 0 < (a::as).length by rw [List.length_cons]; apply Nat.zeroLtSucc
have hz₂ : 0 < (b::bs).length by rw [List.length_cons]; apply Nat.zeroLtSucc
have headEq : a = b from h₂ 0 hz₁ hz₂
have h₁' : as.length = bs.length by rw [List.length_cons, List.length_cons] at h₁; injection h₁; assumption
have h₂' : (i : Nat) → (hi₁ : i < as.length) → (hi₂ : i < bs.length) → as.get i hi₁ = bs.get i hi₂ by
have hz₁ : 0 < (a::as).length := by rw [List.length_cons]; apply Nat.zeroLtSucc
have hz₂ : 0 < (b::bs).length := by rw [List.length_cons]; apply Nat.zeroLtSucc
have headEq : a = b := h₂ 0 hz₁ hz₂
have h₁' : as.length = bs.length := by rw [List.length_cons, List.length_cons] at h₁; injection h₁; assumption
have h₂' : (i : Nat) → (hi₁ : i < as.length) → (hi₂ : i < bs.length) → as.get i hi₁ = bs.get i hi₂ := by
intro i hi₁ hi₂
have hi₁' : i+1 < (a::as).length by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
have hi₂' : i+1 < (b::bs).length by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
have (a::as).get (i+1) hi₁' = (b::bs).get (i+1) hi₂' from h₂ (i+1) hi₁' hi₂'
have hi₁' : i+1 < (a::as).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
have hi₂' : i+1 < (b::bs).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
have : (a::as).get (i+1) hi₁' = (b::bs).get (i+1) hi₂' := h₂ (i+1) hi₁' hi₂'
apply this
have tailEq : as = bs from ih bs h₁' h₂'
have tailEq : as = bs := ih bs h₁' h₂'
rw [headEq, tailEq]
cases a; cases b
apply congrArg
@ -748,7 +748,7 @@ def isPrefixOf [BEq α] (as bs : Array α) : Bool :=
private def allDiffAuxAux [BEq α] (as : Array α) (a : α) : forall (i : Nat), i < as.size → Bool
| 0, h => true
| i+1, h =>
have i < as.size from Nat.ltTrans (Nat.ltSuccSelf _) h;
have : i < as.size := Nat.ltTrans (Nat.ltSuccSelf _) h;
a != as.get ⟨i, this⟩ && allDiffAuxAux as a i this
private partial def allDiffAux [BEq α] (as : Array α) : Nat → Bool

2
src/Init/Data/Array/InsertionSort.lean
View file

@ -21,7 +21,7 @@ where
match he:j with
| 0 => a
| j'+1 =>
have h' : j' < a.size by subst j; exact Nat.ltTrans (Nat.ltSuccSelf _) h
have h' : j' < a.size := by subst j; exact Nat.ltTrans (Nat.ltSuccSelf _) h
if lt (a.get ⟨j, h⟩) (a.get ⟨j', h'⟩) then
swapLoop (a.swap ⟨j, h⟩ ⟨j', h'⟩) j' (by rw [size_swap]; assumption done)
else

2
src/Init/Data/Fin/Basic.lean
View file

@ -29,7 +29,7 @@ protected def ofNat' {n : Nat} (a : Nat) (h : n > 0) : Fin n :=
private theorem mlt {b : Nat} : {a : Nat} → a < n → b % n < n
| 0, h => Nat.mod_lt _ h
| a+1, h =>
have n > 0 from Nat.ltTrans (Nat.zeroLtSucc _) h;
have : n > 0 := Nat.ltTrans (Nat.zeroLtSucc _) h;
Nat.mod_lt _ this
protected def add : Fin n → Fin n → Fin n

44
src/Init/Data/Nat/Basic.lean
View file

@ -67,7 +67,7 @@ theorem succ_Eq_add_one (n : Nat) : succ n = n + 1 :=
protected theorem add_comm : ∀ (n m : Nat), n + m = m + n
| n, 0 => Eq.symm (Nat.zero_add n)
| n, m+1 => by
have succ (n + m) = succ (m + n) by apply congrArg; apply Nat.add_comm
have : succ (n + m) = succ (m + n) := by apply congrArg; apply Nat.add_comm
rw [succ_add m n]
apply this
@ -123,21 +123,21 @@ protected theorem left_distrib (n m k : Nat) : n * (m + k) = n * m + n * k := by
| succ n ih => simp [succ_mul, ih]; rw [Nat.add_assoc, Nat.add_assoc (n*m)]; apply congrArg; apply Nat.add_left_comm
protected theorem right_distrib (n m k : Nat) : (n + m) * k = n * k + m * k :=
have h₁ : (n + m) * k = k * (n + m) from Nat.mul_comm ..
have h₂ : k * (n + m) = k * n + k * m from Nat.left_distrib ..
have h₃ : k * n + k * m = n * k + k * m from Nat.mul_comm n k ▸ rfl
have h₄ : n * k + k * m = n * k + m * k from Nat.mul_comm m k ▸ rfl
have h₁ : (n + m) * k = k * (n + m) := Nat.mul_comm ..
have h₂ : k * (n + m) = k * n + k * m := Nat.left_distrib ..
have h₃ : k * n + k * m = n * k + k * m := Nat.mul_comm n k ▸ rfl
have h₄ : n * k + k * m = n * k + m * k := Nat.mul_comm m k ▸ rfl
((h₁.trans h₂).trans h₃).trans h₄
protected theorem mul_assoc : ∀ (n m k : Nat), (n * m) * k = n * (m * k)
| n, m, 0 => rfl
| n, m, succ k =>
have h₁ : n * m * succ k = n * m * (k + 1) from rfl
have h₂ : n * m * (k + 1) = (n * m * k) + n * m * 1 from Nat.left_distrib ..
have h₃ : (n * m * k) + n * m * 1 = (n * m * k) + n * m by rw [Nat.mul_one (n*m)]
have h₄ : (n * m * k) + n * m = (n * (m * k)) + n * m by rw [Nat.mul_assoc n m k]
have h₅ : (n * (m * k)) + n * m = n * (m * k + m) from (Nat.left_distrib n (m*k) m).symm
have h₆ : n * (m * k + m) = n * (m * succ k) from Nat.mul_succ m k ▸ rfl
have h₁ : n * m * succ k = n * m * (k + 1) := rfl
have h₂ : n * m * (k + 1) = (n * m * k) + n * m * 1 := Nat.left_distrib ..
have h₃ : (n * m * k) + n * m * 1 = (n * m * k) + n * m := by rw [Nat.mul_one (n*m)]
have h₄ : (n * m * k) + n * m = (n * (m * k)) + n * m := by rw [Nat.mul_assoc n m k]
have h₅ : (n * (m * k)) + n * m = n * (m * k + m) := (Nat.left_distrib n (m*k) m).symm
have h₆ : n * (m * k + m) = n * (m * succ k) := Nat.mul_succ m k ▸ rfl
((((h₁.trans h₂).trans h₃).trans h₄).trans h₅).trans h₆
/- Inequalities -/
@ -254,8 +254,8 @@ theorem ltOrEqOrLeSucc {m n : Nat} (h : m ≤ succ n) : m ≤ n ∨ m = succ n :
Decidable.byCases
(fun (h' : m = succ n) => Or.inr h')
(fun (h' : m ≠ succ n) =>
have m < succ n from Nat.ltOfLeAndNe h h'
have succ m ≤ succ n from succLeOfLt this
have : m < succ n := Nat.ltOfLeAndNe h h'
have : succ m ≤ succ n := succLeOfLt this
Or.inl (leOfSuccLeSucc this))
theorem leAddRight : ∀ (n k : Nat), n ≤ n + k
@ -270,8 +270,8 @@ theorem le.dest : ∀ {n m : Nat}, n ≤ m → Exists (fun k => n + k = m)
| zero, succ n, h => ⟨succ n, Nat.add_comm 0 (succ n) ▸ rfl⟩
| succ n, zero, h => Bool.noConfusion h
| succ n, succ m, h =>
have n ≤ m from h
have Exists (fun k => n + k = m) from dest this
have : n ≤ m := h
have : Exists (fun k => n + k = m) := dest this
match this with
| ⟨k, h⟩ => ⟨k, show succ n + k = succ m from ((succ_add n k).symm ▸ h ▸ rfl)⟩
@ -282,7 +282,7 @@ protected theorem notLeOfGt {n m : Nat} (h : n > m) : ¬ n ≤ m := fun h₁ =>
match Nat.ltOrGe n m with
| Or.inl h₂ => absurd (Nat.ltTrans h h₂) (Nat.ltIrrefl _)
| Or.inr h₂ =>
have Heq : n = m from Nat.leAntisymm h₁ h₂
have Heq : n = m := Nat.leAntisymm h₁ h₂
absurd (@Eq.subst _ _ _ _ Heq h) (Nat.ltIrrefl m)
theorem gtOfNotLe {n m : Nat} (h : ¬ n ≤ m) : n > m :=
@ -293,8 +293,8 @@ theorem gtOfNotLe {n m : Nat} (h : ¬ n ≤ m) : n > m :=
protected theorem addLeAddLeft {n m : Nat} (h : n ≤ m) (k : Nat) : k + n ≤ k + m :=
match le.dest h with
| ⟨w, hw⟩ =>
have h₁ : k + n + w = k + (n + w) from Nat.add_assoc ..
have h₂ : k + (n + w) = k + m from congrArg _ hw
have h₁ : k + n + w = k + (n + w) := Nat.add_assoc ..
have h₂ : k + (n + w) = k + m := congrArg _ hw
le.intro <| h₁.trans h₂
protected theorem addLeAddRight {n m : Nat} (h : n ≤ m) (k : Nat) : n + k ≤ m + k := by
@ -336,7 +336,7 @@ theorem succNeZero (n : Nat) : succ n ≠ 0 :=
theorem mulLeMulLeft {n m : Nat} (k : Nat) (h : n ≤ m) : k * n ≤ k * m :=
match le.dest h with
| ⟨l, hl⟩ =>
have k * n + k * l = k * m from Nat.left_distrib k n l ▸ hl.symm ▸ rfl
have : k * n + k * l = k * m := Nat.left_distrib k n l ▸ hl.symm ▸ rfl
le.intro this
theorem mulLeMulRight {n m : Nat} (k : Nat) (h : n ≤ m) : n * k ≤ m * k :=
@ -352,7 +352,7 @@ protected theorem mulLtMulOfPosRight {n m k : Nat} (h : n < m) (hk : k > 0) : n
Nat.mul_comm k m ▸ Nat.mul_comm k n ▸ Nat.mulLtMulOfPosLeft h hk
protected theorem mulPos {n m : Nat} (ha : n > 0) (hb : m > 0) : n * m > 0 :=
have h : 0 * m < n * m from Nat.mulLtMulOfPosRight ha hb
have h : 0 * m < n * m := Nat.mulLtMulOfPosRight ha hb
Nat.zero_mul m ▸ h
/- power -/
@ -368,12 +368,12 @@ theorem powLePowOfLeLeft {n m : Nat} (h : n ≤ m) : ∀ (i : Nat), n^i ≤ m^i
theorem powLePowOfLeRight {n : Nat} (hx : n > 0) {i : Nat} : ∀ {j}, i ≤ j → n^i ≤ n^j
| 0, h =>
have i = 0 from eqZeroOfLeZero h
have : i = 0 := eqZeroOfLeZero h
this.symm ▸ Nat.leRefl _
| succ j, h =>
match ltOrEqOrLeSucc h with
| Or.inl h => show n^i ≤ n^j * n from
have n^i * 1 ≤ n^j * n from Nat.mulLeMul (powLePowOfLeRight hx h) hx
have : n^i * 1 ≤ n^j * n := Nat.mulLeMul (powLePowOfLeRight hx h) hx
Nat.mul_one (n^i) ▸ this
| Or.inr h =>
h.symm ▸ Nat.leRefl _

20
src/Init/Data/Nat/Div.lean
View file

@ -65,14 +65,14 @@ theorem mod.inductionOn.{u}
div.inductionOn x y ind base
theorem mod_zero (a : Nat) : a % 0 = a :=
have (if 0 < 0 ∧ 0 ≤ a then (a - 0) % 0 else a) = a from
have h : ¬ (0 < 0 ∧ 0 ≤ a) from fun ⟨h₁, _⟩ => absurd h₁ (Nat.ltIrrefl _)
have : (if 0 < 0 ∧ 0 ≤ a then (a - 0) % 0 else a) = a :=
have h : ¬ (0 < 0 ∧ 0 ≤ a) := fun ⟨h₁, _⟩ => absurd h₁ (Nat.ltIrrefl _)
ifNeg h
(mod_eq a 0).symm ▸ this
theorem mod_eq_of_lt {a b : Nat} (h : a < b) : a % b = a :=
have (if 0 < b ∧ b ≤ a then (a - b) % b else a) = a from
have h' : ¬(0 < b ∧ b ≤ a) from fun ⟨_, h₁⟩ => absurd h₁ (Nat.notLeOfGt h)
have : (if 0 < b ∧ b ≤ a then (a - b) % b else a) = a :=
have h' : ¬(0 < b ∧ b ≤ a) := fun ⟨_, h₁⟩ => absurd h₁ (Nat.notLeOfGt h)
ifNeg h'
(mod_eq a b).symm ▸ this
@ -85,12 +85,12 @@ theorem mod_lt (x : Nat) {y : Nat} : y > 0 → x % y < y := by
induction x, y using mod.inductionOn with
| base x y h₁ =>
intro h₂
have h₁ : ¬ 0 < y ∨ ¬ y ≤ x from Iff.mp (Decidable.notAndIffOrNot _ _) h₁
have h₁ : ¬ 0 < y ∨ ¬ y ≤ x := Iff.mp (Decidable.notAndIffOrNot _ _) h₁
match h₁ with
| Or.inl h₁ => exact absurd h₂ h₁
| Or.inr h₁ =>
have hgt : y > x from gtOfNotLe h₁
have heq : x % y = x from mod_eq_of_lt hgt
have hgt : y > x := gtOfNotLe h₁
have heq : x % y = x := mod_eq_of_lt hgt
rw [← heq] at hgt
exact hgt
| ind x y h h₂ =>
@ -108,7 +108,7 @@ theorem mod_le (x y : Nat) : x % y ≤ x := by
@[simp] theorem zero_mod (b : Nat) : 0 % b = 0 := by
rw [mod_eq]
have ¬ (0 < b ∧ b ≤ 0) by
have : ¬ (0 < b ∧ b ≤ 0) := by
intro ⟨h₁, h₂⟩
exact absurd (Nat.ltOfLtOfLe h₁ h₂) (Nat.ltIrrefl 0)
simp [this]
@ -117,8 +117,8 @@ theorem mod_le (x y : Nat) : x % y ≤ x := by
rw [mod_eq_sub_mod (Nat.leRefl _), Nat.sub_self, zero_mod]
theorem mod_one (x : Nat) : x % 1 = 0 := by
have h : x % 1 < 1 from mod_lt x (by decide)
have (y : Nat) → y < 1 → y = 0 by
have h : x % 1 < 1 := mod_lt x (by decide)
have : (y : Nat) → y < 1 → y = 0 := by
intro y
cases y with
| zero => intro h; rfl

2
src/Init/Data/Stream.lean
View file

@ -93,7 +93,7 @@ instance : Stream (List α) α where
instance : Stream (Subarray α) α where
next? s :=
if h : s.start < s.stop then
have s.start + 1 ≤ s.stop from Nat.succLeOfLt h
have : s.start + 1 ≤ s.stop := Nat.succLeOfLt h
some (s.as.get ⟨s.start, Nat.ltOfLtOfLe h s.h₂⟩, { s with start := s.start + 1, h₁ := this })
else
none

2
src/Init/Meta.lean
View file

@ -792,7 +792,7 @@ private partial def filterSepElemsMAux {m : Type → Type} [Monad m] (a : Array
if acc.isEmpty then
filterSepElemsMAux a p (i+2) (acc.push stx)
else if hz : i ≠ 0 then
have i.pred < i from Nat.predLt hz
have : i.pred < i := Nat.predLt hz
let sepStx := a.get ⟨i.pred, Nat.ltTrans this h⟩
filterSepElemsMAux a p (i+2) ((acc.push sepStx).push stx)
else

24
src/Init/Prelude.lean
View file

@ -108,7 +108,7 @@ inductive HEq {α : Sort u} (a : α) : {β : Sort u} → β → Prop where
HEq.refl a
theorem eqOfHEq {α : Sort u} {a a' : α} (h : HEq a a') : Eq a a' :=
have (α β : Sort u) → (a : α) → (b : β) → HEq a b → (h : Eq α β) → Eq (cast h a) b from
have : (α β : Sort u) → (a : α) → (b : β) → HEq a b → (h : Eq α β) → Eq (cast h a) b :=
fun α β a b h₁ =>
HEq.rec (motive := fun {β} (b : β) (h : HEq a b) => (h₂ : Eq α β) → Eq (cast h₂ a) b)
(fun (h₂ : Eq α α) => rfl)
@ -555,8 +555,8 @@ theorem Nat.eqOfBeqEqTrue : {n m : Nat} → Eq (beq n m) true → Eq n m
| zero, succ m, h => Bool.noConfusion h
| succ n, zero, h => Bool.noConfusion h
| succ n, succ m, h =>
have Eq (beq n m) true from h
have Eq n m from eqOfBeqEqTrue this
have : Eq (beq n m) true := h
have : Eq n m := eqOfBeqEqTrue this
this ▸ rfl
theorem Nat.neOfBeqEqFalse : {n m : Nat} → Eq (beq n m) false → Not (Eq n m)
@ -564,7 +564,7 @@ theorem Nat.neOfBeqEqFalse : {n m : Nat} → Eq (beq n m) false → Not (Eq n m)
| zero, succ m, h₁, h₂ => Nat.noConfusion h₂
| succ n, zero, h₁, h₂ => Nat.noConfusion h₂
| succ n, succ m, h₁, h₂ =>
have Eq (beq n m) false from h₁
have : Eq (beq n m) false := h₁
Nat.noConfusion h₂ (fun h₂ => absurd h₂ (neOfBeqEqFalse this))
@[extern "lean_nat_dec_eq"]
@ -625,8 +625,8 @@ theorem Nat.leStep : {n m : Nat} → LE.le n m → LE.le n (succ m)
| zero, succ n, h => rfl
| succ n, zero, h => Bool.noConfusion h
| succ n, succ m, h =>
have LE.le n m from h
have LE.le n (succ m) from leStep this
have : LE.le n m := h
have : LE.le n (succ m) := leStep this
succLeSucc this
protected theorem Nat.leTrans : {n m k : Nat} → LE.le n m → LE.le m k → LE.le n k
@ -634,8 +634,8 @@ protected theorem Nat.leTrans : {n m k : Nat} → LE.le n m → LE.le m k → LE
| succ n, zero, k, h₁, h₂ => Bool.noConfusion h₁
| succ n, succ m, zero, h₁, h₂ => Bool.noConfusion h₂
| succ n, succ m, succ k, h₁, h₂ =>
have h₁' : LE.le n m from h₁
have h₂' : LE.le m k from h₂
have h₁' : LE.le n m := h₁
have h₂' : LE.le m k := h₂
show LE.le n k from
Nat.leTrans h₁' h₂'
@ -654,7 +654,7 @@ protected theorem Nat.eqOrLtOfLe : {n m: Nat} → LE.le n m → Or (Eq n m) (LT.
| zero, succ n, h => Or.inr (zeroLe n)
| succ n, zero, h => Bool.noConfusion h
| succ n, succ m, h =>
have LE.le n m from h
have : LE.le n m := h
match Nat.eqOrLtOfLe this with
| Or.inl h => Or.inl (h ▸ rfl)
| Or.inr h => Or.inr (succLeSucc h)
@ -679,8 +679,8 @@ protected theorem Nat.leAntisymm : {n m : Nat} → LE.le n m → LE.le m n → E
| succ n, zero, h₁, h₂ => Bool.noConfusion h₁
| zero, succ m, h₁, h₂ => Bool.noConfusion h₂
| succ n, succ m, h₁, h₂ =>
have h₁' : LE.le n m from h₁
have h₂' : LE.le m n from h₂
have h₁' : LE.le n m := h₁
have h₂' : LE.le m n := h₂
(Nat.leAntisymm h₁' h₂') ▸ rfl
protected theorem Nat.ltOfLeOfNe {n m : Nat} (h₁ : LE.le n m) (h₂ : Not (Eq n m)) : LT.lt n m :=
@ -1038,7 +1038,7 @@ def List.get {α : Type u} : (as : List α) → (i : Nat) → LT.lt i as.length
| nil, i, h => absurd h (Nat.notLtZero _)
| cons a as, 0, h => a
| cons a as, Nat.succ i, h =>
have LT.lt i.succ as.length.succ from length_cons .. ▸ h
have : LT.lt i.succ as.length.succ := length_cons .. ▸ h
get as i (Nat.leOfSuccLeSucc this)
structure String where

10
src/Init/SimpLemmas.lean
View file

@ -35,16 +35,16 @@ theorem impCongr {p₁ p₂ : Sort u} {q₁ q₂ : Sort v} (h₁ : p₁ = p₂)
theorem impCongrCtx {p₁ p₂ q₁ q₂ : Prop} (h₁ : p₁ = p₂) (h₂ : p₂ → q₁ = q₂) : (p₁ → q₁) = (p₂ → q₂) :=
propext <| Iff.intro
(fun h hp₂ =>
have p₁ from h₁ ▸ hp₂
have q₁ from h this
have : p₁ := h₁ ▸ hp₂
have : q₁ := h this
h₂ hp₂ ▸ this)
(fun h hp₁ =>
have hp₂ : p₂ from h₁ ▸ hp₁
have q₂ from h hp₂
have hp₂ : p₂ := h₁ ▸ hp₁
have : q₂ := h hp₂
h₂ hp₂ ▸ this)
theorem forallCongr {α : Sort u} {p q : α → Prop} (h : ∀ a, (p a = q a)) : (∀ a, p a) = (∀ a, q a) :=
have p = q from funext h
have : p = q := funext h
this ▸ rfl
@[congr]

2
src/Init/WF.lean
View file

@ -155,7 +155,7 @@ def Nat.ltWf : WellFounded Nat.lt := by
| succ n ih =>
apply Acc.intro (Nat.succ n)
intro m h
have m = n ∨ m < n from Nat.eqOrLtOfLe (Nat.leOfSuccLeSucc h)
have : m = n ∨ m < n := Nat.eqOrLtOfLe (Nat.leOfSuccLeSucc h)
match this with
| Or.inl e => subst e; assumption
| Or.inr e => exact Acc.inv ih e

2
src/Lean/Data/Lsp/LanguageFeatures.lean
View file

@ -166,7 +166,7 @@ partial instance : ToJson DocumentSymbol where
toJson :=
let rec go
| DocumentSymbol.mk sym =>
have ToJson DocumentSymbol from ⟨go⟩
have : ToJson DocumentSymbol := ⟨go⟩
toJson sym
go

2
src/Lean/Elab/BuiltinNotation.lean
View file

@ -75,7 +75,7 @@ open Meta
| `(suffices $x:ident : $type from $val $[;]? $body) => `(have $x : $type := $body; $val)
| `(suffices $type:term from $val $[;]? $body) => `(have : $type := $body; $val)
| `(suffices $x:ident : $type by%$b $tac:tacticSeq $[;]? $body) => `(have $x : $type := $body; by%$b $tac:tacticSeq)
| `(suffices $type:term by%$b $tac:tacticSeq $[;]? $body) => `(have $type := $body; by%$b $tac:tacticSeq)
| `(suffices $type:term by%$b $tac:tacticSeq $[;]? $body) => `(have : $type := $body; by%$b $tac:tacticSeq)
| _ => Macro.throwUnsupported
open Lean.Parser in

2
src/Std/Data/HashMap.lean
View file

@ -84,7 +84,7 @@ partial def moveEntries [Hashable α] (i : Nat) (source : Array (AssocList α β
def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β :=
let nbuckets := buckets.val.size * 2
have nbuckets > 0 from Nat.mulPos buckets.property (by decide)
have : nbuckets > 0 := Nat.mulPos buckets.property (by decide)
let new_buckets : HashMapBucket α β := ⟨mkArray nbuckets AssocList.nil, by simp; assumption⟩
{ size := size,
buckets := moveEntries 0 buckets.val new_buckets }

2
src/Std/Data/HashSet.lean
View file

@ -71,7 +71,7 @@ partial def moveEntries [Hashable α] (i : Nat) (source : Array (List α)) (targ
def expand [Hashable α] (size : Nat) (buckets : HashSetBucket α) : HashSetImp α :=
let nbuckets := buckets.val.size * 2
have nbuckets > 0 from Nat.mulPos buckets.property (by decide)
have : nbuckets > 0 := Nat.mulPos buckets.property (by decide)
let new_buckets : HashSetBucket α := ⟨mkArray nbuckets [], by rw [Array.size_mkArray]; assumption⟩
{ size := size,
buckets := moveEntries 0 buckets.val new_buckets }

4
src/Std/Data/PersistentHashMap.lean
View file

@ -211,7 +211,7 @@ def isUnaryNode : Node α β → Option (α × β)
| Node.entries entries => isUnaryEntries entries 0 none
| Node.collision keys vals heq =>
if h : 1 = keys.size then
have 0 < keys.size by rw [←h]; decide
have : 0 < keys.size := by rw [←h]; decide
some (keys.get ⟨0, this⟩, vals.get ⟨0, by rw [←heq]; assumption⟩)
else
none
@ -222,7 +222,7 @@ partial def eraseAux [BEq α] : Node α β → USize → α → Node α β × Bo
| some idx =>
let ⟨keys', keq⟩ := keys.eraseIdx' idx
let ⟨vals', veq⟩ := vals.eraseIdx' (Eq.ndrec idx heq)
have keys.size - 1 = vals.size - 1 by rw [heq]
have : keys.size - 1 = vals.size - 1 := by rw [heq]
(Node.collision keys' vals' (keq.trans (this.trans veq.symm)), true)
| none => (n, false)
| n@(Node.entries entries), h, k =>

2
tests/lean/Reformat.lean.expected.out
View file

@ -132,7 +132,7 @@ def HEq.rfl {α : Sort u} {a : α} : HEq a a :=
HEq.refl a
theorem eqOfHEq {α : Sort u} {a a' : α} (h : HEq a a') : Eq a a' :=
have (α β : Sort u) → (a : α) → (b : β) → HEq a b → (h : Eq α β) → Eq (cast h a) b from
have : (α β : Sort u) → (a : α) → (b : β) → HEq a b → (h : Eq α β) → Eq (cast h a) b :=
fun α β a b h₁ =>
HEq.rec (motive := fun {β} (b : β) (h : HEq a b) => (h₂ : Eq α β) → Eq (cast h₂ a) b) (fun (h₂ : Eq α α) => rfl)
h₁

2
tests/lean/Reformat/Input.lean
View file

@ -111,7 +111,7 @@ inductive HEq {α : Sort u} (a : α) : {β : Sort u} → β → Prop
HEq.refl a
theorem eqOfHEq {α : Sort u} {a a' : α} (h : HEq a a') : Eq a a' :=
have (α β : Sort u) → (a : α) → (b : β) → HEq a b → (h : Eq α β) → Eq (cast h a) b from
have : (α β : Sort u) → (a : α) → (b : β) → HEq a b → (h : Eq α β) → Eq (cast h a) b :=
fun α β a b h₁ =>
HEq.rec (motive := fun {β} (b : β) (h : HEq a b) => (h₂ : Eq α β) → Eq (cast h₂ a) b)
(fun (h₂ : Eq α α) => rfl)

6
tests/lean/StxQuot.lean
View file

@ -107,9 +107,3 @@ syntax "foo" term : term
#eval run ``(fun x => y)
#eval run ``(fun x y => x y)
#eval run ``(fun ⟨x, y⟩ => x)
#eval run do
match ← `(have x := y; z) with
| `(have $[$x :]? $type from $val $[;]? $body) => pure 0
| `(have $pattern:term := $val:term $[;]? $body) => pure 1
| _ => pure 2

1
tests/lean/StxQuot.lean.expected.out
View file

@ -54,4 +54,3 @@ StxQuot.lean:101:13-101:14: error: unknown identifier 'x' at quotation precheck;
StxQuot.lean:107:22-107:23: error: unknown identifier 'y' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check.
"(Term.fun\n \"fun\"\n (Term.basicFun\n [`x._@.UnhygienicMain._hyg.1 `y._@.UnhygienicMain._hyg.1]\n \"=>\"\n (Term.app `x._@.UnhygienicMain._hyg.1 [`y._@.UnhygienicMain._hyg.1])))"
"(Term.fun\n \"fun\"\n (Term.basicFun\n [(Term.anonymousCtor \"⟨\" [`x._@.UnhygienicMain._hyg.1 \",\" `y._@.UnhygienicMain._hyg.1] \"⟩\")]\n \"=>\"\n `x._@.UnhygienicMain._hyg.1))"
"1"

2
tests/lean/have.lean
View file

@ -1,5 +1,5 @@
example : False :=
have False from _
have : False := _
example : 5 = 3 :=
have t : True := _

2
tests/lean/interactive/goalIssue.lean
View file

@ -1,6 +1,6 @@
theorem foo1 (x : Nat) : 0 + x = x := by
first
| skip; have x + x = x + x from rfl; done
| skip; have : x + x = x + x := rfl; done
--^ $/lean/plainGoal
| simp

12
tests/lean/interactive/haveInfo.lean
View file

@ -1,26 +1,26 @@
example : False := by
have True by
have : True := by
skip
--^ $/lean/plainGoal
skip
admit
example : False := by
have True by
--^ $/lean/plainGoal
have : True := by
--^ $/lean/plainGoal
skip
skip
admit
example : False := by
have True by
--^ $/lean/plainGoal
have : True := by
--^ $/lean/plainGoal
skip
skip
admit
example : False := by
have True by
have : True := by
skip
--^ $/lean/plainGoal
skip

4
tests/lean/interactive/haveInfo.lean.expected.out
View file

@ -2,10 +2,10 @@
"position": {"line": 2, "character": 4}}
{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
{"textDocument": {"uri": "file://haveInfo.lean"},
"position": {"line": 8, "character": 12}}
"position": {"line": 8, "character": 17}}
{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
{"textDocument": {"uri": "file://haveInfo.lean"},
"position": {"line": 15, "character": 13}}
"position": {"line": 15, "character": 17}}
{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
{"textDocument": {"uri": "file://haveInfo.lean"},
"position": {"line": 23, "character": 2}}

2
tests/lean/interactive/macroGoalIssue.lean
View file

@ -1,5 +1,5 @@
theorem ex (n : Nat) : True := by
have n = 0 + n by rw [Nat.zero_add]
have : n = 0 + n := by rw [Nat.zero_add]
skip
--^ $/lean/plainGoal
exact True.intro

6
tests/lean/precissues.lean
View file

@ -12,15 +12,15 @@ def f (x : Nat) (g : Nat → Nat) := g x
#check f 1 (fun x => x)
#check id have True from ⟨⟩; this -- should fail
#check id have : True := ⟨⟩; this -- should fail
#check id let x := 10; x
#check 1
#check id (have True from ⟨⟩; this)
#check id (have : True := ⟨⟩; this)
#check 0 = have Nat from 1; this
#check 0 = have : Nat := 1; this
#check 0 = let x := 0; x
variable (p q r : Prop)

2
tests/lean/revertlet.lean
View file

@ -1,7 +1,7 @@
theorem ex (n : Nat) (h : n = 0) : 0 + n = 0 := by
let m := n + 1
let v := m + 1
have v = n + 2 from rfl
have : v = n + 2 := rfl
traceState
subst h
traceState

2
tests/lean/run/500_lean3.lean
View file

@ -1,4 +1,4 @@
example (foo bar : OptionM Nat) : False := by
have do { let x ← bar; foo } = bar >>= fun x => foo from rfl
have : do { let x ← bar; foo } = bar >>= fun x => foo := rfl
admit
done

2
tests/lean/run/alg.lean
View file

@ -64,7 +64,7 @@ theorem inv_inv [Group α] (a : α) : (a⁻¹)⁻¹ = a :=
inv_eq_of_mul_eq_one (mul_left_inv a)
theorem mul_right_inv [Group α] (a : α) : a * a⁻¹ = 1 := by
have a⁻¹⁻¹ * a⁻¹ = 1 by rw [mul_left_inv]
have : a⁻¹⁻¹ * a⁻¹ = 1 := by rw [mul_left_inv]
rw [inv_inv] at this
assumption

2
tests/lean/run/balg.lean
View file

@ -81,7 +81,7 @@ theorem inv_inv {G : Group} (a : G) : (a⁻¹)⁻¹ = a :=
inv_eq_of_mul_eq_one (G.mul_left_inv a)
theorem mul_right_inv {G : Group} (a : G) : a * a⁻¹ = 1 := by
have a⁻¹⁻¹ * a⁻¹ = 1 by rw [G.mul_left_inv]; rfl
have : a⁻¹⁻¹ * a⁻¹ = 1 := by rw [G.mul_left_inv]; rfl
rw [inv_inv] at this
assumption

10
tests/lean/run/concatElim.lean
View file

@ -38,8 +38,8 @@ theorem dropLastLen {α} (xs : List α) : (n : Nat) → xs.length = n+1 → (dro
| [] => intros; contradiction
| [a] =>
intro n h
have 1 = n + 1 from h
have 0 = n by injection this; assumption
have : 1 = n + 1 := h
have : 0 = n := by injection this; assumption
subst this
rfl
| x₁::x₂::xs =>
@ -49,8 +49,8 @@ theorem dropLastLen {α} (xs : List α) : (n : Nat) → xs.length = n+1 → (dro
simp [lengthCons] at h
injection h
| succ n =>
have (x₁ :: x₂ :: xs).length = xs.length + 2 by simp [lengthCons]
have xs.length = n by rw [this] at h; injection h with h; injection h with h; assumption
have : (x₁ :: x₂ :: xs).length = xs.length + 2 := by simp [lengthCons]
have : xs.length = n := by rw [this] at h; injection h with h; injection h with h; assumption
simp [dropLast, lengthCons, dropLastLen (x₂::xs) xs.length (lengthCons ..), this]
@[inline]
@ -66,7 +66,7 @@ def concatElim {α}
subst aux
apply base ()
| n+1, xs, h => by
have notNil : xs ≠ [] by intro h1; subst h1; injection h
have notNil : xs ≠ [] := by intro h1; subst h1; injection h
let ih := aux n (dropLast xs) (dropLastLen _ _ h)
let aux := ind (dropLast xs) (last xs notNil) ih
rw [concatEq] at aux

4
tests/lean/run/decClassical.lean
View file

@ -1,9 +1,9 @@
open Classical
theorem ex : if (fun x => x + 1) = (fun x => x + 2) then False else True := by
have (fun x => x + 1) ≠ (fun x => x + 2) by
have : (fun x => x + 1) ≠ (fun x => x + 2) := by
intro h
have 1 = 2 from congrFun h 0
have : 1 = 2 := congrFun h 0
contradiction
rw [ifNeg this]
exact True.intro

4
tests/lean/run/def7.lean
View file

@ -37,8 +37,8 @@ theorem L.appendNil {α} : (as : L α) → append as nil = as
| nil => rfl
| cons a as =>
show cons a (fun _ => append (as ()) nil) = cons a as from
have ih : append (as ()) nil = as () from appendNil $ as ()
have thunkAux : (fun _ => as ()) = as from funext fun x => by
have ih : append (as ()) nil = as () := appendNil $ as ()
have thunkAux : (fun _ => as ()) = as := funext fun x => by
cases x
exact rfl
by rw [ih, thunkAux]

14
tests/lean/run/doNotation3.lean
View file

@ -1,16 +1,16 @@
theorem zeroLtOfLt : {a b : Nat} → a < b → 0 < b
| 0, _, h => h
| a+1, b, h =>
have a < b from Nat.ltTrans (Nat.ltSuccSelf _) h
have : a < b := Nat.ltTrans (Nat.ltSuccSelf _) h
zeroLtOfLt this
def fold {m α β} [Monad m] (as : Array α) (b : β) (f : α → β → m β) : m β := do
let rec loop : (i : Nat) → i ≤ as.size → β → m β
| 0, h, b => b
| i+1, h, b => do
have h' : i < as.size from Nat.ltOfLtOfLe (Nat.ltSuccSelf i) h
have as.size - 1 < as.size from Nat.subLt (zeroLtOfLt h') (by decide)
have as.size - 1 - i < as.size from Nat.ltOfLeOfLt (Nat.subLe (as.size - 1) i) this
have h' : i < as.size := Nat.ltOfLtOfLe (Nat.ltSuccSelf i) h
have : as.size - 1 < as.size := Nat.subLt (zeroLtOfLt h') (by decide)
have : as.size - 1 - i < as.size := Nat.ltOfLeOfLt (Nat.subLe (as.size - 1) i) this
let b ← f (as.get ⟨as.size - 1 - i, this⟩) b
loop i (Nat.leOfLt h') b
loop as.size (Nat.leRefl _) b
@ -25,9 +25,9 @@ let rec loop (i : Nat) (h : i ≤ as.size) (b : β) : m β := do
match i, h with
| 0, h => return b
| i+1, h =>
have h' : i < as.size from Nat.ltOfLtOfLe (Nat.ltSuccSelf i) h
have as.size - 1 < as.size from Nat.subLt (zeroLtOfLt h') (by decide)
have as.size - 1 - i < as.size from Nat.ltOfLeOfLt (Nat.subLe (as.size - 1) i) this
have h' : i < as.size := Nat.ltOfLtOfLe (Nat.ltSuccSelf i) h
have : as.size - 1 < as.size := Nat.subLt (zeroLtOfLt h') (by decide)
have : as.size - 1 - i < as.size := Nat.ltOfLeOfLt (Nat.subLe (as.size - 1) i) this
let b ← f (as.get ⟨as.size - 1 - i, this⟩) b
loop i (Nat.leOfLt h') b
loop as.size (Nat.leRefl _) b

2
tests/lean/run/do_eqv.lean
View file

@ -1,5 +1,5 @@
theorem byCases_Bool_bind [Monad m] (x : m Bool) (f g : Bool → m β) (isTrue : f true = g true) (isFalse : f false = g false) : (x >>= f) = (x >>= g) := by
have f = g by
have : f = g := by
funext b; cases b <;> assumption
rw [this]

6
tests/lean/run/impLambdaTac.lean
View file

@ -19,13 +19,13 @@ example (P : Prop) : ∀ {p : P}, P := by
apply id
example (P : Prop) : ∀ p : P, P := by
have _ from 1
have : _ := 1
apply id
example (P : Prop) : ∀ {p : P}, P := by
refine noImplicitLambda% (have _ from 1; ?_)
refine noImplicitLambda% (have : _ := 1; ?_)
apply id
example (P : Prop) : ∀ {p : P}, P := by
have _ from 1
have : _ := 1
apply id

2
tests/lean/run/inj1.lean
View file

@ -13,7 +13,7 @@ by {
}
theorem test3 {α} (a b : α) (as bs : List α) (h : (x : List α) → (y : List α) → x = y) : as = bs :=
have a::as = b::bs from h (a::as) (b::bs);
have : a::as = b::bs := h (a::as) (b::bs);
by {
injection this with h1 h2;
exact h2

4
tests/lean/run/lean3_zulip_issues_1.lean
View file

@ -29,11 +29,11 @@ def f : wrap → Nat
| _ => 1
example (a : Nat) : True := by
have ∀ n, n ≥ 0 → a ≤ a from fun _ _ => Nat.leRefl ..
have : ∀ n, n ≥ 0 → a ≤ a := fun _ _ => Nat.leRefl ..
exact True.intro
example (ᾰ : Nat) : True := by
have ∀ n, n ≥ 0 → ᾰ ≤ ᾰ from fun _ _ => Nat.leRefl ..
have : ∀ n, n ≥ 0 → ᾰ ≤ ᾰ := fun _ _ => Nat.leRefl ..
exact True.intro
inductive Vec.{u} (α : Type u) : Nat → Type u

28
tests/lean/run/letrecInProofs.lean
View file

@ -16,12 +16,12 @@ theorem Tree.acyclic (x t : Tree) : x = t → x ≮ t := by
apply And.intro _ trivial
intro h; injection h
| node l r, h =>
have ihl : x ≮ l → node s x ≠ l ∧ node s x ≮ l from right x s l
have ihr : x ≮ r → node s x ≠ r ∧ node s x ≮ r from right x s r
have hl : x ≠ l ∧ x ≮ l from h.1
have hr : x ≠ r ∧ x ≮ r from h.2.1
have ihl : node s x ≠ l ∧ node s x ≮ l from ihl hl.2
have ihr : node s x ≠ r ∧ node s x ≮ r from ihr hr.2
have ihl : x ≮ l → node s x ≠ l ∧ node s x ≮ l := right x s l
have ihr : x ≮ r → node s x ≠ r ∧ node s x ≮ r := right x s r
have hl : x ≠ l ∧ x ≮ l := h.1
have hr : x ≠ r ∧ x ≮ r := h.2.1
have ihl : node s x ≠ l ∧ node s x ≮ l := ihl hl.2
have ihr : node s x ≠ r ∧ node s x ≮ r := ihr hr.2
apply And.intro
focus
intro h
@ -39,12 +39,12 @@ theorem Tree.acyclic (x t : Tree) : x = t → x ≮ t := by
apply And.intro _ trivial
intro h; injection h
| node l r, h =>
have ihl : x ≮ l → node x t ≠ l ∧ node x t ≮ l from left x t l
have ihr : x ≮ r → node x t ≠ r ∧ node x t ≮ r from left x t r
have hl : x ≠ l ∧ x ≮ l from h.1
have hr : x ≠ r ∧ x ≮ r from h.2.1
have ihl : node x t ≠ l ∧ node x t ≮ l from ihl hl.2
have ihr : node x t ≠ r ∧ node x t ≮ r from ihr hr.2
have ihl : x ≮ l → node x t ≠ l ∧ node x t ≮ l := left x t l
have ihr : x ≮ r → node x t ≠ r ∧ node x t ≮ r := left x t r
have hl : x ≠ l ∧ x ≮ l := h.1
have hr : x ≠ r ∧ x ≮ r := h.2.1
have ihl : node x t ≠ l ∧ node x t ≮ l := ihl hl.2
have ihr : node x t ≠ r ∧ node x t ≮ r := ihr hr.2
apply And.intro
focus
intro h
@ -59,8 +59,8 @@ theorem Tree.acyclic (x t : Tree) : x = t → x ≮ t := by
let rec aux : (x : Tree) → x ≮ x
| leaf => trivial
| node l r => by
have ih₁ : l ≮ l from aux l
have ih₂ : r ≮ r from aux r
have ih₁ : l ≮ l := aux l
have ih₂ : r ≮ r := aux r
show (node l r ≠ l ∧ node l r ≮ l) ∧ (node l r ≠ r ∧ node l r ≮ r) ∧ True
apply And.intro
focus

2
tests/lean/run/matrix.lean
View file

@ -39,7 +39,7 @@ where
match i, h with
| 0, h => acc
| i+1, h =>
have i < m from Nat.ltOfLtOfLe (Nat.ltSuccSelf _) h
have : i < m := Nat.ltOfLtOfLe (Nat.ltSuccSelf _) h
loop i (Nat.leOfLt this) (acc + u ⟨i, this⟩ * v ⟨i, this⟩)
instance [Zero α] : Zero (Matrix m n α) where

6
tests/lean/run/nativeReflBackdoor.lean
View file

@ -20,13 +20,13 @@ match b with
| true =>
/- The following `nativeDecide` is going to use `g` to evaluate `f`
because of the `implementedBy` directive. -/
have (f true) = false by nativeDecide
have : (f true) = false := by nativeDecide
this
| false => rfl
theorem trueEqFalse : true = false :=
have h₁ : f true = true from rfl;
have h₂ : f true = false from fConst true;
have h₁ : f true = true := rfl;
have h₂ : f true = false := fConst true;
Eq.trans h₁.symm h₂
/-

6
tests/lean/run/newfrontend1.lean
View file

@ -379,7 +379,7 @@ by intros h1 h2 h3;
theorem simple21 (x y z : Nat) : y = z → x = x → y = x → x = z :=
fun h1 _ h3 =>
have x = y from by { apply Eq.symm; assumption };
have : x = y := by { apply Eq.symm; assumption };
Eq.trans this (by assumption)
theorem simple22 (x y z : Nat) : y = z → y = x → id (x = z + 0) :=
@ -391,12 +391,12 @@ fun h1 h2 => show x = z + 0 by
theorem simple23 (x y z : Nat) : y = z → x = x → y = x → x = z :=
fun h1 _ h3 =>
have x = y by apply Eq.symm; assumption
have : x = y := by apply Eq.symm; assumption
Eq.trans this (by assumption)
theorem simple24 (x y z : Nat) : y = z → x = x → y = x → x = z :=
fun h1 _ h3 =>
have h : x = y by apply Eq.symm; assumption
have h : x = y := by apply Eq.symm; assumption
Eq.trans h (by assumption)
def f1 (x : Nat) : Nat :=

4
tests/lean/run/openInScopeBug.lean
View file

@ -13,8 +13,8 @@ theorem ex1 : f (g (g (g x))) = x := by
simp [Foo.ax1, Foo.ax2]
theorem ex2 : f (g (g (g x))) = x :=
have h₁ : f (g (g (g x))) = f (g x) by simp; /- try again with `Foo` scoped lemmas -/ open Foo in simp
have h₂ : f (g x) = x by simp; open Foo in simp
have h₁ : f (g (g (g x))) = f (g x) := by simp; /- try again with `Foo` scoped lemmas -/ open Foo in simp
have h₂ : f (g x) = x := by simp; open Foo in simp
Eq.trans h₁ h₂
-- open Foo in simp -- works

6
tests/lean/run/tactic1.lean
View file

@ -12,7 +12,7 @@ by {
theorem ex3 (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : x = z :=
by {
have y = z from h₂.symm;
have : y = z := h₂.symm;
apply Eq.trans;
exact h₁;
assumption
@ -44,14 +44,14 @@ by {
}
theorem ex7 (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : x = z := by
have y = z by apply Eq.symm; assumption
have : y = z := by apply Eq.symm; assumption
apply Eq.trans
exact h₁
assumption
theorem ex8 (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : x = z :=
by apply Eq.trans h₁;
have y = z by
have : y = z := by
apply Eq.symm;
assumption;
exact this

2
tests/lean/substlet.lean
View file

@ -21,6 +21,6 @@ theorem ex2 (n : Nat) : 0 + n = n := by
theorem ex3 (n : Nat) (h : n = 0) : 0 + n = 0 := by
let m := n + 1
let v := m + 1
have v = n + 2 from rfl
have : v = n + 2 := rfl
subst v -- error
done

4
tests/lean/tacUnsolvedGoalsErrors.lean
View file

@ -1,11 +1,11 @@
theorem ex1 (p q r : Prop) (h1 : p ∨ q) (h2 : p → q) : q :=
have q by -- Error here
have : q := by -- Error here
skip
by skip -- Error here
skip
theorem ex2 (p q r : Prop) (h1 : p ∨ q) (h2 : p → q) : q :=
have q by {
have : q := by {
skip
} -- Error here
by skip -- Error here

2
tests/lean/tacUnsolvedGoalsErrors.lean.expected.out
View file

@ -1,4 +1,4 @@
tacUnsolvedGoalsErrors.lean:2:9-3:8: error: unsolved goals
tacUnsolvedGoalsErrors.lean:2:14-3:8: error: unsolved goals
p q r : Prop
h1 : p ∨ q
h2 : p → q

4
tests/lean/unknownTactic.lean
View file

@ -5,11 +5,11 @@ theorem ex1 (x : Nat) : x = x → x = x := by
#print "---"
theorem ex2 (x : Nat) : x = x → x = x :=
have x = x by foo
have : x = x := by foo
fun h => h
#print "---"
theorem ex3 (x : Nat) : x = x → x = x :=
have x = x by foo (aaa bbb)
have : x = x := by foo (aaa bbb)
fun h => h

8
tests/lean/unknownTactic.lean.expected.out
View file

@ -4,12 +4,12 @@ x : Nat
a✝ : x = x
⊢ x = x
---
unknownTactic.lean:8:17: error: unknown tactic
unknownTactic.lean:8:13-8:19: error: unsolved goals
unknownTactic.lean:8:22: error: unknown tactic
unknownTactic.lean:8:18-8:24: error: unsolved goals
x : Nat
⊢ x = x
---
unknownTactic.lean:14:17: error: unknown tactic
unknownTactic.lean:14:13-14:19: error: unsolved goals
unknownTactic.lean:14:22: error: unknown tactic
unknownTactic.lean:14:18-14:24: error: unsolved goals
x : Nat
⊢ x = x