diff options
| -rw-r--r-- | Coprod.thy | 14 | ||||
| -rw-r--r-- | Equal.thy | 10 | ||||
| -rw-r--r-- | HoTT_Base.thy | 2 | ||||
| -rw-r--r-- | Nat.thy | 5 | ||||
| -rw-r--r-- | Proj.thy | 6 | ||||
| -rw-r--r-- | ex/Synthesis.thy | 81 | ||||
| -rw-r--r-- | scratch.thy | 158 |
7 files changed, 174 insertions, 102 deletions
@@ -44,17 +44,21 @@ and \<And>y. y: B \<Longrightarrow> d(y): C(inr(y)); b: B \<rbrakk> \<Longrightarrow> ind\<^sub>+(c)(d)(inr(b)) \<equiv> d(b)" -(* + + text "Admissible formation inference rules:" axiomatization where Coprod_form_cond1: "\<And>i A B. A + B: U(i) \<Longrightarrow> A: U(i)" and Coprod_form_cond2: "\<And>i A B. A + B: U(i) \<Longrightarrow> B: U(i)" -*) -lemmas Coprod_rules [intro] = - Coprod_form Coprod_intro1 Coprod_intro2 Coprod_elim Coprod_comp1 Coprod_comp2 -(*lemmas Coprod_form_conds [intro] = Coprod_form_cond1 Coprod_form_cond2 *) + + +text "Rule declarations:" + +lemmas Coprod_intro = Coprod_intro1 Coprod_intro2 +lemmas Coprod_rules [intro] = Coprod_form Coprod_intro Coprod_elim Coprod_comp1 Coprod_comp2 +lemmas Coprod_form_conds [wellform] = Coprod_form_cond1 Coprod_form_cond2 lemmas Coprod_comps [comp] = Coprod_comp1 Coprod_comp2 @@ -46,17 +46,21 @@ and a: A \<rbrakk> \<Longrightarrow> ind\<^sub>=(f)(refl(a)) \<equiv> f(a)" + text "Admissible inference rules for equality type formation:" -(* + axiomatization where Equal_form_cond1: "a =\<^sub>A b: U(i) \<Longrightarrow> A: U(i)" and Equal_form_cond2: "a =\<^sub>A b: U(i) \<Longrightarrow> a: A" and Equal_form_cond3: "a =\<^sub>A b: U(i) \<Longrightarrow> b: A" -*) + + +text "Rule declarations:" + lemmas Equal_rules [intro] = Equal_form Equal_intro Equal_elim Equal_comp -(*lemmas Equal_wellform [intro] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3*) +lemmas Equal_wellform [wellform] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3 lemmas Equal_comps [comp] = Equal_comp diff --git a/HoTT_Base.thy b/HoTT_Base.thy index e94ca5c..4fadd5d 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -78,7 +78,7 @@ section \<open>Named theorems\<close> text " Named theorems to be used by proof methods later (see HoTT_Methods.thy). - \<open>wellform\<close> declares necessary wellformedness conditions for type and inhabitation judgments, while \<open>comp\<close> declares computation rules, which are used by the simplification method as equational rewrite rules. + \<open>wellform\<close> declares necessary wellformedness conditions for type and inhabitation judgments, while \<open>comp\<close> declares computation rules, which are usually passed to invocations of the method \<open>subst\<close> to perform equational rewriting. " named_theorems wellform @@ -10,6 +10,8 @@ theory Nat begin +section \<open>Constants and type rules\<close> + axiomatization Nat :: Term ("\<nat>") and zero :: Term ("0") and @@ -42,6 +44,9 @@ and n: \<nat> \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat>(f)(a)(succ n) \<equiv> f(n)(ind\<^sub>\<nat> f a n)" + +text "Rule declarations:" + lemmas Nat_intro = Nat_intro1 Nat_intro2 lemmas Nat_rules [intro] = Nat_form Nat_intro Nat_elim Nat_comp1 Nat_comp2 lemmas Nat_comps [comp] = Nat_comp1 Nat_comp2 @@ -18,12 +18,10 @@ axiomatization snd :: "Term \<Rightarrow> Term" where snd_def: "snd \<equiv> \<l text "Typing judgments and computation rules for the dependent and non-dependent projection functions." - lemma fst_type: assumes "\<Sum>x:A. B(x): U(i)" and "p: \<Sum>x:A. B(x)" shows "fst(p): A" unfolding fst_def by (derive lem: assms) - lemma fst_comp: assumes "A: U(i)" and "B: A \<longrightarrow> U(i)" and "a: A" and "b: B(a)" shows "fst(<a,b>) \<equiv> a" unfolding fst_def @@ -31,7 +29,6 @@ proof show "a: A" and "b: B(a)" by fact+ qed (rule assms)+ - lemma snd_type: assumes "\<Sum>x:A. B(x): U(i)" and "p: \<Sum>x:A. B(x)" shows "snd(p): B(fst p)" unfolding snd_def @@ -47,7 +44,6 @@ proof qed fact+ qed fact - lemma snd_comp: assumes "A: U(i)" and "B: A \<longrightarrow> U(i)" and "a: A" and "b: B(a)" shows "snd(<a,b>) \<equiv> b" unfolding snd_def @@ -58,6 +54,8 @@ proof qed (simple lem: assms) +text "Rule declarations:" + lemmas Proj_types [intro] = fst_type snd_type lemmas Proj_comps [intro] = fst_comp snd_comp diff --git a/ex/Synthesis.thy b/ex/Synthesis.thy new file mode 100644 index 0000000..60655e5 --- /dev/null +++ b/ex/Synthesis.thy @@ -0,0 +1,81 @@ +(* Title: HoTT/ex/Synthesis.thy + Author: Josh Chen + Date: Aug 2018 + +Examples of synthesis. +*) + + +theory Synthesis + imports "../HoTT" +begin + + +section \<open>Synthesis of the predecessor function\<close> + +text " + In this example we construct, with the help of Isabelle, a predecessor function for the natural numbers. + + This is also done in \<open>CTT.thy\<close>; there the work is easier as the equality type is extensional, and also the methods are set up a little more nicely. +" + +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 we look for an inhabitant of this type. + 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 a candidate, namely \<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 diff --git a/scratch.thy b/scratch.thy index 25d2ca7..8800b1a 100644 --- a/scratch.thy +++ b/scratch.thy @@ -1,101 +1,81 @@ +(* Title: HoTT/ex/Synthesis.thy + Author: Josh Chen + Date: Aug 2018 + +Examples of inhabitant synthesis. +*) + + theory scratch imports HoTT - begin -lemma - assumes "\<Sum>x:A. B(x): U(i)" "<a,b>: \<Sum>x:A. B(x)" - shows "a : A" -proof -oops - - -abbreviation pred where "pred \<equiv> \<^bold>\<lambda>n. ind\<^sub>\<nat>(\<lambda>n c. n) 0 n" - -schematic_goal "?a: (pred`0) =\<^sub>\<nat> 0" -apply (subst comp) -apply (rule Nat_intro) -prefer 2 apply (subst comp) -apply (rule Nat_form) -apply assumption -apply (rule Nat_intro) -apply (rule Equal_intro) -apply (rule Nat_intro) -apply (rule Nat_elim) -apply (rule Nat_form) -apply assumption -apply (rule Nat_intro1) -apply assumption -done -schematic_goal "?a : \<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n" -apply (rule Prod_intro) -apply (rule Nat_form) -apply (subst comp) -apply (rule Nat_intro) -apply assumption -prefer 2 apply (subst comp) -apply (rule Nat_form) -apply assumption -apply (rule Nat_intro) -apply assumption -apply (rule Equal_intro) -apply assumption -apply (rule Nat_elim) -apply (rule Nat_form) -apply assumption -apply (rule Nat_intro) -apply assumption +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 -schematic_goal "?a : \<Sum>p:\<nat>\<rightarrow>\<nat>. \<Prod>n:\<nat>. (p`(succ n)) =\<^sub>\<nat> n" -apply (rule Sum_intro) -apply (rule Prod_form) -apply (rule Nat_form)+ -apply (rule Prod_form) -apply (rule Nat_form) -apply (rule Equal_form) -apply (rule Nat_form) -apply (rule Prod_elim) -apply assumption -apply (elim Nat_intro2) -apply assumption -prefer 2 apply (rule Prod_intro) -apply (rule Nat_form) -prefer 3 apply (rule Prod_intro) -apply (rule Nat_form)+ -prefer 3 apply (rule Nat_elim) -back -oops - - -(* Now try to derive pred directly *) -schematic_goal "?a : \<Sum>pred:?A . ((pred`0) =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n)" -(* At some point need to perform induction *) -apply (rule Sum_intro) -defer -apply (rule Sum_form) -apply (rule Equal_form) -apply (rule Nat_form) -apply (rule Prod_elim) -defer -apply (rule Nat_intro1)+ -prefer 5 apply assumption -prefer 4 apply (rule Prod_form) -apply (rule Nat_form)+ -apply (rule Prod_form) -apply (rule Nat_form) -apply (rule Equal_form) -apply (rule Nat_form) -apply (rule Prod_elim) -apply assumption -apply (rule Nat_intro2) -apply assumption+ -(* Now begins the hard part *) -prefer 2 apply (rule Sum_rules) -prefer 2 apply (rule Prod_rules) +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 |