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

chore(frontends/lean/builtin_exprs): make sure have-expression is consistent with let-expression

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-02 16:46:51 -07:00
parent 44730314ff
commit 7ba9a5012a
9 changed files with 113 additions and 111 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
library/init/core.lean
View file

@ -266,8 +266,8 @@ infix ≅ := Heq
@[matchPattern] def Heq.rfl {α : Sort u} {a : α} : a ≅ a := Heq.refl a
theorem eqOfHeq {α : Sort u} {a a' : α} (h : a ≅ a') : a = a' :=
have ∀ (α' : Sort u) (a' : α') (h₁ : @Heq α a α' a') (h₂ : α = α'), (Eq.recOn h₂ a : α') = a', from
fun (α' : Sort u) (a' : α') (h₁ : @Heq α a α' a') => Heq.recOn h₁ (fun h₂ : α = α => rfl),
have ∀ (α' : Sort u) (a' : α') (h₁ : @Heq α a α' a') (h₂ : α = α'), (Eq.recOn h₂ a : α') = a' :=
fun (α' : Sort u) (a' : α') (h₁ : @Heq α a α' a') => Heq.recOn h₁ (fun h₂ : α = α => rfl);
show (Eq.ndrecOn (Eq.refl α) a : α) = a', from
this α a' h (Eq.refl α)
@ -825,7 +825,7 @@ Eq.recOn h Iff.rfl
theorem neqOfNotIff {a b : Prop} : ¬(a ↔ b) → a ≠ b :=
fun h₁ h₂ =>
have a ↔ b, from Eq.subst h₂ (Iff.refl a),
have a ↔ b, from Eq.subst h₂ (Iff.refl a);
absurd this h₁
theorem notIffNotOfIff (h₁ : a ↔ b) : ¬a ↔ ¬b :=
@ -1437,7 +1437,7 @@ protected def hrecOn
(q : Quot r) (f : Π a, β (Quot.mk r a)) (c : ∀ (a b : α) (p : r a b), f a ≅ f b) : β q :=
Quot.recOn q f $
fun a b p => eqOfHeq $
have p₁ : (Eq.rec (f a) (sound p) : β (Quot.mk r b)) ≅ f a, from eqRecHeq (sound p) (f a),
have p₁ : (Eq.rec (f a) (sound p) : β (Quot.mk r b)) ≅ f a := eqRecHeq (sound p) (f a);
Heq.trans p₁ (c a b p)
end
@ -1705,34 +1705,34 @@ theorem chooseSpec {α : Sort u} {p : α → Prop} (h : Exists (fun x => p x)) :
theorem em (p : Prop) : p ∨ ¬p :=
let U (x : Prop) : Prop := x = True ∨ p;
let V (x : Prop) : Prop := x = False ∨ p;
have exU : Exists (fun x => U x), from ⟨True, Or.inl rfl⟩,
have exV : Exists (fun x => V x), from ⟨False, Or.inl rfl⟩,
have exU : Exists (fun x => U x), from ⟨True, Or.inl rfl⟩;
have exV : Exists (fun x => V x), from ⟨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 uDef : U u, from chooseSpec exU;
have vDef : V v, from chooseSpec exV;
have notUvOrP : u ≠ v ∨ p, from
Or.elim uDef
(fun hut : u = True =>
Or.elim vDef
(fun hvf : v = False =>
have hne : u ≠ v, from hvf.symm ▸ hut.symm ▸ trueNeFalse,
have hne : u ≠ v, from hvf.symm ▸ hut.symm ▸ trueNeFalse;
Or.inl hne)
Or.inr)
Or.inr,
Or.inr;
have pImpliesUv : p → u = v, from
fun hp : p =>
have hpred : U = V, from
funext $ fun x : Prop =>
have hl : (x = True ∨ p) → (x = False ∨ p), from
fun a => Or.inr hp,
fun a => Or.inr hp;
have hr : (x = False ∨ p) → (x = True ∨ p), from
fun a => Or.inr hp,
fun a => Or.inr hp;
show (x = True ∨ p) = (x = False ∨ p), from
propext (Iff.intro hl hr),
propext (Iff.intro hl hr);
have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV, from
hpred ▸ fun exU exV => rfl,
show u = v, from h₀ _ _,
hpred ▸ fun exU exV => rfl;
show u = v, from h₀ _ _;
Or.elim notUvOrP
(fun (hne : u ≠ v) => Or.inr (mt pImpliesUv hne))
Or.inl

4
library/init/data/dlist.lean
View file

@ -40,8 +40,8 @@ def cons : α → DList α → DList α
| a ⟨f, h⟩ := ⟨fun t => a :: f t,
fun t =>
show a :: f t = a :: f [] ++ t, from
have h₁ : a :: f t = a :: (f nil ++ t), from h t ▸ rfl,
have h₂ : a :: (f nil ++ t) = a :: f nil ++ t, from (consAppend _ _ _).symm,
have h₁ : a :: f t = a :: (f nil ++ t) := h t ▸ rfl;
have h₂ : a :: (f nil ++ t) = a :: f nil ++ t := (consAppend _ _ _).symm;
Eq.trans h₁ h₂⟩
def append : DList α → DList α → DList α

2
library/init/data/fin/basic.lean
View file

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

10
library/init/data/hashmap/basic.lean
View file

@ -24,12 +24,12 @@ let n := if nbuckets = 0 then 8 else nbuckets;
{ size := 0,
buckets :=
⟨ mkArray n AssocList.nil,
have p₁ : (mkArray n (@AssocList.nil α β)).size = n, from Array.szMkArrayEq _ _,
have p₂ : n = (if nbuckets = 0 then 8 else nbuckets), from rfl,
have p₁ : (mkArray n (@AssocList.nil α β)).size = n, from Array.szMkArrayEq _ _;
have p₂ : n = (if nbuckets = 0 then 8 else nbuckets), from rfl;
have p₃ : (if nbuckets = 0 then 8 else nbuckets) > 0, from
match nbuckets with
| 0 := Nat.zeroLtSucc _
| (Nat.succ x) := Nat.zeroLtSucc _,
| (Nat.succ x) := Nat.zeroLtSucc _;
transRelRight Greater (Eq.trans p₁ p₂) p₃ ⟩ }
namespace HashMapImp
@ -80,8 +80,8 @@ partial def moveEntries [Hashable α] : Nat → Array (AssocList α β) → Hash
def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β :=
let nbuckets := buckets.val.size * 2;
have aux₁ : nbuckets > 0, from Nat.mulPos buckets.property (Nat.zeroLtBit0 Nat.oneNeZero),
have aux₂ : (mkArray nbuckets (@AssocList.nil α β)).size = nbuckets, from Array.szMkArrayEq _ _,
have aux₁ : nbuckets > 0, from Nat.mulPos buckets.property (Nat.zeroLtBit0 Nat.oneNeZero);
have aux₂ : (mkArray nbuckets (@AssocList.nil α β)).size = nbuckets, from Array.szMkArrayEq _ _;
let new_buckets : HashMapBucket α β := ⟨mkArray nbuckets AssocList.nil, aux₂.symm ▸ aux₁⟩;
{ size := size,
buckets := moveEntries 0 buckets.val new_buckets }

8
library/init/data/list/basic.lean
View file

@ -71,10 +71,10 @@ theorem appendAssoc : ∀ (as bs cs : List α), (as ++ bs) ++ cs = as ++ (bs ++
| [] bs cs := rfl
| (a::as) bs cs :=
show ((a::as) ++ bs) ++ cs = (a::as) ++ (bs ++ cs), from
have h₁ : ((a::as) ++ bs) ++ cs = a::(as++bs) ++ cs, from congrArg (fun ds => ds ++ cs) (consAppend a as bs),
have h₂ : a::(as++bs) ++ cs = a::((as++bs) ++ cs), from consAppend a (as++bs) cs,
have h₃ : a::((as++bs) ++ cs) = a::(as ++ (bs ++ cs)), from congrArg (fun as => a::as) (appendAssoc as bs cs),
have h₄ : a::(as ++ (bs ++ cs)) = (a::as ++ (bs ++ cs)), from (consAppend a as (bs++cs)).symm,
have h₁ : ((a::as) ++ bs) ++ cs = a::(as++bs) ++ cs, from congrArg (fun ds => ds ++ cs) (consAppend a as bs);
have h₂ : a::(as++bs) ++ cs = a::((as++bs) ++ cs), from consAppend a (as++bs) cs;
have h₃ : a::((as++bs) ++ cs) = a::(as ++ (bs ++ cs)), from congrArg (fun as => a::as) (appendAssoc as bs cs);
have h₄ : a::(as ++ (bs ++ cs)) = (a::as ++ (bs ++ cs)), from (consAppend a as (bs++cs)).symm;
Eq.trans (Eq.trans (Eq.trans h₁ h₂) h₃) h₄
inductive Mem : α → List α → Prop

132
library/init/data/nat/basic.lean
View file

@ -21,8 +21,8 @@ theorem eqOfBeqEqTt : ∀ {n m : Nat}, beq n m = true → n = m
| zero (succ m) h := Bool.noConfusion h
| (succ n) zero h := Bool.noConfusion h
| (succ n) (succ m) h :=
have beq n m = true, from h,
have n = m, from eqOfBeqEqTt this,
have beq n m = true, from h;
have n = m, from eqOfBeqEqTt this;
congrArg succ this
theorem neOfBeqEqFf : ∀ {n m : Nat}, beq n m = false → n ≠ m
@ -30,8 +30,8 @@ theorem neOfBeqEqFf : ∀ {n m : Nat}, beq n m = false → 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 beq n m = false, from h₁,
have n ≠ m, from neOfBeqEqFf this,
have beq n m = false, from h₁;
have n ≠ m, from neOfBeqEqFf this;
Nat.noConfusion h₂ (fun h₂ => absurd h₂ this)
@[extern cpp "lean::nat_dec_eq"]
@ -157,12 +157,12 @@ protected theorem addLeftCancel : ∀ {n m k : Nat}, n + m = n + k → m = k
| 0 m k h := Nat.zeroAdd m ▸ Nat.zeroAdd k ▸ h
| (succ n) m k h :=
have n+m = n+k, from
have succ (n + m) = succ (n + k), from succAdd n m ▸ succAdd n k ▸ h,
Nat.noConfusion this id,
have succ (n + m) = succ (n + k), from succAdd n m ▸ succAdd n k ▸ h;
Nat.noConfusion this id;
addLeftCancel this
protected theorem addRightCancel {n m k : Nat} (h : n + m = k + m) : n = k :=
have m + n = m + k, from Nat.addComm n m ▸ Nat.addComm k m ▸ h,
have m + n = m + k, from Nat.addComm n m ▸ Nat.addComm k m ▸ h;
Nat.addLeftCancel this
/- Nat.mul theorems -/
@ -181,7 +181,7 @@ theorem succMul : ∀ (n m : Nat), (succ n) * m = (n * m) + m
| n 0 := rfl
| n (succ m) :=
have succ (n * m + m + n) = succ (n * m + n + m), from
congrArg succ (Nat.addRightComm _ _ _),
congrArg succ (Nat.addRightComm _ _ _);
(mulSucc n m).symm ▸ (mulSucc (succ n) m).symm ▸ (succMul n m).symm ▸ this
protected theorem mulComm : ∀ (n m : Nat), n * m = m * n
@ -197,31 +197,31 @@ Nat.mulComm n 1 ▸ Nat.mulOne n
protected theorem leftDistrib : ∀ (n m k : Nat), n * (m + k) = n * m + n * k
| 0 m k := (Nat.zeroMul (m + k)).symm ▸ (Nat.zeroMul m).symm ▸ (Nat.zeroMul k).symm ▸ rfl
| (succ n) m k :=
have h₁ : succ n * (m + k) = n * (m + k) + (m + k), from succMul _ _,
have h₂ : n * (m + k) + (m + k) = (n * m + n * k) + (m + k), from leftDistrib n m k ▸ rfl,
have h₃ : (n * m + n * k) + (m + k) = n * m + (n * k + (m + k)), from Nat.addAssoc _ _ _,
have h₄ : n * m + (n * k + (m + k)) = n * m + (m + (n * k + k)), from congrArg (fun x => n*m + x) (Nat.addLeftComm _ _ _),
have h₅ : n * m + (m + (n * k + k)) = (n * m + m) + (n * k + k), from (Nat.addAssoc _ _ _).symm,
have h₆ : (n * m + m) + (n * k + k) = (n * m + m) + succ n * k, from succMul n k ▸ rfl,
have h₇ : (n * m + m) + succ n * k = succ n * m + succ n * k, from succMul n m ▸ rfl,
have h₁ : succ n * (m + k) = n * (m + k) + (m + k), from succMul _ _;
have h₂ : n * (m + k) + (m + k) = (n * m + n * k) + (m + k), from leftDistrib n m k ▸ rfl;
have h₃ : (n * m + n * k) + (m + k) = n * m + (n * k + (m + k)), from Nat.addAssoc _ _ _;
have h₄ : n * m + (n * k + (m + k)) = n * m + (m + (n * k + k)), from congrArg (fun x => n*m + x) (Nat.addLeftComm _ _ _);
have h₅ : n * m + (m + (n * k + k)) = (n * m + m) + (n * k + k), from (Nat.addAssoc _ _ _).symm;
have h₆ : (n * m + m) + (n * k + k) = (n * m + m) + succ n * k, from succMul n k ▸ rfl;
have h₇ : (n * m + m) + succ n * k = succ n * m + succ n * k, from succMul n m ▸ rfl;
(((((h₁.trans h₂).trans h₃).trans h₄).trans h₅).trans h₆).trans h₇
protected theorem rightDistrib (n m k : Nat) : (n + m) * k = n * k + m * k :=
have h₁ : (n + m) * k = k * (n + m), from Nat.mulComm _ _,
have h₂ : k * (n + m) = k * n + k * m, from Nat.leftDistrib _ _ _,
have h₃ : k * n + k * m = n * k + k * m, from Nat.mulComm n k ▸ rfl,
have h₄ : n * k + k * m = n * k + m * k, from Nat.mulComm m k ▸ rfl,
have h₁ : (n + m) * k = k * (n + m), from Nat.mulComm _ _;
have h₂ : k * (n + m) = k * n + k * m, from Nat.leftDistrib _ _ _;
have h₃ : k * n + k * m = n * k + k * m, from Nat.mulComm n k ▸ rfl;
have h₄ : n * k + k * m = n * k + m * k, from Nat.mulComm m k ▸ rfl;
((h₁.trans h₂).trans h₃).trans h₄
protected theorem mulAssoc : ∀ (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.leftDistrib _ _ _,
have h₃ : (n * m * k) + n * m * 1 = (n * m * k) + n * m, from (Nat.mulOne (n*m)).symm ▸ rfl,
have h₄ : (n * m * k) + n * m = (n * (m * k)) + n * m, from (mulAssoc n m k).symm ▸ rfl,
have h₅ : (n * (m * k)) + n * m = n * (m * k + m), from (Nat.leftDistrib n (m*k) m).symm,
have h₆ : n * (m * k + m) = n * (m * succ k), from Nat.mulSucc m k ▸ rfl,
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.leftDistrib _ _ _;
have h₃ : (n * m * k) + n * m * 1 = (n * m * k) + n * m, from (Nat.mulOne (n*m)).symm ▸ rfl;
have h₄ : (n * m * k) + n * m = (n * (m * k)) + n * m, from (mulAssoc n m k).symm ▸ rfl;
have h₅ : (n * (m * k)) + n * m = n * (m * k + m), from (Nat.leftDistrib n (m*k) m).symm;
have h₆ : n * (m * k + m) = n * (m * succ k), from Nat.mulSucc m k ▸ rfl;
((((h₁.trans h₂).trans h₃).trans h₄).trans h₅).trans h₆
/- Inequalities -/
@ -245,8 +245,8 @@ theorem leStep : ∀ {n m : Nat}, n ≤ m → n ≤ succ m
| zero (succ n) h := rfl
| (succ n) zero h := Bool.noConfusion h
| (succ n) (succ m) h :=
have n ≤ m, from h,
have n ≤ succ m, from leStep this,
have n ≤ m, from h;
have n ≤ succ m, from leStep this;
succLeSucc this
theorem zeroLe : ∀ (n : Nat), 0 ≤ n
@ -286,8 +286,8 @@ protected theorem eqOrLtOfLe : ∀ {n m: Nat}, n ≤ m → n = m ∨ n < m
| zero (succ n) h := Or.inr $ zeroLe n
| (succ n) zero h := Bool.noConfusion h
| (succ n) (succ m) h :=
have n ≤ m, from h,
have n = m ∨ n < m, from eqOrLtOfLe this,
have n ≤ m, from h;
have n = m ∨ n < m, from eqOrLtOfLe this;
Or.elim this
(fun h => Or.inl $ congrArg succ h)
(fun h => Or.inr $ succLtSucc h)
@ -314,9 +314,9 @@ protected theorem leTrans : ∀ {n m k : Nat}, n ≤ m → m ≤ k → n ≤ k
| (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₁' : n ≤ m, from h₁,
have h₂' : m ≤ k, from h₂,
have n ≤ k, from leTrans h₁' h₂',
have h₁' : n ≤ m, from h₁;
have h₂' : m ≤ k, from h₂;
have n ≤ k, from leTrans h₁' h₂';
succLeSucc this
theorem predLe : ∀ (n : Nat), pred n ≤ n
@ -374,9 +374,9 @@ protected theorem leAntisymm : ∀ {n m : Nat}, n ≤ m → m ≤ n → n = m
| (succ n) zero h₁ h₂ := Bool.noConfusion h₁
| zero (succ m) h₁ h₂ := Bool.noConfusion h₂
| (succ n) (succ m) h₁ h₂ :=
have h₁' : n ≤ m, from h₁,
have h₂' : m ≤ n, from h₂,
have n = m, from leAntisymm h₁' h₂',
have h₁' : n ≤ m, from h₁;
have h₂' : m ≤ n, from h₂;
have n = m, from leAntisymm h₁' h₂';
congrArg succ this
protected theorem ltOrGe : ∀ (n m : Nat), n < m ∨ n ≥ m
@ -416,8 +416,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, from Nat.ltOfLeAndNe h h';
have succ m ≤ succ n, from succLeOfLt this;
Or.inl (leOfSuccLeSucc this))
theorem leAddRight : ∀ (n k : Nat), n ≤ n + k
@ -432,8 +432,8 @@ theorem le.dest : ∀ {n m : Nat}, n ≤ m → Exists (fun k => n + k = m)
| zero (succ n) h := ⟨succ n, show 0 + succ n = succ n, from (Nat.addComm 0 (succ n)).symm ▸ 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 le.dest this,
have n ≤ m, from h;
have Exists (fun k => n + k = m), from le.dest this;
match this with
| ⟨k, h⟩ := ⟨k, show succ n + k = succ m, from ((succAdd n k).symm ▸ h ▸ rfl)⟩
@ -443,7 +443,9 @@ h ▸ leAddRight n k
protected theorem notLeOfGt {n m : Nat} (h : n > m) : ¬ n ≤ m :=
fun h₁ => Or.elim (Nat.ltOrGe n m)
(fun h₂ => absurd (Nat.ltTrans h h₂) (Nat.ltIrrefl _))
(fun h₂ => have Heq : n = m, from Nat.leAntisymm h₁ h₂, absurd (@Eq.subst _ _ _ _ Heq h) (Nat.ltIrrefl m))
(fun h₂ =>
have Heq : n = m, from Nat.leAntisymm h₁ h₂;
absurd (@Eq.subst _ _ _ _ Heq h) (Nat.ltIrrefl m))
theorem gtOfNotLe {n m : Nat} (h : ¬ n ≤ m) : n > m :=
Or.elim (Nat.ltOrGe m n)
@ -458,14 +460,14 @@ Or.elim (Nat.ltOrGe 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.addAssoc _ _ _,
have h₂ : k + (n + w) = k + m, from congrArg _ hw,
have h₁ : k + n + w = k + (n + w), from Nat.addAssoc _ _ _;
have h₂ : k + (n + w) = k + m, from congrArg _ hw;
le.intro $ h₁.trans h₂
protected theorem addLeAddRight {n m : Nat} (h : n ≤ m) (k : Nat) : n + k ≤ m + k :=
have h₁ : n + k = k + n, from Nat.addComm _ _,
have h₂ : k + n ≤ k + m, from Nat.addLeAddLeft h k,
have h₃ : k + m = m + k, from Nat.addComm _ _,
have h₁ : n + k = k + n, from Nat.addComm _ _;
have h₂ : k + n ≤ k + m, from Nat.addLeAddLeft h k;
have h₃ : k + m = m + k, from Nat.addComm _ _;
transRelLeft (fun a b => a ≤ b) (transRelRight (fun a b => a ≤ b) h₁ h₂) h₃
protected theorem addLtAddLeft {n m : Nat} (h : n < m) (k : Nat) : k + n < k + m :=
@ -507,8 +509,8 @@ congrArg succ (succAdd n n)
protected theorem zeroLtBit0 : ∀ {n : Nat}, n ≠ 0 → 0 < bit0 n
| 0 h := absurd rfl h
| (succ n) h :=
have h₁ : 0 < succ (succ (bit0 n)), from zeroLtSucc _,
have h₂ : succ (succ (bit0 n)) = bit0 (succ n), from (Nat.bit0SuccEq n).symm,
have h₁ : 0 < succ (succ (bit0 n)), from zeroLtSucc _;
have h₂ : succ (succ (bit0 n)) = bit0 (succ n), from (Nat.bit0SuccEq n).symm;
transRelLeft (fun a b => a < b) h₁ h₂
protected theorem zeroLtBit1 (n : Nat) : 0 < bit1 n :=
@ -538,26 +540,26 @@ protected theorem bit1NeOne : ∀ {n : Nat}, n ≠ 0 → bit1 n ≠ 1
protected theorem bit0NeOne : ∀ n : Nat, bit0 n ≠ 1
| 0 h := absurd h (Ne.symm Nat.oneNeZero)
| (n+1) h :=
have h1 : succ (succ (n + n)) = 1, from succAdd n n ▸ h,
have h1 : succ (succ (n + n)) = 1, from succAdd n n ▸ h;
Nat.noConfusion h1
(fun h2 => absurd h2 (succNeZero (n + n)))
protected theorem addSelfNeOne : ∀ (n : Nat), n + n ≠ 1
| 0 h := Nat.noConfusion h
| (n+1) h :=
have h1 : succ (succ (n + n)) = 1, from succAdd n n ▸ h,
have h1 : succ (succ (n + n)) = 1, from succAdd n n ▸ h;
Nat.noConfusion h1 (fun h2 => absurd h2 (Nat.succNeZero (n + n)))
protected theorem bit1NeBit0 : ∀ (n m : Nat), bit1 n ≠ bit0 m
| 0 m h := absurd h (Ne.symm (Nat.addSelfNeOne m))
| (n+1) 0 h :=
have h1 : succ (bit0 (succ n)) = 0, from h,
have h1 : succ (bit0 (succ n)) = 0, from h;
absurd h1 (Nat.succNeZero _)
| (n+1) (m+1) h :=
have h1 : succ (succ (bit1 n)) = succ (succ (bit0 m)), from
Nat.bit0SuccEq m ▸ Nat.bit1SuccEq n ▸ h,
Nat.bit0SuccEq m ▸ Nat.bit1SuccEq n ▸ h;
have h2 : bit1 n = bit0 m, from
Nat.noConfusion h1 (fun h2' => Nat.noConfusion h2' (fun h2'' => h2'')),
Nat.noConfusion h1 (fun h2' => Nat.noConfusion h2' (fun h2'' => h2''));
absurd h2 (bit1NeBit0 n m)
protected theorem bit0NeBit1 : ∀ (n m : Nat), bit0 n ≠ bit1 m :=
@ -568,17 +570,17 @@ protected theorem bit0Inj : ∀ {n m : Nat}, bit0 n = bit0 m → n = m
| 0 (m+1) h := absurd h.symm (succNeZero _)
| (n+1) 0 h := absurd h (succNeZero _)
| (n+1) (m+1) h :=
have (n+1) + n = (m+1) + m, from Nat.noConfusion h id,
have n + (n+1) = m + (m+1), from Nat.addComm (m+1) m ▸ Nat.addComm (n+1) n ▸ this,
have succ (n + n) = succ (m + m), from this,
have n + n = m + m, from Nat.noConfusion this id,
have n = m, from bit0Inj this,
have (n+1) + n = (m+1) + m, from Nat.noConfusion h id;
have n + (n+1) = m + (m+1), from Nat.addComm (m+1) m ▸ Nat.addComm (n+1) n ▸ this;
have succ (n + n) = succ (m + m), from this;
have n + n = m + m, from Nat.noConfusion this id;
have n = m, from bit0Inj this;
congrArg (fun a => a + 1) this
protected theorem bit1Inj : ∀ {n m : Nat}, bit1 n = bit1 m → n = m :=
fun n m h =>
have succ (bit0 n) = succ (bit0 m), from Nat.bit1EqSuccBit0 n ▸ Nat.bit1EqSuccBit0 m ▸ h,
have bit0 n = bit0 m, from Nat.noConfusion this id,
have succ (bit0 n) = succ (bit0 m), from Nat.bit1EqSuccBit0 n ▸ Nat.bit1EqSuccBit0 m ▸ h;
have bit0 n = bit0 m, from Nat.noConfusion this id;
Nat.bit0Inj this
protected theorem bit0Ne {n m : Nat} : n ≠ m → bit0 n ≠ bit0 m :=
@ -625,9 +627,9 @@ ltSuccOfLe (Nat.addLeAdd h h)
protected theorem bit1LtBit0 : ∀ {n m : Nat}, n < m → bit1 n < bit0 m
| n 0 h := absurd h (notLtZero _)
| n (succ m) h :=
have n ≤ m, from leOfLtSucc h,
have succ (n + n) ≤ succ (m + m), from succLeSucc (addLeAdd this this),
have succ (n + n) ≤ succ m + m, from (succAdd m m).symm ▸ this,
have n ≤ m, from leOfLtSucc h;
have succ (n + n) ≤ succ (m + m), from succLeSucc (addLeAdd this this);
have succ (n + n) ≤ succ m + m, from (succAdd m m).symm ▸ this;
show succ (n + n) < succ (succ m + m), from ltSuccOfLe this
protected theorem oneLeBit1 (n : Nat) : 1 ≤ bit1 n :=
@ -646,7 +648,7 @@ protected theorem oneLeBit0 : ∀ (n : Nat), n ≠ 0 → 1 ≤ bit0 n
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.leftDistrib k n l ▸ hl.symm ▸ rfl,
have k * n + k * l = k * m, from Nat.leftDistrib k n l ▸ hl.symm ▸ rfl;
le.intro this
theorem mulLeMulRight {n m : Nat} (k : Nat) (h : n ≤ m) : n * k ≤ m * k :=
@ -662,7 +664,7 @@ protected theorem mulLtMulOfPosRight {n m k : Nat} (h : n < m) (hk : k > 0) : n
Nat.mulComm k m ▸ Nat.mulComm 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, from Nat.mulLtMulOfPosRight ha hb;
Nat.zeroMul m ▸ h
/- power -/
@ -678,7 +680,7 @@ 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, from eqZeroOfLeZero h;
this.symm ▸ Nat.leRefl _
| (succ j) h :=
Or.elim (ltOrEqOrLeSucc h)

16
library/init/data/nat/div.lean
View file

@ -69,12 +69,12 @@ div.inductionOn x y h₁ h₂
theorem modZero (a : Nat) : a % 0 = a :=
suffices (if 0 < 0 ∧ 0 ≤ a then (a - 0) % 0 else a) = a, from (modDef a 0).symm ▸ this,
have h : ¬ (0 < 0 ∧ 0 ≤ a), from fun ⟨h₁, _⟩ => absurd h₁ (Nat.ltIrrefl _),
have h : ¬ (0 < 0 ∧ 0 ≤ a), from fun ⟨h₁, _⟩ => absurd h₁ (Nat.ltIrrefl _);
ifNeg h
theorem modEqOfLt {a b : Nat} (h : a < b) : a % b = a :=
suffices (if 0 < b ∧ b ≤ a then (a - b) % b else a) = a, from (modDef a b).symm ▸ this,
have h' : ¬(0 < b ∧ b ≤ a), from fun ⟨_, h₁⟩ => absurd h₁ (Nat.notLeOfGt h),
have h' : ¬(0 < b ∧ b ≤ a), from fun ⟨_, h₁⟩ => absurd h₁ (Nat.notLeOfGt h);
ifNeg h'
theorem modEqSubMod {a b : Nat} (h : a ≥ b) : a % b = (a - b) % b :=
@ -85,17 +85,17 @@ Or.elim (eqZeroOrPos b)
theorem modLt (x : Nat) {y : Nat} : y > 0 → x % y < y :=
mod.inductionOn x y
(fun (x y) ⟨_, h₁⟩ (h₂ h₃) =>
have ih : (x - y) % y < y, from h₂ h₃,
have Heq : x % y = (x - y) % y, from modEqSubMod h₁,
have ih : (x - y) % y < y, from h₂ h₃;
have Heq : x % y = (x - y) % y, from modEqSubMod h₁;
Heq.symm ▸ ih)
(fun x y h₁ h₂ =>
have h₁ : ¬ 0 < y ∨ ¬ y ≤ x, from Iff.mp (Decidable.notAndIffOrNot _ _) h₁,
have h₁ : ¬ 0 < y ∨ ¬ y ≤ x, from Iff.mp (Decidable.notAndIffOrNot _ _) h₁;
Or.elim h₁
(fun h₁ => absurd h₂ h₁)
(fun h₁ =>
have hgt : y > x, from gtOfNotLe h₁,
have Heq : x % y = x, from modEqOfLt hgt,
Heq.symm ▸ hgt))
have hgt : y > x, from gtOfNotLe h₁;
have Heq : x % y = x, from modEqOfLt hgt;
Heq.symm ▸ hgt))
theorem modLe (x y : Nat) : x % y ≤ x :=
Or.elim (Nat.ltOrGe x y)

20
library/init/wf.lean
View file

@ -180,7 +180,7 @@ Acc.ndrecOn aca $ fun xa aca iha b =>
@Prod.Lex.recOn α β ra rb (fun p₁ p₂ _ => fst p₂ = xa → snd p₂ = xb → Acc (Lex ra rb) p₁)
p (xa, xb) lt
(fun (a₁ b₁ a₂ b₂ h) (Eq₂ : a₂ = xa) (Eq₃ : b₂ = xb) => iha a₁ (Eq.recOn Eq₂ h) b₁)
(fun (a b₁ b₂ h) (Eq₂ : a = xa) (Eq₃ : b₂ = xb) => Eq.recOn Eq₂.symm (ihb b₁ (Eq.recOn Eq₃ h))),
(fun (a b₁ b₂ h) (Eq₂ : a = xa) (Eq₃ : b₂ = xb) => Eq.recOn Eq₂.symm (ihb b₁ (Eq.recOn Eq₃ h)));
aux rfl rfl
-- The lexicographical order of well founded relations is well-founded
@ -227,19 +227,19 @@ Acc.ndrecOn aca $ fun (xa aca) (iha : ∀ y, r y xa → ∀ b : β y, Acc (Lex r
(fun (a₁ : α) (b₁ : β a₁) (a₂ : α) (b₂ : β a₂) (h : r a₁ a₂) (Eq₂ : a₂ = xa) (Eq₃ : b₂ ≅ xb) =>
have aux : (∀ (y : α), r y xa → ∀ (b : β y), Acc (Lex r s) ⟨y, b⟩) →
r a₁ a₂ → ∀ (b₁ : β a₁), Acc (Lex r s) ⟨a₁, b₁⟩,
from Eq.subst Eq₂ (fun iha h b₁ => iha a₁ h b₁),
from Eq.subst Eq₂ (fun iha h b₁ => iha a₁ h b₁);
aux iha h b₁)
(fun (a : α) (b₁ b₂ : β a) (h : s a b₁ b₂) (Eq₂ : a = xa) (Eq₃ : b₂ ≅ xb) =>
have aux : ∀ (xb : β xa), (∀ (y : β xa), s xa y xb → Acc (s xa) y) →
(∀ (y : β xa), s xa y xb → Acc (Lex r s) ⟨xa, y⟩) →
Lex r s p ⟨xa, xb⟩ → ∀ (b₁ : β a), s a b₁ b₂ → b₂ ≅ xb → Acc (Lex r s) ⟨a, b₁⟩,
from Eq.subst Eq₂ $ fun xb acb ihb lt b₁ h Eq₃ =>
have newEq₃ : b₂ = xb, from eqOfHeq Eq₃,
have newEq₃ : b₂ = xb, from eqOfHeq Eq₃;
have aux : (∀ (y : β a), s a y xb → Acc (Lex r s) ⟨a, y⟩) →
∀ (b₁ : β a), s a b₁ b₂ → Acc (Lex r s) ⟨a, b₁⟩,
from Eq.subst newEq₃ (fun ihb b₁ h => ihb b₁ h),
aux ihb b₁ h,
aux xb acb ihb lt b₁ h Eq₃),
from Eq.subst newEq₃ (fun ihb b₁ h => ihb b₁ h);
aux ihb b₁ h;
aux xb acb ihb lt b₁ h Eq₃);
aux rfl (Heq.refl xb)
-- The lexicographical order of well founded relations is well-founded
@ -281,13 +281,13 @@ Acc.recOn acb $ fun (xb acb) (ihb : ∀ y, s y xb → ∀ a, Acc (RevLex r s)
p ⟨xa, xb⟩ lt
(fun (a₁ a₂ b) (h : r a₁ a₂) (Eq₂ : a₂ = xa) (Eq₃ : b = xb) =>
show Acc (RevLex r s) ⟨a₁, b⟩, from
have r₁ : r a₁ xa, from Eq.recOn Eq₂ h,
have aux : Acc (RevLex r s) ⟨a₁, xb⟩, from iha a₁ r₁,
have r₁ : r a₁ xa, from Eq.recOn Eq₂ h;
have aux : Acc (RevLex r s) ⟨a₁, xb⟩, from iha a₁ r₁;
Eq.recOn (Eq.symm Eq₃) aux)
(fun (a₁ b₁ a₂ b₂) (h : s b₁ b₂) (Eq₂ : a₂ = xa) (Eq₃ : b₂ = xb) =>
show Acc (RevLex r s) (mk a₁ b₁), from
have s₁ : s b₁ xb, from Eq.recOn Eq₃ h,
ihb b₁ s₁ a₁),
have s₁ : s b₁ xb, from Eq.recOn Eq₃ h;
ihb b₁ s₁ a₁);
aux rfl rfl
def revLexWf (ha : WellFounded r) (hb : WellFounded s) : WellFounded (RevLex r s) :=

2
src/frontends/lean/builtin_exprs.cpp
View file

@ -417,7 +417,7 @@ static expr parse_have(parser & p, unsigned, expr const *, pos_info const & pos)
p.check_token_next(get_comma_tk(), "invalid 'have' declaration, ',' expected");
proof = parse_proof(p);
}
p.check_token_next(get_comma_tk(), "invalid 'have' declaration, ',' expected");
p.check_token_next(get_semicolon_tk(), "invalid 'have' declaration, ';' expected");
parser::local_scope scope(p);
expr l = p.save_pos(mk_local(id, prop), pos);
p.add_local(l);