aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--hott/Equivalence.thy24
-rw-r--r--hott/Identity.thy17
-rw-r--r--spartan/core/Spartan.thy18
-rw-r--r--spartan/core/implicits.ML21
4 files changed, 45 insertions, 35 deletions
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)
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index a4ad300..fa6148f 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -52,7 +52,7 @@ paragraph \<open>
typedecl o
-judgment has_type :: \<open>o \<Rightarrow> o \<Rightarrow> prop\<close> ("(2_:/ _)" 999)
+consts has_type :: \<open>o \<Rightarrow> o \<Rightarrow> prop\<close> ("(2_:/ _)" 999)
text \<open>Type annotations for type-checking and inference.\<close>
@@ -232,6 +232,10 @@ method_setup rule =
\<open>Attrib.thms >> (fn ths => K (CONTEXT_METHOD (
CHEADGOAL o SIDE_CONDS (rule_ctac ths))))\<close>
+method_setup rules =
+ \<open>Attrib.thms >> (fn ths => K (CONTEXT_METHOD (
+ CREPEAT o CHEADGOAL o SIDE_CONDS (rule_ctac ths))))\<close>
+
method_setup dest =
\<open>Scan.lift (Scan.option (Args.parens Parse.int))
-- Attrib.thms >> (fn (n_opt, ths) => K (CONTEXT_METHOD (
@@ -255,6 +259,8 @@ method_setup cases =
\<open>Args.term >> (fn tm => K (CONTEXT_METHOD (
CHEADGOAL o SIDE_CONDS (cases_ctac tm))))\<close>
+method facts = fact+
+
subsection \<open>Reflexivity\<close>
@@ -310,7 +316,8 @@ setup \<open>map_theory_simpset (fn ctxt =>
ctxt addSolver (mk_solver "" (fn ctxt' =>
NO_CONTEXT_TACTIC ctxt' o Types.check_infer (Simplifier.prems_of ctxt'))))\<close>
-method reduce uses add = changed \<open>((simp add: comp add | sub comp); typechk?)+\<close>
+method reduce uses add =
+ changed \<open>repeat_new \<open>(simp add: comp add | sub comp); typechk?\<close>\<close>
subsection \<open>Implicits\<close>
@@ -327,10 +334,7 @@ ML_file \<open>implicits.ML\<close>
attribute_setup implicit = \<open>Scan.succeed Implicits.implicit_defs_attr\<close>
-ML \<open>
-val _ = Context.>>
- (Syntax_Phases.term_check 1 "" (fn ctxt => map (Implicits.make_holes ctxt)))
-\<close>
+ML \<open>val _ = Context.>> (Syntax_Phases.term_check 1 "" Implicits.make_holes)\<close>
text \<open>Automatically insert inhabitation judgments where needed:\<close>
@@ -488,7 +492,7 @@ lemma snd_type [typechk]:
lemma snd_comp [comp]:
assumes "a: A" "b: B a" "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
shows "snd A B <a, b> \<equiv> b"
- unfolding snd_def by reduce+
+ unfolding snd_def by reduce
subsection \<open>Notation\<close>
diff --git a/spartan/core/implicits.ML b/spartan/core/implicits.ML
index 4d73c8d..ab64b0f 100644
--- a/spartan/core/implicits.ML
+++ b/spartan/core/implicits.ML
@@ -3,7 +3,7 @@ sig
val implicit_defs: Proof.context -> (term * term) Symtab.table
val implicit_defs_attr: attribute
-val make_holes: Proof.context -> term -> term
+val make_holes: Proof.context -> term list -> term list
end = struct
@@ -25,16 +25,15 @@ val implicit_defs_attr = Thm.declaration_attribute (fn th =>
Defs.map (Symtab.update (Term.term_name head, (head, def')))
end)
-fun make_holes ctxt =
+fun make_holes_single ctxt tm name_ctxt =
let
fun iarg_to_hole (Const (\<^const_name>\<open>iarg\<close>, T)) =
Const (\<^const_name>\<open>hole\<close>, T)
| iarg_to_hole t = t
fun expand head args =
- let
- fun betapplys (head', args') =
- Term.betapplys (map_aterms iarg_to_hole head', args')
+ let fun betapplys (head', args') =
+ Term.betapplys (map_aterms iarg_to_hole head', args')
in
case head of
Abs (x, T, t) =>
@@ -66,13 +65,17 @@ fun make_holes ctxt =
in subst t (take n vs) Ts $ subst u (drop n vs) Ts end
| subst t _ _ = t
- val vars = map (fn n => Var ((n, 0), dummyT))
- (Name.invent (Variable.names_of ctxt) "*" (count t))
+ val names = Name.invent name_ctxt "*" (count t)
+ val vars = map (fn n => Var ((n, 0), dummyT)) names
in
- subst t vars []
+ (subst t vars [], fold Name.declare names name_ctxt)
end
in
- Lib.traverse_term expand #> holes_to_vars
+ holes_to_vars (Lib.traverse_term expand tm)
end
+fun make_holes ctxt tms = #1
+ (fold_map (make_holes_single ctxt) tms (Variable.names_of ctxt))
+
+
end
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 10:36:26 +0000