diff options
| -rw-r--r-- | ROOT | 3 | ||||
| -rw-r--r-- | hott/Equivalence.thy | 23 | ||||
| -rw-r--r-- | hott/Identity.thy | 6 | ||||
| -rw-r--r-- | hott/List_HoTT.thy | 4 | ||||
| -rw-r--r-- | hott/Propositions.thy | 8 | ||||
| -rw-r--r-- | hott/Univalence.thy | 35 | ||||
| -rw-r--r-- | mltt/core/MLTT.thy | 48 | ||||
| -rw-r--r-- | mltt/core/goals.ML | 101 | ||||
| -rw-r--r-- | mltt/core/lib.ML | 5 | ||||
| -rw-r--r-- | mltt/lib/List.thy | 10 | ||||
| -rw-r--r-- | mltt/lib/Maybe.thy | 2 | ||||
| -rw-r--r-- | mltt/lib/Prelude.thy | 2 |
12 files changed, 164 insertions, 83 deletions
@@ -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" |