From cd806bfabba040d0ee99dd5f7451456ab26238ed Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 12 Jul 2014 07:08:12 +0100 Subject: [PATCH] refactor(library/standard): move cast and heq to separate file Signed-off-by: Leonardo de Moura --- library/standard/cast.lean | 77 +++++++++++++++++++++++++++++++++ library/standard/classical.lean | 2 +- library/standard/logic.lean | 68 ----------------------------- library/standard/standard.lean | 3 +- 4 files changed, 79 insertions(+), 71 deletions(-) create mode 100644 library/standard/cast.lean diff --git a/library/standard/cast.lean b/library/standard/cast.lean new file mode 100644 index 000000000..ec1fd4797 --- /dev/null +++ b/library/standard/cast.lean @@ -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)) diff --git a/library/standard/classical.lean b/library/standard/classical.lean index 0aae0fbf4..b38593966 100644 --- a/library/standard/classical.lean +++ b/library/standard/classical.lean @@ -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 diff --git a/library/standard/logic.lean b/library/standard/logic.lean index cfdf6857c..e03cc781c 100644 --- a/library/standard/logic.lean +++ b/library/standard/logic.lean @@ -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 diff --git a/library/standard/standard.lean b/library/standard/standard.lean index 9a37da551..5fe71f0fe 100644 --- a/library/standard/standard.lean +++ b/library/standard/standard.lean @@ -1,2 +1 @@ -import logic tactic num string pair - +import logic tactic num string pair cast