diff options
Diffstat (limited to 'scratch.thy')
-rw-r--r-- | scratch.thy | 158 |
1 files changed, 69 insertions, 89 deletions
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 |