aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2018-05-30 10:46:48 +0200
committerJosh Chen2018-05-30 10:46:48 +0200
commit29015c5877876df28890209d2ad341c6cabd1cc8 (patch)
tree9dea556485d004aa7e2af3a273e83dd73bb414cb
parent607c3971e08d1ded22bd9f1cabdd309653af1248 (diff)
Fixed dependent product rules, hopefully final now.
-rw-r--r--HoTT.thy5
-rw-r--r--HoTT_Theorems.thy99
2 files changed, 29 insertions, 75 deletions
diff --git a/HoTT.thy b/HoTT.thy
index 96bd3c1..cf21304 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -70,11 +70,10 @@ axiomatization
appl :: "[Term, Term] \<Rightarrow> Term" (infixl "`" 60)
where
Prod_form: "\<And>(A::Term) (B::Term \<Rightarrow> Term). \<lbrakk>A : U; B : A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Prod>x:A. B(x) : U" and
- Prod_intro [intro]: "\<And>(A::Term) (B::Term \<Rightarrow> Term) (b::Term \<Rightarrow> Term). \<lbrakk>A : U; B : A \<rightarrow> U; \<And>x::Term. x : A \<Longrightarrow> b(x) : B(x)\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x:A. b(x) : \<Prod>x:A. B(x)" and
+ Prod_intro [intro]: "\<And>(A::Term) (B::Term \<Rightarrow> Term) (b::Term \<Rightarrow> Term). (\<And>x::Term. x : A \<Longrightarrow> b(x) : B(x)) \<Longrightarrow> \<^bold>\<lambda>x:A. b(x) : \<Prod>x:A. B(x)" and
Prod_elim [elim]: "\<And>(A::Term) (B::Term \<Rightarrow> Term) (f::Term) (a::Term). \<lbrakk>f : \<Prod>x:A. B(x); a : A\<rbrakk> \<Longrightarrow> f`a : B(a)" and
- Prod_comp [simp]: "\<And>(A::Term) (B::Term \<Rightarrow> Term) (b::Term \<Rightarrow> Term) (a::Term). \<lbrakk>A : U; B : A \<rightarrow> U; \<And>x::Term. x : A \<Longrightarrow> b(x) : B(x); a : A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b(x))`a \<equiv> b(a)" and
+ Prod_comp [simp]: "\<And>(A::Term) (B::Term \<Rightarrow> Term) (b::Term \<Rightarrow> Term) (a::Term). \<lbrakk>\<And>x::Term. x : A \<Longrightarrow> b(x) : B(x); a : A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b(x))`a \<equiv> b(a)" and
Prod_uniq [simp]: "\<And>(A::Term) (B::Term \<Rightarrow> Term) (f::Term). f : \<Prod>x:A. B(x) \<Longrightarrow> \<^bold>\<lambda>x:A. (f`x) \<equiv> f"
-(* Thinking about the premises for the computation rule... they make simplification rather cumbersome, should I remove them? Would this potentially result in logical problems with being able to state untrue statements? (But probably not prove them?) *)
text "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)."
diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy
index d83a08c..10a0d2c 100644
--- a/HoTT_Theorems.thy
+++ b/HoTT_Theorems.thy
@@ -6,10 +6,11 @@ text "A bunch of theorems and other statements for sanity-checking, as well as t
Things that *should* be automated:
\<bullet> Checking that \<open>A\<close> is a well-formed type, when writing things like \<open>x : A\<close> and \<open>A : U\<close>.
- \<bullet> Checking that the argument to a (dependent/non-dependent) function matches the type? Also the arguments to a pair?"
+ \<bullet> Checking that the argument to a (dependent/non-dependent) function matches the type? Also the arguments to a pair?
+"
\<comment> \<open>Turn on trace for unification and the simplifier, for debugging.\<close>
-declare[[unify_trace_simp, unify_trace_types, simp_trace, simp_trace_depth_limit=2]]
+declare[[unify_trace_simp, unify_trace_types, simp_trace, simp_trace_depth_limit=1]]
section \<open>Functions\<close>
@@ -17,97 +18,51 @@ subsection \<open>Typing functions\<close>
text "Declaring \<open>Prod_intro\<close> with the \<open>intro\<close> attribute (in HoTT.thy) enables \<open>standard\<close> to prove the following."
-lemma id_function: "A : U \<Longrightarrow> \<^bold>\<lambda>x:A. x : A\<rightarrow>A" ..
+lemma "\<^bold>\<lambda>x:A. x : A\<rightarrow>A" ..
-text "Here is the same result, stated and proved differently.
-The standard method invoked after the keyword \<open>proof\<close> is applied to the goal \<open>\<^bold>\<lambda>x. x: A\<rightarrow>A\<close>, and so we need to show the prover how to continue, as opposed to the previous lemma."
-
-lemma
- assumes "A : U"
- shows "\<^bold>\<lambda>x:A. x : A\<rightarrow>A"
-proof
- show "A : U" using assms .
- show "\<lambda>x. A : A \<rightarrow> U" using assms ..
-qed
-
-text "Note that there is no provision for declaring the type of bound variables outside of the scope of a lambda expression.
-More generally, we cannot write an assumption stating 'Let \<open>x\<close> be a variable of type \<open>A\<close>'."
-
-proposition "\<lbrakk>A : U; A \<equiv> B\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x:A. x : B\<rightarrow>A"
+proposition "A \<equiv> B \<Longrightarrow> \<^bold>\<lambda>x:A. x : B\<rightarrow>A"
proof -
- assume
- 1: "A : U" and
- 2: "A \<equiv> B"
- from id_function[OF 1] have 3: "\<^bold>\<lambda>x:A. x : A\<rightarrow>A" .
- from 2 have "A\<rightarrow>A \<equiv> B\<rightarrow>A" by simp
- with 3 show "\<^bold>\<lambda>x:A. x : B\<rightarrow>A" ..
-qed
-
-text "It is instructive to try to prove \<open>\<lbrakk>A : U; B : U\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x. \<^bold>\<lambda>y. x : A\<rightarrow>B\<rightarrow>A\<close>.
-First we prove an intermediate step."
-
-lemma constant_function: "\<lbrakk>A : U; B : U; x : A\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>y:B. x : B\<rightarrow>A" ..
-
-text "And now the actual result:"
-
-proposition
- assumes 1: "A : U" and 2: "B : U"
- shows "\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x : A\<rightarrow>B\<rightarrow>A"
-proof
- show "A : U" using assms(1) .
- show "\<And>x. x : A \<Longrightarrow> \<^bold>\<lambda>y:B. x : B \<rightarrow> A" using assms by (rule constant_function)
-
- from assms have "B \<rightarrow> A : U" by (rule Prod_formation)
- then show "\<lambda>x. B \<rightarrow> A: A \<rightarrow> U" using assms(1) by (rule constant_type_family)
+ assume assm: "A \<equiv> B"
+ have id: "\<^bold>\<lambda>x:A. x : A\<rightarrow>A" ..
+ from assm have "A\<rightarrow>A \<equiv> B\<rightarrow>A" by simp
+ with id show "\<^bold>\<lambda>x:A. x : B\<rightarrow>A" ..
qed
-text "Maybe a nicer way to write it:"
-
-proposition alternating_function: "\<lbrakk>A : U; B: U\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x : A\<rightarrow>B\<rightarrow>A"
+proposition "\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x : A\<rightarrow>B\<rightarrow>A"
proof
- fix x
- show "\<lbrakk>A : U; B : U; x : A\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>y:B. x : B \<rightarrow> A" by (rule constant_function)
- show "\<lbrakk>A : U; B : U\<rbrakk> \<Longrightarrow> B\<rightarrow>A : U" by (rule Prod_formation)
+ fix a
+ assume "a : A"
+ then show "\<^bold>\<lambda>y:B. a : B \<rightarrow> A" ..
qed
subsection \<open>Function application\<close>
-lemma "\<lbrakk>A : U; a : A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. x)`a \<equiv> a" by simp
+proposition "\<lbrakk>A : U; a : A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. x)`a \<equiv> a" by simp
+
+text "Two arguments:"
lemma
- assumes
- "A:U" and
- "B:U" and
- "a:A" and
- "b:B"
+ assumes "a:A" and "b:B"
shows "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x)`a`b \<equiv> a"
proof -
have "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x)`a \<equiv> \<^bold>\<lambda>y:B. a"
- proof (rule Prod_comp[of A "\<lambda>_. B\<rightarrow>A"])
- have "B \<rightarrow> A : U" using constant_type_family[OF assms(1) assms(2)] assms(2) by (rule Prod_formation)
- then show "\<lambda>x. B \<rightarrow> A: A \<rightarrow> U" using assms(1) by (rule constant_type_family[of "B\<rightarrow>A"])
-
- show "\<And>x. x : A \<Longrightarrow> \<^bold>\<lambda>y:B. x : B \<rightarrow> A" using assms(2) assms(1) ..
- show "A:U" using assms(1) .
- show "a:A" using assms(3) .
- qed (* Why do I need to do the above for the last two goals? Can't Isabelle do it automatically? *)
-
+ proof (rule Prod_comp[of A _ "\<lambda>_. B\<rightarrow>A"])
+ fix x
+ assume "x:A"
+ then show "\<^bold>\<lambda>y:B. x : B \<rightarrow> A" ..
+ qed (rule assms)
then have "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x)`a`b \<equiv> (\<^bold>\<lambda>y:B. a)`b" by simp
-
- also have "(\<^bold>\<lambda>y:B. a)`b \<equiv> a"
- proof (rule Prod_comp[of B "\<lambda>_. A"])
- show "\<lambda>y. A: B \<rightarrow> U" using assms(1) assms(2) by (rule constant_type_family)
- show "\<And>y. y : B \<Longrightarrow> a : A" using assms(3) .
- show "B:U" using assms(2) .
- show "b:B" using assms(4) .
- qed
-
+ also have "(\<^bold>\<lambda>y:B. a)`b \<equiv> a" using assms by (simp add: Prod_comp[of B _ "\<lambda>_. A"])
finally show "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x)`a`b \<equiv> a" .
qed
+text "Note that the propositions and proofs above often say nothing about the well-formedness of the types, or the well-typedness of the lambdas involved; one has to be very explicit and prove such things separately!
+This is the result of the choices made regarding the premises of the type rules."
+
text "Polymorphic identity function."
consts Ui::Term
+
definition Id where "Id \<equiv> \<^bold>\<lambda>A:Ui. \<^bold>\<lambda>x:A. x"
(* Have to think about universes... *)