From 77aa10763429d2ded040071fbf7bee331dd52f5e Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Fri, 31 Jul 2020 18:10:10 +0200 Subject: (REF) Tweak attribute names in preparation for new logical introduction rule behavior --- hott/Equivalence.thy | 32 ++++++++++++++++---------------- hott/Identity.thy | 4 ++-- hott/Nat.thy | 6 +++--- spartan/core/Spartan.thy | 29 ++++++++++++++++------------- spartan/core/goals.ML | 2 +- spartan/core/tactics.ML | 2 +- spartan/core/typechecking.ML | 7 +++---- spartan/lib/List.thy | 10 +++++----- spartan/lib/Maybe.thy | 2 +- spartan/lib/Prelude.thy | 8 ++++---- 10 files changed, 52 insertions(+), 50 deletions(-) diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy index 66c64f6..619ed84 100644 --- a/hott/Equivalence.thy +++ b/hott/Equivalence.thy @@ -12,7 +12,7 @@ definition homotopy_i (infix "~" 100) translations "f ~ g" \ "CONST homotopy A B f g" -Lemma homotopy_type [typechk]: +Lemma homotopy_type [type]: assumes "A: U i" "\x. x: A \ B x: U i" @@ -161,7 +161,7 @@ subsection \Quasi-inverses\ definition "is_qinv A B f \ \g: B \ A. homotopy A (fn _. A) (g \\<^bsub>A\<^esub> f) (id A) \ homotopy B (fn _. B) (f \\<^bsub>B\<^esub> g) (id B)" -lemma is_qinv_type [typechk]: +lemma is_qinv_type [type]: assumes "A: U i" "B: U i" "f: A \ B" shows "is_qinv A B f: U i" unfolding is_qinv_def @@ -193,12 +193,12 @@ Lemma is_qinvI: show "g \ f ~ id A \ f \ g ~ id B" by (intro; fact) qed -Lemma is_qinv_components [typechk]: +Lemma is_qinv_components [type]: assumes "A: U i" "B: U i" "f: A \ B" "pf: is_qinv f" shows - fst_of_is_qinv: "fst pf: B \ A" and - p\<^sub>2\<^sub>1_of_is_qinv: "p\<^sub>2\<^sub>1 pf: fst pf \ f ~ id A" and - p\<^sub>2\<^sub>2_of_is_qinv: "p\<^sub>2\<^sub>2 pf: f \ fst pf ~ id B" + qinv_of_is_qinv: "fst pf: B \ A" and + ret_of_is_qinv: "p\<^sub>2\<^sub>1 pf: fst pf \ f ~ id A" and + sec_of_is_qinv: "p\<^sub>2\<^sub>2 pf: f \ fst pf ~ id B" using assms unfolding is_qinv_def by typechk+ @@ -211,8 +211,8 @@ using [[debug_typechk]] back \ \Typechecking/inference goes too far here. Problem would likely be solved with definitional unfolding\ \<^item> by (fact \f:_\) - \<^item> by (rule p\<^sub>2\<^sub>2_of_is_qinv) - \<^item> by (rule p\<^sub>2\<^sub>1_of_is_qinv) + \<^item> by (rule sec_of_is_qinv) + \<^item> by (rule ret_of_is_qinv) done Lemma (def) funcomp_is_qinv: @@ -251,7 +251,7 @@ definition "is_biinv A B f \ (\g: B \ A. homotopy A (fn _. A) (g \\<^bsub>A\<^esub> f) (id A)) \ (\g: B \ A. homotopy B (fn _. B) (f \\<^bsub>B\<^esub> g) (id B))" -lemma is_biinv_type [typechk]: +lemma is_biinv_type [type]: assumes "A: U i" "B: U i" "f: A \ B" shows "is_biinv A B f: U i" unfolding is_biinv_def by typechk @@ -273,13 +273,13 @@ Lemma is_biinvI: show ": {}" by typechk qed -Lemma is_biinv_components [typechk]: +Lemma is_biinv_components [type]: assumes "A: U i" "B: U i" "f: A \ B" "pf: is_biinv f" shows - p\<^sub>1\<^sub>1_of_is_biinv: "p\<^sub>1\<^sub>1 pf: B \ A" and - p\<^sub>2\<^sub>1_of_is_biinv: "p\<^sub>2\<^sub>1 pf: B \ A" and - p\<^sub>1\<^sub>2_of_is_biinv: "p\<^sub>1\<^sub>2 pf: p\<^sub>1\<^sub>1 pf \ f ~ id A" and - p\<^sub>2\<^sub>2_of_is_biinv: "p\<^sub>2\<^sub>2 pf: f \ p\<^sub>2\<^sub>1 pf ~ id B" + section_of_is_biinv: "p\<^sub>1\<^sub>1 pf: B \ A" and + retraction_of_is_biinv: "p\<^sub>2\<^sub>1 pf: B \ A" and + ret_of_is_biinv: "p\<^sub>1\<^sub>2 pf: p\<^sub>1\<^sub>1 pf \ f ~ id A" and + sec_of_is_biinv: "p\<^sub>2\<^sub>2 pf: f \ p\<^sub>2\<^sub>1 pf ~ id B" using assms unfolding is_biinv_def by typechk+ @@ -350,7 +350,7 @@ text \ definition equivalence (infix "\" 110) where "A \ B \ \f: A \ B. Equivalence.is_biinv A B f" -lemma equivalence_type [typechk]: +lemma equivalence_type [type]: assumes "A: U i" "B: U i" shows "A \ B: U i" unfolding equivalence_def by typechk @@ -376,7 +376,7 @@ Lemma (def) equivalence_symmetric: apply elim apply (dest (4) is_biinv_imp_is_qinv) apply intro - \<^item> by (rule fst_of_is_qinv) facts + \<^item> by (rule qinv_of_is_qinv) facts \<^item> by (rule is_qinv_imp_is_biinv) (rule qinv_is_qinv) done diff --git a/hott/Identity.thy b/hott/Identity.thy index d6efbf8..b9ebafb 100644 --- a/hott/Identity.thy +++ b/hott/Identity.thy @@ -41,7 +41,7 @@ axiomatization where lemmas [form] = IdF and - [intro, intros] = IdI and + [intr, intro] = IdI and [elim ?p ?a ?b] = IdE and [comp] = Id_comp and [refl] = IdI @@ -567,7 +567,7 @@ interpretation \2: notation \2.horiz_pathcomp (infix "\" 121) notation \2.horiz_pathcomp' (infix "\''" 121) -Lemma [typechk]: +Lemma [type]: assumes "\: \2 A a" and "\: \2 A a" shows horiz_pathcomp_type: "\ \ \: \2 A a" and horiz_pathcomp'_type: "\ \' \: \2 A a" diff --git a/hott/Nat.thy b/hott/Nat.thy index fd567f3..716703a 100644 --- a/hott/Nat.thy +++ b/hott/Nat.thy @@ -39,7 +39,7 @@ where lemmas [form] = NatF and - [intro, intros] = Nat_zero Nat_suc and + [intr, intro] = Nat_zero Nat_suc and [elim "?n"] = NatE and [comp] = Nat_comp_zero Nat_comp_suc @@ -62,7 +62,7 @@ subsection \Addition\ definition add (infixl "+" 120) where "m + n \ NatRec Nat m (K suc) n" -lemma add_type [typechk]: +lemma add_type [type]: assumes "m: Nat" "n: Nat" shows "m + n: Nat" unfolding add_def by typechk @@ -123,7 +123,7 @@ subsection \Multiplication\ definition mul (infixl "*" 121) where "m * n \ NatRec Nat 0 (K $ add m) n" -lemma mul_type [typechk]: +lemma mul_type [type]: assumes "m: Nat" "n: Nat" shows "m * n: Nat" unfolding mul_def by typechk diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy index 27edd51..180354c 100644 --- a/spartan/core/Spartan.thy +++ b/spartan/core/Spartan.thy @@ -188,16 +188,15 @@ ML_file \context_tactical.ML\ subsection \Type-checking/inference\ -named_theorems form and intro and intros and comp and typechk -\ \`intros` stores the introduction rule variants used by the - `intro` and `intros` methods.\ +\ \Rule attributes for the type-checker\ +named_theorems form and intr and comp and type -ML_file \elimination.ML\ \ \elimination rules\ +\ \Defines elimination automation and the `elim` attribute\ +ML_file \elimination.ML\ lemmas [form] = PiF SigF and - [intro] = PiI SigI and - [intros] = PiI[rotated] SigI and + [intr] = PiI SigI and [elim ?f] = PiE and [elim ?p] = SigE and [comp] = beta Sig_comp and @@ -222,6 +221,10 @@ ML_file \goals.ML\ subsection \Proof methods\ +named_theorems intro \ \Logical introduction rules\ + +lemmas [intro] = PiI[rotated] SigI + ML_file \cases.ML\ \ \case reasoning rules\ ML_file \tactics.ML\ @@ -394,7 +397,7 @@ syntax translations "g \\<^bsub>A\<^esub> f" \ "CONST funcomp A g f" -lemma funcompI [typechk]: +lemma funcompI [type]: assumes "A: U i" "B: U i" @@ -444,7 +447,7 @@ subsection \Identity function\ abbreviation id where "id A \ \x: A. x" lemma - id_type [typechk]: "A: U i \ id A: A \ A" and + id_type [type]: "A: U i \ id A: A \ A" and id_comp [comp]: "x: A \ (id A) x \ x" \ \for the occasional manual rewrite\ by reduce+ @@ -458,7 +461,7 @@ lemma id_right [comp]: shows "f \\<^bsub>A\<^esub> (id A) \ f" by (subst eta_exp[of f]) (reduce, rule eta) -lemma id_U [typechk]: +lemma id_U [type]: "id (U i): U i \ U i" using Ui_in_USi by typechk @@ -468,7 +471,7 @@ section \Pairs\ definition "fst A B \ \p: \x: A. B x. SigInd A B (fn _. A) (fn x y. x) p" definition "snd A B \ \p: \x: A. B x. SigInd A B (fn p. B (fst A B p)) (fn x y. y) p" -lemma fst_type [typechk]: +lemma fst_type [type]: assumes "A: U i" "\x. x: A \ B x: U i" shows "fst A B: (\x: A. B x) \ A" unfolding fst_def by typechk @@ -479,7 +482,7 @@ lemma fst_comp [comp]: shows "fst A B \ a" unfolding fst_def by reduce -lemma snd_type [typechk]: +lemma snd_type [type]: assumes "A: U i" "\x. x: A \ B x: U i" shows "snd A B: \p: \x: A. B x. B (fst A B p)" unfolding snd_def by typechk reduce @@ -503,14 +506,14 @@ translations subsection \Projections\ -Lemma fst [typechk]: +Lemma fst [type]: assumes "A: U i" "\x. x: A \ B x: U i" "p: \x: A. B x" shows "fst p: A" by typechk -Lemma snd [typechk]: +Lemma snd [type]: assumes "A: U i" "\x. x: A \ B x: U i" "p: \x: A. B x" diff --git a/spartan/core/goals.ML b/spartan/core/goals.ML index 540f5c7..a04bd0e 100644 --- a/spartan/core/goals.ML +++ b/spartan/core/goals.ML @@ -151,7 +151,7 @@ fun gen_schematic_theorem map (apsnd (map (Local_Defs.fold new_lthy prf_tm_defs))) res in Local_Theory.notes_kind kind - [((name, @{attributes [typechk]} @ atts), + [((name, @{attributes [type]} @ atts), [(maps #2 res_folded, [])])] new_lthy end diff --git a/spartan/core/tactics.ML b/spartan/core/tactics.ML index 19d3d71..959050e 100644 --- a/spartan/core/tactics.ML +++ b/spartan/core/tactics.ML @@ -57,7 +57,7 @@ end (*Applies some introduction rule*) fun intro_ctac i (ctxt, st) = TACTIC_CONTEXT ctxt (resolve_tac ctxt - (Named_Theorems.get ctxt \<^named_theorems>\intros\) i st) + (Named_Theorems.get ctxt \<^named_theorems>\intro\) i st) (* Induction/elimination *) diff --git a/spartan/core/typechecking.ML b/spartan/core/typechecking.ML index a6e1726..b7a7f9b 100644 --- a/spartan/core/typechecking.ML +++ b/spartan/core/typechecking.ML @@ -37,8 +37,7 @@ fun put_types typings = foldr1 (op o) (map put_type typings) (* Context tactics for type-checking *) -val debug_typechk = - Attrib.setup_config_bool \<^binding>\debug_typechk\ (K false) +val debug_typechk = Attrib.setup_config_bool \<^binding>\debug_typechk\ (K false) fun debug_tac ctxt s = if Config.get ctxt debug_typechk then print_tac ctxt s else all_tac @@ -73,9 +72,9 @@ fun check_infer_step facts i (ctxt, st) = map (Simplifier.norm_hhf ctxt) facts (*MAYBE FIXME: Remove `typechk` from this list, and instead perform definitional unfolding to (w?)hnf.*) - @(Named_Theorems.get ctxt \<^named_theorems>\typechk\) + @(Named_Theorems.get ctxt \<^named_theorems>\type\) @(Named_Theorems.get ctxt \<^named_theorems>\form\) - @(Named_Theorems.get ctxt \<^named_theorems>\intro\) + @(Named_Theorems.get ctxt \<^named_theorems>\intr\) @(map #1 (Elim.rules ctxt))) in (resolve_from_net_tac ctxt net) i end else no_tac) diff --git a/spartan/lib/List.thy b/spartan/lib/List.thy index 34873e4..dd51582 100644 --- a/spartan/lib/List.thy +++ b/spartan/lib/List.thy @@ -45,7 +45,7 @@ where lemmas [form] = ListF and - [intro, intros] = List_nil List_cons and + [intr, intro] = List_nil List_cons and [elim "?xs"] = ListE and [comp] = List_comp_nil List_comp_cons @@ -106,7 +106,7 @@ translations "head" \ "CONST List.head A" "tail" \ "CONST List.tail A" -Lemma head_type [typechk]: +Lemma head_type [type]: assumes "A: U i" "xs: List A" shows "head xs: Maybe A" unfolding head_def by typechk @@ -116,7 +116,7 @@ Lemma head_of_cons [comp]: shows "head (x # xs) \ some x" unfolding head_def by reduce -Lemma tail_type [typechk]: +Lemma tail_type [type]: assumes "A: U i" "xs: List A" shows "tail xs: List A" unfolding tail_def by typechk @@ -157,7 +157,7 @@ definition map_i ("map") where [implicit]: "map \ List.map ? ?" translations "map" \ "CONST List.map A B" -Lemma map_type [typechk]: +Lemma map_type [type]: assumes "A: U i" "B: U i" "f: A \ B" "xs: List A" shows "map f xs: List B" unfolding map_def by typechk @@ -177,7 +177,7 @@ definition rev_i ("rev") where [implicit]: "rev \ List.rev ?" translations "rev" \ "CONST List.rev A" -Lemma rev_type [typechk]: +Lemma rev_type [type]: assumes "A: U i" "xs: List A" shows "rev xs: List A" unfolding rev_def by typechk diff --git a/spartan/lib/Maybe.thy b/spartan/lib/Maybe.thy index a2e1638..0a7ec21 100644 --- a/spartan/lib/Maybe.thy +++ b/spartan/lib/Maybe.thy @@ -56,7 +56,7 @@ Lemma Maybe_comp_some: lemmas [form] = MaybeF and - [intro, intros] = Maybe_none Maybe_some and + [intr, intro] = Maybe_none Maybe_some and [comp] = Maybe_comp_none Maybe_comp_some and MaybeE [elim "?m"] = MaybeInd[rotated 4] lemmas diff --git a/spartan/lib/Prelude.thy b/spartan/lib/Prelude.thy index 36f12d2..6adbce8 100644 --- a/spartan/lib/Prelude.thy +++ b/spartan/lib/Prelude.thy @@ -43,8 +43,8 @@ axiomatization where lemmas [form] = SumF and - [intro] = Sum_inl Sum_inr and - [intros] = Sum_inl[rotated] Sum_inr[rotated] and + [intr] = Sum_inl Sum_inr and + [intro] = Sum_inl[rotated] Sum_inr[rotated] and [elim ?s] = SumE and [comp] = Sum_comp_inl Sum_comp_inr @@ -79,7 +79,7 @@ and lemmas [form] = TopF BotF and - [intro, intros] = TopI and + [intr, intro] = TopI and [elim ?a] = TopE and [elim ?x] = BotE and [comp] = Top_comp @@ -129,7 +129,7 @@ Lemma if_false: lemmas [form] = BoolF and - [intro, intros] = Bool_true Bool_false and + [intr, intro] = Bool_true Bool_false and [comp] = if_true if_false and [elim ?x] = ifelse lemmas -- cgit v1.2.3