From decb363a30a30c1875bf4b93bc544c28edf3149e Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Sat, 7 Jul 2018 23:03:33 +0200 Subject: Library snapshot. Methods written, everything nicely organized. --- Equal.thy | 1 + EqualProps.thy | 22 ++++++++-------------- HoTT.thy | 1 - HoTT_Base.thy | 2 +- Prod.thy | 1 + Proj.thy | 35 ++++++++++++++++++++++++++++++++--- Sum.thy | 3 ++- 7 files changed, 45 insertions(+), 20 deletions(-) diff --git a/Equal.thy b/Equal.thy index 7732dd0..18a4207 100644 --- a/Equal.thy +++ b/Equal.thy @@ -9,6 +9,7 @@ theory Equal imports HoTT_Base begin + axiomatization Equal :: "[Term, Term, Term] \ Term" and refl :: "Term \ Term" ("(refl'(_'))" 1000) and diff --git a/EqualProps.thy b/EqualProps.thy index 2807587..cb267c6 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -22,22 +22,14 @@ definition inv :: "[Term, Term, Term] \ Term" ("(1inv[_,/ _,/ _])") lemma inv_type: assumes "p : x =\<^sub>A y" shows "inv[A,x,y]`p : y =\<^sub>A x" - by (derive lems: assms unfolds: inv_def) + unfolding inv_def + by (derive lems: assms) lemma inv_comp: assumes "a : A" shows "inv[A,a,a]`refl(a) \ refl(a)" - -proof - - have "inv[A,a,a]`refl(a) \ indEqual[A] (\x y _. y =\<^sub>A x) (\x. refl(x)) a a refl(a)" - by (derive lems: assms unfolds: inv_def) - - also have "indEqual[A] (\x y _. y =\<^sub>A x) (\x. refl(x)) a a refl(a) \ refl(a)" - by (simple lems: assms) - - finally show "inv[A,a,a]`refl(a) \ refl(a)" . -qed + unfolding inv_def by (simplify lems: assms) section \Transitivity / Path composition\ @@ -50,6 +42,7 @@ definition rcompose :: "Term \ Term" ("(1rcompose[_])") (\x. \<^bold>\z:A. \<^bold>\p:(x =\<^sub>A z). indEqual[A](\x z _. x =\<^sub>A z) (\x. refl(x)) x z p) x y p" + text "``Natural'' composition function abbreviation, effectively equivalent to a function of type \\x,y,z:A. x =\<^sub>A y \ y =\<^sub>A z \ x =\<^sub>A z\." abbreviation compose :: "[Term, Term, Term, Term] \ Term" ("(1compose[_,/ _,/ _,/ _])") @@ -59,14 +52,15 @@ abbreviation compose :: "[Term, Term, Term, Term] \ Term" ("(1compo lemma compose_type: assumes "p : x =\<^sub>A y" and "q : y =\<^sub>A z" shows "compose[A,x,y,z]`p`q : x =\<^sub>A z" - by (derive lems: assms unfolds: rcompose_def) + unfolding rcompose_def + by (derive lems: assms) lemma compose_comp: assumes "a : A" shows "compose[A,a,a,a]`refl(a)`refl(a) \ refl(a)" - -sorry \ \Long and tedious proof if the Simplifier is not set up.\ + unfolding rcompose_def + by (simplify lems: assms) lemmas Equal_simps [intro] = inv_comp compose_comp diff --git a/HoTT.thy b/HoTT.thy index 42796c1..948dd14 100644 --- a/HoTT.thy +++ b/HoTT.thy @@ -5,7 +5,6 @@ Load all the component modules for the HoTT logic. *) theory HoTT - imports (* Basic theories *) diff --git a/HoTT_Base.thy b/HoTT_Base.thy index cfced79..60e5167 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -15,7 +15,7 @@ section \Setup\ text "Named theorems to be used by proof methods later (see HoTT_Methods.thy). \wellform\ declares necessary wellformedness conditions for type and inhabitation judgments, while -\comp\ declares computation rules used when simplifying function application." +\comp\ declares computation rules, which are used by the simplification method as equational rewrite rules." named_theorems wellform named_theorems comp diff --git a/Prod.thy b/Prod.thy index 544a719..bf4e4e9 100644 --- a/Prod.thy +++ b/Prod.thy @@ -9,6 +9,7 @@ theory Prod imports HoTT_Base begin + axiomatization Prod :: "[Term, Typefam] \ Term" and lambda :: "[Term, Term \ Term] \ Term" and diff --git a/Proj.thy b/Proj.thy index 7957669..805a624 100644 --- a/Proj.thy +++ b/Proj.thy @@ -12,6 +12,7 @@ theory Proj Sum begin + consts fst :: "[Term, 'a] \ Term" ("(1fst[/_,/ _])") snd :: "[Term, 'a] \ Term" ("(1snd[/_,/ _])") @@ -49,13 +50,17 @@ text "Typing judgments and computation rules for the dependent and non-dependent lemma fst_dep_type: assumes "p : \x:A. B x" shows "fst[A,B]`p : A" - by (derive lems: assms unfolds: fst_dep_def) + unfolding fst_dep_def + by (derive lems: assms) lemma fst_dep_comp: assumes "B: A \ U" and "a : A" and "b : B a" shows "fst[A,B]`(a,b) \ a" + unfolding fst_dep_def + by (simplify lems: assms) +\ \ (* Old proof *) proof - have "fst[A,B]`(a,b) \ indSum[A,B] (\_. A) (\x y. x) (a,b)" by (derive lems: assms unfolds: fst_dep_def) @@ -65,8 +70,9 @@ proof - finally show "fst[A,B]`(a,b) \ a" . qed +\ - +\ \ (* Old lemma *) text "In proving results about the second dependent projection function we often use the following lemma." lemma lem: @@ -77,12 +83,16 @@ proof - have "fst[A,B]`(x,y) \ x" using assms by (rule fst_dep_comp) then show "y : B (fst[A,B]`(x,y))" using assms by simp qed +\ lemma snd_dep_type: assumes "p : \x:A. B x" shows "snd[A,B]`p : B (fst[A,B]`p)" + unfolding fst_dep_def snd_dep_def + by (simplify lems: assms) +\ \ (* Old proof *) proof (derive lems: assms unfolds: snd_dep_def) show "fst[A, B] : (\x:A. B x) \ A" by (derive lems: assms unfolds: fst_dep_def) @@ -90,12 +100,16 @@ proof (derive lems: assms unfolds: snd_dep_def) have "B: A \ U" by (wellformed jdgmt: assms) then show "y : B (fst[A, B]`(x,y))" using asm by (rule lem) qed (assumption | rule assms)+ +\ lemma snd_dep_comp: assumes "B: A \ U" and "a : A" and "b : B a" shows "snd[A,B]`(a,b) \ b" + unfolding snd_dep_def fst_dep_def + by (simplify lems: assms) +\ \ (* Old proof *) proof - have "snd[A,B]`(a,b) \ indSum[A, B] (\q. B (fst[A,B]`q)) (\x y. y) (a,b)" proof (derive lems: assms unfolds: snd_dep_def) @@ -115,6 +129,7 @@ proof - finally show "snd[A,B]`(a,b) \ b" . qed +\ text "For non-dependent projection functions:" @@ -122,13 +137,17 @@ text "For non-dependent projection functions:" lemma fst_nondep_type: assumes "p : A \ B" shows "fst[A,B]`p : A" - by (derive lems: assms unfolds: fst_nondep_def) + unfolding fst_nondep_def + by (derive lems: assms) lemma fst_nondep_comp: assumes "a : A" and "b : B" shows "fst[A,B]`(a,b) \ a" + unfolding fst_nondep_def + by (simplify lems: assms) +\ \ (* Old proof *) proof - have "fst[A,B]`(a,b) \ indSum[A, \_. B] (\_. A) (\x y. x) (a,b)" by (derive lems: assms unfolds: fst_nondep_def) @@ -138,12 +157,16 @@ proof - finally show "fst[A,B]`(a,b) \ a" . qed +\ lemma snd_nondep_type: assumes "p : A \ B" shows "snd[A,B]`p : B" + unfolding snd_nondep_def + by (derive lems: assms) +\ \ (* Old proof *) proof show "snd[A,B] : A \ B \ B" proof (derive unfolds: snd_nondep_def) @@ -151,11 +174,16 @@ proof show "indSum[A, \_. B] (\_. B) (\x y. y) q : B" by (derive lems: asm) qed (wellformed jdgmt: assms)+ qed (rule assms) +\ lemma snd_nondep_comp: assumes "a : A" and "b : B" shows "snd[A,B]`(a,b) \ b" + unfolding snd_nondep_def + by (simplify lems: assms) + +\ \ (* Old proof *) proof - have "snd[A,B]`(a,b) \ indSum[A, \_. B] (\_. B) (\x y. y) (a,b)" by (derive lems: assms unfolds: snd_nondep_def) @@ -165,6 +193,7 @@ proof - finally show "snd[A,B]`(a,b) \ b" . qed +\ end \ No newline at end of file diff --git a/Sum.thy b/Sum.thy index fe38960..46bb022 100644 --- a/Sum.thy +++ b/Sum.thy @@ -9,6 +9,7 @@ theory Sum imports HoTT_Base begin + axiomatization Sum :: "[Term, Typefam] \ Term" and pair :: "[Term, Term] \ Term" ("(1'(_,/ _'))") and @@ -54,7 +55,7 @@ lemmas Sum_rules [intro] = Sum_form Sum_intro Sum_elim Sum_comp lemmas Sum_form_conds [elim, wellform] = Sum_form_cond1 Sum_form_cond2 lemmas Sum_comps [comp] = Sum_comp -\ \Nondependent pair\ +text "Nondependent pair." abbreviation Pair :: "[Term, Term] \ Term" (infixr "\" 50) where "A \ B \ \_:A. B" -- cgit v1.2.3