aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2018-08-16 16:11:42 +0200
committerJosh Chen2018-08-16 16:13:33 +0200
commit8ed9cf8682c07fc47b86c2d0aaeb8b4628aeaa31 (patch)
tree8aad54e91d8174a4fe4d24443d5ad120612ec2e2
parentca8e7a2681c133abdd082cfa29d6994fa73f2d47 (diff)
Prod.thy now has the correct definitional equality structure rule. Definition of function composition and properties.
-rw-r--r--Coprod.thy2
-rw-r--r--Equal.thy2
-rw-r--r--EqualProps.thy2
-rw-r--r--HoTT.thy2
-rw-r--r--HoTT_Base.thy2
-rw-r--r--HoTT_Methods.thy2
-rw-r--r--HoTT_Theorems.thy2
-rw-r--r--Nat.thy2
-rw-r--r--Prod.thy28
-rw-r--r--ProdProps.thy100
-rw-r--r--Proj.thy2
-rw-r--r--Sum.thy2
-rw-r--r--ex/Synthesis.thy16
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