From 1be12499f63119d9455e2baa917659806732ca7d Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Thu, 12 Jul 2018 01:46:30 +0200 Subject: Unit and Null types. Methods. --- HoTT_Base.thy | 3 ++- HoTT_Methods.thy | 7 +++++-- Prod.thy | 19 +++++++++++++++++++ Sum.thy | 13 +++++++++++++ scratch.thy | 50 ++++++++++++++++++++++++++++++++++---------------- 5 files changed, 73 insertions(+), 19 deletions(-) diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 703f1aa..8c45d35 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -54,7 +54,7 @@ and Numeral_lt_trans: "\m n. m <- n \ S m <- S n" lemmas Numeral_rules [intro] = Numeral_lt_min Numeral_lt_trans - \ \Lets \standard\ automatically solve inequalities.\ + \ \Enables \standard\ to automatically solve inequalities.\ text "Universe types:" @@ -64,6 +64,7 @@ where Universe_hierarchy: "\i j. i <- j \ U(i) : U(j)" and Universe_cumulative: "\A i j. \A : U(i); i <- j\ \ A : U(j)" + \ \WARNING: \rule Universe_cumulative\ can result in an infinite rewrite loop!\ section \Type families\ diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index c314ed4..8a4417d 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -49,14 +49,17 @@ method wellformed uses jdgmt declares wellform = subsection \Derivation search\ -text "Combine \simple\ and \wellformed\ to search for derivations of judgments. +text "Combine \simple\, \wellformed\ and the universe hierarchy rules to search for derivations of judgments. \wellformed\ uses the facts passed as \lems\ to derive any required typing judgments. Definitions passed as \unfolds\ are unfolded throughout." method derive uses lems unfolds = ( unfold unfolds | simple lems: lems | - match lems in lem: "?X : ?Y" \ \wellformed jdgmt: lem\ + match lems in lem: "?X : ?Y" \ \wellformed jdgmt: lem\ | + rule Universe_hierarchy | + (rule Universe_cumulative, simple lems: lems) | + (rule Universe_cumulative, match lems in lem: "?X : ?Y" \ \wellformed jdgmt: lem\) )+ diff --git a/Prod.thy b/Prod.thy index 445ddd8..fbea4df 100644 --- a/Prod.thy +++ b/Prod.thy @@ -69,4 +69,23 @@ abbreviation Function :: "[Term, Term] \ Term" (infixr "\ B \ \_:A. B" +section \Unit type\ + +axiomatization + Unit :: Term ("\") and + pt :: Term ("\") and + indUnit :: "[Typefam, Term, Term] \ Term" +where + Unit_form: "\ : U(0)" +and + Unit_intro: "\ : \" +and + Unit_elim: "\i C c a. \C: \ \ U(i); c : C \; a : \\ \ indUnit C c a : C a" +and + Unit_comp: "\i C c. \C: \ \ U(i); c : C \\ \ indUnit C c \ \ c" + +lemmas Unit_rules [intro] = Unit_form Unit_intro Unit_elim Unit_comp +lemmas Unit_comps [comp] = Unit_comp + + end \ No newline at end of file diff --git a/Sum.thy b/Sum.thy index b608e75..99b4df2 100644 --- a/Sum.thy +++ b/Sum.thy @@ -60,4 +60,17 @@ abbreviation Pair :: "[Term, Term] \ Term" (infixr "\" 50) where "A \ B \ \_:A. B" +section \Null type\ + +axiomatization + Null :: Term ("\") and + indNull :: "[Typefam, Term] \ Term" +where + Null_form: "\ : U(0)" +and + Null_elim: "\i C z. \C: \ \ U(i); z : \\ \ indNull C z : C z" + +lemmas Null_rules [intro] = Null_form Null_elim + + end \ No newline at end of file diff --git a/scratch.thy b/scratch.thy index 3f66083..ae1bdb5 100644 --- a/scratch.thy +++ b/scratch.thy @@ -3,10 +3,11 @@ theory scratch begin -term "UN" - (* Typechecking *) -schematic_goal "\a : A; b : B\ \ (a,b) : ?A" +schematic_goal "\A : U(i); B : U(i); a : A; b : B\ \ (a,b) : ?A" + by derive + +lemma "\ : U(S S S 0)" by derive @@ -24,13 +25,13 @@ have "f`a`b`c \ d" by (simplify lems: asm) end -lemma "a : A \ indEqual[A] (\x y _. y =\<^sub>A x) (\x. refl(x)) a a refl(a) \ refl(a)" +lemma "\A : U(i); a : A\ \ indEqual[A] (\x y _. y =\<^sub>A x) (\x. refl(x)) a a refl(a) \ refl(a)" by simplify lemma "\a : A; \x. x : A \ b x : X\ \ (\<^bold>\x:A. b x)`a \ b a" by simplify -schematic_goal "\a : A; \x. x : A \ b x : X\ \ (\<^bold>\x:A. b x)`a \ ?x" +schematic_goal "\a : A; b: A \ X\ \ (\<^bold>\x:A. b x)`a \ ?x" by rsimplify lemma @@ -38,7 +39,7 @@ lemma shows "(\<^bold>\x:A. b x)`a \ b a" by (simplify lems: assms) -lemma "\a : A; b : B a; B: A \ U; \x y. \x : A; y : B x\ \ c x y : D x y\ +lemma "\a : A; b : B a; B: A \ U(i); \x y. \x : A; y : B x\ \ c x y : D x y\ \ (\<^bold>\x:A. \<^bold>\y:B x. c x y)`a`b \ c a b" by (simplify) @@ -53,7 +54,6 @@ lemma assumes "a : A" "b : B a" - "B: A \ U" "\x y. \x : A; y : B x\ \ c x y : D x y" shows "(\<^bold>\x:A. \<^bold>\y:B x. c x y)`a`b \ c a b" by (simplify lems: assms) @@ -63,19 +63,20 @@ assumes "a : A" "b : B a" "c : C a b" - "B: A \ U" - "\x. x : A\ C x: B x \ U" "\x y z. \x : A; y : B x; z : C x y\ \ d x y z : D x y z" shows "(\<^bold>\x:A. \<^bold>\y:B x. \<^bold>\z:C x y. d x y z)`a`b`c \ d a b c" by (simplify lems: assms) +(* Polymorphic identity function *) + +definition Id :: "Numeral \ Term" where "Id n \ \<^bold>\A:U(n). \<^bold>\x:A. x" + +lemma assumes "A : U 0" and "x:A" shows "(Id 0)`A`x \ x" unfolding Id_def by (simplify lems: assms) -(* HERE IS HOW WE ATTEMPT TO DO PATH INDUCTION --- VERY GOOD CANDIDATE FOR THESIS SECTION *) -schematic_goal "\A : U; x : A; y : A\ \ ?x : x =\<^sub>A y \ y =\<^sub>A x" +(* See if we can find path inverse *) +schematic_goal "\A : U(i); x : A; y : A\ \ ?x : x =\<^sub>A y \ y =\<^sub>A x" apply (rule Prod_intro) - apply (rule Equal_form) - apply assumption+ apply (rule Equal_elim) back back @@ -84,9 +85,26 @@ schematic_goal "\A : U; x : A; y : A\ \ ?x : x = back back back - back back back back back back - -thm comp + defer + back + back + back + back + back + back + back + back + back + apply (rule Equal_form) + apply assumption+ + defer + defer + apply assumption + defer + defer + apply (rule Equal_intro) + apply assumption+ +oops end \ No newline at end of file -- cgit v1.2.3