25 files changed, 66 insertions, 163 deletions
diff --git a/LICENSE b/LICENSE
index b8b61ab..2ff901d 100644
--- a/LICENSE
+++ b/LICENSE
@@ -1,15 +1,15 @@
 Isabelle/HoTT
-Copyright (c) 2018–2020 Joshua Chen
+Copyright (c) 2018–2021 Joshua Chen
 
 All files are licensed under the terms of the
 GNU Lesser General Public License v3.0 reproduced below,
 WITH THE EXCEPTION OF the following files:
-  spartan/core/context_tactical.ML
-  spartan/core/elaborated_statement.ML
-  spartan/core/eqsubst.ML
-  spartan/core/focus.ML
-  spartan/core/goals.ML
-  spartan/core/rewrite.ML
+  mltt/core/comp.ML
+  mltt/core/context_tactical.ML
+  mltt/core/elaborated_statement.ML
+  mltt/core/eqsubst.ML
+  mltt/core/focus.ML
+  mltt/core/goals.ML
 
 These have been modified from source code which is part of the official
 Isabelle distribution (https://isabelle.in.tum.de/) and licensed under the
diff --git a/ROOT b/ROOT
index 014767a..2d97bbb 100644
--- a/ROOT
+++ b/ROOT
@@ -1,16 +1,16 @@
-session Spartan_Core in "spartan/core" = Pure +
+session MLTT_Core in "mltt/core" = Pure +
   description
-    "Spartan type theory: a minimal dependent type theory based on intensional
-    Martin-Löf type theory with cumulative Russell-style universes, Pi types and
-    Sigma types."
+    "Core MLTT: minimal dependent type theory based on intensional Martin-Löf
+    type theory with cumulative Russell-style universes, Pi types and Sigma
+    types."
   sessions
     "HOL-Eisbach"
   theories
-    Spartan (global)
+    MLTT (global)
 
-session Spartan in spartan = Spartan_Core +
+session MLTT in mltt = MLTT_Core +
   description
-    "Dependent type theory based on Spartan."
+    "Dependent type theory based on MLTT_Core."
   directories
     lib
   theories
@@ -18,7 +18,7 @@ session Spartan in spartan = Spartan_Core +
     Maybe
     List
 
-session HoTT in hott = Spartan +
+session HoTT in hott = MLTT +
   description
     "Homotopy type theory, following the development in
       The Univalent Foundations Program,
diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy
index 9fe11a7..745bc67 100644
--- a/hott/Equivalence.thy
+++ b/hott/Equivalence.thy
@@ -400,8 +400,8 @@ Lemma
   by (eq p) (rule equivalence_refl)
 
 text \<open>
-  The following proof is wordy because (1) the typechecker doesn't normalize,
-  and (2) we don't yet have universe level inference.
+  The following proof is wordy because (1) typechecker normalization is still
+  rudimentary, and (2) we don't yet have universe level inference.
 \<close>
 
 Lemma (def) equiv_if_equal:
diff --git a/hott/Identity.thy b/hott/Identity.thy
index caab2e3..0531b74 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -6,7 +6,7 @@ text \<open>
 \<close>
 
 theory Identity
-imports Spartan
+imports MLTT
 
 begin
 
@@ -109,7 +109,7 @@ method pathcomp for p q :: o = rule pathcomp[where ?p=p and ?q=q]
 section \<open>Notation\<close>
 
 definition Id_i (infix "=" 110)
-  where [implicit]: "Id_i x y \<equiv> x =\<^bsub>{}\<^esub> y"
+  where [implicit]: "x = y \<equiv> x =\<^bsub>{}\<^esub> y"
 
 definition pathinv_i ("_\<inverse>" [1000])
   where [implicit]: "pathinv_i p \<equiv> pathinv {} {} {} p"
@@ -532,47 +532,40 @@ method right_whisker = (rule right_whisker)
 
 section \<open>Horizontal path-composition\<close>
 
-locale horiz_pathcomposable =
-\<comment> \<open>Conditions under which horizontal path-composition is defined.\<close>
-fixes
-  i A a b c p q r s
-assumes [type]:
-  "A: U i" "a: A" "b: A" "c: A"
-  "p: a =\<^bsub>A\<^esub> b" "q: a =\<^bsub>A\<^esub> b"
-  "r: b =\<^bsub>A\<^esub> c" "s: b =\<^bsub>A\<^esub> c"
+locale horiz_pathcomposable = \<comment> \<open>Conditions under which horizontal path-composition is defined.\<close>
+fixes i A a b c p q r s
+assumes [type]: "A: U i" "a: A" "b: A" "c: A"
+                "p: a =\<^bsub>A\<^esub> b" "q: a =\<^bsub>A\<^esub> b" "r: b =\<^bsub>A\<^esub> c" "s: b =\<^bsub>A\<^esub> c"
 begin
-
-Lemma (def) horiz_pathcomp:
-  assumes "\<alpha>: p = q" "\<beta>: r = s"
-  shows "p \<bullet> r = q \<bullet> s"
-proof (rule pathcomp)
-  show "p \<bullet> r = q \<bullet> r" by right_whisker fact
-  show ".. = q \<bullet> s" by left_whisker fact
-qed typechk
-
-text \<open>A second horizontal composition:\<close>
-
-Lemma (def) horiz_pathcomp':
-  assumes "\<alpha>: p = q" "\<beta>: r = s"
-  shows "p \<bullet> r = q \<bullet> s"
-proof (rule pathcomp)
-  show "p \<bullet> r = p \<bullet> s" by left_whisker fact
-  show ".. = q \<bullet> s" by right_whisker fact
-qed typechk
-
-notation horiz_pathcomp (infix "\<star>" 121)
-notation horiz_pathcomp' (infix "\<star>''" 121)
-
-Lemma (def) horiz_pathcomp_eq_horiz_pathcomp':
-  assumes "\<alpha>: p = q" "\<beta>: r = s"
-  shows "\<alpha> \<star> \<beta> = \<alpha> \<star>' \<beta>"
-  unfolding horiz_pathcomp_def horiz_pathcomp'_def
-  apply (eq \<alpha>, eq \<beta>)
-    focus vars p apply (eq p)
-      focus vars a _ _ _ r by (eq r) (compute, refl)
-    done
-  done
-
+  Lemma (def) horiz_pathcomp:
+    assumes "\<alpha>: p = q" "\<beta>: r = s" shows "p \<bullet> r = q \<bullet> s"
+  proof (rule pathcomp)
+    show "p \<bullet> r = q \<bullet> r" by right_whisker fact
+    show ".. = q \<bullet> s" by left_whisker fact
+  qed typechk
+
+  Lemma (def) horiz_pathcomp':
+    assumes "\<alpha>: p = q" "\<beta>: r = s" shows "p \<bullet> r = q \<bullet> s"
+  proof (rule pathcomp)
+    show "p \<bullet> r = p \<bullet> s" by left_whisker fact
+    show ".. = q \<bullet> s" by right_whisker fact
+  qed typechk
+
+  notation horiz_pathcomp (infix "\<star>" 121)
+  notation horiz_pathcomp' (infix "\<star>''" 121)
+
+  Lemma (def) horiz_pathcomp_eq_horiz_pathcomp':
+    assumes "\<alpha>: p = q" "\<beta>: r = s" shows "\<alpha> \<star> \<beta> = \<alpha> \<star>' \<beta>"
+    unfolding horiz_pathcomp_def horiz_pathcomp'_def
+    proof (eq \<alpha>, eq \<beta>)
+      fix p q assuming "p: a = b" "q: b = c"
+      show "refl p \<bullet>\<^sub>r q \<bullet> (p \<bullet>\<^sub>l refl q) = p \<bullet>\<^sub>l refl q \<bullet> (refl p \<bullet>\<^sub>r q)"
+      proof (eq p)
+        fix a r assuming "a: A" "r: a = c"
+        show "refl (refl a) \<bullet>\<^sub>r r \<bullet> (refl a \<bullet>\<^sub>l refl r) = refl a \<bullet>\<^sub>l refl r \<bullet> (refl (refl a) \<bullet>\<^sub>r r)"
+          by (eq r) (compute, refl)
+      qed
+    qed
 end
 
 
diff --git a/hott/List_HoTT.thy b/hott/List_HoTT.thy
index 9bd1517..d866f59 100644
--- a/hott/List_HoTT.thy
+++ b/hott/List_HoTT.thy
@@ -1,6 +1,6 @@
 theory List_HoTT
 imports
-  Spartan.List
+  MLTT.List
   Nat
 
 begin
diff --git a/spartan/core/Spartan.thy b/mltt/core/MLTT.thy
index 5046b6a..18bd2b7 100644
--- a/spartan/core/Spartan.thy
+++ b/mltt/core/MLTT.thy
@@ -1,6 +1,4 @@
-text \<open>Spartan type theory\<close>
-
-theory Spartan
+theory MLTT
 imports
   Pure
   "HOL-Eisbach.Eisbach"
@@ -511,14 +509,14 @@ Lemma snd_comp [comp]:
 subsection \<open>Notation\<close>
 
 definition fst_i ("fst")
-  where [implicit]: "fst \<equiv> Spartan.fst {} {}"
+  where [implicit]: "fst \<equiv> MLTT.fst {} {}"
 
 definition snd_i ("snd")
-  where [implicit]: "snd \<equiv> Spartan.snd {} {}"
+  where [implicit]: "snd \<equiv> MLTT.snd {} {}"
 
 translations
-  "fst" \<leftharpoondown> "CONST Spartan.fst A B"
-  "snd" \<leftharpoondown> "CONST Spartan.snd A B"
+  "fst" \<leftharpoondown> "CONST MLTT.fst A B"
+  "snd" \<leftharpoondown> "CONST MLTT.snd A B"
 
 subsection \<open>Projections\<close>
 
@@ -541,10 +539,10 @@ method snd for p::o = rule snd[where ?p=p]
 
 text \<open>Double projections:\<close>
 
-definition [implicit]: "p\<^sub>1\<^sub>1 p \<equiv> Spartan.fst {} {} (Spartan.fst {} {} p)"
-definition [implicit]: "p\<^sub>1\<^sub>2 p \<equiv> Spartan.snd {} {} (Spartan.fst {} {} p)"
-definition [implicit]: "p\<^sub>2\<^sub>1 p \<equiv> Spartan.fst {} {} (Spartan.snd {} {} p)"
-definition [implicit]: "p\<^sub>2\<^sub>2 p \<equiv> Spartan.snd {} {} (Spartan.snd {} {} p)"
+definition [implicit]: "p\<^sub>1\<^sub>1 p \<equiv> MLTT.fst {} {} (MLTT.fst {} {} p)"
+definition [implicit]: "p\<^sub>1\<^sub>2 p \<equiv> MLTT.snd {} {} (MLTT.fst {} {} p)"
+definition [implicit]: "p\<^sub>2\<^sub>1 p \<equiv> MLTT.fst {} {} (MLTT.snd {} {} p)"
+definition [implicit]: "p\<^sub>2\<^sub>2 p \<equiv> MLTT.snd {} {} (MLTT.snd {} {} p)"
 
 translations
   "CONST p\<^sub>1\<^sub>1 p" \<leftharpoondown> "fst (fst p)"
diff --git a/spartan/core/calc.ML b/mltt/core/calc.ML
index 67dc7fc..67dc7fc 100644
--- a/spartan/core/calc.ML
+++ b/mltt/core/calc.ML
diff --git a/spartan/core/cases.ML b/mltt/core/cases.ML
index 560a9f1..560a9f1 100644
--- a/spartan/core/cases.ML
+++ b/mltt/core/cases.ML
diff --git a/spartan/core/comp.ML b/mltt/core/comp.ML
index 2e50753..2e50753 100644
--- a/spartan/core/comp.ML
+++ b/mltt/core/comp.ML
diff --git a/spartan/core/context_facts.ML b/mltt/core/context_facts.ML
index 5aa7c70..5aa7c70 100644
--- a/spartan/core/context_facts.ML
+++ b/mltt/core/context_facts.ML
diff --git a/spartan/core/context_tactical.ML b/mltt/core/context_tactical.ML
index d0fed61..d0fed61 100644
--- a/spartan/core/context_tactical.ML
+++ b/mltt/core/context_tactical.ML
diff --git a/spartan/core/elaborated_statement.ML b/mltt/core/elaborated_statement.ML
index 33f88cf..33f88cf 100644
--- a/spartan/core/elaborated_statement.ML
+++ b/mltt/core/elaborated_statement.ML
diff --git a/spartan/core/elaboration.ML b/mltt/core/elaboration.ML
index 9e5e0bd..9e5e0bd 100644
--- a/spartan/core/elaboration.ML
+++ b/mltt/core/elaboration.ML
diff --git a/spartan/core/elimination.ML b/mltt/core/elimination.ML
index cf9d21e..cf9d21e 100644
--- a/spartan/core/elimination.ML
+++ b/mltt/core/elimination.ML
diff --git a/spartan/core/eqsubst.ML b/mltt/core/eqsubst.ML
index 5ae8c73..5ae8c73 100644
--- a/spartan/core/eqsubst.ML
+++ b/mltt/core/eqsubst.ML
diff --git a/spartan/core/focus.ML b/mltt/core/focus.ML
index b963cfe..b963cfe 100644
--- a/spartan/core/focus.ML
+++ b/mltt/core/focus.ML
diff --git a/spartan/core/goals.ML b/mltt/core/goals.ML
index 7d52495..7d52495 100644
--- a/spartan/core/goals.ML
+++ b/mltt/core/goals.ML
diff --git a/spartan/core/implicits.ML b/mltt/core/implicits.ML
index 2b63f49..2b63f49 100644
--- a/spartan/core/implicits.ML
+++ b/mltt/core/implicits.ML
diff --git a/spartan/core/lib.ML b/mltt/core/lib.ML
index e43ad98..e43ad98 100644
--- a/spartan/core/lib.ML
+++ b/mltt/core/lib.ML
diff --git a/spartan/core/tactics.ML b/mltt/core/tactics.ML
index 923a3a7..6876d5c 100644
--- a/spartan/core/tactics.ML
+++ b/mltt/core/tactics.ML
@@ -129,7 +129,7 @@ fun elim_ctac tms =
                 |> filter (fn (_, i) => i > 0)
                 (*`t1: T1` comes before `t2: T2` if T1 contains t2 as subterm.
                   If they are incomparable, then order by decreasing
-                  `subterm_count [p, x, y] T`*)
+                  `subterm_count_distinct tms T`*)
                 |> sort (fn (((t1, _), i), ((_, T2), j)) =>
                     Lib.cond_order (Lib.subterm_order T2 t1) (int_ord (j, i)))
                 |> map (#1 o #1)
diff --git a/spartan/core/types.ML b/mltt/core/types.ML
index 5e0d484..5e0d484 100644
--- a/spartan/core/types.ML
+++ b/mltt/core/types.ML
diff --git a/spartan/lib/List.thy b/mltt/lib/List.thy
index 4beb9b6..4beb9b6 100644
--- a/spartan/lib/List.thy
+++ b/mltt/lib/List.thy
diff --git a/spartan/lib/Maybe.thy b/mltt/lib/Maybe.thy
index 452acc2..452acc2 100644
--- a/spartan/lib/Maybe.thy
+++ b/mltt/lib/Maybe.thy
diff --git a/spartan/lib/Prelude.thy b/mltt/lib/Prelude.thy
index 56adbfc..0393968 100644
--- a/spartan/lib/Prelude.thy
+++ b/mltt/lib/Prelude.thy
@@ -1,5 +1,5 @@
 theory Prelude
-imports Spartan
+imports MLTT
 
 begin
 
@@ -84,6 +84,8 @@ lemmas
   [elim ?x] = BotE and
   [comp] = Top_comp
 
+abbreviation (input) Not ("\<not>_" [1000] 1000) where "\<not>A \<equiv> A \<rightarrow> \<bottom>"
+
 
 section \<open>Booleans\<close>
 
diff --git a/spartan/core/equality.ML b/spartan/core/equality.ML
deleted file mode 100644
index 023147b..0000000
--- a/spartan/core/equality.ML
+++ /dev/null
@@ -1,90 +0,0 @@
-(*  Title:      equality.ML
-    Author:     Joshua Chen
-
-Equality reasoning with identity types.
-*)
-
-structure Equality:
-sig
-
-val dest_Id: term -> term * term * term
-
-val push_hyp_tac: term * term -> Proof.context -> int -> tactic
-val induction_tac: term -> term -> term -> term -> Proof.context -> tactic
-val equality_context_tac: Facts.ref -> Proof.context -> context_tactic
-
-end = struct
-
-fun dest_Id tm = case tm of
-    Const (\<^const_name>\<open>Id\<close>, _) $ A $ x $ y => (A, x, y)
-  | _ => error "dest_Id"
-
-(*Context assumptions that have already been pushed into the type family*)
-structure Inserts = Proof_Data (
-  type T = term Item_Net.T
-  val init = K (Item_Net.init Term.aconv_untyped single)
-)
-
-fun push_hyp_tac (t, _) =
-  Subgoal.FOCUS_PARAMS (fn {context = ctxt, concl, ...} =>
-    let
-      val (_, C) = Lib.dest_typing (Thm.term_of concl)
-      val B = Thm.cterm_of ctxt (Lib.lambda_var t C)
-      val a = Thm.cterm_of ctxt t
-      (*The resolvent is PiE[where ?B=B and ?a=a]*)
-      val resolvent =
-        Drule.infer_instantiate' ctxt [NONE, NONE, SOME B, SOME a] @{thm PiE}
-    in
-      HEADGOAL (resolve_tac ctxt [resolvent])
-      THEN SOMEGOAL (known_tac ctxt)
-    end)
-
-fun induction_tac p A x y ctxt =
-  let
-    val [p, A, x, y] = map (Thm.cterm_of ctxt) [p, A, x, y]
-  in
-    HEADGOAL (resolve_tac ctxt
-      [Drule.infer_instantiate' ctxt [SOME p, SOME A, SOME x, SOME y] @{thm IdE}])
-  end
-
-val side_conds_tac = TRY oo typechk_tac
-
-fun equality_context_tac fact ctxt =
-  let
-    val eq_th = Proof_Context.get_fact_single ctxt fact
-    val (p, (A, x, y)) = (Lib.dest_typing ##> dest_Id) (Thm.prop_of eq_th)
-
-    val hyps =
-      Facts.props (Proof_Context.facts_of ctxt)
-      |> filter (fn (th, _) => Lib.is_typing (Thm.prop_of th))
-      |> map (Lib.dest_typing o Thm.prop_of o fst)
-      |> filter_out (fn (t, _) =>
-          Term.aconv (t, p) orelse Item_Net.member (Inserts.get ctxt) t)
-      |> map (fn (t, T) => ((t, T), Lib.subterm_count_distinct [p, x, y] T))
-      |> filter (fn (_, i) => i > 0)
-      (*`t1: T1` comes before `t2: T2` if T1 contains t2 as subterm.
-        If they are incomparable, then order by decreasing
-        `subterm_count [p, x, y] T`*)
-      |> sort (fn (((t1, _), i), ((_, T2), j)) =>
-          Lib.cond_order (Lib.subterm_order T2 t1) (int_ord (j, i)))
-      |> map #1
-
-    val record_inserts =
-      Inserts.map (fold (fn (t, _) => fn net => Item_Net.update t net) hyps)
-
-    val tac =
-      fold (fn hyp => fn tac => tac THEN HEADGOAL (push_hyp_tac hyp ctxt))
-        hyps all_tac
-      THEN (
-        induction_tac p A x y ctxt
-        THEN RANGE (replicate 3 (typechk_tac ctxt) @ [side_conds_tac ctxt]) 1
-      )
-      THEN (
-        REPEAT_DETERM_N (length hyps) (SOMEGOAL (resolve_tac ctxt @{thms PiI}))
-        THEN ALLGOALS (side_conds_tac ctxt)
-      )
-  in
-    fn (ctxt, st) => Context_Tactic.TACTIC_CONTEXT (record_inserts ctxt) (tac st)
-  end
-
-end