From c530305cbcafba9f66f1a55a1b5177a62f52535c Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Wed, 5 Aug 2020 15:21:43 +0200
Subject: 1. fix intros method. 2. Couple extra lemmas; good small test cases
for normalization in typechecking/elaboration.
---
hott/Equivalence.thy | 21 ++++++++++++++++++++-
hott/Identity.thy | 40 ++++++++++++++++++++++++++++++++++++++++
spartan/core/Spartan.thy | 3 ++-
spartan/core/context_tactical.ML | 2 +-
4 files changed, 63 insertions(+), 3 deletions(-)
diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy
index a4eea93..d85e6de 100644
--- a/hott/Equivalence.thy
+++ b/hott/Equivalence.thy
@@ -144,6 +144,8 @@ Lemma (def) commute_homotopy:
apply (transport eq: pathcomp_refl, transport eq: refl_pathcomp)
by refl
+\<comment> \<open>TODO: *Really* need normalization during type-checking and better equality
+ type rewriting to do the proof below properly\<close>
Corollary (def) commute_homotopy':
assumes
"A: U i"
@@ -151,7 +153,24 @@ Corollary (def) commute_homotopy':
"f: A \<rightarrow> A"
"H: f ~ (id A)"
shows "H (f x) = f [H x]"
-oops
+ proof -
+ from \<open>H: f ~ id A\<close> have "H: \<Prod>x: A. f x = x"
+ by (reduce add: homotopy_def)
+
+ have "(id A)[H x]: f x = x"
+ by (rewrite at "\<hole> = _" id_comp[symmetric],
+ rewrite at "_ = \<hole>" id_comp[symmetric])
+
+ have "H (f x) \<bullet> H x = H (f x) \<bullet> (id A)[H x]"
+ by (rule left_whisker) (fact, rule
+ ap_id[where ?A=A and ?x="f x" and ?y=x, simplified id_comp, symmetric])
+ also have [simplified id_comp]: "H (f x) \<bullet> (id A)[H x] = f[H x] \<bullet> H x"
+ by (rule commute_homotopy)
+ finally have *: "{}" by this
+
+ show "H (f x) = f [H x]"
+ by pathcomp_cancelr (fact, typechk+)
+ qed
section \<open>Quasi-inverse and bi-invertibility\<close>
diff --git a/hott/Identity.thy b/hott/Identity.thy
index b06604f..4829b6f 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -292,6 +292,46 @@ Lemma apply_transport:
method transport uses eq = (rule apply_transport[OF _ _ _ _ eq])
+Lemma (def) pathcomp_cancel_left:
+ assumes
+ "A: U i" "x: A" "y: A" "z: A"
+ "p: x = y" "q: y = z" "r: y = z"
+ "\<alpha>: p \<bullet> q = p \<bullet> r"
+ shows "q = r"
+ proof -
+ have "q = (p\<inverse> \<bullet> p) \<bullet> q"
+ by (transport eq: inv_pathcomp, transport eq: refl_pathcomp) refl
+ also have ".. = p\<inverse> \<bullet> (p \<bullet> r)"
+ by (transport eq: pathcomp_assoc[symmetric], transport eq: \<open>\<alpha>:_\<close>) refl
+ also have ".. = r" thm inv_pathcomp
+ by (transport eq: pathcomp_assoc,
+ transport eq: inv_pathcomp,
+ transport eq: refl_pathcomp) refl
+ finally show "{}" by this
+ qed
+
+Lemma (def) pathcomp_cancel_right:
+ assumes
+ "A: U i" "x: A" "y: A" "z: A"
+ "p: x = y" "q: x = y" "r: y = z"
+ "\<alpha>: p \<bullet> r = q \<bullet> r"
+ shows "p = q"
+ proof -
+ have "p = p \<bullet> r \<bullet> r\<inverse>"
+ by (transport eq: pathcomp_assoc[symmetric],
+ transport eq: pathcomp_inv,
+ transport eq: pathcomp_refl) refl
+ also have ".. = q"
+ by (transport eq: \<open>\<alpha>:_\<close>,
+ transport eq: pathcomp_assoc[symmetric],
+ transport eq: pathcomp_inv,
+ transport eq: pathcomp_refl) refl
+ finally show "{}" by this
+ qed
+
+method pathcomp_cancell = rule pathcomp_cancel_left[rotated 7]
+method pathcomp_cancelr = rule pathcomp_cancel_right[rotated 7]
+
Lemma (def) transport_left_inv:
assumes
"A: U i"
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index ea72208..7f13036 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -248,7 +248,8 @@ method_setup intros =
K (CONTEXT_METHOD (fn facts =>
case n_opt of
SOME n => CREPEAT_N n (CHEADGOAL (SIDE_CONDS 0 intro_ctac facts))
- | NONE => CREPEAT (CCHANGED (CHEADGOAL (SIDE_CONDS 0 intro_ctac facts))))))\<close>
+ | NONE => CCHANGED (CREPEAT (CCHANGED (
+ CHEADGOAL (SIDE_CONDS 0 intro_ctac facts)))))))\<close>
method_setup elim =
\<open>Scan.repeat Args.term >> (fn tms => K (CONTEXT_METHOD (
diff --git a/spartan/core/context_tactical.ML b/spartan/core/context_tactical.ML
index 0aa6f20..d0fed61 100644
--- a/spartan/core/context_tactical.ML
+++ b/spartan/core/context_tactical.ML
@@ -92,7 +92,7 @@ fun CREPEAT ctac =
fun CREPEAT1 ctac = ctac CTHEN CREPEAT ctac
-fun CREPEAT_N 0 _ = all_ctac
+fun CREPEAT_N 0 _ = no_ctac
| CREPEAT_N n ctac = ctac CTHEN CREPEAT_N (n - 1) ctac
fun CFILTER pred ctac cst =
--
cgit v1.2.3