From e6473c383b479610cee4c0119e5811a12a938cf9 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 14 Aug 2018 17:43:03 +0200 Subject: Well-formation rules are back in the methods; new theory synthesizing the natural number predecessor function. --- Coprod.thy | 14 +++-- Equal.thy | 10 ++-- HoTT_Base.thy | 2 +- Nat.thy | 5 ++ Proj.thy | 6 +-- ex/Synthesis.thy | 81 ++++++++++++++++++++++++++++ scratch.thy | 158 ++++++++++++++++++++++++------------------------------- 7 files changed, 174 insertions(+), 102 deletions(-) create mode 100644 ex/Synthesis.thy diff --git a/Coprod.thy b/Coprod.thy index d47c24e..178e345 100644 --- a/Coprod.thy +++ b/Coprod.thy @@ -44,17 +44,21 @@ and \y. y: B \ d(y): C(inr(y)); b: B \ \ ind\<^sub>+(c)(d)(inr(b)) \ d(b)" -(* + + text "Admissible formation inference rules:" axiomatization where Coprod_form_cond1: "\i A B. A + B: U(i) \ A: U(i)" and Coprod_form_cond2: "\i A B. A + B: U(i) \ 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 \ \ ind\<^sub>=(f)(refl(a)) \ f(a)" + text "Admissible inference rules for equality type formation:" -(* + axiomatization where Equal_form_cond1: "a =\<^sub>A b: U(i) \ A: U(i)" and Equal_form_cond2: "a =\<^sub>A b: U(i) \ a: A" and Equal_form_cond3: "a =\<^sub>A b: U(i) \ 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 \Named theorems\ text " Named theorems to be used by proof methods later (see HoTT_Methods.thy). - \wellform\ declares necessary wellformedness conditions for type and inhabitation judgments, while \comp\ declares computation rules, which are used by the simplification method as equational rewrite rules. + \wellform\ declares necessary wellformedness conditions for type and inhabitation judgments, while \comp\ declares computation rules, which are usually passed to invocations of the method \subst\ 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 \Constants and type rules\ + axiomatization Nat :: Term ("\") and zero :: Term ("0") and @@ -42,6 +44,9 @@ and n: \ \ \ ind\<^sub>\(f)(a)(succ n) \ f(n)(ind\<^sub>\ 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 \ Term" where snd_def: "snd \ \x:A. B(x): U(i)" and "p: \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 \ U(i)" and "a: A" and "b: B(a)" shows "fst() \ 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 "\x:A. B(x): U(i)" and "p: \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 \ U(i)" and "a: A" and "b: B(a)" shows "snd() \ 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 \Synthesis of the predecessor function\ + +text " + In this example we construct, with the help of Isabelle, a predecessor function for the natural numbers. + + This is also done in \CTT.thy\; 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: "\pred:\\\ . ((pred`0) =\<^sub>\ 0) \ (\n:\. (pred`(succ n)) =\<^sub>\ n): U(O)" +by simple + +text " + Now we look for an inhabitant of this type. + Observe that we're looking for a lambda term \pred\ satisfying \(pred`0) =\<^sub>\ 0\ and \\n:\. (pred`(succ n)) =\<^sub>\ n\. + What if we require **definitional** equality instead of just propositional equality? +" + +schematic_goal "?p`0 \ 0" and "\n. n: \ \ (?p`(succ n)) \ 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 \\<^bold>\n. ind\<^sub>\ (\a b. a) n n\. + We prove this has the required type and properties. +" + +definition pred :: Term where "pred \ \<^bold>\n. ind\<^sub>\ (\a b. a) n n" + +lemma pred_type: "pred: \ \ \" unfolding pred_def by simple + +lemma pred_props: "\n. refl(n)>: ((pred`0) =\<^sub>\ 0) \ (\n:\. (pred`(succ n)) =\<^sub>\ n)" +proof (simple lem: pred_type) + have *: "pred`0 \ 0" unfolding pred_def + proof (subst comp) + show "\n. n: \ \ ind\<^sub>\ (\a b. a) n n: \" by simple + show "ind\<^sub>\ (\a b. a) 0 0 \ 0" + proof (rule Nat_comps) + show "\: U(O)" .. + qed simple + qed rule + then show "refl(0): (pred`0) =\<^sub>\ 0" by (subst *) simple + + show "\<^bold>\n. refl(n): \n:\. (pred`(succ(n))) =\<^sub>\ n" + unfolding pred_def proof + show "\n. n: \ \ refl(n): ((\<^bold>\n. ind\<^sub>\ (\a b. a) n n)`succ(n)) =\<^sub>\ n" + proof (subst comp) + show "\n. n: \ \ ind\<^sub>\ (\a b. a) n n: \" by simple + show "\n. n: \ \ refl(n): ind\<^sub>\ (\a b. a) (succ n) (succ n) =\<^sub>\ n" + proof (subst comp) + show "\: U(O)" .. + qed simple + qed rule + qed rule +qed + +theorem + "\n. refl(n)>>: \pred:\\\ . ((pred`0) =\<^sub>\ 0) \ (\n:\. (pred`(succ n)) =\<^sub>\ 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 "\x:A. B(x): U(i)" ": \x:A. B(x)" - shows "a : A" -proof -oops - - -abbreviation pred where "pred \ \<^bold>\n. ind\<^sub>\(\n c. n) 0 n" - -schematic_goal "?a: (pred`0) =\<^sub>\ 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 : \n:\. (pred`(succ n)) =\<^sub>\ 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 \Synthesis of the predecessor function\ + +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: "\pred:\\\ . ((pred`0) =\<^sub>\ 0) \ (\n:\. (pred`(succ n)) =\<^sub>\ n): U(O)" +by simple + +text " + Now look for an inhabitant. + Observe that we're looking for a lambda term \pred\ satisfying \(pred`0) =\<^sub>\ 0\ and \\n:\. (pred`(succ n)) =\<^sub>\ n\. + What if we require **definitional** equality instead of just propositional equality? +" + +schematic_goal "?p`0 \ 0" and "\n. n: \ \ (?p`(succ n)) \ 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 : \p:\\\. \n:\. (p`(succ n)) =\<^sub>\ 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 : \pred:?A . ((pred`0) =\<^sub>\ 0) \ (\n:\. (pred`(succ n)) =\<^sub>\ 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 \\<^bold>\n. ind\<^sub>\ (\a b. a) n n\. + We prove this has the required type and properties. +" + +definition pred :: Term where "pred \ \<^bold>\n. ind\<^sub>\ (\a b. a) n n" + +lemma pred_type: "pred: \ \ \" unfolding pred_def by simple + +lemma pred_props: "\n. refl(n)>: ((pred`0) =\<^sub>\ 0) \ (\n:\. (pred`(succ n)) =\<^sub>\ n)" +proof (simple lem: pred_type) + have *: "pred`0 \ 0" unfolding pred_def + proof (subst comp) + show "\n. n: \ \ ind\<^sub>\ (\a b. a) n n: \" by simple + show "ind\<^sub>\ (\a b. a) 0 0 \ 0" + proof (rule Nat_comps) + show "\: U(O)" .. + qed simple + qed rule + then show "refl(0): (pred`0) =\<^sub>\ 0" by (subst *) simple + show "\<^bold>\n. refl(n): \n:\. (pred`(succ(n))) =\<^sub>\ n" + unfolding pred_def proof + show "\n. n: \ \ refl(n): ((\<^bold>\n. ind\<^sub>\ (\a b. a) n n)`succ(n)) =\<^sub>\ n" + proof (subst comp) + show "\n. n: \ \ ind\<^sub>\ (\a b. a) n n: \" by simple + show "\n. n: \ \ refl(n): ind\<^sub>\ (\a b. a) (succ n) (succ n) =\<^sub>\ n" + proof (subst comp) + show "\: U(O)" .. + qed simple + qed rule + qed rule +qed +theorem + "\n. refl(n)>>: \pred:\\\ . ((pred`0) =\<^sub>\ 0) \ (\n:\. (pred`(succ n)) =\<^sub>\ n)" +by (simple lem: pred_welltyped pred_type pred_props) end \ No newline at end of file -- cgit v1.2.3