Rename to distinguish function and path composition; function composition proofs, which have issues...

5 files changed, 93 insertions, 101 deletions

diff --git a/EqualProps.thy b/EqualProps.thy
index 2a13ed2..f3b355a 100644
--- a/EqualProps.thy
+++ b/EqualProps.thy
@@ -48,17 +48,17 @@ text "
   Raw composition function, of type \<open>\<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)\<close> polymorphic over the type \<open>A\<close>.
 "
 
-axiomatization reqcompose :: Term where
-  reqcompose_def: "reqcompose \<equiv> \<^bold>\<lambda>x y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= (\<lambda>x. refl(x)) q) p"
+axiomatization rpathcomp :: Term where
+  rpathcomp_def: "rpathcomp \<equiv> \<^bold>\<lambda>x y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= (\<lambda>x. refl(x)) q) p"
 
 text "
   More complicated proofs---the nested path inductions require more explicit step-by-step rule applications:
 "
 
-lemma reqcompose_type:
+lemma rpathcomp_type:
   assumes "A: U(i)"
-  shows "reqcompose: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
-unfolding reqcompose_def
+  shows "rpathcomp: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
+unfolding rpathcomp_def
 proof
   fix x assume 1: "x: A"
   show "\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
@@ -85,17 +85,17 @@ qed fact
 
 corollary
   assumes "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z"
-  shows "reqcompose`x`y`p`z`q: x =\<^sub>A z"
-  by (simple lems: assms reqcompose_type)
+  shows "rpathcomp`x`y`p`z`q: x =\<^sub>A z"
+  by (simple lems: assms rpathcomp_type)
 
 text "
   The following proof is very long, chiefly because for every application of \<open>`\<close> we have to show the wellformedness of the type family appearing in the equality computation rule.
 "
 
-lemma reqcompose_comp:
+lemma rpathcomp_comp:
   assumes "A: U(i)" and "a: A"
-  shows "reqcompose`a`a`refl(a)`a`refl(a) \<equiv> refl(a)"
-unfolding reqcompose_def
+  shows "rpathcomp`a`a`refl(a)`a`refl(a) \<equiv> refl(a)"
+unfolding rpathcomp_def
 proof compute
   { fix x assume 1: "x: A"
   show "\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
@@ -197,28 +197,28 @@ qed fact
 
 text "The raw object lambda term is cumbersome to use, so we define a simpler constant instead."
 
-axiomatization eqcompose :: "[Term, Term] \<Rightarrow> Term"  (infixl "\<bullet>" 60) where
-  eqcompose_def: "\<lbrakk>
+axiomatization pathcomp :: "[Term, Term] \<Rightarrow> Term"  (infixl "\<bullet>" 60) where
+  pathcomp_def: "\<lbrakk>
     A: U(i);
     x: A; y: A; z: A;
     p: x =\<^sub>A y; q: y =\<^sub>A z
-  \<rbrakk> \<Longrightarrow> p \<bullet> q \<equiv> reqcompose`x`y`p`z`q"
+  \<rbrakk> \<Longrightarrow> p \<bullet> q \<equiv> rpathcomp`x`y`p`z`q"
 
 
-lemma eqcompose_type:
+lemma pathcomp_type:
   assumes "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z"
   shows "p \<bullet> q: x =\<^sub>A z"
-proof (subst eqcompose_def)
+proof (subst pathcomp_def)
   show "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" by fact+
-qed (simple lems: assms reqcompose_type)
+qed (simple lems: assms rpathcomp_type)
 
-lemma eqcompose_comp:
+lemma pathcomp_comp:
   assumes "A : U(i)" and "a : A" shows "refl(a) \<bullet> refl(a) \<equiv> refl(a)"
-by (subst eqcompose_def) (simple lems: assms reqcompose_comp)
+by (subst pathcomp_def) (simple lems: assms rpathcomp_comp)
 
 
-lemmas EqualProps_rules [intro] = inv_type eqcompose_type
-lemmas EqualProps_comps [comp] = inv_comp eqcompose_comp
+lemmas EqualProps_rules [intro] = inv_type pathcomp_type
+lemmas EqualProps_comps [comp] = inv_comp pathcomp_comp
 
 
 end
\ No newline at end of file
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index d3aed66..c3703bf 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -62,7 +62,7 @@ ML_file "~~/src/Tools/eqsubst.ML"
 
 text "Perform basic single-step computations:"
 
-method compute uses lems = (subst comp lems)
+method compute uses lems = (subst lems comp)
 
 
 end
\ No newline at end of file
diff --git a/Prod.thy b/Prod.thy
index 496bf3e..cb455ac 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -68,21 +68,31 @@ lemmas Prod_rules [intro] = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq
 lemmas Prod_wellform [wellform] = Prod_form_cond1 Prod_form_cond2
 lemmas Prod_comps [comp] = Prod_comp Prod_uniq
 
-subsection \<open>Composition\<close>
 
-axiomatization fncompose :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<circ>" 70) where
-  fncompose_type: "\<lbrakk>
+section \<open>Function composition\<close>
+
+axiomatization compose :: "[Term, Term] \<Rightarrow> Term"  (infixr "o" 70)
+
+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);
     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
-  fncompose_comp: "\<lbrakk>
-    A: U(i);
-    \<And>x. x: A \<Longrightarrow> b(x): B;
-    \<And>x. x: A \<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))"
+  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)
+  \<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>
diff --git a/ProdProps.thy b/ProdProps.thy
new file mode 100644
index 0000000..7c2c658
--- /dev/null
+++ b/ProdProps.thy
@@ -0,0 +1,54 @@
+(*  Title:  HoTT/ProdProps.thy
+    Author: Josh Chen
+    Date:   Aug 2018
+
+Properties of the dependent product.
+*)
+
+theory ProdProps
+  imports
+    HoTT_Methods
+    Prod
+begin
+
+
+section \<open>Composition\<close>
+
+text "
+  The following rule is admissible, but we cannot derive it only using the rules for the \<Pi>-type.
+"
+
+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))"
+oops
+
+text "However we can derive a variant with more explicit premises:"
+
+lemma compose_comp2:
+  assumes
+    "A: U(i)" "B: U(i)" and
+    "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 *)
+
+
+text "We can show associativity of composition in general."
+
+lemma compose_assoc:
+  "(f \<circ> g) \<circ> h \<equiv> f \<circ> (g \<circ> h)"
+proof 
+
+
+end
\ No newline at end of file
diff --git a/scratch.thy b/scratch.thy
index 8800b1a..f0514c3 100644
--- a/scratch.thy
+++ b/scratch.thy
@@ -1,81 +1,9 @@
-(*  Title:  HoTT/ex/Synthesis.thy
-    Author: Josh Chen
-    Date:   Aug 2018
-
-Examples of inhabitant synthesis.
-*)
-
-
 theory scratch
   imports HoTT
 begin
 
 
-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
-
-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