From b0ba102b783418560f9b7b15239681b11ea4c877 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 26 May 2020 16:50:35 +0200 Subject: new material --- hott/Eckmann_Hilton.thy | 21 +++++++++++++++++++++ hott/Equivalence.thy | 15 ++++++++------- hott/Identity.thy | 28 +++++----------------------- hott/More_List.thy | 22 +++++++++++++++++++++- hott/Nat.thy | 6 +++--- 5 files changed, 58 insertions(+), 34 deletions(-) create mode 100644 hott/Eckmann_Hilton.thy (limited to 'hott') 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 "\p: a = b; q: a = b; r: b = c; \: p =\<^bsub>a = b\<^esub> q\ \ p \ r = q \ r" + apply (eq r) + focus prems prms vars x s t \ + proof - + have "t \ refl x = t" by (rule pathcomp_refl) + also have ".. = s" by (rule \\:_\) + also have ".. = s \ refl x" by (rule pathcomp_refl[symmetric]) + finally show "t \ refl x = s \ 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 \For calculations:\ +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: \ \Here it would really be nice to have automation for transport and propositional equality.\ apply (rule use_transport[where ?y="H x \ refl (g x)"]) - \ by (rule pathcomp_right_refl) - \ by (rule pathinv) (rule pathcomp_left_refl) + \ by (rule pathcomp_refl) + \ by (rule pathinv) (rule refl_pathcomp) \ by typechk done done @@ -256,12 +258,12 @@ Lemma (derive) biinv_imp_qinv: \ proof - have "g ~ g \ (id B)" by reduce refl - also have "g \ (id B) ~ g \ f \ h" + also have ".. ~ g \ f \ h" by (rule homotopy_funcomp_right) (rule \H2:_\[symmetric]) - also have "g \ f \ h ~ (id A) \ h" + also have ".. ~ (id A) \ h" by (subst funcomp_assoc[symmetric]) (rule homotopy_funcomp_left, rule \H1:_\) - also have "(id A) \ h ~ h" by reduce refl + also have ".. ~ h" by reduce refl finally have "g ~ h" by this then have "f \ g ~ f \ h" by (rule homotopy_funcomp_right) @@ -348,8 +350,7 @@ text \ \ 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 \ 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 \Calculational reasoning\ -consts rhs :: \'a\ ("''''") - -ML \ -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>\has_type\ $ _ $ (\<^const>\Id\ $ _ $ _ $ y)] => y - | _ => Term.dummy - in - map_aterms (fn t => case t of Const (\<^const_name>\rhs\, _) => rhs | _ => t) - end -in val _ = Context.>> - (Syntax_Phases.term_check 5 "" (fn ctxt => map (last_rhs ctxt))) -end -\ +congruence "x = y" rhs y lemmas [sym] = pathinv[rotated 3] and @@ -147,28 +129,28 @@ lemmas section \Basic propositional equalities\ -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) \ 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 \ (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\ \ 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 \ p\ = 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 (\n: Nat. suc n) [0, suc (suc 0), suc 0] \ ?xs" + unfolding map_def by (subst comps)+ +end + +section \Length\ + +definition [implicit]: + "len \ ListRec ? Nat 0 (\_ _ n. suc n)" + +experiment begin + Lemma "len [] \ 0" by reduce + Lemma "len [0, suc 0, suc (suc 0)] \ ?n" by (subst comps)+ +end + +section \Equality on lists\ + +(*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 \Non-dependent recursion\ -abbreviation "NatRec C \ NatInd (K C)" +abbreviation "NatRec C \ NatInd (\_. C)" section \Basic arithmetic\ @@ -100,10 +100,10 @@ Lemma (derive) add_comm: shows "m + n = n + m" apply (elim m) \ by (reduce; rule add_zero[symmetric]) - \ prems prms vars m ih + \ 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 -- cgit v1.2.3