diff options
| -rw-r--r-- | Coprod.thy | 2 | ||||
| -rw-r--r-- | Equal.thy | 2 | ||||
| -rw-r--r-- | EqualProps.thy | 2 | ||||
| -rw-r--r-- | HoTT.thy | 2 | ||||
| -rw-r--r-- | HoTT_Base.thy | 2 | ||||
| -rw-r--r-- | HoTT_Methods.thy | 2 | ||||
| -rw-r--r-- | HoTT_Theorems.thy | 2 | ||||
| -rw-r--r-- | Nat.thy | 2 | ||||
| -rw-r--r-- | Prod.thy | 28 | ||||
| -rw-r--r-- | ProdProps.thy | 100 | ||||
| -rw-r--r-- | Proj.thy | 2 | ||||
| -rw-r--r-- | Sum.thy | 2 | ||||
| -rw-r--r-- | ex/Synthesis.thy | 16 |
13 files changed, 105 insertions, 59 deletions
@@ -62,4 +62,4 @@ lemmas Coprod_form_conds [wellform] = Coprod_form_cond1 Coprod_form_cond2 lemmas Coprod_comps [comp] = Coprod_comp1 Coprod_comp2 -end
\ No newline at end of file +end @@ -65,4 +65,4 @@ lemmas Equal_comps [comp] = Equal_comp -end
\ No newline at end of file +end diff --git a/EqualProps.thy b/EqualProps.thy index f3b355a..5eea920 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -221,4 +221,4 @@ lemmas EqualProps_rules [intro] = inv_type pathcomp_type lemmas EqualProps_comps [comp] = inv_comp pathcomp_comp -end
\ No newline at end of file +end @@ -23,4 +23,4 @@ EqualProps Proj begin -end
\ No newline at end of file +end diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 4fadd5d..647593e 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -85,4 +85,4 @@ named_theorems wellform named_theorems comp -end
\ No newline at end of file +end diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index c3703bf..316841d 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -65,4 +65,4 @@ text "Perform basic single-step computations:" method compute uses lems = (subst lems comp) -end
\ No newline at end of file +end diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy index a3a1f63..79614d3 100644 --- a/HoTT_Theorems.thy +++ b/HoTT_Theorems.thy @@ -203,4 +203,4 @@ The next thing to do is to implement induction to automate such proofs. When we get more stuff working, I'd like to aim for formalizing the encode-decode method to be able to prove the only naturals are 0 and those obtained from it by \<open>succ\<close>." *) -end
\ No newline at end of file +end @@ -52,4 +52,4 @@ lemmas Nat_rules [intro] = Nat_form Nat_intro Nat_elim Nat_comp1 Nat_comp2 lemmas Nat_comps [comp] = Nat_comp1 Nat_comp2 -end
\ No newline at end of file +end @@ -43,11 +43,15 @@ and and Prod_elim: "\<lbrakk>f: \<Prod>x:A. B(x); a: A\<rbrakk> \<Longrightarrow> f`a: B(a)" and - Prod_comp: "\<lbrakk>a: A; \<And>x. x: A \<Longrightarrow> b(x): B(x)\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. b(x))`a \<equiv> b(a)" + Prod_comp: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b(x): B(x); a: A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. b(x))`a \<equiv> b(a)" and Prod_uniq: "f : \<Prod>x:A. B(x) \<Longrightarrow> \<^bold>\<lambda>x. (f`x) \<equiv> f" +and + Prod_eq: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b(x) \<equiv> b'(x); A: U(i)\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x. b(x) \<equiv> \<^bold>\<lambda>x. b'(x)" text " + The Pure rules for \<open>\<equiv>\<close> only let us judge strict syntactic equality of object lambda expressions; Prod_eq is the actual definitional equality rule. + Note that the syntax \<open>\<^bold>\<lambda>\<close> (bold lambda) used for dependent functions clashes with the proof term syntax (cf. \<section>2.5.2 of the Isabelle/Isar Implementation). " @@ -64,9 +68,9 @@ and text "Set up the standard reasoner to use the type rules:" -lemmas Prod_rules [intro] = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq +lemmas Prod_rules [intro] = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq Prod_eq lemmas Prod_wellform [wellform] = Prod_form_cond1 Prod_form_cond2 -lemmas Prod_comps [comp] = Prod_comp Prod_uniq +lemmas Prod_comps [comp] = Prod_comp Prod_uniq Prod_eq section \<open>Function composition\<close> @@ -77,23 +81,13 @@ syntax "_COMPOSE" :: "[Term, Term] \<Rightarrow> Term" (infixr "\<circ>" 70) translations "g \<circ> f" \<rightleftharpoons> "g o f" axiomatization where - compose_type: "\<lbrakk> - g: \<Prod>x:B. C(x); + compose_def: "\<lbrakk> f: A \<rightarrow> B; - (\<Prod>x:B. C(x)): U(i); - A \<rightarrow> B: U(i) - \<rbrakk> \<Longrightarrow> g \<circ> f: \<Prod>x:A. C(f`x)" -and - compose_comp: "\<lbrakk> g: \<Prod>x:B. C(x); - f: A \<rightarrow> B; - (\<Prod>x:B. C(x)): U(i); - A \<rightarrow> B: U(i) + A \<rightarrow> B: U(i); + (\<Prod>x:B. C(x)): U(i) \<rbrakk> \<Longrightarrow> g \<circ> f \<equiv> \<^bold>\<lambda>x. g`(f`x)" -lemmas compose_rules [intro] = compose_type -lemmas compose_comps [comp] = compose_comp - section \<open>Unit type\<close> @@ -114,4 +108,4 @@ lemmas Unit_rules [intro] = Unit_form Unit_intro Unit_elim Unit_comp lemmas Unit_comps [comp] = Unit_comp -end
\ No newline at end of file +end diff --git a/ProdProps.thy b/ProdProps.thy index 7c2c658..e48b3e6 100644 --- a/ProdProps.thy +++ b/ProdProps.thy @@ -15,40 +15,94 @@ begin section \<open>Composition\<close> text " - The following rule is admissible, but we cannot derive it only using the rules for the \<Pi>-type. + The proof of associativity is surprisingly intricate; it involves telling Isabelle to use the correct rule for \<Pi>-type judgmental equality, and the correct substitutions in the subgoals thereafter, among other things. " -lemma compose_comp': "\<lbrakk> - A: U(i); - \<And>x. x: A \<Longrightarrow> b(x): B; - \<And>x. x: B \<Longrightarrow> c(x): C(x) - \<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. c(x)) \<circ> (\<^bold>\<lambda>x. b(x)) \<equiv> \<^bold>\<lambda>x. c(b(x))" +lemma compose_assoc: + assumes + "A \<rightarrow> B: U(i)" "B \<rightarrow> C: U(i)" and + "\<Prod>x:C. D(x): U(i)" and + "f: A \<rightarrow> B" "g: B \<rightarrow> C" "h: \<Prod>x:C. D(x)" + shows "(h \<circ> g) \<circ> f \<equiv> h \<circ> (g \<circ> f)" + +proof (subst (0 1 2 3) compose_def) + text "Compute the different bracketings and show they are equivalent:" + + show "\<^bold>\<lambda>x. (\<^bold>\<lambda>y. h`(g`y))`(f`x) \<equiv> \<^bold>\<lambda>x. h`((\<^bold>\<lambda>y. g`(f`y))`x)" + proof (subst Prod_eq) + show "\<^bold>\<lambda>x. h`((\<^bold>\<lambda>y. g`(f`y))`x) \<equiv> \<^bold>\<lambda>x. h`((\<^bold>\<lambda>y. g`(f`y))`x)" by simp + show "\<And>x. x: A \<Longrightarrow> (\<^bold>\<lambda>y. h`(g`y))`(f`x) \<equiv> h`((\<^bold>\<lambda>y. g`(f`y))`x)" + proof compute + show "\<And>x. x: A \<Longrightarrow> h`(g`(f`x)) \<equiv> h`((\<^bold>\<lambda>y. g`(f`y))`x)" + proof compute + show "\<And>x. x: A \<Longrightarrow> g`(f`x): C" by (simple lems: assms) + qed + show "\<And>x. x: B \<Longrightarrow> h`(g`x): D(g`x)" by (simple lems: assms) + qed (simple lems: assms) + qed (wellformed lems: assms) + + text " + Finish off any remaining subgoals that Isabelle can't prove automatically. + These typically require the application of specific substitutions or computation rules. + " + show "g \<circ> f: A \<rightarrow> C" by (subst compose_def) (derive lems: assms) + + show "h \<circ> g: \<Prod>x:B. D(g`x)" + proof (subst compose_def) + show "\<^bold>\<lambda>x. h`(g`x): \<Prod>x:B. D(g`x)" + proof + show "\<And>x. x: B \<Longrightarrow> h`(g`x): D(g`x)" + proof + show "\<And>x. x: B \<Longrightarrow> g`x: C" by (simple lems: assms) + qed (simple lems: assms) + qed (wellformed lems: assms) + qed fact+ + + show "\<Prod>x:B. D (g`x): U(i)" + proof + show "\<And>x. x: B \<Longrightarrow> D(g`x): U(i)" + proof - + have *: "D: C \<longrightarrow> U(i)" by (wellformed lems: assms) + + fix x assume asm: "x: B" + have "g`x: C" by (simple lems: assms asm) + then show "D(g`x): U(i)" by (rule *) + qed + qed (wellformed lems: assms) + + have "A: U(i)" by (wellformed lems: assms) + moreover have "C: U(i)" by (wellformed lems: assms) + ultimately show "A \<rightarrow> C: U(i)" .. +qed (simple lems: assms) + + +text "The following rule is correct, but we cannot prove it using just the rules of the theory." + +lemma compose_comp': + assumes "A: U(i)" and "\<And>x. x: A \<Longrightarrow> b(x): B" and "\<And>x. x: B \<Longrightarrow> c(x): C(x)" + shows "(\<^bold>\<lambda>x. c(x)) \<circ> (\<^bold>\<lambda>x. b(x)) \<equiv> \<^bold>\<lambda>x. c(b(x))" oops text "However we can derive a variant with more explicit premises:" -lemma compose_comp2: +lemma compose_comp: assumes - "A: U(i)" "B: U(i)" and - "C: B \<longrightarrow> U(i)" and + "A: U(i)" "B: U(i)" "C: B \<longrightarrow> U(i)" and "\<And>x. x: A \<Longrightarrow> b(x): B" and "\<And>x. x: B \<Longrightarrow> c(x): C(x)" shows "(\<^bold>\<lambda>x. c(x)) \<circ> (\<^bold>\<lambda>x. b(x)) \<equiv> \<^bold>\<lambda>x. c(b(x))" -proof (subst (0) comp) - show "\<^bold>\<lambda>x. (\<^bold>\<lambda>u. c(u))`((\<^bold>\<lambda>v. b(v))`x) \<equiv> \<^bold>\<lambda>x. c(b(x))" - proof (subst (0) comp) - show "\<^bold>\<lambda>x. c((\<^bold>\<lambda>v. b(v))`x) \<equiv> \<^bold>\<lambda>x. c(b(x))" - proof - - have *: "\<And>x. x: A \<Longrightarrow> (\<^bold>\<lambda>v. b(v))`x \<equiv> b(x)" by simple (rule assms) - show "\<^bold>\<lambda>x. c((\<^bold>\<lambda>v. b(v))`x) \<equiv> \<^bold>\<lambda>x. c(b(x))" - proof (subst *) - +proof (subst compose_def) + show "\<^bold>\<lambda>x. (\<^bold>\<lambda>x. c(x))`((\<^bold>\<lambda>x. b(x))`x) \<equiv> \<^bold>\<lambda>x. c(b(x))" + proof + show "\<And>a. a: A \<Longrightarrow> (\<^bold>\<lambda>x. c(x))`((\<^bold>\<lambda>x. b(x))`a) \<equiv> c(b(a))" + proof compute + show "\<And>a. a: A \<Longrightarrow> c((\<^bold>\<lambda>x. b(x))`a) \<equiv> c(b(a))" by compute (simple lems: assms) + qed (simple lems: assms) + qed fact +qed (simple lems: assms) -text "We can show associativity of composition in general." -lemma compose_assoc: - "(f \<circ> g) \<circ> h \<equiv> f \<circ> (g \<circ> h)" -proof +lemmas compose_comps [comp] = compose_def compose_comp -end
\ No newline at end of file +end @@ -60,4 +60,4 @@ lemmas Proj_types [intro] = fst_type snd_type lemmas Proj_comps [comp] = fst_comp snd_comp -end
\ No newline at end of file +end @@ -77,4 +77,4 @@ and lemmas Empty_rules [intro] = Empty_form Empty_elim -end
\ No newline at end of file +end diff --git a/ex/Synthesis.thy b/ex/Synthesis.thy index ef6673c..cd5c4e1 100644 --- a/ex/Synthesis.thy +++ b/ex/Synthesis.thy @@ -19,9 +19,7 @@ text " 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. -" +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 @@ -40,11 +38,11 @@ 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>. + The above proof finds a candidate, namely \<open>\<^bold>\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) 0 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" +definition pred :: Term where "pred \<equiv> \<^bold>\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) 0 n" lemma pred_type: "pred: \<nat> \<rightarrow> \<nat>" unfolding pred_def by simple @@ -52,7 +50,7 @@ lemma pred_props: "<refl(0), \<^bold>\<lambda>n. refl(n)>: ((pred`0) =\<^sub>\<n proof (simple lems: pred_type) have *: "pred`0 \<equiv> 0" unfolding pred_def proof compute - show "\<And>n. n: \<nat> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>a b. a) n n: \<nat>" by simple + show "\<And>n. n: \<nat> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>a b. a) 0 n: \<nat>" by simple show "ind\<^sub>\<nat> (\<lambda>a b. a) 0 0 \<equiv> 0" proof (rule Nat_comps) show "\<nat>: U(O)" .. @@ -62,10 +60,10 @@ proof (simple lems: pred_type) 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" + show "\<And>n. n: \<nat> \<Longrightarrow> refl(n): ((\<^bold>\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) 0 n)`succ(n)) =\<^sub>\<nat> n" proof compute - 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" + show "\<And>n. n: \<nat> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>a b. a) 0 n: \<nat>" by simple + show "\<And>n. n: \<nat> \<Longrightarrow> refl(n): ind\<^sub>\<nat> (\<lambda>a b. a) 0 (succ n) =\<^sub>\<nat> n" proof compute show "\<nat>: U(O)" .. qed simple |