refactor(library): rename heq.of_eq heq.to_eq auxiliary lemmas

This commit is contained in:
Leonardo de Moura 2016-01-09 12:32:18 -08:00
parent af42d3ff2d
commit d3242a2068
17 changed files with 81 additions and 63 deletions

View file

@ -261,13 +261,13 @@ namespace vector
assert e₂ : x = y, begin unfold to_list at h₁, injection h₁, assumption end, assert e₂ : x = y, begin unfold to_list at h₁, injection h₁, assumption end,
have to_list xs = to_list ys, begin unfold to_list at h₁, injection h₁, assumption end, have to_list xs = to_list ys, begin unfold to_list at h₁, injection h₁, assumption end,
assert xs == ys, from heq_of_list_eq this e₁, assert xs == ys, from heq_of_list_eq this e₁,
assert y :: xs == y :: ys, begin clear heq_of_list_eq h₁ h₂, revert xs ys this, induction e₁, intro xs ys h, rewrite [heq.to_eq h] end, assert y :: xs == y :: ys, begin clear heq_of_list_eq h₁ h₂, revert xs ys this, induction e₁, intro xs ys h, rewrite [eq_of_heq h] end,
show x :: xs == y :: ys, by rewrite e₂; exact this show x :: xs == y :: ys, by rewrite e₂; exact this
theorem list_eq_of_heq {n m} {v₁ : vector A n} {v₂ : vector A m} : v₁ == v₂ → n = m → to_list v₁ = to_list v₂ := theorem list_eq_of_heq {n m} {v₁ : vector A n} {v₂ : vector A m} : v₁ == v₂ → n = m → to_list v₁ = to_list v₂ :=
begin begin
intro h₁ h₂, revert v₁ v₂ h₁, intro h₁ h₂, revert v₁ v₂ h₁,
subst n, intro v₁ v₂ h₁, rewrite [heq.to_eq h₁] subst n, intro v₁ v₂ h₁, rewrite [eq_of_heq h₁]
end end
theorem of_list_to_list {n : nat} (v : vector A n) : of_list (to_list v) == v := theorem of_list_to_list {n : nat} (v : vector A n) : of_list (to_list v) == v :=

View file

