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

chore: cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-10 15:21:57 -08:00
parent 7f364feeb5
commit c665d5e20a
6 changed files with 30 additions and 167 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Init/Classical.lean
View file

@ -113,10 +113,10 @@ theorem axiomOfChoice {α : Sort u} {β : α → Sort v} {r : ∀ x, β x → Pr
theorem skolem {α : Sort u} {b : α → Sort v} {p : ∀ x, b x → Prop} : (∀ x, Exists (fun y => p x y)) ↔ Exists (fun (f : ∀ x, b x) => ∀ x, p x (f x)) :=
⟨axiomOfChoice, fun ⟨f, hw⟩ (x) => ⟨f x, hw x⟩⟩
theorem propComplete (a : Prop) : a = True ∨ a = False :=
match em a with
| Or.inl t => Or.inl (eqTrueIntro t)
| Or.inr f => Or.inr (eqFalseIntro f)
theorem propComplete (a : Prop) : a = True ∨ a = False := by
cases em a
| 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 }
-- this supercedes byCases in Decidable
theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=

140
src/Init/Core.lean
View file

@ -322,13 +322,6 @@ protected def Nat.prio := std.priority.default + 100
def std.prec.max : Nat := 1024 -- the strength of application, identifiers, (, [, etc.
def std.prec.arrow : Nat := 25
/-
The next def is "max + 10". It can be used e.g. for postfix operations that should
be stronger than application.
-/
def std.prec.maxPlus : Nat := std.prec.max + 10
/- Remark: tasks have an efficient implementation in the runtime. -/
structure Task (α : Type u) : Type u := pure ::
(get : α)
@ -449,21 +442,6 @@ theorem congrFun {α : Sort u} {β : α → Sort v} {f g : ∀ x, β x} (h : f =
theorem congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : a₁ = a₂) : f a₁ = f a₂ :=
congr rfl h
theorem transRelLeft {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : r a b) (h₂ : b = c) : r a c :=
h₂ ▸ h₁
theorem transRelRight {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : a = b) (h₂ : r b c) : r a c :=
h₁ ▸ h₂
theorem ofEqTrue {p : Prop} (h : p = True) : p :=
h ▸ trivial
theorem notOfEqFalse {p : Prop} (h : p = False) : ¬p :=
fun hp => h ▸ hp
theorem castProofIrrel {α β : Sort u} (h₁ h₂ : α = β) (a : α) : cast h₁ a = cast h₂ a :=
rfl
theorem castEq {α : Sort u} (h : α = α) (a : α) : cast h a = a :=
rfl
@ -552,9 +530,6 @@ end
theorem eqRecHEq {α : Sort u} {φ : α → Sort v} : {a a' : α} → (h : a = a') → (p : φ a) → (Eq.recOn (motive := fun x _ => φ x) h p) ≅ p
| a, _, rfl, p => HEq.refl p
theorem ofHEqTrue {a : Prop} (h : a ≅ True) : a :=
ofEqTrue (eqOfHEq h)
theorem heqOfEqRecEq {α β : Sort u} {a : α} {b : β} (h₁ : α = β) (h₂ : Eq.rec (motive := fun α _ => α) a h₁ = b) : a ≅ b := by
subst h₁
apply heqOfEq
@ -566,16 +541,6 @@ theorem castHEq : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a
variables {a b c d : Prop}
/- xor -/
def Xor (a b : Prop) : Prop :=
(a ∧ ¬ b) ∨ (b ∧ ¬ a)
theorem Iff.left : (a ↔ b) → a → b :=
Iff.mp
theorem Iff.right : (a ↔ b) → b → a :=
Iff.mpr
theorem iffIffImpliesAndImplies (a b : Prop) : (a ↔ b) ↔ (a → b) ∧ (b → a) :=
Iff.intro (fun h => And.intro h.mp h.mpr) (fun h => Iff.intro h.left h.right)
@ -591,44 +556,11 @@ theorem Iff.trans (h₁ : a ↔ b) (h₂ : b ↔ c) : a ↔ c :=
(fun hc => Iff.mpr h₁ (Iff.mpr h₂ hc))
theorem Iff.symm (h : a ↔ b) : b ↔ a :=
Iff.intro (Iff.right h) (Iff.left h)
Iff.intro (Iff.mpr h) (Iff.mp h)
theorem Iff.comm : (a ↔ b) ↔ (b ↔ a) :=
Iff.intro Iff.symm Iff.symm
theorem Eq.toIff {a b : Prop} (h : a = b) : a ↔ b :=
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);
absurd this h₁
theorem notIffNotOfIff (h₁ : a ↔ b) : ¬a ↔ ¬b :=
Iff.intro
(fun (hna : ¬ a) (hb : b) => hna (Iff.right h₁ hb))
(fun (hnb : ¬ b) (ha : a) => hnb (Iff.left h₁ ha))
theorem ofIffTrue (h : a ↔ True) : a :=
Iff.mp (Iff.symm h) trivial
theorem notOfIffFalse : (a ↔ False) → ¬a :=
Iff.mp
theorem iffTrueIntro (h : a) : a ↔ True :=
Iff.intro
(fun hl => trivial)
(fun hr => h)
theorem iffFalseIntro (h : ¬a) : a ↔ False :=
Iff.intro h (False.rec (fun _ => a))
theorem notNotIntro (ha : a) : ¬¬a :=
fun hna => hna ha
theorem notTrue : (¬ True) ↔ False :=
iffFalseIntro (notNotIntro trivial)
/- Exists -/
theorem Exists.elim {α : Sort u} {p : α → Prop} {b : Prop}
@ -648,7 +580,7 @@ instance {α : Type u} [DecidableEq α] : BEq α :=
theorem decideTrueEqTrue (h : Decidable True) : @decide True h = true :=
match h with
| isTrue h => rfl
| isFalse h => False.elim (Iff.mp notTrue h)
| isFalse h => False.elim $ h ⟨⟩
theorem decideFalseEqFalse (h : Decidable False) : @decide False h = false :=
match h with
@ -719,9 +651,6 @@ theorem byContradiction [dec : Decidable p] (h : ¬p → False) : p :=
theorem ofNotNot [Decidable p] : ¬ ¬ p → p :=
fun hnn => byContradiction (fun hn => absurd hn hnn)
theorem notNotIff (p) [Decidable p] : (¬ ¬ p) ↔ p :=
Iff.intro ofNotNot notNotIntro
theorem notAndIffOrNot (p q : Prop) [d₁ : Decidable p] [d₂ : Decidable q] : ¬ (p ∧ q) ↔ ¬ p ∨ ¬ q :=
Iff.intro
(fun h => match d₁, d₂ with
@ -737,11 +666,13 @@ end Decidable
section
variables {p q : Prop}
@[inline] def decidableOfDecidableOfIff (hp : Decidable p) (h : p ↔ q) : Decidable q :=
if hp : p then isTrue (Iff.mp h hp)
else isFalse (Iff.mp (notIffNotOfIff h) hp)
if hp : p then
isTrue (Iff.mp h hp)
else
isFalse fun hq => absurd (Iff.mpr h hq) hp
@[inline] def decidableOfDecidableOfEq (hp : Decidable p) (h : p = q) : Decidable q :=
decidableOfDecidableOfIff hp h.toIff
h ▸ hp
end
section
@ -783,21 +714,6 @@ instance [Decidable p] [Decidable q] : Decidable (p ↔ q) :=
isFalse fun h => hp (h.2 hq)
else
isTrue ⟨fun h => absurd h hp, fun h => absurd h hq⟩
instance [Decidable p] [Decidable q] : Decidable (Xor p q) :=
if hp : p then
if hq : q then
isFalse fun h => match h with
| Or.inl ⟨_, h⟩ => h hq
| Or.inr ⟨_, h⟩ => h hp
else
isTrue $ Or.inl ⟨hp, hq⟩
else if hq : q then
isTrue $ Or.inr ⟨hq, hp⟩
else
isFalse fun h => match h with
| Or.inl ⟨h, _⟩ => hp h
| Or.inr ⟨h, _⟩ => hq h
end
@[inline] instance {α : Sort u} [DecidableEq α] (a b : α) : Decidable (a ≠ b) :=
@ -805,14 +721,11 @@ end
| isTrue h => isFalse $ fun h' => absurd h h'
| isFalse h => isTrue h
theorem Bool.falseNeTrue (h : false = true) : False :=
Bool.noConfusion h
@[inline] instance : DecidableEq Bool :=
fun a b => match a, b with
| false, false => isTrue rfl
| false, true => isFalse Bool.falseNeTrue
| true, false => isFalse (Ne.symm Bool.falseNeTrue)
| false, true => isFalse fun h => Bool.noConfusion h
| true, false => isFalse fun h => Bool.noConfusion h
| true, true => isTrue rfl
/- if-then-else expression theorems -/
@ -996,32 +909,6 @@ inductive TC {α : Sort u} (r : α → α → Prop) : α → α → Prop
| base : ∀ a b, r a b → TC r a b
| trans : ∀ a b c, TC r a b → TC r b c → TC r a c
section Binary
variables {α : Type u} {β : Type v}
variable (f : α → α → α)
def Commutative :=
∀ a b, f a b = f b a
def Associative :=
∀ a b c, f (f a b) c = f a (f b c)
def RightCommutative (h : β → α → β) :=
∀ b a₁ a₂, h (h b a₁) a₂ = h (h b a₂) a₁
def LeftCommutative (h : α → β → β) :=
∀ a₁ a₂ b, h a₁ (h a₂ b) = h a₂ (h a₁ b)
theorem leftComm : Commutative f → Associative f → LeftCommutative f :=
fun hcomm hassoc a b c =>
((Eq.symm (hassoc a b c)).trans (hcomm a b ▸ rfl : f (f a b) c = f (f b a) c)).trans (hassoc b a c)
theorem rightComm : Commutative f → Associative f → RightCommutative f :=
fun hcomm hassoc a b c =>
((hassoc a b c).trans (hcomm b c ▸ rfl : f a (f b c) = f a (f c b))).trans (Eq.symm (hassoc a c b))
end Binary
/- Subtype -/
namespace Subtype
@ -1030,9 +917,6 @@ def existsOfSubtype {α : Type u} {p : α → Prop} : { x // p x } → Exists (f
variables {α : Type u} {p : α → Prop}
theorem tagIrrelevant {a : α} (h1 h2 : p a) : mk a h1 = mk a h2 :=
rfl
protected theorem eq : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2
| ⟨x, h1⟩, ⟨_, _⟩, rfl => rfl
@ -1175,12 +1059,6 @@ end Setoid
axiom propext {a b : Prop} : (a ↔ b) → a = b
theorem eqTrueIntro {a : Prop} (h : a) : a = True :=
propext (iffTrueIntro h)
theorem eqFalseIntro {a : Prop} (h : ¬a) : a = False :=
propext (iffFalseIntro h)
/- Quotients -/
-- Iff can now be used to do substitutions in a calculation

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

@ -55,7 +55,7 @@ def mkArray {α : Type u} (n : Nat) (v : α) : Array α := {
data := fun _ => v
}
theorem szMkArrayEq (n : Nat) (v : α) : (mkArray n v).sz = n :=
theorem sizeMkArrayEq (n : Nat) (v : α) : (mkArray n v).size = n :=
rfl
def empty : Array α :=

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

@ -152,11 +152,13 @@ protected theorem addAssoc : ∀ (n m k : Nat), (n + m) + k = n + (m + k)
| n, m, 0 => rfl
| n, m, succ k => congrArg succ (Nat.addAssoc n m k)
protected theorem addLeftComm : ∀ (n m k : Nat), n + (m + k) = m + (n + k) :=
leftComm Nat.add Nat.addComm Nat.addAssoc
protected theorem addLeftComm (n m k : Nat) : n + (m + k) = m + (n + k) := by
rw [← Nat.addAssoc, Nat.addComm n m, Nat.addAssoc]
exact rfl
protected theorem addRightComm : ∀ (n m k : Nat), (n + m) + k = (n + k) + m :=
rightComm Nat.add Nat.addComm Nat.addAssoc
protected theorem addRightComm (n m k : Nat) : (n + m) + k = (n + k) + m := by
rw [Nat.addAssoc, Nat.addComm m k, ← Nat.addAssoc]
exact rfl
protected theorem addLeftCancel : ∀ {n m k : Nat}, n + m = n + k → m = k
| 0, m, k, h => Nat.zeroAdd m ▸ Nat.zeroAdd k ▸ h
@ -481,11 +483,10 @@ protected theorem addLeAddLeft {n m : Nat} (h : n ≤ m) (k : Nat) : k + n ≤ k
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 _ _
transRelLeft (fun a b => a ≤ b) (transRelRight (fun a b => a ≤ b) h₁ h₂) h₃
protected theorem addLeAddRight {n m : Nat} (h : n ≤ m) (k : Nat) : n + k ≤ m + k := by
rw [Nat.addComm n k, Nat.addComm m k]
apply Nat.addLeAddLeft
assumption
protected theorem addLtAddLeft {n m : Nat} (h : n < m) (k : Nat) : k + n < k + m :=
ltOfSuccLe (addSucc k n ▸ Nat.addLeAddLeft (succLeOfLt h) k)

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

@ -12,7 +12,7 @@ def HashMapBucket (α : Type u) (β : Type v) :=
def HashMapBucket.update {α : Type u} {β : Type v} (data : HashMapBucket α β) (i : USize) (d : AssocList α β) (h : i.toNat < data.val.size) : HashMapBucket α β :=
⟨ data.val.uset i d h,
transRelRight Greater (Array.szFSetEq (data.val) ⟨USize.toNat i, h⟩ d) data.property ⟩
by rw [Array.szFSetEq]; exact data.property ⟩
structure HashMapImp (α : Type u) (β : Type v) :=
(size : Nat)
@ -23,13 +23,7 @@ def mkHashMapImp {α : Type u} {β : Type v} (nbuckets := 8) : HashMapImp α β
{ 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₃ : (if nbuckets = 0 then 8 else nbuckets) > 0 from
match nbuckets with
| 0 => Nat.zeroLtSucc _
| (Nat.succ x) => Nat.zeroLtSucc _
transRelRight Greater (Eq.trans p₁ p₂) p₃ ⟩ }
by rw [Array.sizeMkArrayEq]; cases nbuckets; decide!; apply Nat.zeroLtSucc; done ⟩ }
namespace HashMapImp
variables {α : Type u} {β : Type v}
@ -85,9 +79,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 (decide! : 2 > 0)
have (mkArray nbuckets (@AssocList.nil α β)).size = nbuckets from Array.szMkArrayEq _ _
have Array.size (mkArray nbuckets AssocList.nil) > 0 by rw this; assumption
let new_buckets : HashMapBucket α β := ⟨mkArray nbuckets AssocList.nil, this⟩
let new_buckets : HashMapBucket α β := ⟨mkArray nbuckets AssocList.nil, by rw [Array.sizeMkArrayEq]; assumption⟩
{ size := size,
buckets := moveEntries 0 buckets.val new_buckets }

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

@ -11,7 +11,7 @@ def HashSetBucket (α : Type u) :=
def HashSetBucket.update {α : Type u} (data : HashSetBucket α) (i : USize) (d : List α) (h : i.toNat < data.val.size) : HashSetBucket α :=
⟨ data.val.uset i d h,
transRelRight Greater (Array.szFSetEq (data.val) ⟨USize.toNat i, h⟩ d) data.property ⟩
by rw [Array.szFSetEq]; exact data.property ⟩
structure HashSetImp (α : Type u) :=
(size : Nat)
@ -22,13 +22,7 @@ def mkHashSetImp {α : Type u} (nbuckets := 8) : HashSetImp α :=
{ size := 0,
buckets :=
⟨ mkArray n [],
have p₁ : (mkArray n ([] : List α)).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 _
transRelRight Greater (Eq.trans p₁ p₂) p₃ ⟩ }
by rw [Array.sizeMkArrayEq]; cases nbuckets; decide!; apply Nat.zeroLtSucc ⟩ }
namespace HashSetImp
variables {α : Type u}
@ -78,9 +72,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 (decide! : 2 > 0)
have (mkArray nbuckets ([] : List α)).size = nbuckets from Array.szMkArrayEq _ _
have Array.size (mkArray nbuckets List.nil) > 0 by rw this; assumption
let new_buckets : HashSetBucket α := ⟨mkArray nbuckets [], this⟩;
let new_buckets : HashSetBucket α := ⟨mkArray nbuckets [], by rw [Array.sizeMkArrayEq]; assumption⟩
{ size := size,
buckets := moveEntries 0 buckets.val new_buckets }