refactor(library/standard): move cast and heq to separate file
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
1d273fcfdd
commit
cd806bfabb
4 changed files with 79 additions and 71 deletions
77
library/standard/cast.lean
Normal file
77
library/standard/cast.lean
Normal file
|
|
@ -0,0 +1,77 @@
|
|||
-- 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
|
||||
|
||||
definition cast {A B : Type} (H : A = B) (a : A) : B
|
||||
:= eq_rec a H
|
||||
|
||||
theorem cast_refl {A : Type} (a : A) : cast (refl A) a = a
|
||||
:= refl (cast (refl A) a)
|
||||
|
||||
theorem cast_proof_irrel {A B : Type} (H1 H2 : A = B) (a : A) : cast H1 a = cast H2 a
|
||||
:= refl (cast H1 a)
|
||||
|
||||
theorem cast_eq {A : Type} (H : A = A) (a : A) : cast H a = a
|
||||
:= calc cast H a = cast (refl A) a : cast_proof_irrel H (refl A) a
|
||||
... = a : cast_refl a
|
||||
|
||||
definition heq {A B : Type} (a : A) (b : B) := ∃ H, cast H a = b
|
||||
|
||||
infixl `==`:50 := heq
|
||||
|
||||
theorem heq_type_eq {A B : Type} {a : A} {b : B} (H : a == b) : A = B
|
||||
:= obtain w Hw, from H, w
|
||||
|
||||
theorem eq_to_heq {A : Type} {a b : A} (H : a = b) : a == b
|
||||
:= exists_intro (refl A) (trans (cast_refl a) H)
|
||||
|
||||
theorem heq_to_eq {A : Type} {a b : A} (H : a == b) : a = b
|
||||
:= obtain (w : A = A) (Hw : cast w a = b), from H,
|
||||
calc a = cast w a : symm (cast_eq w a)
|
||||
... = b : Hw
|
||||
|
||||
theorem hrefl {A : Type} (a : A) : a == a
|
||||
:= eq_to_heq (refl a)
|
||||
|
||||
theorem heqt_elim {a : Bool} (H : a == true) : a
|
||||
:= eqt_elim (heq_to_eq H)
|
||||
|
||||
opaque_hint (hiding cast)
|
||||
|
||||
theorem hsubst {A B : Type} {a : A} {b : B} {P : ∀ (T : Type), T → Bool} (H1 : a == b) (H2 : P A a) : P B b
|
||||
:= have Haux1 : ∀ H : A = A, P A (cast H a), from
|
||||
assume H : A = A, subst (symm (cast_eq H a)) H2,
|
||||
obtain (Heq : A = B) (Hw : cast Heq a = b), from H1,
|
||||
have Haux2 : P B (cast Heq a), from subst Heq Haux1 Heq,
|
||||
subst Hw Haux2
|
||||
|
||||
theorem hsymm {A B : Type} {a : A} {b : B} (H : a == b) : b == a
|
||||
:= hsubst H (hrefl a)
|
||||
|
||||
theorem htrans {A B C : Type} {a : A} {b : B} {c : C} (H1 : a == b) (H2 : b == c) : a == c
|
||||
:= hsubst H2 H1
|
||||
|
||||
theorem htrans_left {A B : Type} {a : A} {b c : B} (H1 : a == b) (H2 : b = c) : a == c
|
||||
:= htrans H1 (eq_to_heq H2)
|
||||
|
||||
theorem htrans_right {A C : Type} {a b : A} {c : C} (H1 : a = b) (H2 : b == c) : a == c
|
||||
:= htrans (eq_to_heq H1) H2
|
||||
|
||||
calc_trans htrans
|
||||
calc_trans htrans_left
|
||||
calc_trans htrans_right
|
||||
|
||||
theorem cast_heq {A B : Type} (H : A = B) (a : A) : cast H a == a
|
||||
:= have H1 : ∀ (H : A = A) (a : A), cast H a == a, from
|
||||
λ H a, eq_to_heq (cast_eq H a),
|
||||
subst H H1 H a
|
||||
|
||||
theorem cast_eq_to_heq {A B : Type} {a : A} {b : B} {H : A = B} (H1 : cast H a = b) : a == b
|
||||
:= calc a == cast H a : hsymm (cast_heq H a)
|
||||
... = b : H1
|
||||
|
||||
theorem cast_trans {A B C : Type} (Hab : A = B) (Hbc : B = C) (a : A) : cast Hbc (cast Hab a) = cast (trans Hab Hbc) a
|
||||
:= heq_to_eq (calc cast Hbc (cast Hab a) == cast Hab a : cast_heq Hbc (cast Hab a)
|
||||
... == a : cast_heq Hab a
|
||||
... == cast (trans Hab Hbc) a : hsymm (cast_heq (trans Hab Hbc) a))
|
||||
|
|
@ -1,7 +1,7 @@
|
|||
-- 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
|
||||
import logic cast
|
||||
|
||||
axiom boolcomplete (a : Bool) : a = true ∨ a = false
|
||||
|
||||
|
|
|
|||
|
|
@ -218,71 +218,3 @@ theorem inhabited_Bool [instance] : inhabited Bool
|
|||
|
||||
theorem inhabited_fun [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A → B)
|
||||
:= inhabited_elim H (take (b : B), inhabited_intro (λ a : A, b))
|
||||
|
||||
definition cast {A B : Type} (H : A = B) (a : A) : B
|
||||
:= eq_rec a H
|
||||
|
||||
theorem cast_refl {A : Type} (a : A) : cast (refl A) a = a
|
||||
:= refl (cast (refl A) a)
|
||||
|
||||
theorem cast_proof_irrel {A B : Type} (H1 H2 : A = B) (a : A) : cast H1 a = cast H2 a
|
||||
:= refl (cast H1 a)
|
||||
|
||||
theorem cast_eq {A : Type} (H : A = A) (a : A) : cast H a = a
|
||||
:= calc cast H a = cast (refl A) a : cast_proof_irrel H (refl A) a
|
||||
... = a : cast_refl a
|
||||
|
||||
definition heq {A B : Type} (a : A) (b : B) := ∃ H, cast H a = b
|
||||
|
||||
infixl `==`:50 := heq
|
||||
|
||||
theorem heq_type_eq {A B : Type} {a : A} {b : B} (H : a == b) : A = B
|
||||
:= obtain w Hw, from H, w
|
||||
|
||||
theorem eq_to_heq {A : Type} {a b : A} (H : a = b) : a == b
|
||||
:= exists_intro (refl A) (trans (cast_refl a) H)
|
||||
|
||||
theorem heq_to_eq {A : Type} {a b : A} (H : a == b) : a = b
|
||||
:= obtain (w : A = A) (Hw : cast w a = b), from H,
|
||||
calc a = cast w a : symm (cast_eq w a)
|
||||
... = b : Hw
|
||||
|
||||
theorem hrefl {A : Type} (a : A) : a == a
|
||||
:= eq_to_heq (refl a)
|
||||
|
||||
theorem heqt_elim {a : Bool} (H : a == true) : a
|
||||
:= eqt_elim (heq_to_eq H)
|
||||
|
||||
opaque_hint (hiding cast)
|
||||
|
||||
theorem hsubst {A B : Type} {a : A} {b : B} {P : ∀ (T : Type), T → Bool} (H1 : a == b) (H2 : P A a) : P B b
|
||||
:= have Haux1 : ∀ H : A = A, P A (cast H a), from
|
||||
assume H : A = A, subst (symm (cast_eq H a)) H2,
|
||||
obtain (Heq : A = B) (Hw : cast Heq a = b), from H1,
|
||||
have Haux2 : P B (cast Heq a), from subst Heq Haux1 Heq,
|
||||
subst Hw Haux2
|
||||
|
||||
theorem hsymm {A B : Type} {a : A} {b : B} (H : a == b) : b == a
|
||||
:= hsubst H (hrefl a)
|
||||
|
||||
theorem htrans {A B C : Type} {a : A} {b : B} {c : C} (H1 : a == b) (H2 : b == c) : a == c
|
||||
:= hsubst H2 H1
|
||||
|
||||
theorem htrans_left {A B : Type} {a : A} {b c : B} (H1 : a == b) (H2 : b = c) : a == c
|
||||
:= htrans H1 (eq_to_heq H2)
|
||||
|
||||
theorem htrans_right {A C : Type} {a b : A} {c : C} (H1 : a = b) (H2 : b == c) : a == c
|
||||
:= htrans (eq_to_heq H1) H2
|
||||
|
||||
calc_trans htrans
|
||||
calc_trans htrans_left
|
||||
calc_trans htrans_right
|
||||
|
||||
theorem cast_heq {A B : Type} (H : A = B) (a : A) : cast H a == a
|
||||
:= have H1 : ∀ (H : A = A) (a : A), cast H a == a, from
|
||||
λ H a, eq_to_heq (cast_eq H a),
|
||||
subst H H1 H a
|
||||
|
||||
theorem cast_eq_to_heq {A B : Type} {a : A} {b : B} {H : A = B} (H1 : cast H a = b) : a == b
|
||||
:= calc a == cast H a : hsymm (cast_heq H a)
|
||||
... = b : H1
|
||||
|
|
|
|||
|
|
@ -1,2 +1 @@
|
|||
import logic tactic num string pair
|
||||
|
||||
import logic tactic num string pair cast
|
||||
|
|
|
|||
Loading…
Reference in a new issue