@ -18,7 +18,7 @@ namespace sigma
theorem dpair_heq {a : A} {a' : A'} {b : B a} {b' : B' a'} theorem dpair_heq {a : A} {a' : A'} {b : B a} {b' : B' a'}
(HB : B == B') (Ha : a == a') (Hb : b == b') : ⟨a, b⟩ == ⟨a', b'⟩ := (HB : B == B') (Ha : a == a') (Hb : b == b') : ⟨a, b⟩ == ⟨a', b'⟩ :=
hcongr_arg4 @mk (heq.type_eq Ha) HB Ha Hb hcongr_arg4 @mk (type_eq_of_heq Ha) HB Ha Hb
protected theorem heq {p : Σa : A, B a} {p' : Σa' : A', B' a'} (HB : B == B') : protected theorem heq {p : Σa : A, B a} {p' : Σa' : A', B' a'} (HB : B == B') :
∀(H₁ : p.1 == p'.1) (H₂ : p.2 == p'.2), p == p' := ∀(H₁ : p.1 == p'.1) (H₂ : p.2 == p'.2), p == p' :=
@ -51,7 +51,7 @@ namespace sigma
theorem ndtrip_eq {A B : Type} {C : A → B → Type} {a₁ a₂ : A} {b₁ b₂ : B} theorem ndtrip_eq {A B : Type} {C : A → B → Type} {a₁ a₂ : A} {b₁ b₂ : B}
{c₁ : C a₁ b₁} {c₂ : C a₂ b₂} (H₁ : a₁ = a₂) (H₂ : b₁ = b₂) {c₁ : C a₁ b₁} {c₂ : C a₂ b₂} (H₁ : a₁ = a₂) (H₂ : b₁ = b₂)
(H₃ : cast (congr_arg2 C H₁ H₂) c₁ = c₂) : ⟨a₁, b₁, c₁⟩ = ⟨a₂, b₂, c₂⟩ := (H₃ : cast (congr_arg2 C H₁ H₂) c₁ = c₂) : ⟨a₁, b₁, c₁⟩ = ⟨a₂, b₂, c₂⟩ :=
hdcongr_arg3 dtrip H₁ (heq.of_eq H₂) H₃ hdcongr_arg3 dtrip H₁ (heq_of_eq H₂) H₃
theorem ndtrip_equal {A B : Type} {C : A → B → Type} {p₁ p₂ : Σa b, C a b} : theorem ndtrip_equal {A B : Type} {C : A → B → Type} {p₁ p₂ : Σa b, C a b} :
∀(H₁ : pr1 p₁ = pr1 p₂) (H₂ : pr2' p₁ = pr2' p₂) ∀(H₁ : pr1 p₁ = pr1 p₂) (H₂ : pr2' p₁ = pr2' p₂)

View file

@ -91,7 +91,7 @@ namespace tuple
theorem list_eq_of_heq {n m} {v₁ : tuple A n} {v₂ : tuple A m} : v₁ == v₂ → n = m → to_list v₁ = to_list v₂ := theorem list_eq_of_heq {n m} {v₁ : tuple A n} {v₂ : tuple A m} : v₁ == v₂ → n = m → to_list v₁ = to_list v₂ :=
begin begin
intro h₁ h₂, revert v₁ v₂ h₁, intro h₁ h₂, revert v₁ v₂ h₁,
subst n, intro v₁ v₂ h₁, rewrite [heq.to_eq h₁] subst n, intro v₁ v₂ h₁, rewrite [eq_of_heq h₁]
end end
theorem of_list_to_list {n : nat} (v : tuple A n) : of_list (to_list v) == v := theorem of_list_to_list {n : nat} (v : tuple A n) : of_list (to_list v) == v :=

View file

@ -168,39 +168,39 @@ end
infixl ` == `:50 := heq infixl ` == `:50 := heq
namespace heq section
universe variable u universe variable u
variables {A B C : Type.{u}} {a a' : A} {b b' : B} {c : C} variables {A B C : Type.{u}} {a a' : A} {b b' : B} {c : C}
theorem to_eq (H : a == a') : a = a' := theorem eq_of_heq (H : a == a') : a = a' :=
have H₁ : ∀ (Ht : A = A), eq.rec a Ht = a, from have H₁ : ∀ (Ht : A = A), eq.rec a Ht = a, from
λ Ht, eq.refl a, λ Ht, eq.refl a,
heq.rec H₁ H (eq.refl A) heq.rec H₁ H (eq.refl A)
theorem elim {A : Type} {a : A} {P : A → Type} {b : A} (H₁ : a == b) theorem heq.elim {A : Type} {a : A} {P : A → Type} {b : A} (H₁ : a == b)
: P a → P b := eq.rec_on (to_eq H₁) : P a → P b := eq.rec_on (eq_of_heq H₁)
theorem subst {P : ∀T : Type, T → Prop} : a == b → P A a → P B b := theorem heq.subst {P : ∀T : Type, T → Prop} : a == b → P A a → P B b :=
heq.rec_on heq.rec_on
theorem symm (H : a == b) : b == a := theorem heq.symm (H : a == b) : b == a :=
heq.rec_on H (refl a) heq.rec_on H (heq.refl a)
theorem of_eq (H : a = a') : a == a' := theorem heq_of_eq (H : a = a') : a == a' :=
eq.subst H (refl a) eq.subst H (heq.refl a)
theorem trans (H₁ : a == b) (H₂ : b == c) : a == c := theorem heq.trans (H₁ : a == b) (H₂ : b == c) : a == c :=
subst H₂ H₁ heq.subst H₂ H₁
theorem of_heq_of_eq (H₁ : a == b) (H₂ : b = b') : a == b' := theorem heq_of_heq_of_eq (H₁ : a == b) (H₂ : b = b') : a == b' :=
trans H₁ (of_eq H₂) heq.trans H₁ (heq_of_eq H₂)
theorem of_eq_of_heq (H₁ : a = a') (H₂ : a' == b) : a == b := theorem heq_of_eq_of_heq (H₁ : a = a') (H₂ : a' == b) : a == b :=
trans (of_eq H₁) H₂ heq.trans (heq_of_eq H₁) H₂
definition type_eq (H : a == b) : A = B := definition type_eq_of_heq (H : a == b) : A = B :=
heq.rec_on H (eq.refl A) heq.rec_on H (eq.refl A)
end heq end
open eq.ops open eq.ops
theorem eq_rec_heq {A : Type} {P : A → Type} {a a' : A} (H : a = a') (p : P a) : H ▹ p == p := theorem eq_rec_heq {A : Type} {P : A → Type} {a a' : A} (H : a = a') (p : P a) : H ▹ p == p :=
@ -213,7 +213,7 @@ theorem heq_of_eq_rec_right {A : Type} {P : A → Type} : ∀ {a a' : A} {p₁ :
| a a p₁ p₂ (eq.refl a) h := eq.rec_on h !heq.refl | a a p₁ p₂ (eq.refl a) h := eq.rec_on h !heq.refl
theorem of_heq_true {a : Prop} (H : a == true) : a := theorem of_heq_true {a : Prop} (H : a == true) : a :=
of_eq_true (heq.to_eq H) of_eq_true (eq_of_heq H)
theorem eq_rec_compose : ∀ {A B C : Type} (p₁ : B = C) (p₂ : A = B) (a : A), p₁ ▹ (p₂ ▹ a : B) = (p₂ ⬝ p₁) ▹ a theorem eq_rec_compose : ∀ {A B C : Type} (p₁ : B = C) (p₂ : A = B) (a : A), p₁ ▹ (p₂ ▹ a : B) = (p₂ ⬝ p₁) ▹ a
| A A A (eq.refl A) (eq.refl A) a := calc | A A A (eq.refl A) (eq.refl A) a := calc
@ -223,16 +223,16 @@ theorem eq_rec_compose : ∀ {A B C : Type} (p₁ : B = C) (p₂ : A = B) (a : A
theorem eq_rec_eq_eq_rec {A₁ A₂ : Type} {p : A₁ = A₂} : ∀ {a₁ : A₁} {a₂ : A₂}, p ▹ a₁ = a₂ → a₁ = p⁻¹ ▹ a₂ := theorem eq_rec_eq_eq_rec {A₁ A₂ : Type} {p : A₁ = A₂} : ∀ {a₁ : A₁} {a₂ : A₂}, p ▹ a₁ = a₂ → a₁ = p⁻¹ ▹ a₂ :=
eq.drec_on p (λ a₁ a₂ h, eq.drec_on h rfl) eq.drec_on p (λ a₁ a₂ h, eq.drec_on h rfl)
theorem eq_rec_of_heq_left : ∀ {A₁ A₂ : Type} {a₁ : A₁} {a₂ : A₂} (h : a₁ == a₂), heq.type_eq h ▹ a₁ = a₂ theorem eq_rec_of_heq_left : ∀ {A₁ A₂ : Type} {a₁ : A₁} {a₂ : A₂} (h : a₁ == a₂), type_eq_of_heq h ▹ a₁ = a₂
| A A a a (heq.refl a) := rfl | A A a a (heq.refl a) := rfl
theorem eq_rec_of_heq_right {A₁ A₂ : Type} {a₁ : A₁} {a₂ : A₂} (h : a₁ == a₂) : a₁ = (heq.type_eq h)⁻¹ ▹ a₂ := theorem eq_rec_of_heq_right {A₁ A₂ : Type} {a₁ : A₁} {a₂ : A₂} (h : a₁ == a₂) : a₁ = (type_eq_of_heq h)⁻¹ ▹ a₂ :=
eq_rec_eq_eq_rec (eq_rec_of_heq_left h) eq_rec_eq_eq_rec (eq_rec_of_heq_left h)
attribute heq.refl [refl] attribute heq.refl [refl]
attribute heq.trans [trans] attribute heq.trans [trans]
attribute heq.of_heq_of_eq [trans] attribute heq_of_heq_of_eq [trans]
attribute heq.of_eq_of_heq [trans] attribute heq_of_eq_of_heq [trans]
attribute heq.symm [symm] attribute heq.symm [symm]
/- and -/ /- and -/

View file

@ -78,7 +78,7 @@ namespace quot
protected definition hrec_on [reducible] protected definition hrec_on [reducible]
(q : quot s) (f : Π a, B ⟦a⟧) (c : ∀ (a b : A) (p : a ≈ b), f a == f b) : B q := (q : quot s) (f : Π a, B ⟦a⟧) (c : ∀ (a b : A) (p : a ≈ b), f a == f b) : B q :=
quot.rec_on q f quot.rec_on q f
(λ a b p, heq.to_eq (calc (λ a b p, eq_of_heq (calc
eq.rec (f a) (sound p) == f a : eq_rec_heq eq.rec (f a) (sound p) == f a : eq_rec_heq
... == f b : c a b p)) ... == f b : c a b p))
end end

View file

@ -33,7 +33,7 @@ namespace heq
C b H₁ := C b H₁ :=
heq.rec (λ H₁ : a == a, show C a H₁, from H₂) H₁ H₁ heq.rec (λ H₁ : a == a, show C a H₁, from H₂) H₁ H₁
theorem to_cast_eq (H : a == b) : cast (type_eq H) a = b := theorem to_cast_eq (H : a == b) : cast (type_eq_of_heq H) a = b :=
drec_on H !cast_eq drec_on H !cast_eq
end heq end heq
@ -96,7 +96,7 @@ section
theorem rec_on_pull (H : P = P') (f : Π x, P x) (a : A) : theorem rec_on_pull (H : P = P') (f : Π x, P x) (a : A) :
eq.rec_on H f a = eq.rec_on (congr_fun H a) (f a) := eq.rec_on H f a = eq.rec_on (congr_fun H a) (f a) :=
heq.to_eq (calc eq_of_heq (calc
eq.rec_on H f a == f a : rec_on_app H f a eq.rec_on H f a == f a : rec_on_app H f a
... == eq.rec_on (congr_fun H a) (f a) : heq.symm (eq_rec_heq (congr_fun H a) (f a))) ... == eq.rec_on (congr_fun H a) (f a) : heq.symm (eq_rec_heq (congr_fun H a) (f a)))
@ -107,7 +107,7 @@ end
-- function extensionality wrt heterogeneous equality -- function extensionality wrt heterogeneous equality
theorem hfunext {A : Type} {B : A → Type} {B' : A → Type} {f : Π x, B x} {g : Π x, B' x} theorem hfunext {A : Type} {B : A → Type} {B' : A → Type} {f : Π x, B x} {g : Π x, B' x}
(H : ∀ a, f a == g a) : f == g := (H : ∀ a, f a == g a) : f == g :=
cast_to_heq (funext (λ a, heq.to_eq (heq.trans (cast_app (funext (λ x, heq.type_eq (H x))) f a) (H a)))) cast_to_heq (funext (λ a, eq_of_heq (heq.trans (cast_app (funext (λ x, type_eq_of_heq (H x))) f a) (H a))))
section section
variables {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type} variables {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type}
@ -123,34 +123,34 @@ section
theorem dcongr_arg2 (f : Πa, B a → F) (Ha : a = a') (Hb : eq.rec_on Ha b = b') theorem dcongr_arg2 (f : Πa, B a → F) (Ha : a = a') (Hb : eq.rec_on Ha b = b')
: f a b = f a' b' := : f a b = f a' b' :=
heq.to_eq (hcongr_arg2 f Ha (eq_rec_to_heq Hb)) eq_of_heq (hcongr_arg2 f Ha (eq_rec_to_heq Hb))
theorem dcongr_arg3 (f : Πa b, C a b → F) (Ha : a = a') (Hb : eq.rec_on Ha b = b') theorem dcongr_arg3 (f : Πa b, C a b → F) (Ha : a = a') (Hb : eq.rec_on Ha b = b')
(Hc : cast (dcongr_arg2 C Ha Hb) c = c') : f a b c = f a' b' c' := (Hc : cast (dcongr_arg2 C Ha Hb) c = c') : f a b c = f a' b' c' :=
heq.to_eq (hcongr_arg3 f Ha (eq_rec_to_heq Hb) (eq_rec_to_heq Hc)) eq_of_heq (hcongr_arg3 f Ha (eq_rec_to_heq Hb) (eq_rec_to_heq Hc))
theorem dcongr_arg4 (f : Πa b c, D a b c → F) (Ha : a = a') (Hb : eq.rec_on Ha b = b') theorem dcongr_arg4 (f : Πa b c, D a b c → F) (Ha : a = a') (Hb : eq.rec_on Ha b = b')
(Hc : cast (dcongr_arg2 C Ha Hb) c = c') (Hc : cast (dcongr_arg2 C Ha Hb) c = c')
(Hd : cast (dcongr_arg3 D Ha Hb Hc) d = d') : f a b c d = f a' b' c' d' := (Hd : cast (dcongr_arg3 D Ha Hb Hc) d = d') : f a b c d = f a' b' c' d' :=
heq.to_eq (hcongr_arg4 f Ha (eq_rec_to_heq Hb) (eq_rec_to_heq Hc) (eq_rec_to_heq Hd)) eq_of_heq (hcongr_arg4 f Ha (eq_rec_to_heq Hb) (eq_rec_to_heq Hc) (eq_rec_to_heq Hd))
-- mixed versions (we want them for example if C a' b' is a subsingleton, like a proposition. -- mixed versions (we want them for example if C a' b' is a subsingleton, like a proposition.
-- Then proving eq is easier than proving heq) -- Then proving eq is easier than proving heq)
theorem hdcongr_arg3 (f : Πa b, C a b → F) (Ha : a = a') (Hb : b == b') theorem hdcongr_arg3 (f : Πa b, C a b → F) (Ha : a = a') (Hb : b == b')
(Hc : cast (heq.to_eq (hcongr_arg2 C Ha Hb)) c = c') (Hc : cast (eq_of_heq (hcongr_arg2 C Ha Hb)) c = c')
: f a b c = f a' b' c' := : f a b c = f a' b' c' :=
heq.to_eq (hcongr_arg3 f Ha Hb (eq_rec_to_heq Hc)) eq_of_heq (hcongr_arg3 f Ha Hb (eq_rec_to_heq Hc))
theorem hhdcongr_arg4 (f : Πa b c, D a b c → F) (Ha : a = a') (Hb : b == b') theorem hhdcongr_arg4 (f : Πa b c, D a b c → F) (Ha : a = a') (Hb : b == b')
(Hc : c == c') (Hc : c == c')
(Hd : cast (dcongr_arg3 D Ha (!eq.rec_on_irrel_arg ⬝ heq.to_cast_eq Hb) (Hd : cast (dcongr_arg3 D Ha (!eq.rec_on_irrel_arg ⬝ heq.to_cast_eq Hb)
(!eq.rec_on_irrel_arg ⬝ heq.to_cast_eq Hc)) d = d') (!eq.rec_on_irrel_arg ⬝ heq.to_cast_eq Hc)) d = d')
: f a b c d = f a' b' c' d' := : f a b c d = f a' b' c' d' :=
heq.to_eq (hcongr_arg4 f Ha Hb Hc (eq_rec_to_heq Hd)) eq_of_heq (hcongr_arg4 f Ha Hb Hc (eq_rec_to_heq Hd))
theorem hddcongr_arg4 (f : Πa b c, D a b c → F) (Ha : a = a') (Hb : b == b') theorem hddcongr_arg4 (f : Πa b c, D a b c → F) (Ha : a = a') (Hb : b == b')
(Hc : cast (heq.to_eq (hcongr_arg2 C Ha Hb)) c = c') (Hc : cast (eq_of_heq (hcongr_arg2 C Ha Hb)) c = c')
(Hd : cast (hdcongr_arg3 D Ha Hb Hc) d = d') (Hd : cast (hdcongr_arg3 D Ha Hb Hc) d = d')
: f a b c d = f a' b' c' d' := : f a b c d = f a' b' c' d' :=
heq.to_eq (hcongr_arg4 f Ha Hb (eq_rec_to_heq Hc) (eq_rec_to_heq Hd)) eq_of_heq (hcongr_arg4 f Ha Hb (eq_rec_to_heq Hc) (eq_rec_to_heq Hd))
end end

View file

@ -44,6 +44,7 @@ name const * g_eq_refl = nullptr;
name const * g_eq_subst = nullptr; name const * g_eq_subst = nullptr;
name const * g_eq_symm = nullptr; name const * g_eq_symm = nullptr;
name const * g_eq_trans = nullptr; name const * g_eq_trans = nullptr;
name const * g_eq_of_heq = nullptr;
name const * g_exists_elim = nullptr; name const * g_exists_elim = nullptr;
name const * g_false = nullptr; name const * g_false = nullptr;
name const * g_false_of_true_iff_false = nullptr; name const * g_false_of_true_iff_false = nullptr;
@ -61,7 +62,9 @@ name const * g_has_zero = nullptr;
name const * g_has_zero_zero = nullptr; name const * g_has_zero_zero = nullptr;
name const * g_heq = nullptr; name const * g_heq = nullptr;
name const * g_heq_refl = nullptr; name const * g_heq_refl = nullptr;
name const * g_heq_to_eq = nullptr; name const * g_heq_symm = nullptr;
name const * g_heq_trans = nullptr;
name const * g_heq_of_eq = nullptr;
name const * g_iff = nullptr; name const * g_iff = nullptr;
name const * g_iff_elim_left = nullptr; name const * g_iff_elim_left = nullptr;
name const * g_iff_elim_right = nullptr; name const * g_iff_elim_right = nullptr;
@ -304,6 +307,7 @@ void initialize_constants() {
g_eq_subst = new name{"eq", "subst"}; g_eq_subst = new name{"eq", "subst"};
g_eq_symm = new name{"eq", "symm"}; g_eq_symm = new name{"eq", "symm"};
g_eq_trans = new name{"eq", "trans"}; g_eq_trans = new name{"eq", "trans"};
g_eq_of_heq = new name{"eq_of_heq"};
g_exists_elim = new name{"exists", "elim"}; g_exists_elim = new name{"exists", "elim"};
g_false = new name{"false"}; g_false = new name{"false"};
g_false_of_true_iff_false = new name{"false_of_true_iff_false"}; g_false_of_true_iff_false = new name{"false_of_true_iff_false"};
@ -321,7 +325,9 @@ void initialize_constants() {
g_has_zero_zero = new name{"has_zero", "zero"}; g_has_zero_zero = new name{"has_zero", "zero"};
g_heq = new name{"heq"}; g_heq = new name{"heq"};
g_heq_refl = new name{"heq", "refl"}; g_heq_refl = new name{"heq", "refl"};
g_heq_to_eq = new name{"heq", "to_eq"}; g_heq_symm = new name{"heq", "symm"};
g_heq_trans = new name{"heq", "trans"};
g_heq_of_eq = new name{"heq_of_eq"};
g_iff = new name{"iff"}; g_iff = new name{"iff"};
g_iff_elim_left = new name{"iff", "elim_left"}; g_iff_elim_left = new name{"iff", "elim_left"};
g_iff_elim_right = new name{"iff", "elim_right"}; g_iff_elim_right = new name{"iff", "elim_right"};
@ -565,6 +571,7 @@ void finalize_constants() {
delete g_eq_subst; delete g_eq_subst;
delete g_eq_symm; delete g_eq_symm;
delete g_eq_trans; delete g_eq_trans;
delete g_eq_of_heq;
delete g_exists_elim; delete g_exists_elim;
delete g_false; delete g_false;
delete g_false_of_true_iff_false; delete g_false_of_true_iff_false;
@ -582,7 +589,9 @@ void finalize_constants() {
delete g_has_zero_zero; delete g_has_zero_zero;
delete g_heq; delete g_heq;
delete g_heq_refl; delete g_heq_refl;
delete g_heq_to_eq; delete g_heq_symm;
delete g_heq_trans;
delete g_heq_of_eq;
delete g_iff; delete g_iff;
delete g_iff_elim_left; delete g_iff_elim_left;
delete g_iff_elim_right; delete g_iff_elim_right;
@ -825,6 +834,7 @@ name const & get_eq_refl_name() { return *g_eq_refl; }
name const & get_eq_subst_name() { return *g_eq_subst; } name const & get_eq_subst_name() { return *g_eq_subst; }
name const & get_eq_symm_name() { return *g_eq_symm; } name const & get_eq_symm_name() { return *g_eq_symm; }
name const & get_eq_trans_name() { return *g_eq_trans; } name const & get_eq_trans_name() { return *g_eq_trans; }
name const & get_eq_of_heq_name() { return *g_eq_of_heq; }
name const & get_exists_elim_name() { return *g_exists_elim; } name const & get_exists_elim_name() { return *g_exists_elim; }
name const & get_false_name() { return *g_false; } name const & get_false_name() { return *g_false; }
name const & get_false_of_true_iff_false_name() { return *g_false_of_true_iff_false; } name const & get_false_of_true_iff_false_name() { return *g_false_of_true_iff_false; }
@ -842,7 +852,9 @@ name const & get_has_zero_name() { return *g_has_zero; }
name const & get_has_zero_zero_name() { return *g_has_zero_zero; } name const & get_has_zero_zero_name() { return *g_has_zero_zero; }
name const & get_heq_name() { return *g_heq; } name const & get_heq_name() { return *g_heq; }
name const & get_heq_refl_name() { return *g_heq_refl; } name const & get_heq_refl_name() { return *g_heq_refl; }
name const & get_heq_to_eq_name() { return *g_heq_to_eq; } name const & get_heq_symm_name() { return *g_heq_symm; }
name const & get_heq_trans_name() { return *g_heq_trans; }
name const & get_heq_of_eq_name() { return *g_heq_of_eq; }
name const & get_iff_name() { return *g_iff; } name const & get_iff_name() { return *g_iff; }
name const & get_iff_elim_left_name() { return *g_iff_elim_left; } name const & get_iff_elim_left_name() { return *g_iff_elim_left; }
name const & get_iff_elim_right_name() { return *g_iff_elim_right; } name const & get_iff_elim_right_name() { return *g_iff_elim_right; }

View file

@ -46,6 +46,7 @@ name const & get_eq_refl_name();
name const & get_eq_subst_name(); name const & get_eq_subst_name();
name const & get_eq_symm_name(); name const & get_eq_symm_name();
name const & get_eq_trans_name(); name const & get_eq_trans_name();
name const & get_eq_of_heq_name();
name const & get_exists_elim_name(); name const & get_exists_elim_name();
name const & get_false_name(); name const & get_false_name();
name const & get_false_of_true_iff_false_name(); name const & get_false_of_true_iff_false_name();
@ -63,7 +64,9 @@ name const & get_has_zero_name();
name const & get_has_zero_zero_name(); name const & get_has_zero_zero_name();
name const & get_heq_name(); name const & get_heq_name();
name const & get_heq_refl_name(); name const & get_heq_refl_name();
name const & get_heq_to_eq_name(); name const & get_heq_symm_name();
name const & get_heq_trans_name();
name const & get_heq_of_eq_name();
name const & get_iff_name(); name const & get_iff_name();
name const & get_iff_elim_left_name(); name const & get_iff_elim_left_name();
name const & get_iff_elim_right_name(); name const & get_iff_elim_right_name();

View file

@ -39,6 +39,7 @@ eq.refl
eq.subst eq.subst
eq.symm eq.symm
eq.trans eq.trans
eq_of_heq
exists.elim exists.elim
false false
false_of_true_iff_false false_of_true_iff_false
@ -56,7 +57,9 @@ has_zero
has_zero.zero has_zero.zero
heq heq
heq.refl heq.refl
heq.to_eq heq.symm
heq.trans
heq_of_eq
iff iff
iff.elim_left iff.elim_left
iff.elim_right iff.elim_right

View file

@ -123,7 +123,7 @@ tactic intros_num_tactic(unsigned num, list<name> _ns) {
goal new_goal(new_meta, new_type); goal new_goal(new_meta, new_type);
expr H = mk_local(ngen.next(), binding_domain(t)); expr H = mk_local(ngen.next(), binding_domain(t));
levels heq_lvl = const_levels(get_app_fn(Htype)); levels heq_lvl = const_levels(get_app_fn(Htype));
expr arg = mk_app(mk_constant(get_heq_to_eq_name(), heq_lvl), A, lhs, rhs, H); expr arg = mk_app(mk_constant(get_eq_of_heq_name(), heq_lvl), A, lhs, rhs, H);
expr V = Fun(H, mk_app(new_meta, arg)); expr V = Fun(H, mk_app(new_meta, arg));
substitution new_subst = s.get_subst(); substitution new_subst = s.get_subst();
assign(new_subst, g, V); assign(new_subst, g, V);

View file

@ -605,7 +605,7 @@ class inversion_tac {
goal new_g(new_meta, new_type); goal new_g(new_meta, new_type);
hyps.pop_back(); hyps.pop_back();
expr H = mk_local(m_ngen.next(), g.get_unused_name(binding_name(type)), binding_domain(type), binder_info()); expr H = mk_local(m_ngen.next(), g.get_unused_name(binding_name(type)), binding_domain(type), binder_info());
expr to_eq = mk_app(mk_constant(get_heq_to_eq_name(), const_levels(heq_fn)), args[0], args[1], args[3], H); expr to_eq = mk_app(mk_constant(get_eq_of_heq_name(), const_levels(heq_fn)), args[0], args[1], args[3], H);
expr val = Fun(H, mk_app(mk_app(new_mvar, hyps), to_eq)); expr val = Fun(H, mk_app(mk_app(new_mvar, hyps), to_eq));
assign(g, val); assign(g, val);
return new_g; return new_g;

View file

@ -1,4 +1,4 @@
import logic.cast import logic.cast
theorem cast_heq : ∀ {A B : Type} (H : A = B) (a : A), cast H a == a theorem cast_heq : ∀ {A B : Type} (H : A = B) (a : A), cast H a == a
| A A (eq.refl A) a := heq.of_eq (cast_refl a) | A A (eq.refl A) a := heq_of_eq (cast_refl a)

View file

@ -43,7 +43,7 @@ pquot.rec f
have aux₁ : f a == f b, from sound a b H, have aux₁ : f a == f b, from sound a b H,
have aux₂ : pquot.abs R a = pquot.abs R b, from pquot.eq R H, have aux₂ : pquot.abs R a = pquot.abs R b, from pquot.eq R H,
have aux₃ : ∀ (c₁ c₂ : C (pquot.abs R a)) (e : c₁ == c₂), P (pquot.abs R a) c₁ → P (pquot.abs R a) c₂, from have aux₃ : ∀ (c₁ c₂ : C (pquot.abs R a)) (e : c₁ == c₂), P (pquot.abs R a) c₁ → P (pquot.abs R a) c₂, from
λ c₁ c₂ e H, eq.rec_on (heq.to_eq e) H, λ c₁ c₂ e H, eq.rec_on (eq_of_heq e) H,
have aux₄ : ∀ (c₁ : C (pquot.abs R a)) (c₂ : C (pquot.abs R b)) (e : c₁ == c₂), P (pquot.abs R a) c₁ → P (pquot.abs R b) c₂, from have aux₄ : ∀ (c₁ : C (pquot.abs R a)) (c₂ : C (pquot.abs R b)) (e : c₁ == c₂), P (pquot.abs R a) c₁ → P (pquot.abs R b) c₂, from
eq.rec_on aux₂ aux₃, eq.rec_on aux₂ aux₃,
show P (pquot.abs R b) (f b), from show P (pquot.abs R b) (f b), from
@ -55,7 +55,7 @@ definition pquot.lift {A : Type} {R : A → A → Prop} {B : Type}
(sound : ∀ (a b : A), R a b → f a = f b) (sound : ∀ (a b : A), R a b → f a = f b)
(q : pquot R) (q : pquot R)
: B := : B :=
pquot.rec_on q f (λ (a b : A) (H : R a b), heq.of_eq (sound a b H)) pquot.rec_on q f (λ (a b : A) (H : R a b), heq_of_eq (sound a b H))
theorem pquot.induction_on {A : Type} {R : A → A → Prop} {P : pquot R → Prop} theorem pquot.induction_on {A : Type} {R : A → A → Prop} {P : pquot R → Prop}
(q : pquot R) (q : pquot R)

View file

@ -19,7 +19,7 @@ namespace vector
theorem vcons.inj₂ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → v₁ = v₂ := theorem vcons.inj₂ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → v₁ = v₂ :=
begin begin
intro h, apply heq.to_eq, apply (no_confusion h), intros, eassumption, intro h, apply eq_of_heq, apply (no_confusion h), intros, eassumption,
end end
set_option pp.universes true set_option pp.universes true

View file

@ -34,8 +34,8 @@ well_founded.intro (λ (bv : vec A),
have gen₂ : ∀ (m : nat) (Heq₁ : n₂ = m) (v : vector A m) (ih : acc (direct_subterm A) (to_vec v)) have gen₂ : ∀ (m : nat) (Heq₁ : n₂ = m) (v : vector A m) (ih : acc (direct_subterm A) (to_vec v))
(Heq₂ : @cons A a₂ n₂ v₂ == @cons A a₁ m v), acc (direct_subterm A) (to_vec v₂), from (Heq₂ : @cons A a₂ n₂ v₂ == @cons A a₁ m v), acc (direct_subterm A) (to_vec v₂), from
λ m Heq₁, eq.rec_on Heq₁ (λ (v : vector A n₂) (ih : acc (direct_subterm A) (to_vec v)) (Heq₂ : @cons A a₂ n₂ v₂ == @cons A a₁ n₂ v), λ m Heq₁, eq.rec_on Heq₁ (λ (v : vector A n₂) (ih : acc (direct_subterm A) (to_vec v)) (Heq₂ : @cons A a₂ n₂ v₂ == @cons A a₁ n₂ v),
vector.no_confusion (heq.to_eq Heq₂) (λ (e₄ : a₂ = a₁) (e₅ : n₂ = n₂) (e₆ : v₂ == v), vector.no_confusion (eq_of_heq Heq₂) (λ (e₄ : a₂ = a₁) (e₅ : n₂ = n₂) (e₆ : v₂ == v),
eq.rec_on (heq.to_eq (heq.symm e₆)) ih)), eq.rec_on (eq_of_heq (heq.symm e₆)) ih)),
gen₂ n₁ e₃ v₁ ih e₂))), gen₂ n₁ e₃ v₁ ih e₂))),
gen (to_vec (cons a₁ v₁)) lt₁ rfl)))) gen (to_vec (cons a₁ v₁)) lt₁ rfl))))

View file

@ -1,7 +1,7 @@
import logic import logic
theorem test {A B : Type} {a : A} {b : B} (H : a == b) : theorem test {A B : Type} {a : A} {b : B} (H : a == b) :
eq.rec_on (heq.type_eq H) a = b eq.rec_on (type_eq_of_heq H) a = b
:= :=
-- Remark the error message should not occur in the token theorem -- Remark the error message should not occur in the token theorem
heq.rec_on H rfl heq.rec_on H rfl

View file

@ -3,6 +3,6 @@ unifier_bug.lean:7:0: error: type mismatch at application
term term
rfl rfl
has type has type
eq.rec_on (heq.type_eq H) a = eq.rec_on (heq.type_eq H) a eq.rec_on (type_eq_of_heq H) a = eq.rec_on (type_eq_of_heq H) a
but is expected to have type but is expected to have type
eq.rec_on (heq.type_eq H) a = b eq.rec_on (type_eq_of_heq H) a = b