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

chore: Heq ==> HEq

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-04 11:13:31 -08:00
parent 07f3ff61ea
commit 1784b0ee67
8 changed files with 61 additions and 73 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

78
src/Init/Core.lean
View file

@ -50,7 +50,7 @@ reserve infix ` ≤ `:50
reserve infix ` < `:50
reserve infix ` >= `:50
reserve infix ` ≥ `:50
reserve infix ` > `:50
reserve infix ` > `:50
/- boolean operations -/
@ -205,8 +205,8 @@ constant Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop}
-/
init_quot
inductive Heq {α : Sort u} (a : α) : ∀ {β : Sort u}, β → Prop
| refl : Heq a
inductive HEq {α : Sort u} (a : α) : ∀ {β : Sort u}, β → Prop
| refl : HEq a
structure Prod (α : Type u) (β : Type v) :=
(fst : α) (snd : β)
@ -242,14 +242,14 @@ h₂ ▸ h₁
theorem Eq.symm {α : Sort u} {a b : α} (h : a = b) : b = a :=
h ▸ rfl
infix `~=` := Heq
infix `≅` := Heq
infix `~=` := HEq
infix `≅` := HEq
@[matchPattern] def Heq.rfl {α : Sort u} {a : α} : a ≅ a := Heq.refl a
@[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' :=
fun (α' : Sort u) (a' : α') (h₁ : @Heq α a α' a') => Heq.recOn h₁ (fun (h₂ : α = α) => rfl);
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' :=
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 α)
@ -659,10 +659,10 @@ fun h₁ => h (h₁.symm)
theorem falseOfNe : a ≠ a → False := Ne.irrefl
theorem neFalseOfSelf : p → p ≠ False :=
fun (hp : p) (Heq : p = False) => Heq ▸ hp
fun (hp : p) (h : p = False) => h ▸ hp
theorem neTrueOfNot : ¬p → p ≠ True :=
fun (hnp : ¬p) (Heq : p = True) => (Heq ▸ hnp) trivial
fun (hnp : ¬p) (h : p = True) => (h ▸ hnp) trivial
theorem trueNeFalse : ¬True = False :=
neFalseOfSelf trivial
@ -680,46 +680,46 @@ section
variables {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ}
@[elabAsEliminator]
theorem Heq.ndrec.{u1, u2} {α : Sort u2} {a : α} {C : ∀ {β : Sort u2}, β → Sort u1} (m : C a) {β : Sort u2} {b : β} (h : a ≅ b) : C b :=
@Heq.rec α a (fun β b _ => C b) m β b h
theorem HEq.ndrec.{u1, u2} {α : Sort u2} {a : α} {C : ∀ {β : Sort u2}, β → Sort u1} (m : C a) {β : Sort u2} {b : β} (h : a ≅ b) : C b :=
@HEq.rec α a (fun β b _ => C b) m β b h
@[elabAsEliminator]
theorem Heq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {C : ∀ {β : Sort u2}, β → Sort u1} {β : Sort u2} {b : β} (h : a ≅ b) (m : C a) : C b :=
@Heq.rec α a (fun β b _ => C b) m β b h
theorem HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {C : ∀ {β : Sort u2}, β → Sort u1} {β : Sort u2} {b : β} (h : a ≅ b) (m : C a) : C b :=
@HEq.rec α a (fun β b _ => C b) m β b h
theorem Heq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a ≅ b) (h₂ : p a) : p b :=
Eq.recOn (eqOfHeq h₁) h₂
theorem HEq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a ≅ b) (h₂ : p a) : p b :=
Eq.recOn (eqOfHEq h₁) h₂
theorem Heq.subst {p : ∀ (T : Sort u), T → Prop} (h₁ : a ≅ b) (h₂ : p α a) : p β b :=
Heq.ndrecOn h₁ h₂
theorem HEq.subst {p : ∀ (T : Sort u), T → Prop} (h₁ : a ≅ b) (h₂ : p α a) : p β b :=
HEq.ndrecOn h₁ h₂
theorem Heq.symm (h : a ≅ b) : b ≅ a :=
Heq.ndrecOn h (Heq.refl a)
theorem HEq.symm (h : a ≅ b) : b ≅ a :=
HEq.ndrecOn h (HEq.refl a)
theorem heqOfEq (h : a = a') : a ≅ a' :=
Eq.subst h (Heq.refl a)
Eq.subst h (HEq.refl a)
theorem Heq.trans (h₁ : a ≅ b) (h₂ : b ≅ c) : a ≅ c :=
Heq.subst h₂ h₁
theorem HEq.trans (h₁ : a ≅ b) (h₂ : b ≅ c) : a ≅ c :=
HEq.subst h₂ h₁
theorem heqOfHeqOfEq (h₁ : a ≅ b) (h₂ : b = b') : a ≅ b' :=
Heq.trans h₁ (heqOfEq h₂)
theorem heqOfHEqOfEq (h₁ : a ≅ b) (h₂ : b = b') : a ≅ b' :=
HEq.trans h₁ (heqOfEq h₂)
theorem heqOfEqOfHeq (h₁ : a = a') (h₂ : a' ≅ b) : a ≅ b :=
Heq.trans (heqOfEq h₁) h₂
theorem heqOfEqOfHEq (h₁ : a = a') (h₂ : a' ≅ b) : a ≅ b :=
HEq.trans (heqOfEq h₁) h₂
def typeEqOfHeq (h : a ≅ b) : α = β :=
Heq.ndrecOn h (Eq.refl α)
def typeEqOfHEq (h : a ≅ b) : α = β :=
HEq.ndrecOn h (Eq.refl α)
end
theorem eqRecHeq {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} (h : a = a') (p : φ a), (Eq.recOn h p : φ a') ≅ p
| a, _, rfl, p => Heq.refl p
theorem eqRecHEq {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} (h : a = a') (p : φ a), (Eq.recOn h p : φ a') ≅ p
| a, _, rfl, p => HEq.refl p
theorem ofHeqTrue {a : Prop} (h : a ≅ True) : a :=
ofEqTrue (eqOfHeq h)
theorem ofHEqTrue {a : Prop} (h : a ≅ True) : a :=
ofEqTrue (eqOfHEq h)
theorem castHeq : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a
| α, _, rfl, a => Heq.refl a
theorem castHEq : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a
| α, _, rfl, a => HEq.refl a
variables {a b c d : Prop}
@ -1385,9 +1385,9 @@ Quot.rec f (fun a b h => Subsingleton.elim _ (f b)) q
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 := eqRecHeq (sound p) (f a);
Heq.trans p₁ (c a b p)
fun a b p => eqOfHEq $
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
end Quot

4
src/Init/WF.lean
View file

@ -233,13 +233,13 @@ Acc.ndrecOn aca $ fun (xa aca) (iha : ∀ y, r y xa → ∀ (b : β y), Acc (Lex
(∀ (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₃);
aux rfl (Heq.refl xb)
aux rfl (HEq.refl xb)
-- The lexicographical order of well founded relations is well-founded
def lexWf (ha : WellFounded r) (hb : ∀ x, WellFounded (s x)) : WellFounded (Lex r s) :=

14
src/library/constants.cpp
View file

@ -114,7 +114,6 @@ name const * g_list_to_array = nullptr;
name const * g_match_failed = nullptr;
name const * g_monad = nullptr;
name const * g_monad_fail = nullptr;
name const * g_lean_name = nullptr;
name const * g_lean_name_anonymous = nullptr;
name const * g_lean_name_num = nullptr;
name const * g_lean_name_str = nullptr;
@ -239,7 +238,7 @@ void initialize_constants() {
g_eq_subst = new name{"Eq", "subst"};
g_eq_symm = new name{"Eq", "symm"};
g_eq_trans = new name{"Eq", "trans"};
g_eq_of_heq = new name{"eqOfHeq"};
g_eq_of_heq = new name{"eqOfHEq"};
g_eq_true_intro = new name{"eqTrueIntro"};
g_eq_false_intro = new name{"eqFalseIntro"};
g_eq_self_iff_true = new name{"eqSelfIffTrue"};
@ -268,10 +267,10 @@ void initialize_constants() {
g_has_zero = new name{"HasZero"};
g_has_zero_zero = new name{"HasZero", "zero"};
g_has_coe_t = new name{"HasCoeT"};
g_heq = new name{"Heq"};
g_heq_refl = new name{"Heq", "refl"};
g_heq_symm = new name{"Heq", "symm"};
g_heq_trans = new name{"Heq", "trans"};
g_heq = new name{"HEq"};
g_heq_refl = new name{"HEq", "refl"};
g_heq_symm = new name{"HEq", "symm"};
g_heq_trans = new name{"HEq", "trans"};
g_heq_of_eq = new name{"heqOfEq"};
g_huge_fuel = new name{"hugeFuel"};
g_id = new name{"id"};
@ -303,7 +302,6 @@ void initialize_constants() {
g_match_failed = new name{"matchFailed"};
g_monad = new name{"Monad"};
g_monad_fail = new name{"MonadFail"};
g_lean_name = new name{"Lean", "Name"};
g_lean_name_anonymous = new name{"Lean", "Name", "anonymous"};
g_lean_name_num = new name{"Lean", "Name", "num"};
g_lean_name_str = new name{"Lean", "Name", "str"};
@ -493,7 +491,6 @@ void finalize_constants() {
delete g_match_failed;
delete g_monad;
delete g_monad_fail;
delete g_lean_name;
delete g_lean_name_anonymous;
delete g_lean_name_num;
delete g_lean_name_str;
@ -682,7 +679,6 @@ name const & get_list_to_array_name() { return *g_list_to_array; }
name const & get_match_failed_name() { return *g_match_failed; }
name const & get_monad_name() { return *g_monad; }
name const & get_monad_fail_name() { return *g_monad_fail; }
name const & get_lean_name_name() { return *g_lean_name; }
name const & get_lean_name_anonymous_name() { return *g_lean_name_anonymous; }
name const & get_lean_name_num_name() { return *g_lean_name_num; }
name const & get_lean_name_str_name() { return *g_lean_name_str; }

1
src/library/constants.h
View file

@ -116,7 +116,6 @@ name const & get_list_to_array_name();
name const & get_match_failed_name();
name const & get_monad_name();
name const & get_monad_fail_name();
name const & get_lean_name_name();
name const & get_lean_name_anonymous_name();
name const & get_lean_name_num_name();
name const & get_lean_name_str_name();

11
src/library/constants.txt
View file

@ -45,7 +45,7 @@ Eq.refl
Eq.subst
Eq.symm
Eq.trans
eqOfHeq
eqOfHEq
eqTrueIntro
eqFalseIntro
eqSelfIffTrue
@ -74,10 +74,10 @@ HasWellFounded.wf
HasZero
HasZero.zero
HasCoeT
Heq
Heq.refl
Heq.symm
Heq.trans
HEq
HEq.refl
HEq.symm
HEq.trans
heqOfEq
hugeFuel
id
@ -109,7 +109,6 @@ List.toArray
matchFailed
Monad
MonadFail
Lean.Name
Lean.Name.anonymous
Lean.Name.num
Lean.Name.str

14
stage0/src/library/constants.cpp
View file

@ -114,7 +114,6 @@ name const * g_list_to_array = nullptr;
name const * g_match_failed = nullptr;
name const * g_monad = nullptr;
name const * g_monad_fail = nullptr;
name const * g_lean_name = nullptr;
name const * g_lean_name_anonymous = nullptr;
name const * g_lean_name_num = nullptr;
name const * g_lean_name_str = nullptr;
@ -239,7 +238,7 @@ void initialize_constants() {
g_eq_subst = new name{"Eq", "subst"};
g_eq_symm = new name{"Eq", "symm"};
g_eq_trans = new name{"Eq", "trans"};
g_eq_of_heq = new name{"eqOfHeq"};
g_eq_of_heq = new name{"eqOfHEq"};
g_eq_true_intro = new name{"eqTrueIntro"};
g_eq_false_intro = new name{"eqFalseIntro"};
g_eq_self_iff_true = new name{"eqSelfIffTrue"};
@ -268,10 +267,10 @@ void initialize_constants() {
g_has_zero = new name{"HasZero"};
g_has_zero_zero = new name{"HasZero", "zero"};
g_has_coe_t = new name{"HasCoeT"};
g_heq = new name{"Heq"};
g_heq_refl = new name{"Heq", "refl"};
g_heq_symm = new name{"Heq", "symm"};
g_heq_trans = new name{"Heq", "trans"};
g_heq = new name{"HEq"};
g_heq_refl = new name{"HEq", "refl"};
g_heq_symm = new name{"HEq", "symm"};
g_heq_trans = new name{"HEq", "trans"};
g_heq_of_eq = new name{"heqOfEq"};
g_huge_fuel = new name{"hugeFuel"};
g_id = new name{"id"};
@ -303,7 +302,6 @@ void initialize_constants() {
g_match_failed = new name{"matchFailed"};
g_monad = new name{"Monad"};
g_monad_fail = new name{"MonadFail"};
g_lean_name = new name{"Lean", "Name"};
g_lean_name_anonymous = new name{"Lean", "Name", "anonymous"};
g_lean_name_num = new name{"Lean", "Name", "num"};
g_lean_name_str = new name{"Lean", "Name", "str"};
@ -493,7 +491,6 @@ void finalize_constants() {
delete g_match_failed;
delete g_monad;
delete g_monad_fail;
delete g_lean_name;
delete g_lean_name_anonymous;
delete g_lean_name_num;
delete g_lean_name_str;
@ -682,7 +679,6 @@ name const & get_list_to_array_name() { return *g_list_to_array; }
name const & get_match_failed_name() { return *g_match_failed; }
name const & get_monad_name() { return *g_monad; }
name const & get_monad_fail_name() { return *g_monad_fail; }
name const & get_lean_name_name() { return *g_lean_name; }
name const & get_lean_name_anonymous_name() { return *g_lean_name_anonymous; }
name const & get_lean_name_num_name() { return *g_lean_name_num; }
name const & get_lean_name_str_name() { return *g_lean_name_str; }

1
stage0/src/library/constants.h
View file

@ -116,7 +116,6 @@ name const & get_list_to_array_name();
name const & get_match_failed_name();
name const & get_monad_name();
name const & get_monad_fail_name();
name const & get_lean_name_name();
name const & get_lean_name_anonymous_name();
name const & get_lean_name_num_name();
name const & get_lean_name_str_name();

11
stage0/src/library/constants.txt
View file

@ -45,7 +45,7 @@ Eq.refl
Eq.subst
Eq.symm
Eq.trans
eqOfHeq
eqOfHEq
eqTrueIntro
eqFalseIntro
eqSelfIffTrue
@ -74,10 +74,10 @@ HasWellFounded.wf
HasZero
HasZero.zero
HasCoeT
Heq
Heq.refl
Heq.symm
Heq.trans
HEq
HEq.refl
HEq.symm
HEq.trans
heqOfEq
hugeFuel
id
@ -109,7 +109,6 @@ List.toArray
matchFailed
Monad
MonadFail
Lean.Name
Lean.Name.anonymous
Lean.Name.num
Lean.Name.str