refactor(library/logic/cast): move heq declaration to a separate module
heq is be needed for some automatically generated constructions. So, we want it available with the least number of dependencies.
This commit is contained in:
parent
c7992f2cac
commit
ad2ecfb7a8
2 changed files with 53 additions and 42 deletions
|
@ -1,7 +1,7 @@
|
||||||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
-- Author: Leonardo de Moura
|
-- Author: Leonardo de Moura
|
||||||
import .eq .quantifiers
|
import logic.eq logic.heq logic.quantifiers
|
||||||
open eq.ops
|
open eq.ops
|
||||||
|
|
||||||
-- cast.lean
|
-- cast.lean
|
||||||
|
@ -23,55 +23,17 @@ section
|
||||||
rfl
|
rfl
|
||||||
end
|
end
|
||||||
|
|
||||||
inductive heq {A : Type} (a : A) : Π {B : Type}, B → Prop :=
|
|
||||||
refl : heq a a
|
|
||||||
infixl `==`:50 := heq
|
|
||||||
|
|
||||||
namespace heq
|
namespace heq
|
||||||
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 drec_on {C : Π {B : Type} (b : B), a == b → Type} (H₁ : a == b) (H₂ : C a (refl a)) : C b H₁ :=
|
|
||||||
rec (λ H₁ : a == a, show C a H₁, from H₂) H₁ H₁
|
|
||||||
|
|
||||||
theorem subst {P : ∀T : Type, T → Prop} (H₁ : a == b) (H₂ : P A a) : P B b :=
|
|
||||||
rec_on H₁ H₂
|
|
||||||
|
|
||||||
theorem symm (H : a == b) : b == a :=
|
|
||||||
subst H (refl a)
|
|
||||||
|
|
||||||
theorem type_eq (H : a == b) : A = B :=
|
|
||||||
subst H (eq.refl A)
|
|
||||||
|
|
||||||
theorem from_eq (H : a = a') : a == a' :=
|
|
||||||
eq.subst H (refl a)
|
|
||||||
|
|
||||||
theorem trans (H₁ : a == b) (H₂ : b == c) : a == c :=
|
|
||||||
subst H₂ H₁
|
|
||||||
|
|
||||||
theorem trans_left (H₁ : a == b) (H₂ : b = b') : a == b' :=
|
|
||||||
trans H₁ (from_eq H₂)
|
|
||||||
|
|
||||||
theorem trans_right (H₁ : a = a') (H₂ : a' == b) : a == b :=
|
|
||||||
trans (from_eq 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 H) a = b :=
|
||||||
drec_on H !cast_eq
|
drec_on H !cast_eq
|
||||||
|
|
||||||
theorem to_eq (H : a == a') : a = a' :=
|
|
||||||
calc
|
|
||||||
a = cast (eq.refl A) a : cast_eq
|
|
||||||
... = a' : to_cast_eq H
|
|
||||||
|
|
||||||
theorem elim {D : Type} (H₁ : a == b) (H₂ : ∀ (Hab : A = B), cast Hab a = b → D) : D :=
|
theorem elim {D : Type} (H₁ : a == b) (H₂ : ∀ (Hab : A = B), cast Hab a = b → D) : D :=
|
||||||
H₂ (type_eq H₁) (to_cast_eq H₁)
|
H₂ (type_eq H₁) (to_cast_eq H₁)
|
||||||
|
|
||||||
end heq
|
end heq
|
||||||
|
|
||||||
calc_trans heq.trans
|
|
||||||
calc_trans heq.trans_left
|
|
||||||
calc_trans heq.trans_right
|
|
||||||
calc_symm heq.symm
|
|
||||||
|
|
||||||
section
|
section
|
||||||
universe variables u v
|
universe variables u v
|
||||||
variables {A A' B C : Type.{u}} {P P' : A → Type.{v}} {a a' : A} {b : B}
|
variables {A A' B C : Type.{u}} {P P' : A → Type.{v}} {a a' : A} {b : B}
|
||||||
|
@ -91,9 +53,6 @@ section
|
||||||
theorem hproof_irrel {a b : Prop} (H : a = b) (H₁ : a) (H₂ : b) : H₁ == H₂ :=
|
theorem hproof_irrel {a b : Prop} (H : a = b) (H₁ : a) (H₂ : b) : H₁ == H₂ :=
|
||||||
eq_rec_to_heq (proof_irrel (cast H H₁) H₂)
|
eq_rec_to_heq (proof_irrel (cast H H₁) H₂)
|
||||||
|
|
||||||
theorem heq.true_elim {a : Prop} (H : a == true) : a :=
|
|
||||||
eq_true_elim (heq.to_eq H)
|
|
||||||
|
|
||||||
--TODO: generalize to eq.rec. This is a special case of rec_on_compose in eq.lean
|
--TODO: generalize to eq.rec. This is a special case of rec_on_compose in eq.lean
|
||||||
theorem cast_trans (Hab : A = B) (Hbc : B = C) (a : A) :
|
theorem cast_trans (Hab : A = B) (Hbc : B = C) (a : A) :
|
||||||
cast Hbc (cast Hab a) = cast (Hab ⬝ Hbc) a :=
|
cast Hbc (cast Hab a) = cast (Hab ⬝ Hbc) a :=
|
||||||
|
|
52
library/logic/heq.lean
Normal file
52
library/logic/heq.lean
Normal file
|
@ -0,0 +1,52 @@
|
||||||
|
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||||
|
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
|
-- Author: Leonardo de Moura
|
||||||
|
import logic.eq
|
||||||
|
|
||||||
|
inductive heq {A : Type} (a : A) : Π {B : Type}, B → Prop :=
|
||||||
|
refl : heq a a
|
||||||
|
infixl `==`:50 := heq
|
||||||
|
|
||||||
|
namespace heq
|
||||||
|
universe variable u
|
||||||
|
variables {A B C : Type.{u}} {a a' : A} {b b' : B} {c : C}
|
||||||
|
theorem drec_on {C : Π {B : Type} (b : B), a == b → Type} (H₁ : a == b) (H₂ : C a (refl a)) : C b H₁ :=
|
||||||
|
rec (λ H₁ : a == a, show C a H₁, from H₂) H₁ H₁
|
||||||
|
|
||||||
|
theorem subst {P : ∀T : Type, T → Prop} (H₁ : a == b) (H₂ : P A a) : P B b :=
|
||||||
|
rec_on H₁ H₂
|
||||||
|
|
||||||
|
theorem symm (H : a == b) : b == a :=
|
||||||
|
subst H (refl a)
|
||||||
|
|
||||||
|
theorem type_eq (H : a == b) : A = B :=
|
||||||
|
subst H (eq.refl A)
|
||||||
|
|
||||||
|
theorem from_eq (H : a = a') : a == a' :=
|
||||||
|
eq.subst H (refl a)
|
||||||
|
|
||||||
|
theorem to_eq (H : a == a') : a = a' :=
|
||||||
|
have H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a, from
|
||||||
|
take Ht, eq.refl (eq.rec_on Ht a),
|
||||||
|
have H₂ : ∀ (Ht : A = A), eq.rec_on Ht a = a', from
|
||||||
|
heq.rec_on H H₁,
|
||||||
|
H₂ (type_eq H)
|
||||||
|
|
||||||
|
theorem trans (H₁ : a == b) (H₂ : b == c) : a == c :=
|
||||||
|
subst H₂ H₁
|
||||||
|
|
||||||
|
theorem trans_left (H₁ : a == b) (H₂ : b = b') : a == b' :=
|
||||||
|
trans H₁ (from_eq H₂)
|
||||||
|
|
||||||
|
theorem trans_right (H₁ : a = a') (H₂ : a' == b) : a == b :=
|
||||||
|
trans (from_eq H₁) H₂
|
||||||
|
|
||||||
|
theorem true_elim {a : Prop} (H : a == true) : a :=
|
||||||
|
eq_true_elim (heq.to_eq H)
|
||||||
|
|
||||||
|
end heq
|
||||||
|
|
||||||
|
calc_trans heq.trans
|
||||||
|
calc_trans heq.trans_left
|
||||||
|
calc_trans heq.trans_right
|
||||||
|
calc_symm heq.symm
|
Loading…
Reference in a new issue