From 306721649f0963ab225deb8d5670cfe196bb360d Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 21 Jul 2020 16:28:05 +0200
Subject: 1. Bugfix: implicits now properly name schematic variables. Fixes
 problems caused by variable name clashes. 2. reduce method now more
 principled: restricts to repeating on first subgoal. 3. An example
 declarative proof in Equivalence.thy.

---
 hott/Equivalence.thy | 24 ++++++++++++------------
 hott/Identity.thy    | 17 ++++++++++-------
 2 files changed, 22 insertions(+), 19 deletions(-)

(limited to 'hott')

diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy
index 88adc8b..d976677 100644
--- a/hott/Equivalence.thy
+++ b/hott/Equivalence.thy
@@ -338,18 +338,18 @@ Lemma (derive) equivalence_symmetric:
 Lemma (derive) equivalence_transitive:
   assumes "A: U i" "B: U i" "C: U i"
   shows "A \<simeq> B \<rightarrow> B \<simeq> C \<rightarrow> A \<simeq> C"
-  (* proof intros
-    fix AB BC assume "AB: A \<simeq> B" "BC: B \<simeq> C"
-    let "?f: {}" = "(fst AB) :: o" *)
-  apply intros
-  unfolding equivalence_def
-    focus vars p q apply (elim p, elim q)
-      focus vars f biinv\<^sub>f g biinv\<^sub>g apply intro
-        \<guillemotright> apply (rule funcompI) defer by assumption+ known
-        \<guillemotright> by (rule funcomp_biinv)
-      done
-    done
-  done
+  proof intros
+    fix AB BC assume *: "AB: A \<simeq> B" "BC: B \<simeq> C"
+    then have
+      "fst AB: A \<rightarrow> B" and 1: "snd AB: biinv (fst AB)"
+      "fst BC: B \<rightarrow> C" and 2: "snd BC: biinv (fst BC)"
+      unfolding equivalence_def by typechk+
+    then have "fst BC \<circ> fst AB: A \<rightarrow> C" by typechk
+    moreover have "biinv (fst BC \<circ> fst AB)"
+      using * unfolding equivalence_def by (rules funcomp_biinv 1 2)
+    ultimately show "A \<simeq> C"
+      unfolding equivalence_def by intro facts
+  qed
 
 text \<open>
   Equal types are equivalent. We give two proofs: the first by induction, and
diff --git a/hott/Identity.thy b/hott/Identity.thy
index 1cb3946..29ce26a 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -49,6 +49,9 @@ lemmas
 
 section \<open>Path induction\<close>
 
+\<comment> \<open>With `p: x = y` in the context the invokation `eq p` is essentially
+  `elim p x y`, with some extra bits before and after.\<close>
+
 method_setup eq =
   \<open>Args.term >> (fn tm => K (CONTEXT_METHOD (
     CHEADGOAL o SIDE_CONDS (
@@ -155,12 +158,12 @@ translations
 Lemma lu_refl [comp]:
   assumes "A: U i" "x: A"
   shows "lu (refl x) \<equiv> refl (refl x)"
-  unfolding refl_pathcomp_def by reduce+
+  unfolding refl_pathcomp_def by reduce
 
 Lemma ru_refl [comp]:
   assumes "A: U i" "x: A"
   shows "ru (refl x) \<equiv> refl (refl x)"
-  unfolding pathcomp_refl_def by reduce+
+  unfolding pathcomp_refl_def by reduce
 
 Lemma (derive) inv_pathcomp:
   assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y"
@@ -374,7 +377,7 @@ Lemma transport_const_comp [comp]:
     "x: A" "b: B"
     "A: U i" "B: U i"
   shows "trans_const B (refl x) b\<equiv> refl b"
-  unfolding transport_const_def by reduce+
+  unfolding transport_const_def by reduce
 
 Lemma (derive) pathlift:
   assumes
@@ -398,7 +401,7 @@ Lemma pathlift_comp [comp]:
     "\<And>x. x: A \<Longrightarrow> P x: U i"
     "A: U i"
   shows "lift P (refl x) u \<equiv> refl <x, u>"
-  unfolding pathlift_def by reduce+
+  unfolding pathlift_def by reduce
 
 Lemma (derive) pathlift_fst:
   assumes
@@ -438,7 +441,7 @@ Lemma dependent_map_comp [comp]:
     "A: U i"
     "\<And>x. x: A \<Longrightarrow> P x: U i"
   shows "apd f (refl x) \<equiv> refl (f x)"
-  unfolding apd_def by reduce+
+  unfolding apd_def by reduce
 
 Lemma (derive) apd_ap:
   assumes
@@ -495,13 +498,13 @@ Lemma whisker_refl [comp]:
   assumes "A: U i" "a: A" "b: A"
   shows "\<lbrakk>p: a = b; q: a = b; \<alpha>: p =\<^bsub>a = b\<^esub> q\<rbrakk> \<Longrightarrow>
     \<alpha> \<bullet>\<^sub>r\<^bsub>a\<^esub> (refl b) \<equiv> ru p \<bullet> \<alpha> \<bullet> (ru q)\<inverse>"
-  unfolding right_whisker_def by reduce+
+  unfolding right_whisker_def by reduce
 
 Lemma refl_whisker [comp]:
   assumes "A: U i" "a: A" "b: A"
   shows "\<lbrakk>p: a = b; q: a = b; \<alpha>: p = q\<rbrakk> \<Longrightarrow>
     (refl a) \<bullet>\<^sub>l\<^bsub>b\<^esub> \<alpha> \<equiv> (lu p) \<bullet> \<alpha> \<bullet> (lu q)\<inverse>"
-  unfolding left_whisker_def by reduce+
+  unfolding left_whisker_def by reduce
 
 method left_whisker = (rule left_whisker)
 method right_whisker = (rule right_whisker)
-- 
cgit v1.2.3