Prod.thy now has the correct definitional equality structure rule. Definition of function composition and properties.

13 files changed, 105 insertions, 59 deletions

diff --git a/Coprod.thy b/Coprod.thy
index 178e345..f2225f6 100644
--- a/Coprod.thy
+++ b/Coprod.thy
@@ -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
diff --git a/Equal.thy b/Equal.thy
index 9fc478a..bd7dd93 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -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
diff --git a/HoTT.thy b/HoTT.thy
index ce77ec7..724eebc 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -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
diff --git a/Nat.thy b/Nat.thy
index 21c9b1c..b710ff2 100644
--- a/Nat.thy
+++ b/Nat.thy
@@ -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
diff --git a/Prod.thy b/Prod.thy
index cb455ac..120fc59 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -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
diff --git a/Proj.thy b/Proj.thy
index d5ae6fa..76f9f11 100644
--- a/Proj.thy
+++ b/Proj.thy
@@ -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
diff --git a/Sum.thy b/Sum.thy
index 145c303..8522af1 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -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