From 82836fe9e0c2b07772980ab62df5823678c5a232 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 29 Jul 2015 15:00:50 -0700 Subject: [PATCH] feat(library/init/logic): make sure standard library can be compiled when proofs are erased --- library/init/logic.lean | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/library/init/logic.lean b/library/init/logic.lean index ed198ac1b..91f1e61a4 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -169,13 +169,6 @@ open eq.ops theorem eq_rec_heq {A : Type} {P : A → Type} {a a' : A} (H : a = a') (p : P a) : H ▹ p == p := eq.drec_on H !heq.refl -theorem eq_rec_of_heq_left : ∀ {A₁ A₂ : Type} {a₁ : A₁} {a₂ : A₂} (h : a₁ == a₂), heq.type_eq h ▹ a₁ = a₂ -| A A a a (heq.refl a) := rfl - -reveal eq.symm -theorem eq_rec_of_heq_right : ∀ {A₁ A₂ : Type} {a₁ : A₁} {a₂ : A₂} (h : a₁ == a₂), a₁ = (heq.type_eq h)⁻¹ ▹ a₂ -| A A a a (heq.refl a) := rfl - theorem heq_of_eq_rec_left {A : Type} {P : A → Type} : ∀ {a a' : A} {p₁ : P a} {p₂ : P a'} (e : a = a') (h₂ : e ▹ p₁ = p₂), p₁ == p₂ | a a p₁ p₂ (eq.refl a) h := eq.rec_on h !heq.refl @@ -190,6 +183,15 @@ theorem eq_rec_compose : ∀ {A B C : Type} (p₁ : B = C) (p₂ : A = B) (a : A eq.refl A ▹ eq.refl A ▹ a = eq.refl A ▹ a : rfl ... = (eq.refl A ⬝ eq.refl A) ▹ a : {proof_irrel (eq.refl A) (eq.refl A ⬝ eq.refl 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) + +theorem eq_rec_of_heq_left : ∀ {A₁ A₂ : Type} {a₁ : A₁} {a₂ : A₂} (h : a₁ == a₂), heq.type_eq h ▹ a₁ = a₂ +| 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₂ := +eq_rec_eq_eq_rec (eq_rec_of_heq_left h) + attribute heq.refl [refl] attribute heq.trans [trans] attribute heq.of_heq_of_eq [trans]