diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt index 56d2f1a904..7b918ae741 100644 --- a/src/builtin/CMakeLists.txt +++ b/src/builtin/CMakeLists.txt @@ -93,7 +93,8 @@ add_theory("if_then_else.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean") add_theory("Int.lean" "${CMAKE_CURRENT_BINARY_DIR}/if_then_else.olean") add_theory("Real.lean" "${CMAKE_CURRENT_BINARY_DIR}/Int.olean") add_theory("specialfn.lean" "${CMAKE_CURRENT_BINARY_DIR}/Real.olean") -## add_theory("cast.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean") +add_theory("heq.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean") +add_theory("cast.lean" "${CMAKE_CURRENT_BINARY_DIR}/heq.olean") update_interface("kernel.olean" "kernel" "-n") update_interface("Nat.olean" "library/arith" "-n") diff --git a/src/builtin/cast.lean b/src/builtin/cast.lean index e95a686242..b429bfca80 100644 --- a/src/builtin/cast.lean +++ b/src/builtin/cast.lean @@ -1,90 +1,35 @@ --- "Type casting" library. +import heq --- Heterogeneous substitution -axiom hsubst {A B : TypeU} {a : A} {b : B} (P : ∀ T : TypeU, T → Bool) : P A a → a == b → P B b +variable cast {A B : TypeH} : A = B → A → B -universe M >= 1 -universe U >= M + 1 -definition TypeM := (Type M) +axiom cast_heq {A B : TypeH} (H : A = B) (a : A) : cast H a == a --- Type equality axiom, if two values are equal, then their types are equal -theorem type_eq {A B : TypeM} {a : A} {b : B} (H : a == b) : A == B -:= hsubst (λ (T : TypeU) (x : T), A == T) (refl A) H +theorem cast_app {A A' : TypeH} {B : A → TypeH} {B' : A' → TypeH} (f : ∀ x, B x) (a : A) (Ha : A = A') (Hb : (∀ x, B x) = (∀ x, B' x)) : + cast Hb f (cast Ha a) == f a +:= let s1 : cast Hb f == f := cast_heq Hb f, + s2 : cast Ha a == a := cast_heq Ha a + in hcongr s1 s2 --- Heterogenous symmetry -theorem hsymm {A B : TypeU} {a : A} {b : B} (H : a == b) : b == a -:= hsubst (λ (T : TypeU) (x : T), x == a) (refl a) H +-- The following theorems can be used as rewriting rules --- Heterogenous transitivity -theorem htrans {A B C : TypeU} {a : A} {b : B} {c : C} (H1 : a == b) (H2 : b == c) : a == c -:= hsubst (λ (T : TypeU) (x : T), a == x) H1 H2 +theorem cast_eq {A : TypeH} (H : A = A) (a : A) : cast H a = a +:= to_eq (cast_heq H a) --- The cast operator allows us to cast an element of type A --- into B if we provide a proof that types A and B are equal. -variable cast {A B : TypeU} : A == B → A → B +theorem cast_trans {A B C : TypeH} (Hab : A = B) (Hbc : B = C) (a : A) : cast Hbc (cast Hab a) = cast (trans Hab Hbc) a +:= let s1 : cast Hbc (cast Hab a) == cast Hab a := cast_heq Hbc (cast Hab a), + s2 : cast Hab a == a := cast_heq Hab a, + s3 : cast (trans Hab Hbc) a == a := cast_heq (trans Hab Hbc) a, + s4 : cast Hbc (cast Hab a) == cast (trans Hab Hbc) a := htrans (htrans s1 s2) (hsymm s3) + in to_eq s4 --- The CastEq axiom states that for any cast of x is equal to x. -axiom cast_eq {A B : TypeU} (H : A == B) (x : A) : x == cast H x +theorem cast_pull {A : TypeH} {B B' : A → TypeH} (f : ∀ x, B x) (a : A) (Hb : (∀ x, B x) = (∀ x, B' x)) (Hba : (B a) = (B' a)) : + cast Hb f a = cast Hba (f a) +:= let s1 : cast Hb f a == f a := hcongr (cast_heq Hb f) (hrefl a), + s2 : cast Hba (f a) == f a := cast_heq Hba (f a) + in to_eq (htrans s1 (hsymm s2)) --- The CastApp axiom "propagates" the cast over application -axiom cast_app {A A' : TypeU} {B : A → TypeU} {B' : A' → TypeU} - (H1 : (∀ x, B x) == (∀ x, B' x)) (H2 : A == A') - (f : ∀ x, B x) (x : A) : - cast H1 f (cast H2 x) == f x --- Heterogeneous congruence -theorem hcongr - {A A' : TypeM} {B : A → TypeM} {B' : A' → TypeM} - {f : ∀ x, B x} {g : ∀ x, B' x} {a : A} {b : A'} - (H1 : f == g) - (H2 : a == b) - : f a == g b -:= let L1 : A == A' := type_eq H2, - L2 : A' == A := symm L1, - b' : A := cast L2 b, - L3 : b == b' := cast_eq L2 b, - L4 : a == b' := htrans H2 L3, - L5 : f a == f b' := congr2 f L4, - S1 : (∀ x, B' x) == (∀ x, B x) := symm (type_eq H1), - g' : (∀ x, B x) := cast S1 g, - L6 : g == g' := cast_eq S1 g, - L7 : f == g' := htrans H1 L6, - L8 : f b' == g' b' := congr1 b' L7, - L9 : f a == g' b' := htrans L5 L8, - L10 : g' b' == g b := cast_app S1 L2 g b - in htrans L9 L10 -theorem hfunext - {A : TypeM} {B B' : A → TypeM} {f : ∀ x : A, B x} {g : ∀ x : A, B' x} (H : ∀ x : A, f x == g x) : f == g -:= let L1 : (∀ x : A, B x = B' x) := λ x : A, type_eq (H x), - L2 : (∀ x : A, B x) = (∀ x : A, B' x) := allext L1, - g' : (∀ x : A, B x) := cast (symm L2) g, - Hgg : g == g' := cast_eq (symm L2) g, - Hggx : (∀ x : A, g x == g' x) := λ x : A, hcongr Hgg (refl x) , - L3 : (∀ x : A, f x == g' x) := λ x : A, htrans (H x) (Hggx x), - Hfg : f == g' := funext L3 - in htrans Hfg (hsymm Hgg) -exit -- Stop here, the following axiom is not sound --- The following axiom is unsound when we treat Pi and --- forall as the "same thing". The main problem is the --- rule that says (Pi x : A, B) has type Bool if B has type Bool instead of --- max(typeof(A), typeof(B)) --- --- Here is the problematic axiom --- If two (dependent) function spaces are equal, then their domains are equal. -axiom dominj {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} - (H : (∀ x : A, B x) == (∀ x : A', B' x)) : - A == A' --- Here is a derivation of false using the dominj axiom -theorem unsat : false := -let L1 : (∀ x : true, true) := (λ x : true, trivial), - L2 : (∀ x : false, true) := (λ x : false, trivial), - -- When we keep Pi/forall as different things, the following two steps can't be used - L3 : (∀ x : true, true) = true := eqt_intro L1, - L4 : (∀ x : false, true) = true := eqt_intro L2, - L5 : (∀ x : true, true) = (∀ x : false, true) := trans L3 (symm L4), - L6 : true = false := dominj L5 -in L6 diff --git a/src/builtin/heq.lean b/src/builtin/heq.lean index 8ed6aa1829..87c973708e 100644 --- a/src/builtin/heq.lean +++ b/src/builtin/heq.lean @@ -8,13 +8,13 @@ universe H ≥ 1 universe U ≥ H + 1 definition TypeH := (Type H) -axiom heq_eq {A : TypeH} (a : A) : a == a ↔ a = a +axiom heq_eq {A : TypeH} (a b : A) : a == b ↔ a = b -definition to_eq {A : TypeH} {a : A} (H : a == a) : a = a -:= (heq_eq a) ◂ H +definition to_eq {A : TypeH} {a b : A} (H : a == b) : a = b +:= (heq_eq a b) ◂ H -definition to_heq {A : TypeH} {a : A} (H : a = a) : a == a -:= (symm (heq_eq a)) ◂ H +definition to_heq {A : TypeH} {a b : A} (H : a = b) : a == b +:= (symm (heq_eq a b)) ◂ H theorem hrefl {A : TypeH} (a : A) : a == a := to_heq (refl a) @@ -34,15 +34,3 @@ axiom hpiext {A A' : TypeH} {B : A → TypeH} {B' : A' → TypeH} : axiom hallext {A A' : TypeH} {B : A → Bool} {B' : A' → Bool} : A = A' → (∀ x x', x == x' → B x == B' x') → (∀ x, B x) == (∀ x, B' x) - -variable cast {A B : TypeH} : A = B → A → B - -axiom cast_eq {A B : TypeH} (H : A = B) (a : A) : a == cast H a - -theorem cast_app {A A' : TypeH} {B : A → TypeH} {B' : A' → TypeH} {f : ∀ x, B x} {a : A} (Ha : A = A') (Hb : (∀ x, B x) = (∀ x, B' x)) : - cast Hb f (cast Ha a) == f a -:= let s1 : cast Hb f == f := hsymm (cast_eq Hb f), - s2 : cast Ha a == a := hsymm (cast_eq Ha a) - in hcongr s1 s2 - - diff --git a/src/builtin/obj/cast.olean b/src/builtin/obj/cast.olean index 3712292705..363cd6d3b9 100644 Binary files a/src/builtin/obj/cast.olean and b/src/builtin/obj/cast.olean differ diff --git a/src/builtin/obj/heq.olean b/src/builtin/obj/heq.olean new file mode 100644 index 0000000000..6ece1454a2 Binary files /dev/null and b/src/builtin/obj/heq.olean differ diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index 958e9faac6..395f6b4f80 100644 Binary files a/src/builtin/obj/kernel.olean and b/src/builtin/obj/kernel.olean differ