aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--ROOT3
-rw-r--r--hott/Equivalence.thy23
-rw-r--r--hott/Identity.thy6
-rw-r--r--hott/List_HoTT.thy4
-rw-r--r--hott/Propositions.thy8
-rw-r--r--hott/Univalence.thy35
-rw-r--r--mltt/core/MLTT.thy48
-rw-r--r--mltt/core/goals.ML101
-rw-r--r--mltt/core/lib.ML5
-rw-r--r--mltt/lib/List.thy10
-rw-r--r--mltt/lib/Maybe.thy2
-rw-r--r--mltt/lib/Prelude.thy2
12 files changed, 164 insertions, 83 deletions
diff --git a/ROOT b/ROOT
index 2d97bbb..a04ca48 100644
--- a/ROOT
+++ b/ROOT
@@ -29,4 +29,7 @@ session HoTT in hott = MLTT +
Identity
Equivalence
Nat
+ Propositions
+ Univalence
+ Bool_HoTT
List_HoTT
diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy
index 745bc67..8007b89 100644
--- a/hott/Equivalence.thy
+++ b/hott/Equivalence.thy
@@ -202,7 +202,7 @@ Lemma is_qinvI:
unfolding is_qinv_def
proof intro
show "g: B \<rightarrow> A" by fact
- show "g \<circ> f ~ id A \<and> f \<circ> g ~ id B" by (intro; fact)
+ show "g \<circ> f ~ id A \<times> f \<circ> g ~ id B" by (intro; fact)
qed
Lemma is_qinv_components [type]:
@@ -405,8 +405,9 @@ text \<open>
\<close>
Lemma (def) equiv_if_equal:
+ notes Ui_in_USi [form]
assumes
- "A: U i" "B: U i" "p: A =\<^bsub>U i\<^esub> B"
+ "A: U i" "B: U i" "p: A = B"
shows "<transp (id (U i)) p, ?isequiv>: A \<simeq> B"
unfolding equivalence_def
apply intro defer
@@ -415,13 +416,10 @@ Lemma (def) equiv_if_equal:
apply (comp at A in "A \<rightarrow> B" id_comp[symmetric])
using [[solve_side_conds=1]]
apply (comp at B in "_ \<rightarrow> B" id_comp[symmetric])
- apply (rule transport, rule Ui_in_USi)
- by (rule lift_universe_codomain, rule Ui_in_USi)
+ using Ui_in_USi by (rule transport, rule lift_universe_codomain)
\<^enum> vars A
- using [[solve_side_conds=1]]
apply (comp transport_comp)
- \<circ> by (rule Ui_in_USi)
- \<circ> by compute (rule U_lift)
+ \<circ> by (rule U_lift)
\<circ> by compute (rule id_is_biinv)
done
done
@@ -430,9 +428,16 @@ Lemma (def) equiv_if_equal:
apply (comp at A in "A \<rightarrow> B" id_comp[symmetric])
using [[solve_side_conds=1]]
apply (comp at B in "_ \<rightarrow> B" id_comp[symmetric])
- apply (rule transport, rule Ui_in_USi)
- by (rule lift_universe_codomain, rule Ui_in_USi)
+ using Ui_in_USi by (rule transport, rule lift_universe_codomain)
done
+Definition idtoeqv: ":= MLTT.fst (A \<rightarrow> B) is_biinv (equiv_if_equal i A B p)"
+ where "A: U i" "B: U i" "p: A =\<^bsub>U i\<^esub> B"
+ using equiv_if_equal unfolding equivalence_def
+ by typechk
+
+definition idtoeqv_i ("idtoeqv")
+ where [implicit]: "idtoeqv p \<equiv> Equivalence.idtoeqv {} {} {} p"
+
end
diff --git a/hott/Identity.thy b/hott/Identity.thy
index 9ae0894..ce0e0ec 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -259,16 +259,16 @@ section \<open>Transport\<close>
Lemma (def) transport:
assumes
"A: U i"
- "\<And>x. x: A \<Longrightarrow> P x: U i"
"x: A" "y: A"
"p: x = y"
+ "\<And>x. x: A \<Longrightarrow> P x: U i"
shows "P x \<rightarrow> P y"
by (eq p) intro
definition transport_i ("transp")
- where [implicit]: "transp P p \<equiv> transport {} P {} {} p"
+ where [implicit]: "transp P p \<equiv> transport {} {} {} p P"
-translations "transp P p" \<leftharpoondown> "CONST transport A P x y p"
+translations "transp P p" \<leftharpoondown> "CONST transport A x y p P"
Lemma transport_comp [comp]:
assumes
diff --git a/hott/List_HoTT.thy b/hott/List_HoTT.thy
index d866f59..a48d2ab 100644
--- a/hott/List_HoTT.thy
+++ b/hott/List_HoTT.thy
@@ -10,8 +10,8 @@ section \<open>Length\<close>
definition [implicit]: "len \<equiv> ListRec {} Nat 0 (fn _ _ rec. suc rec)"
experiment begin
- Lemma "len [] \<equiv> ?n" by (subst comp; typechk?)
- Lemma "len [0, suc 0, suc (suc 0)] \<equiv> ?n" by (subst comp; typechk?)+
+ Lemma "len [] \<equiv> ?n" by compute
+ Lemma "len [0, suc 0, suc (suc 0)] \<equiv> ?n" by compute
end
diff --git a/hott/Propositions.thy b/hott/Propositions.thy
index 66e34d2..2c98a5a 100644
--- a/hott/Propositions.thy
+++ b/hott/Propositions.thy
@@ -5,8 +5,11 @@ imports
begin
-definition isProp where "isProp A \<equiv> \<Prod>x y: A. x =\<^bsub>A\<^esub> y"
-definition isSet where "isSet A \<equiv> \<Prod>x y: A. \<Prod>p q: x =\<^bsub>A\<^esub> y. p =\<^bsub>x =\<^bsub>A\<^esub> y\<^esub> q"
+Definition isProp: ":= \<Prod>x y: A. x = y"
+ where "A: U i" by typechk
+
+Definition isSet: ":=\<Prod>x y: A. \<Prod>p q: x = y. p = q"
+ where "A: U i" by typechk
Theorem isProp_Top: "isProp \<top>"
unfolding isProp_def
@@ -16,4 +19,5 @@ Theorem isProp_Bot: "isProp \<bottom>"
unfolding isProp_def
by (intros, elim)
+
end
diff --git a/hott/Univalence.thy b/hott/Univalence.thy
new file mode 100644
index 0000000..114577b
--- /dev/null
+++ b/hott/Univalence.thy
@@ -0,0 +1,35 @@
+theory Univalence
+imports Equivalence
+
+begin
+
+declare Ui_in_USi [form]
+
+Definition univalent_U: ":= \<Prod> A B: U i. \<Prod> p: A = B. is_biinv (idtoeqv p)"
+ by (typechk; rule U_lift)+
+
+axiomatization univalence where
+ univalence: "\<And>i. univalence i: univalent_U i"
+
+Lemma (def) idtoeqv_is_qinv:
+ assumes "A: U i" "B: U i" "p: A = B"
+ shows "is_qinv (idtoeqv p)"
+ by (rule is_qinv_if_is_biinv) (rule univalence[unfolded univalent_U_def])
+
+Definition ua: ":= fst (idtoeqv_is_qinv i A B p)"
+ where "A: U i" "B: U i" "p: A = B"
+ by typechk
+
+definition ua_i ("ua")
+ where [implicit]: "ua p \<equiv> Univalence.ua {} {} {} p"
+
+Definition ua_idtoeqv [folded ua_def]: ":= fst (snd (idtoeqv_is_qinv i A B p))"
+ where "A: U i" "B: U i" "p: A = B"
+ by typechk
+
+Definition idtoeqv_ua [folded ua_def]: ":= snd (snd (idtoeqv_is_qinv i A B p))"
+ where "A: U i" "B: U i" "p: A = B"
+ by typechk
+
+
+end
diff --git a/mltt/core/MLTT.thy b/mltt/core/MLTT.thy
index 5888a90..29c7248 100644
--- a/mltt/core/MLTT.thy
+++ b/mltt/core/MLTT.thy
@@ -220,6 +220,27 @@ in
end
\<close>
+section \<open>Implicits\<close>
+
+text \<open>
+ \<open>{}\<close> is used to mark implicit arguments in definitions, while \<open>?\<close> is expanded
+ immediately for elaboration in statements.
+\<close>
+
+consts
+ iarg :: \<open>'a\<close> ("{}")
+ hole :: \<open>'b\<close> ("?")
+
+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 "" Implicits.make_holes)\<close>
+
+text \<open>Automatically insert inhabitation judgments where needed:\<close>
+syntax inhabited :: \<open>o \<Rightarrow> prop\<close> ("(_)")
+translations "inhabited A" \<rightharpoonup> "CONST has_type ? A"
+
section \<open>Statements and goals\<close>
@@ -228,6 +249,10 @@ ML_file \<open>elaboration.ML\<close>
ML_file \<open>elaborated_statement.ML\<close>
ML_file \<open>goals.ML\<close>
+text \<open>Syntax for definition bodies.\<close>
+syntax defn :: \<open>o \<Rightarrow> prop\<close> ("(:=_)")
+translations "defn t" \<rightharpoonup> "CONST has_type t ?"
+
section \<open>Proof methods\<close>
@@ -328,29 +353,6 @@ consts "rhs" :: \<open>'a\<close> ("..")
ML_file \<open>calc.ML\<close>
-section \<open>Implicits\<close>
-
-text \<open>
- \<open>{}\<close> is used to mark implicit arguments in definitions, while \<open>?\<close> is expanded
- immediately for elaboration in statements.
-\<close>
-
-consts
- iarg :: \<open>'a\<close> ("{}")
- hole :: \<open>'b\<close> ("?")
-
-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 "" Implicits.make_holes)\<close>
-
-text \<open>Automatically insert inhabitation judgments where needed:\<close>
-
-syntax inhabited :: \<open>o \<Rightarrow> prop\<close> ("(_)")
-translations "inhabited A" \<rightharpoonup> "CONST has_type ? A"
-
-
subsection \<open>Implicit lambdas\<close>
definition lam_i where [implicit]: "lam_i f \<equiv> lam {} f"
diff --git a/mltt/core/goals.ML b/mltt/core/goals.ML
index d69c800..4d03133 100644
--- a/mltt/core/goals.ML
+++ b/mltt/core/goals.ML
@@ -28,6 +28,15 @@ val short_statement =
[Element.Fixes fixes, Element.Assumes assumes], Element.Shows shows)
)
+val where_statement = Scan.optional (Parse.$$$ "where" |-- Parse.!!! Parse_Spec.statement) []
+
+val def_statement =
+ Parse_Spec.statement -- where_statement >>
+ (fn (shows, assumes) =>
+ (false, Binding.empty_atts, [],
+ [Element.Fixes [], Element.Assumes assumes], Element.Shows shows)
+ )
+
fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt =
let
val (stmt, elems_ctxt) = prep_stmt raw_elems raw_stmt ctxt
@@ -58,56 +67,60 @@ fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt =
end
end
+fun make_name_binding name suffix local_name =
+ let val base_local_name = Long_Name.base_name local_name
+ in Binding.qualified_name
+ ((case base_local_name of "" => name | _ => base_local_name) ^
+ (case suffix
+ of SOME s => "_" ^ s
+ | NONE => ""))
+ end
+
fun define_proof_term name (local_name, [th]) lthy =
let
- fun make_name_binding suffix local_name =
- let val base_local_name = Long_Name.base_name local_name
- in Binding.qualified_name
- ((case base_local_name of "" => name | _ => base_local_name) ^
- (case suffix
- of SOME "prf" => "_prf"
- | SOME "def" => "_def"
- | _ => ""))
- end
-
val (prems, concl) =
(Logic.strip_assums_hyp (Thm.prop_of th),
Logic.strip_assums_concl (Thm.prop_of th))
in
if not (Lib.is_typing concl) then ([], lthy)
else let
- val prems_vars = distinct Term.aconv (flat
- (map (Lib.collect_subterms is_Var) prems))
+ val prems_vars = distinct Term.aconv (
+ flat (map (Lib.collect_subterms is_Var) prems))
- val concl_vars = Lib.collect_subterms is_Var
- (Lib.term_of_typing concl)
+ val concl_vars = distinct Term.aconv (
+ Lib.collect_subterms is_Var (Lib.term_of_typing concl))
val params = sort (uncurry Lib.lvl_order) (inter Term.aconv concl_vars prems_vars)
val prf_tm = fold_rev lambda params (Lib.term_of_typing concl)
+ val levels = filter Lib.is_lvl (distinct Term.aconv (
+ Lib.collect_subterms is_Var prf_tm))
+
+ val prf_tm' = fold_rev lambda levels prf_tm
+
val ((_, (_, raw_def)), lthy') = Local_Theory.define
- ((make_name_binding NONE local_name, Mixfix.NoSyn),
- ((make_name_binding (SOME "prf") local_name, []), prf_tm)) lthy
+ ((make_name_binding name NONE local_name, Mixfix.NoSyn),
+ ((make_name_binding name (SOME "prf") local_name, []), prf_tm')) lthy
val def = fold
(fn th1 => fn th2 => Thm.combination th2 th1)
- (map (Thm.reflexive o Thm.cterm_of lthy) params)
+ (map (Thm.reflexive o Thm.cterm_of lthy) (params @ levels))
raw_def
val ((_, def'), lthy'') = Local_Theory.note
- ((make_name_binding (SOME "def") local_name, []), [def])
+ ((make_name_binding name (SOME "def") local_name, []), [def])
lthy'
in
(def', lthy'')
end
end
| define_proof_term _ _ _ = error
- ("Unimplemented: proof terms for multiple facts in one statement")
+ ("Can't generate proof terms for multiple facts in one statement")
fun gen_schematic_theorem
bundle_includes prep_att prep_stmt
- gen_prf_tm long kind
+ gen_prf_tm long kind defn
before_qed after_qed
(name, raw_atts) raw_includes raw_elems raw_concl
do_print lthy
@@ -137,7 +150,7 @@ fun gen_schematic_theorem
lthy,
true)
- val (res', lthy'') =
+ val ((name_def, defs), (res', lthy'')) =
if gen_prf_tm
then
let
@@ -147,28 +160,46 @@ fun gen_schematic_theorem
(define_proof_term (Binding.name_of name) result lthy))
res
([], lthy')
+
val res_folded =
map (apsnd (map (Local_Defs.fold new_lthy prf_tm_defs))) res
+
+ val name_def =
+ make_name_binding (Binding.name_of name) (SOME "def") (#1 (hd res_folded))
+
+ val name_type =
+ if defn then
+ make_name_binding (Binding.name_of name) (SOME "type") (#1 (hd res_folded))
+ else name
in
+ ((name_def, prf_tm_defs),
Local_Theory.notes_kind kind
- [((name, @{attributes [type]} @ atts),
+ [((name_type, @{attributes [type]} @ atts),
[(maps #2 res_folded, [])])]
- new_lthy
+ new_lthy)
end
else
+ ((Binding.empty, []),
Local_Theory.notes_kind kind
[((name, atts), [(maps #2 res, [])])]
- lthy'
-
- val _ = Proof_Display.print_results do_print pos lthy''
- ((kind, Binding.name_of name), map (fn (_, ths) => ("", ths)) res')
+ lthy')
+ (*Display theorems*)
val _ =
- if substmts then map
- (fn (name, ths) => Proof_Display.print_results do_print pos lthy''
- (("and", name), [("", ths)]))
- res
- else []
+ if defn then
+ single (Proof_Display.print_results do_print pos lthy''
+ ((kind, Binding.name_of name_def), [("", defs)]))
+ else
+ (if long then
+ Proof_Display.print_results do_print pos lthy''
+ ((kind, Binding.name_of name), map (fn (_, ths) => ("", ths)) res')
+ else ();
+ if substmts then
+ map (fn (name, ths) =>
+ Proof_Display.print_results do_print pos lthy''
+ ((kind, name), [("", ths)]))
+ res
+ else [])
in
after_qed results' lthy''
end
@@ -194,14 +225,14 @@ fun theorem spec descr =
(fn (opt_derive, (long, binding, includes, elems, concl)) =>
schematic_theorem_cmd
(case opt_derive of SOME "def" => true | _ => false)
- long descr NONE (K I) binding includes elems concl))
+ long descr false NONE (K I) binding includes elems concl))
fun definition spec descr =
Outer_Syntax.local_theory_to_proof' spec "definition with explicit type checking obligation"
- ((long_statement || short_statement) >>
+ (def_statement >>
(fn (long, binding, includes, elems, concl) =>
schematic_theorem_cmd
- true long descr NONE (K I) binding includes elems concl))
+ true long descr true NONE (K I) binding includes elems concl))
in
diff --git a/mltt/core/lib.ML b/mltt/core/lib.ML
index f15daf6..98d83cc 100644
--- a/mltt/core/lib.ML
+++ b/mltt/core/lib.ML
@@ -14,6 +14,7 @@ val dest_eq: term -> term * term
val mk_Var: string -> int -> typ -> term
val lambda_var: term -> term -> term
+val is_lvl: term -> bool
val is_typing: term -> bool
val mk_typing: term -> term -> term
val dest_typing: term -> term * term
@@ -83,6 +84,8 @@ fun lambda_var x tm =
(* Object *)
+fun is_lvl t = case fastype_of t of Type (\<^type_name>\<open>lvl\<close>, _) => true | _ => false
+
fun is_typing (Const (\<^const_name>\<open>has_type\<close>, _) $ _ $ _) = true
| is_typing _ = false
@@ -189,7 +192,6 @@ fun subterm_order t1 t2 =
else EQUAL
fun lvl_order t1 t2 =
- let val _ = @{print} (fastype_of t1) in
case fastype_of t1 of
Type (\<^type_name>\<open>lvl\<close>, _) => (case fastype_of t2 of
Type (\<^type_name>\<open>lvl\<close>, _) => EQUAL
@@ -199,7 +201,6 @@ fun lvl_order t1 t2 =
Type (\<^type_name>\<open>lvl\<close>, _) => GREATER
| _ => EQUAL)
| _ => EQUAL
- end
fun cond_order o1 o2 = case o1 of EQUAL => o2 | _ => o1
diff --git a/mltt/lib/List.thy b/mltt/lib/List.thy
index 4beb9b6..0cd43c8 100644
--- a/mltt/lib/List.thy
+++ b/mltt/lib/List.thy
@@ -83,7 +83,7 @@ section \<open>Standard functions\<close>
subsection \<open>Head and tail\<close>
-Definition head:
+Lemma (def) head:
assumes "A: U i" "xs: List A"
shows "Maybe A"
proof (cases xs)
@@ -91,7 +91,7 @@ proof (cases xs)
show "\<And>x. x: A \<Longrightarrow> some x: Maybe A" by intro
qed
-Definition tail:
+Lemma (def) tail:
assumes "A: U i" "xs: List A"
shows "List A"
proof (cases xs)
@@ -128,7 +128,7 @@ Lemma tail_of_cons [comp]:
subsection \<open>Append\<close>
-Definition app:
+Lemma (def) app:
assumes "A: U i" "xs: List A" "ys: List A"
shows "List A"
apply (elim xs)
@@ -143,7 +143,7 @@ translations "app" \<leftharpoondown> "CONST List.app A"
subsection \<open>Map\<close>
-Definition map:
+Lemma (def) map:
assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "xs: List A"
shows "List B"
proof (elim xs)
@@ -165,7 +165,7 @@ Lemma map_type [type]:
subsection \<open>Reverse\<close>
-Definition rev:
+Lemma (def) rev:
assumes "A: U i" "xs: List A"
shows "List A"
apply (elim xs)
diff --git a/mltt/lib/Maybe.thy b/mltt/lib/Maybe.thy
index 452acc2..257bc8f 100644
--- a/mltt/lib/Maybe.thy
+++ b/mltt/lib/Maybe.thy
@@ -17,7 +17,7 @@ lemma
Maybe_some: "a: A \<Longrightarrow> some A a: Maybe A"
unfolding Maybe_def none_def some_def by typechk+
-Definition MaybeInd:
+Lemma (def) MaybeInd:
assumes
"A: U i"
"\<And>m. m: Maybe A \<Longrightarrow> C m: U i"
diff --git a/mltt/lib/Prelude.thy b/mltt/lib/Prelude.thy
index 0393968..86165cd 100644
--- a/mltt/lib/Prelude.thy
+++ b/mltt/lib/Prelude.thy
@@ -100,7 +100,7 @@ Lemma
unfolding Bool_def true_def false_def by typechk+
\<comment> \<open>Definitions like these should be handled by a future function package\<close>
-Definition ifelse [rotated 1]:
+Lemma (def) ifelse [rotated 1]:
assumes *[unfolded Bool_def true_def false_def]:
"\<And>x. x: Bool \<Longrightarrow> C x: U i"
"x: Bool"