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

7 files changed, 174 insertions, 102 deletions

diff --git a/Coprod.thy b/Coprod.thy
index d47c24e..178e345 100644
--- a/Coprod.thy
+++ b/Coprod.thy
@@ -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
 
 
diff --git a/Equal.thy b/Equal.thy
index 93f623f..9fc478a 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -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
diff --git a/Nat.thy b/Nat.thy
index 388df0f..21c9b1c 100644
--- a/Nat.thy
+++ b/Nat.thy
@@ -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
diff --git a/Proj.thy b/Proj.thy
index aa7e8ec..5c05eb2 100644
--- a/Proj.thy
+++ b/Proj.thy
@@ -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