diff options
| -rw-r--r-- | hott/Eckmann_Hilton.thy | 21 | ||||
| -rw-r--r-- | hott/Equivalence.thy | 15 | ||||
| -rw-r--r-- | hott/Identity.thy | 28 | ||||
| -rw-r--r-- | hott/More_List.thy | 22 | ||||
| -rw-r--r-- | hott/Nat.thy | 6 |
5 files changed, 58 insertions, 34 deletions
diff --git a/hott/Eckmann_Hilton.thy b/hott/Eckmann_Hilton.thy new file mode 100644 index 0000000..7355fde --- /dev/null +++ b/hott/Eckmann_Hilton.thy @@ -0,0 +1,21 @@ +theory Eckmann_Hilton +imports Identity + +begin + +Lemma (derive) left_whisker: + assumes "A: U i" "a: A" "b: A" "c: A" + shows "\<lbrakk>p: a = b; q: a = b; r: b = c; \<alpha>: p =\<^bsub>a = b\<^esub> q\<rbrakk> \<Longrightarrow> p \<bullet> r = q \<bullet> r" + apply (eq r) + focus prems prms vars x s t \<gamma> + proof - + have "t \<bullet> refl x = t" by (rule pathcomp_refl) + also have ".. = s" by (rule \<open>\<gamma>:_\<close>) + also have ".. = s \<bullet> refl x" by (rule pathcomp_refl[symmetric]) + finally show "t \<bullet> refl x = s \<bullet> refl x" by this + qed + done + + + +end diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy index 2975738..9e7b83a 100644 --- a/hott/Equivalence.thy +++ b/hott/Equivalence.thy @@ -61,6 +61,8 @@ Lemma (derive) htrans: text \<open>For calculations:\<close> +congruence "f ~ g" rhs g + lemmas homotopy_sym [sym] = hsym[rotated 4] and homotopy_trans [trans] = htrans[rotated 5] @@ -81,8 +83,8 @@ Lemma (derive) commute_homotopy: \<comment> \<open>Here it would really be nice to have automation for transport and propositional equality.\<close> apply (rule use_transport[where ?y="H x \<bullet> refl (g x)"]) - \<guillemotright> by (rule pathcomp_right_refl) - \<guillemotright> by (rule pathinv) (rule pathcomp_left_refl) + \<guillemotright> by (rule pathcomp_refl) + \<guillemotright> by (rule pathinv) (rule refl_pathcomp) \<guillemotright> by typechk done done @@ -256,12 +258,12 @@ Lemma (derive) biinv_imp_qinv: \<close> proof - have "g ~ g \<circ> (id B)" by reduce refl - also have "g \<circ> (id B) ~ g \<circ> f \<circ> h" + also have ".. ~ g \<circ> f \<circ> h" by (rule homotopy_funcomp_right) (rule \<open>H2:_\<close>[symmetric]) - also have "g \<circ> f \<circ> h ~ (id A) \<circ> h" + also have ".. ~ (id A) \<circ> h" by (subst funcomp_assoc[symmetric]) (rule homotopy_funcomp_left, rule \<open>H1:_\<close>) - also have "(id A) \<circ> h ~ h" by reduce refl + also have ".. ~ h" by reduce refl finally have "g ~ h" by this then have "f \<circ> g ~ f \<circ> h" by (rule homotopy_funcomp_right) @@ -348,8 +350,7 @@ text \<open> \<close> Lemma - assumes - "A: U i" "B: U i" "p: A =\<^bsub>U i\<^esub> B" + assumes "A: U i" "B: U i" "p: A =\<^bsub>U i\<^esub> B" shows "A \<simeq> B" by (eq p) (rule equivalence_refl) diff --git a/hott/Identity.thy b/hott/Identity.thy index 3fef536..d60f4c2 100644 --- a/hott/Identity.thy +++ b/hott/Identity.thy @@ -120,25 +120,7 @@ translations section \<open>Calculational reasoning\<close> -consts rhs :: \<open>'a\<close> ("''''") - -ML \<open> -local fun last_rhs ctxt = - let - val this_name = Name_Space.full_name (Proof_Context.naming_of ctxt) - (Binding.name Auto_Bind.thisN) - val this = #thms (the (Proof_Context.lookup_fact ctxt this_name)) - handle Option => [] - val rhs = case map Thm.prop_of this of - [\<^const>\<open>has_type\<close> $ _ $ (\<^const>\<open>Id\<close> $ _ $ _ $ y)] => y - | _ => Term.dummy - in - map_aterms (fn t => case t of Const (\<^const_name>\<open>rhs\<close>, _) => rhs | _ => t) - end -in val _ = Context.>> - (Syntax_Phases.term_check 5 "" (fn ctxt => map (last_rhs ctxt))) -end -\<close> +congruence "x = y" rhs y lemmas [sym] = pathinv[rotated 3] and @@ -147,28 +129,28 @@ lemmas section \<open>Basic propositional equalities\<close> -Lemma (derive) pathcomp_left_refl: +Lemma (derive) refl_pathcomp: assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y" shows "(refl x) \<bullet> p = p" apply (eq p) apply (reduce; intros) done -Lemma (derive) pathcomp_right_refl: +Lemma (derive) pathcomp_refl: assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y" shows "p \<bullet> (refl y) = p" apply (eq p) apply (reduce; intros) done -Lemma (derive) pathcomp_left_inv: +Lemma (derive) inv_pathcomp: assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y" shows "p\<inverse> \<bullet> p = refl y" apply (eq p) apply (reduce; intros) done -Lemma (derive) pathcomp_right_inv: +Lemma (derive) pathcomp_inv: assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y" shows "p \<bullet> p\<inverse> = refl x" apply (eq p) diff --git a/hott/More_List.thy b/hott/More_List.thy index 2f868b8..aa57635 100644 --- a/hott/More_List.thy +++ b/hott/More_List.thy @@ -1,8 +1,28 @@ theory More_List -imports Spartan.List +imports + Spartan.List + Nat begin +experiment begin + Lemma "map (\<lambda>n: Nat. suc n) [0, suc (suc 0), suc 0] \<equiv> ?xs" + unfolding map_def by (subst comps)+ +end + +section \<open>Length\<close> + +definition [implicit]: + "len \<equiv> ListRec ? Nat 0 (\<lambda>_ _ n. suc n)" + +experiment begin + Lemma "len [] \<equiv> 0" by reduce + Lemma "len [0, suc 0, suc (suc 0)] \<equiv> ?n" by (subst comps)+ +end + +section \<open>Equality on lists\<close> + +(*Hmmm.*) end diff --git a/hott/Nat.thy b/hott/Nat.thy index d54ea7b..c36154e 100644 --- a/hott/Nat.thy +++ b/hott/Nat.thy @@ -44,7 +44,7 @@ lemmas text \<open>Non-dependent recursion\<close> -abbreviation "NatRec C \<equiv> NatInd (K C)" +abbreviation "NatRec C \<equiv> NatInd (\<lambda>_. C)" section \<open>Basic arithmetic\<close> @@ -100,10 +100,10 @@ Lemma (derive) add_comm: shows "m + n = n + m" apply (elim m) \<guillemotright> by (reduce; rule add_zero[symmetric]) - \<guillemotright> prems prms vars m ih + \<guillemotright> prems vars m ih proof reduce have "suc (m + n) = suc (n + m)" by (eq ih) intro - also have "'' = n + suc m" by (rule add_suc[symmetric]) + also have ".. = n + suc m" by (rule add_suc[symmetric]) finally show "suc (m + n) = n + suc m" by this qed done |