diff options
Diffstat (limited to '')
| -rw-r--r-- | EqualProps.thy | 192 |
1 files changed, 152 insertions, 40 deletions
diff --git a/EqualProps.thy b/EqualProps.thy index d645fb6..3d99456 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -1,6 +1,6 @@ (* Title: HoTT/EqualProps.thy Author: Josh Chen - Date: Jun 2018 + Date: Aug 2018 Properties of equality. *) @@ -18,22 +18,28 @@ section \<open>Symmetry / Path inverse\<close> axiomatization inv :: "Term \<Rightarrow> Term" ("_\<inverse>" [1000] 1000) where inv_def: "inv \<equiv> \<lambda>p. ind\<^sub>= (\<lambda>x. refl(x)) p" +text " + In the proof below we begin by using path induction on \<open>p\<close> with the application of \<open>rule Equal_elim\<close>, telling Isabelle the specific substitutions to use. + The proof is finished with a standard application of the relevant type rules. +" lemma inv_type: assumes "A : U(i)" and "x : A" and "y : A" and "p: x =\<^sub>A y" shows "p\<inverse>: y =\<^sub>A x" unfolding inv_def -proof (rule Equal_elim[where ?x=x and ?y=y]) \<comment> \<open>Path induction\<close> - show "\<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> y =\<^sub>A x: U(i)" using assms(1) .. - show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" .. -qed (fact assms)+ +by (rule Equal_elim[where ?x=x and ?y=y]) (simple lem: assms) + \<comment> \<open>The type doesn't depend on \<open>p\<close> so we don't need to specify \<open>?p\<close> in the \<open>where\<close> clause above.\<close> +text " + The next proof requires explicitly telling Isabelle what to substitute on the RHS of the typing judgment after the initial application of the type rules. + (If viewing this inside Isabelle, place the cursor after the \<open>proof\<close> statement and observe the second subgoal.) +" -lemma inv_comp: assumes "A : U(i)" and "a : A" shows "(refl a)\<inverse> \<equiv> refl(a)" +lemma inv_comp: + assumes "A : U(i)" and "a : A" shows "(refl a)\<inverse> \<equiv> refl(a)" unfolding inv_def proof show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" .. - show "\<And>x. x: A \<Longrightarrow> x =\<^sub>A x: U(i)" using assms(1) .. -qed (fact assms) +qed (simple lem: assms) section \<open>Transitivity / Path composition\<close> @@ -45,67 +51,173 @@ text " axiomatization rcompose :: Term where rcompose_def: "rcompose \<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 rcompose_type: assumes "A: U(i)" shows "rcompose: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" unfolding rcompose_def proof - show "\<And>x. x: A \<Longrightarrow> - \<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z p. ind\<^sub>= refl p) p: \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" + 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)" proof - show "\<And>x y. \<lbrakk>x: A ; y: A\<rbrakk> \<Longrightarrow> - \<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z p. ind\<^sub>= refl p) p: x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" + fix y assume 2: "y: A" + show "\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" proof - { fix x y p assume asm: "x: A" "y: A" "p: x =\<^sub>A y" - show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z p. ind\<^sub>= refl p) p: \<Prod>z:A. y =[A] z \<rightarrow> x =[A] z" + fix p assume 3: "p: x =\<^sub>A y" + show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z" proof (rule Equal_elim[where ?x=x and ?y=y]) - show "\<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> \<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z: U(i)" + show "\<And>u. u: A \<Longrightarrow> \<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A z \<rightarrow> u =\<^sub>A z" proof - show "\<And>x y z. \<lbrakk>x: A; y: A; z: A\<rbrakk> \<Longrightarrow> y =\<^sub>A z \<rightarrow> x =\<^sub>A z: U(i)" - by (rule Prod_form Equal_form assms | assumption)+ - qed (rule assms) - - show "\<And>x. x: A \<Longrightarrow> \<^bold>\<lambda>z p. ind\<^sub>= refl p: \<Prod>z:A. x =\<^sub>A z \<rightarrow> x =\<^sub>A z" - proof - show "\<And>x z. \<lbrakk>x: A; z: A\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>p. ind\<^sub>= refl p: x =\<^sub>A z \<rightarrow> x =\<^sub>A z" + show "\<And>u z. \<lbrakk>u: A; z: A\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z" proof - { fix x z p assume asm: "x: A" "z: A" "p: x =\<^sub>A z" - show "ind\<^sub>= refl p: x =[A] z" - proof (rule Equal_elim[where ?x=x and ?y=z]) - show "\<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> x =\<^sub>A y: U(i)" by standard (rule assms) - show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" .. - qed (fact asm)+ } - show "\<And>x z. \<lbrakk>x: A; z: A\<rbrakk> \<Longrightarrow> x =\<^sub>A z: U(i)" by standard (rule assms) - qed + fix u z q assume asm: "u: A" "z: A" "q: u =\<^sub>A z" + show "ind\<^sub>= refl q: u =\<^sub>A z" + by (rule Equal_elim[where ?x=u and ?y=z]) (simple lem: assms asm) + qed (simple lem: assms) qed (rule assms) - qed (rule asm)+ } - show "\<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> x =\<^sub>A y: U(i)" by standard (rule assms) - qed + qed (simple lem: assms 1 2 3) + qed (simple lem: assms 1 2) qed (rule assms) -qed (fact assms) +qed fact corollary assumes "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" shows "rcompose`x`y`p`z`q: x =\<^sub>A z" - by standard+ (rule rcompose_type assms)+ + by (simple lem: assms rcompose_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 rcompose_comp: + assumes "A: U(i)" and "a: A" + shows "rcompose`a`a`refl(a)`a`refl(a) \<equiv> refl(a)" +unfolding rcompose_def +proof (subst comp) + { 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)" + proof + fix y assume 2: "y: A" + show "\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" + proof + fix p assume 3: "p: x =\<^sub>A y" + show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z" + proof (rule Equal_elim[where ?x=x and ?y=y]) + show "\<And>u. u: A \<Longrightarrow> \<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A z \<rightarrow> u =\<^sub>A z" + proof + show "\<And>u z. \<lbrakk>u: A; z: A\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z" + proof + fix u z assume asm: "u: A" "z: A" + show "\<And>q. q: u =\<^sub>A z \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z" + by (rule Equal_elim[where ?x=u and ?y=z]) (simple lem: assms asm) + qed (simple lem: assms) + qed (rule assms) + qed (simple lem: assms 1 2 3) + qed (simple lem: assms 1 2) + qed (rule assms) } + + show "(\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p)`a`refl(a)`a`refl(a) \<equiv> refl(a)" + proof (subst comp) + { fix y assume 1: "y: A" + show "\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: a =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> a =\<^sub>A z)" + proof + fix p assume 2: "p: a =\<^sub>A y" + show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>z:A. y =\<^sub>A z \<rightarrow> a =\<^sub>A z" + proof (rule Equal_elim[where ?x=a and ?y=y]) + fix u assume 3: "u: A" + show "\<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =[A] z \<rightarrow> u =[A] z" + proof + fix z assume 4: "z: A" + show "\<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z" + proof + show "\<And>q. q: u =\<^sub>A z \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z" + by (rule Equal_elim[where ?x=u and ?y=z]) (simple lem: assms 3 4) + qed (simple lem: assms 3 4) + qed fact + qed (simple lem: assms 1 2) + qed (simple lem: assms 1) } + + show "(\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z. \<^bold>\<lambda>q. ind\<^sub>= refl q) p)`refl(a)`a`refl(a) \<equiv> refl(a)" + proof (subst comp) + { fix p assume 1: "p: a =\<^sub>A a" + show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z. \<^bold>\<lambda>q. ind\<^sub>= refl q) p: \<Prod>z:A. a =\<^sub>A a \<rightarrow> a =\<^sub>A z" + proof (rule Equal_elim[where ?x=a and ?y=a]) + fix u assume 2: "u: A" + show "\<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A u\<rightarrow> u =\<^sub>A z" + proof + fix z assume 3: "z: A" + show "\<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A u \<rightarrow> u =\<^sub>A z" + proof + show "\<And>q. q: u =\<^sub>A u \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z" + by (rule Equal_elim[where ?x=u and ?y=z]) (simple lem: assms 2 3) + qed (simple lem: assms 2) + qed fact + qed (simple lem: assms 1) } + + show "(ind\<^sub>=(\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q)(refl(a)))`a`refl(a) \<equiv> refl(a)" + proof (subst comp) + { fix u assume 1: "u: A" + show "\<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A u\<rightarrow> u =\<^sub>A z" + proof + fix z assume 2: "z: A" + show "\<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A u \<rightarrow> u =\<^sub>A z" + proof + show "\<And>q. q: u =\<^sub>A u \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z" + by (rule Equal_elim[where ?x=u and ?y=z]) (simple lem: assms 1 2) + qed (simple lem: assms 1) + qed fact } + + show "(\<^bold>\<lambda>z q. ind\<^sub>= refl q)`a`refl(a) \<equiv> refl(a)" + proof (subst comp) + { fix a assume 1: "a: A" + show "\<^bold>\<lambda>q. ind\<^sub>= refl q: a =\<^sub>A a \<rightarrow> a =\<^sub>A a" + proof + show "\<And>q. q: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= refl q: a =\<^sub>A a" + by (rule Equal_elim[where ?x=a and ?y=a]) (simple lem: assms 1) + qed (simple lem: assms 1) } + + show "(\<^bold>\<lambda>q. ind\<^sub>= refl q)`refl(a) \<equiv> refl(a)" + proof (subst comp) + show "\<And>p. p: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= refl p: a =\<^sub>A a" + by (rule Equal_elim[where ?x=a and ?y=a]) (simple lem: assms) + show "ind\<^sub>= refl (refl(a)) \<equiv> refl(a)" + proof + show "\<And>x. x: A \<Longrightarrow> refl(x): x =\<^sub>A x" .. + qed (simple lem: assms) + qed (simple lem: assms) + qed fact + qed (simple lem: assms) + qed (simple lem: assms) + qed fact +qed fact + + +text "The raw object lambda term is cumbersome to use, so we define a simpler constant instead." axiomatization compose :: "[Term, Term] \<Rightarrow> Term" (infixl "\<bullet>" 60) where - compose_comp: "\<lbrakk> + compose_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> rcompose`x`y`p`z`q" +lemma compose_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 compose_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 lem: assms rcompose_type) + lemma compose_comp: - assumes "A : U(i)" and "a : A" shows "compose[A,a,a,a]`refl(a)`refl(a) \<equiv> refl(a)" - unfolding rcompose_def - by (simplify lems: assms) + assumes "A : U(i)" and "a : A" shows "refl(a) \<bullet> refl(a) \<equiv> refl(a)" +by (subst compose_def) (simple lem: assms rcompose_comp) -lemmas EqualProps_rules [intro] = inv_type inv_comp compose_type compose_comp +lemmas EqualProps_rules [intro] = inv_type compose_type lemmas EqualProps_comps [comp] = inv_comp compose_comp |