Well-formation rules are back in the methods; new theory synthesizing the natural number predecessor function.

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