aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--hott/Nat.thy51
-rw-r--r--spartan/lib/elimination.ML5
-rw-r--r--spartan/lib/focus.ML2
-rw-r--r--spartan/lib/tactics.ML3
-rw-r--r--spartan/theories/Equivalence.thy8
-rw-r--r--spartan/theories/Identity.thy13
-rw-r--r--spartan/theories/Spartan.thy7
7 files changed, 68 insertions, 21 deletions
diff --git a/hott/Nat.thy b/hott/Nat.thy
index 59ec517..3d938cd 100644
--- a/hott/Nat.thy
+++ b/hott/Nat.thy
@@ -49,10 +49,53 @@ abbreviation "NatRec C \<equiv> NatInd (K C)"
section \<open>Basic arithmetic\<close>
-definition add (infixl "+" 50) where
- [comps]: "m + n \<equiv> NatRec Nat n (K suc) m"
-
-definition mul (infixl "*" 55) where
+definition add (infixl "+" 120) where "m + n \<equiv> NatRec Nat n (K suc) m"
+
+lemma add_type [typechk]:
+ assumes "m: Nat" "n: Nat"
+ shows "m + n: Nat"
+ unfolding add_def by typechk
+
+lemma add_rec [comps]:
+ assumes "m: Nat" "n: Nat"
+ shows "suc m + n \<equiv> suc (m + n)"
+ unfolding add_def by reduce
+
+lemma zero_add [comps]:
+ assumes "n: Nat"
+ shows "0 + n \<equiv> n"
+ unfolding add_def by reduce
+
+Lemma (derive) add_zero:
+ assumes "n: Nat"
+ shows "n + 0 = n"
+ apply (elim n)
+ \<guillemotright> by (reduce; intro)
+ \<guillemotright> vars _ IH by reduce (elim IH; intro)
+ done
+
+Lemma (derive) add_assoc:
+ assumes "l: Nat" "m: Nat" "n: Nat"
+ shows "l + (m + n) = (l + m) + n"
+ apply (elim l)
+ \<guillemotright> by reduce intro
+ \<guillemotright> vars _ IH by reduce (elim IH; intro)
+ done
+
+Lemma (derive) add_comm:
+ assumes "m: Nat" "n: Nat"
+ shows "m + n = n + m"
+ apply (elim m)
+ \<guillemotright> by (reduce; rule add_zero[sym])
+ \<guillemotright> vars m p
+ apply (elim n)
+ (*Should also change the `n`s in the premises!*)
+ (*FIXME: Elimination tactic needs to do the same kind of thing as the
+ equality tactic with pushing context premises into the statement, applying
+ the appropriate elimination rule and then pulling back out.*)
+oops
+
+definition mul (infixl "*" 120) where
[comps]: "m * n \<equiv> NatRec Nat 0 (K $ add n) m"
diff --git a/spartan/lib/elimination.ML b/spartan/lib/elimination.ML
index 85ce669..bd23c94 100644
--- a/spartan/lib/elimination.ML
+++ b/spartan/lib/elimination.ML
@@ -6,6 +6,7 @@ Type elimination automation.
structure Elim = struct
+(** Context data **)
(* Elimination rule data *)
structure Rules = Generic_Data (
type T = thm Termtab.table
@@ -30,4 +31,8 @@ val _ = Theory.setup (
fn context => (rules (Context.proof_of context)))
)
+(** General elimination-induction tactic **)
+
+
+
end
diff --git a/spartan/lib/focus.ML b/spartan/lib/focus.ML
index dd8d3d9..1d8de78 100644
--- a/spartan/lib/focus.ML
+++ b/spartan/lib/focus.ML
@@ -105,7 +105,7 @@ val schematic_subgoal_cmd = gen_schematic_subgoal Attrib.attribute_cmd
val parser =
opt_fact_binding
- -- (Scan.option (\<^keyword>\<open>premises\<close> |-- Parse.!!! opt_fact_binding))
+ -- (Scan.option (\<^keyword>\<open>prems\<close> |-- Parse.!!! opt_fact_binding))
-- for_params >> (fn ((a, b), c) =>
Toplevel.proofs (Seq.make_results o Seq.single o #2 o schematic_subgoal_cmd a b c))
diff --git a/spartan/lib/tactics.ML b/spartan/lib/tactics.ML
index 0e09533..c72947a 100644
--- a/spartan/lib/tactics.ML
+++ b/spartan/lib/tactics.ML
@@ -104,8 +104,7 @@ fun intro_tac ctxt = SUBGOAL (fn (_, i) => SIDE_CONDS
fun intros_tac ctxt = SUBGOAL (fn (_, i) =>
(CHANGED o REPEAT o CHANGED o intro_tac ctxt) i)
-(* Basic elimination tactic *)
-(*Only uses existing type judgments from the context
+(*Basic elimination tactic, only uses existing type judgments from the context
(performs no type synthesis)*)
fun elims_tac opt_tm ctxt = case opt_tm of
NONE => SUBGOAL (fn (_, i) => eresolve_tac ctxt (Elim.rules ctxt) i)
diff --git a/spartan/theories/Equivalence.thy b/spartan/theories/Equivalence.thy
index 44b77dd..97cd18d 100644
--- a/spartan/theories/Equivalence.thy
+++ b/spartan/theories/Equivalence.thy
@@ -197,7 +197,7 @@ Lemma (derive) funcomp_qinv:
shows "qinv f \<rightarrow> qinv g \<rightarrow> qinv (g \<circ> f)"
apply (intros, unfold qinv_def, elims)
focus
- premises hyps
+ prems prms
vars _ _ finv _ ginv _ HfA HfB HgB HgC
apply intro
@@ -246,7 +246,7 @@ Lemma (derive) biinv_imp_qinv:
apply elims
text \<open>Name the components:\<close>
- focus premises vars _ _ _ g H1 h H2
+ focus prems vars _ _ _ g H1 h H2
thm \<open>g:_\<close> \<open>h:_\<close> \<open>H1:_\<close> \<open>H2:_\<close>
text \<open>
@@ -384,14 +384,14 @@ Lemma (derive) id_imp_equiv:
supply [[auto_typechk=false]]
\<guillemotright> apply (equality \<open>p:_\<close>)
- \<^item> premises vars A B
+ \<^item> prems vars A B
apply (rewrite at A in "A \<rightarrow> B" id_comp[symmetric])
apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric])
apply (rule transport, rule U_in_U)
apply (rule lift_universe_codomain, rule U_in_U)
apply (typechk, rule U_in_U)
done
- \<^item> premises vars A
+ \<^item> prems vars A
apply (subst transport_comp)
\<^enum> by (rule U_in_U)
\<^enum> by reduce (rule lift_universe)
diff --git a/spartan/theories/Identity.thy b/spartan/theories/Identity.thy
index 19b8b7a..4a4cc40 100644
--- a/spartan/theories/Identity.thy
+++ b/spartan/theories/Identity.thy
@@ -15,7 +15,7 @@ axiomatization
refl :: \<open>o \<Rightarrow> o\<close> and
IdInd :: \<open>o \<Rightarrow> (o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o) \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close>
-syntax "_Id" :: \<open>o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> ("(2_ =\<^bsub>_\<^esub>/ _)" [111, 0, 111] 110)
+syntax "_Id" :: \<open>o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> ("(2_ =\<^bsub>_\<^esub>/ _)" [111, 0, 111] 110)
translations "a =\<^bsub>A\<^esub> b" \<rightleftharpoons> "CONST Id A a b"
@@ -71,7 +71,7 @@ Lemma (derive) pathcomp:
shows
"x =\<^bsub>A\<^esub> z"
apply (equality \<open>p:_\<close>)
- focus premises vars x p
+ focus prems vars x p
apply (equality \<open>p:_\<close>)
apply intro
done
@@ -158,9 +158,9 @@ Lemma (derive) pathcomp_assoc:
"p: x =\<^bsub>A\<^esub> y" "q: y =\<^bsub>A\<^esub> z" "r: z =\<^bsub>A\<^esub> w"
shows "p \<bullet> (q \<bullet> r) = p \<bullet> q \<bullet> r"
apply (equality \<open>p:_\<close>)
- focus premises vars x p
+ focus prems vars x p
apply (equality \<open>p:_\<close>)
- focus premises vars x p
+ focus prems vars x p
apply (equality \<open>p:_\<close>)
apply (reduce; intros)
done
@@ -200,7 +200,7 @@ Lemma (derive) ap_pathcomp:
shows
"f[p \<bullet> q] = f[p] \<bullet> f[q]"
apply (equality \<open>p:_\<close>)
- focus premises vars x p
+ focus prems vars x p
apply (equality \<open>p:_\<close>)
apply (reduce; intro)
done
@@ -302,7 +302,7 @@ Lemma (derive) transport_pathcomp:
"p: x =\<^bsub>A\<^esub> y" "q: y =\<^bsub>A\<^esub> z"
shows "trans P q (trans P p u) = trans P (p \<bullet> q) u"
apply (equality \<open>p:_\<close>)
- focus premises vars x p
+ focus prems vars x p
apply (equality \<open>p:_\<close>)
apply (reduce; intros)
done
@@ -430,4 +430,5 @@ Lemma (derive) apd_ap:
shows "apd f p = trans_const B p (f x) \<bullet> f[p]"
by (equality \<open>p:_\<close>) (reduce; intro)
+
end
diff --git a/spartan/theories/Spartan.thy b/spartan/theories/Spartan.thy
index a79f209..5274ea2 100644
--- a/spartan/theories/Spartan.thy
+++ b/spartan/theories/Spartan.thy
@@ -8,7 +8,7 @@ imports
keywords
"Theorem" "Lemma" "Corollary" "Proposition" :: thy_goal_stmt and
"focus" "\<guillemotright>" "\<^item>" "\<^enum>" "~" :: prf_script_goal % "proof" and
- "derive" "vars":: quasi_command and
+ "derive" "prems" "vars":: quasi_command and
"print_coercions" :: thy_decl
begin
@@ -138,9 +138,6 @@ axiomatization where
\<rbrakk> \<Longrightarrow> \<Sum>x: A. B x \<equiv> \<Sum>x: A. B' x"
-
-
-
section \<open>Proof commands\<close>
named_theorems typechk
@@ -152,6 +149,7 @@ ML_file \<open>../lib/focus.ML\<close>
section \<open>Congruence automation\<close>
+(*Work in progress*)
ML_file \<open>../lib/congruence.ML\<close>
@@ -188,6 +186,7 @@ method_setup elim =
method elims = elim+
+(*This could possibly use additional simplification hints via a simp: modifier*)
method_setup typechk =
\<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (
CHANGED (ALLGOALS (TRY o typechk_tac ctxt))))\<close>
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-26 18:57:05 +0000