diff options
| -rw-r--r-- | EqualProps.thy | 40 | ||||
| -rw-r--r-- | HoTT_Methods.thy | 2 | ||||
| -rw-r--r-- | Prod.thy | 26 | ||||
| -rw-r--r-- | ProdProps.thy | 54 | ||||
| -rw-r--r-- | scratch.thy | 72 |
5 files changed, 93 insertions, 101 deletions
diff --git a/EqualProps.thy b/EqualProps.thy index 2a13ed2..f3b355a 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -48,17 +48,17 @@ text " Raw composition function, of type \<open>\<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)\<close> polymorphic over the type \<open>A\<close>. " -axiomatization reqcompose :: Term where - reqcompose_def: "reqcompose \<equiv> \<^bold>\<lambda>x y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= (\<lambda>x. refl(x)) q) p" +axiomatization rpathcomp :: Term where + rpathcomp_def: "rpathcomp \<equiv> \<^bold>\<lambda>x y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= (\<lambda>x. refl(x)) q) p" text " More complicated proofs---the nested path inductions require more explicit step-by-step rule applications: " -lemma reqcompose_type: +lemma rpathcomp_type: assumes "A: U(i)" - shows "reqcompose: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" -unfolding reqcompose_def + shows "rpathcomp: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" +unfolding rpathcomp_def proof fix x assume 1: "x: A" show "\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" @@ -85,17 +85,17 @@ qed fact corollary assumes "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" - shows "reqcompose`x`y`p`z`q: x =\<^sub>A z" - by (simple lems: assms reqcompose_type) + shows "rpathcomp`x`y`p`z`q: x =\<^sub>A z" + by (simple lems: assms rpathcomp_type) text " The following proof is very long, chiefly because for every application of \<open>`\<close> we have to show the wellformedness of the type family appearing in the equality computation rule. " -lemma reqcompose_comp: +lemma rpathcomp_comp: assumes "A: U(i)" and "a: A" - shows "reqcompose`a`a`refl(a)`a`refl(a) \<equiv> refl(a)" -unfolding reqcompose_def + shows "rpathcomp`a`a`refl(a)`a`refl(a) \<equiv> refl(a)" +unfolding rpathcomp_def proof compute { fix x assume 1: "x: A" show "\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" @@ -197,28 +197,28 @@ qed fact text "The raw object lambda term is cumbersome to use, so we define a simpler constant instead." -axiomatization eqcompose :: "[Term, Term] \<Rightarrow> Term" (infixl "\<bullet>" 60) where - eqcompose_def: "\<lbrakk> +axiomatization pathcomp :: "[Term, Term] \<Rightarrow> Term" (infixl "\<bullet>" 60) where + pathcomp_def: "\<lbrakk> A: U(i); x: A; y: A; z: A; p: x =\<^sub>A y; q: y =\<^sub>A z - \<rbrakk> \<Longrightarrow> p \<bullet> q \<equiv> reqcompose`x`y`p`z`q" + \<rbrakk> \<Longrightarrow> p \<bullet> q \<equiv> rpathcomp`x`y`p`z`q" -lemma eqcompose_type: +lemma pathcomp_type: assumes "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" shows "p \<bullet> q: x =\<^sub>A z" -proof (subst eqcompose_def) +proof (subst pathcomp_def) show "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" by fact+ -qed (simple lems: assms reqcompose_type) +qed (simple lems: assms rpathcomp_type) -lemma eqcompose_comp: +lemma pathcomp_comp: assumes "A : U(i)" and "a : A" shows "refl(a) \<bullet> refl(a) \<equiv> refl(a)" -by (subst eqcompose_def) (simple lems: assms reqcompose_comp) +by (subst pathcomp_def) (simple lems: assms rpathcomp_comp) -lemmas EqualProps_rules [intro] = inv_type eqcompose_type -lemmas EqualProps_comps [comp] = inv_comp eqcompose_comp +lemmas EqualProps_rules [intro] = inv_type pathcomp_type +lemmas EqualProps_comps [comp] = inv_comp pathcomp_comp end
\ No newline at end of file diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index d3aed66..c3703bf 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -62,7 +62,7 @@ ML_file "~~/src/Tools/eqsubst.ML" text "Perform basic single-step computations:" -method compute uses lems = (subst comp lems) +method compute uses lems = (subst lems comp) end
\ No newline at end of file @@ -68,21 +68,31 @@ lemmas Prod_rules [intro] = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq lemmas Prod_wellform [wellform] = Prod_form_cond1 Prod_form_cond2 lemmas Prod_comps [comp] = Prod_comp Prod_uniq -subsection \<open>Composition\<close> -axiomatization fncompose :: "[Term, Term] \<Rightarrow> Term" (infixr "\<circ>" 70) where - fncompose_type: "\<lbrakk> +section \<open>Function composition\<close> + +axiomatization compose :: "[Term, Term] \<Rightarrow> Term" (infixr "o" 70) + +syntax "_COMPOSE" :: "[Term, Term] \<Rightarrow> Term" (infixr "\<circ>" 70) +translations "g \<circ> f" \<rightleftharpoons> "g o f" + +axiomatization where + compose_type: "\<lbrakk> g: \<Prod>x:B. C(x); f: A \<rightarrow> B; (\<Prod>x:B. C(x)): U(i); A \<rightarrow> B: U(i) \<rbrakk> \<Longrightarrow> g \<circ> f: \<Prod>x:A. C(f`x)" and - fncompose_comp: "\<lbrakk> - A: U(i); - \<And>x. x: A \<Longrightarrow> b(x): B; - \<And>x. x: A \<Longrightarrow> c(x): C(x) - \<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. c(x)) \<circ> (\<^bold>\<lambda>x. b(x)) \<equiv> \<^bold>\<lambda>x. c(b(x))" + compose_comp: "\<lbrakk> + g: \<Prod>x:B. C(x); + f: A \<rightarrow> B; + (\<Prod>x:B. C(x)): U(i); + A \<rightarrow> B: U(i) + \<rbrakk> \<Longrightarrow> g \<circ> f \<equiv> \<^bold>\<lambda>x. g`(f`x)" + +lemmas compose_rules [intro] = compose_type +lemmas compose_comps [comp] = compose_comp section \<open>Unit type\<close> diff --git a/ProdProps.thy b/ProdProps.thy new file mode 100644 index 0000000..7c2c658 --- /dev/null +++ b/ProdProps.thy @@ -0,0 +1,54 @@ +(* Title: HoTT/ProdProps.thy + Author: Josh Chen + Date: Aug 2018 + +Properties of the dependent product. +*) + +theory ProdProps + imports + HoTT_Methods + Prod +begin + + +section \<open>Composition\<close> + +text " + The following rule is admissible, but we cannot derive it only using the rules for the \<Pi>-type. +" + +lemma compose_comp': "\<lbrakk> + A: U(i); + \<And>x. x: A \<Longrightarrow> b(x): B; + \<And>x. x: B \<Longrightarrow> c(x): C(x) + \<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. c(x)) \<circ> (\<^bold>\<lambda>x. b(x)) \<equiv> \<^bold>\<lambda>x. c(b(x))" +oops + +text "However we can derive a variant with more explicit premises:" + +lemma compose_comp2: + assumes + "A: U(i)" "B: U(i)" and + "C: B \<longrightarrow> U(i)" and + "\<And>x. x: A \<Longrightarrow> b(x): B" and + "\<And>x. x: B \<Longrightarrow> c(x): C(x)" + shows "(\<^bold>\<lambda>x. c(x)) \<circ> (\<^bold>\<lambda>x. b(x)) \<equiv> \<^bold>\<lambda>x. c(b(x))" +proof (subst (0) comp) + show "\<^bold>\<lambda>x. (\<^bold>\<lambda>u. c(u))`((\<^bold>\<lambda>v. b(v))`x) \<equiv> \<^bold>\<lambda>x. c(b(x))" + proof (subst (0) comp) + show "\<^bold>\<lambda>x. c((\<^bold>\<lambda>v. b(v))`x) \<equiv> \<^bold>\<lambda>x. c(b(x))" + proof - + have *: "\<And>x. x: A \<Longrightarrow> (\<^bold>\<lambda>v. b(v))`x \<equiv> b(x)" by simple (rule assms) + show "\<^bold>\<lambda>x. c((\<^bold>\<lambda>v. b(v))`x) \<equiv> \<^bold>\<lambda>x. c(b(x))" + proof (subst *) + + +text "We can show associativity of composition in general." + +lemma compose_assoc: + "(f \<circ> g) \<circ> h \<equiv> f \<circ> (g \<circ> h)" +proof + + +end
\ No newline at end of file diff --git a/scratch.thy b/scratch.thy index 8800b1a..f0514c3 100644 --- a/scratch.thy +++ b/scratch.thy @@ -1,81 +1,9 @@ -(* Title: HoTT/ex/Synthesis.thy - Author: Josh Chen - Date: Aug 2018 - -Examples of inhabitant synthesis. -*) - - theory scratch imports HoTT begin -section \<open>Synthesis of the predecessor function\<close> - -text " - In this example we try, with the help of Isabelle, to synthesize a predecessor function for the natural numbers. - - This -" - -text " - First we show that the property we want is well-defined: -" - -lemma pred_welltyped: "\<Sum>pred:\<nat>\<rightarrow>\<nat> . ((pred`0) =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n): U(O)" -by simple - -text " - Now look for an inhabitant. - Observe that we're looking for a lambda term \<open>pred\<close> satisfying \<open>(pred`0) =\<^sub>\<nat> 0\<close> and \<open>\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n\<close>. - What if we require **definitional** equality instead of just propositional equality? -" - -schematic_goal "?p`0 \<equiv> 0" and "\<And>n. n: \<nat> \<Longrightarrow> (?p`(succ n)) \<equiv> n" -apply (subst comp, rule Nat_rules) -prefer 3 apply (subst comp, rule Nat_rules) -prefer 3 apply (rule Nat_rules) -prefer 8 apply (rule Nat_rules | assumption)+ -done - -text " - The above proof finds the candidate \<open>\<^bold>\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) n n\<close>. - We prove this has the required type and properties. -" - -definition pred :: Term where "pred \<equiv> \<^bold>\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) n n" - -lemma pred_type: "pred: \<nat> \<rightarrow> \<nat>" unfolding pred_def by simple - -lemma pred_props: "<refl(0), \<^bold>\<lambda>n. refl(n)>: ((pred`0) =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n)" -proof (simple lem: pred_type) - have *: "pred`0 \<equiv> 0" unfolding pred_def - proof (subst comp) - show "\<And>n. n: \<nat> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>a b. a) n n: \<nat>" by simple - show "ind\<^sub>\<nat> (\<lambda>a b. a) 0 0 \<equiv> 0" - proof (rule Nat_comps) - show "\<nat>: U(O)" .. - qed simple - qed rule - then show "refl(0): (pred`0) =\<^sub>\<nat> 0" by (subst *) simple - - show "\<^bold>\<lambda>n. refl(n): \<Prod>n:\<nat>. (pred`(succ(n))) =\<^sub>\<nat> n" - unfolding pred_def proof - show "\<And>n. n: \<nat> \<Longrightarrow> refl(n): ((\<^bold>\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) n n)`succ(n)) =\<^sub>\<nat> n" - proof (subst comp) - show "\<And>n. n: \<nat> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>a b. a) n n: \<nat>" by simple - show "\<And>n. n: \<nat> \<Longrightarrow> refl(n): ind\<^sub>\<nat> (\<lambda>a b. a) (succ n) (succ n) =\<^sub>\<nat> n" - proof (subst comp) - show "\<nat>: U(O)" .. - qed simple - qed rule - qed rule -qed -theorem - "<pred, <refl(0), \<^bold>\<lambda>n. refl(n)>>: \<Sum>pred:\<nat>\<rightarrow>\<nat> . ((pred`0) =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n)" -by (simple lem: pred_welltyped pred_type pred_props) end
\ No newline at end of file |