diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Reflection/ExprInversion.v | 3 | ||||
-rw-r--r-- | src/Reflection/InlineWf.v | 2 | ||||
-rw-r--r-- | src/Util/PartiallyReifiedProp.v | 4 | ||||
-rw-r--r-- | src/Util/Tactics.v | 148 | ||||
-rw-r--r-- | src/Util/Tactics/BreakMatch.v | 116 | ||||
-rw-r--r-- | src/Util/Tactics/DestructHead.v | 29 | ||||
-rw-r--r-- | src/Util/Tactics/DestructHyps.v | 48 | ||||
-rw-r--r-- | src/Util/Tactics/Head.v | 10 | ||||
-rw-r--r-- | src/Util/Tactics/SpecializeBy.v | 33 | ||||
-rw-r--r-- | src/Util/Tactics/SplitInContext.v | 22 | ||||
-rw-r--r-- | src/Util/Tuple.v | 4 |
11 files changed, 273 insertions, 146 deletions
diff --git a/src/Reflection/ExprInversion.v b/src/Reflection/ExprInversion.v index 2c2533454..06a4f5b30 100644 --- a/src/Reflection/ExprInversion.v +++ b/src/Reflection/ExprInversion.v @@ -1,7 +1,8 @@ Require Import Crypto.Reflection.Syntax. Require Import Crypto.Util.Sigma. Require Import Crypto.Util.Option. -Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Notations. Section language. diff --git a/src/Reflection/InlineWf.v b/src/Reflection/InlineWf.v index dd0fb08a3..5b9f27f48 100644 --- a/src/Reflection/InlineWf.v +++ b/src/Reflection/InlineWf.v @@ -2,7 +2,7 @@ Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.WfProofs. Require Import Crypto.Reflection.Inline. -Require Import Crypto.Util.Tactics Crypto.Util.Sigma Crypto.Util.Prod. +Require Import Crypto.Util.Tactics.SpecializeBy Crypto.Util.Tactics.DestructHead Crypto.Util.Sigma Crypto.Util.Prod. Local Open Scope ctype_scope. Section language. diff --git a/src/Util/PartiallyReifiedProp.v b/src/Util/PartiallyReifiedProp.v index ef1567bd8..023bcb9e0 100644 --- a/src/Util/PartiallyReifiedProp.v +++ b/src/Util/PartiallyReifiedProp.v @@ -5,7 +5,9 @@ Require Import Coq.Setoids.Setoid. Require Import Coq.Program.Tactics. Require Import Crypto.Util.Notations. -Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.DestructHyps. +Require Import Crypto.Util.Tactics.BreakMatch. Delimit Scope reified_prop_scope with reified_prop. Inductive reified_Prop := rTrue | rFalse | rAnd (x y : reified_Prop) | rOr (x y : reified_Prop) | rImpl (x y : reified_Prop) | rForall {T} (f : T -> reified_Prop) | rEq {T} (x y : T) | inject (_ : Prop). diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index 128fdcfd0..e6f5a1cac 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -1,5 +1,11 @@ (** * Generic Tactics *) Require Export Crypto.Util.FixCoqMistakes. +Require Export Crypto.Util.Tactics.BreakMatch. +Require Export Crypto.Util.Tactics.Head. +Require Export Crypto.Util.Tactics.DestructHyps. +Require Export Crypto.Util.Tactics.DestructHead. +Require Export Crypto.Util.Tactics.SpecializeBy. +Require Export Crypto.Util.Tactics.SplitInContext. (** Test if a tactic succeeds, but always roll-back the results *) Tactic Notation "test" tactic3(tac) := @@ -11,15 +17,6 @@ Tactic Notation "not" tactic3(tac) := try ((test tac); fail 1 tac "succeeds"). Ltac get_goal := match goal with |- ?G => G end. -(** find the head of the given expression *) -Ltac head expr := - match expr with - | ?f _ => head f - | _ => expr - end. - -Ltac head_hnf expr := let expr' := eval hnf in expr in head expr'. - (** [contains x expr] succeeds iff [x] appears in [expr] *) Ltac contains search_for in_term := idtac; @@ -63,59 +60,6 @@ Ltac subst_evars := Ltac subst_let := repeat match goal with | x := _ |- _ => subst x end. -(** destruct discriminees of [match]es in the goal *) -(* Prioritize breaking apart things in the context, then things which - don't need equations, then simple matches (which can be displayed - as [if]s), and finally matches in general. *) -Ltac break_match_step only_when := - match goal with - | [ |- appcontext[match ?e with _ => _ end] ] - => only_when e; is_var e; destruct e - | [ |- appcontext[match ?e with _ => _ end] ] - => only_when e; - match type of e with - | sumbool _ _ => destruct e - end - | [ |- appcontext[if ?e then _ else _] ] - => only_when e; destruct e eqn:? - | [ |- appcontext[match ?e with _ => _ end] ] - => only_when e; destruct e eqn:? - end. -Ltac break_match_hyps_step only_when := - match goal with - | [ H : appcontext[match ?e with _ => _ end] |- _ ] - => only_when e; is_var e; destruct e - | [ H : appcontext[match ?e with _ => _ end] |- _ ] - => only_when e; - match type of e with - | sumbool _ _ => destruct e - end - | [ H : appcontext[if ?e then _ else _] |- _ ] - => only_when e; destruct e eqn:? - | [ H : appcontext[match ?e with _ => _ end] |- _ ] - => only_when e; destruct e eqn:? - end. -Ltac break_match := repeat break_match_step ltac:(fun _ => idtac). -Ltac break_match_hyps := repeat break_match_hyps_step ltac:(fun _ => idtac). -Ltac break_match_when_head_step T := - break_match_step - ltac:(fun e => let T' := type of e in - let T' := head T' in - constr_eq T T'). -Ltac break_match_hyps_when_head_step T := - break_match_hyps_step - ltac:(fun e => let T' := type of e in - let T' := head T' in - constr_eq T T'). -Ltac break_match_when_head T := repeat break_match_when_head_step T. -Ltac break_match_hyps_when_head T := repeat break_match_hyps_when_head_step T. -Ltac break_innermost_match_step := - break_match_step ltac:(fun v => lazymatch v with - | appcontext[match _ with _ => _ end] => fail - | _ => idtac - end). -Ltac break_innermost_match := repeat break_innermost_match_step. - Ltac free_in x y := idtac; match y with @@ -211,86 +155,6 @@ Ltac inversion_all_matches matcher := inversion_all_matches_then matcher ltac:( Ltac inversion_one_match matcher := inversion_one_match_then matcher ltac:( simpl in * ). Ltac inversion_all_matches' matcher := inversion_all_matches_then matcher idtac. -(* matches anything whose type has a [T] in it *) -Ltac destruct_type_matcher T HT := - match HT with - | context[T] => idtac - end. -Ltac destruct_type T := destruct_all_matches ltac:(destruct_type_matcher T). -Ltac destruct_type' T := destruct_all_matches' ltac:(destruct_type_matcher T). - -Ltac destruct_head_matcher T HT := - match head HT with - | T => idtac - end. -Ltac destruct_head T := destruct_all_matches ltac:(destruct_head_matcher T). -Ltac destruct_one_head T := destruct_one_match ltac:(destruct_head_matcher T). -Ltac destruct_head' T := destruct_all_matches' ltac:(destruct_head_matcher T). - -Ltac inversion_head T := inversion_all_matches ltac:(destruct_head_matcher T). -Ltac inversion_one_head T := inversion_one_match ltac:(destruct_head_matcher T). -Ltac inversion_head' T := inversion_all_matches' ltac:(destruct_head_matcher T). - - -Ltac head_hnf_matcher T HT := - match head_hnf HT with - | T => idtac - end. -Ltac destruct_head_hnf T := destruct_all_matches ltac:(head_hnf_matcher T). -Ltac destruct_one_head_hnf T := destruct_one_match ltac:(head_hnf_matcher T). -Ltac destruct_head_hnf' T := destruct_all_matches' ltac:(head_hnf_matcher T). - -Ltac inversion_head_hnf T := inversion_all_matches ltac:(head_hnf_matcher T). -Ltac inversion_one_head_hnf T := inversion_one_match ltac:(head_hnf_matcher T). -Ltac inversion_head_hnf' T := inversion_all_matches' ltac:(head_hnf_matcher T). - -Ltac destruct_sig_matcher HT := - match eval hnf in HT with - | ex _ => idtac - | ex2 _ _ => idtac - | sig _ => idtac - | sig2 _ _ => idtac - | sigT _ => idtac - | sigT2 _ _ => idtac - | and _ _ => idtac - | prod _ _ => idtac - end. -Ltac destruct_sig := destruct_all_matches destruct_sig_matcher. -Ltac destruct_sig' := destruct_all_matches' destruct_sig_matcher. - -Ltac transparent_specialize_one H arg := - first [ let test := eval unfold H in H in idtac; - let H' := fresh in rename H into H'; pose (H' arg) as H; subst H' - | specialize (H arg) ]. - -(** try to specialize all non-dependent hypotheses using [tac], maintaining transparency *) -Ltac specialize_by' tac := - idtac; - match goal with - | [ H : ?A -> ?B |- _ ] => - match type of A with - Prop => - let H' := fresh in - assert (H' : A) by tac; - transparent_specialize_one H H'; - try clear H' (* if [H] was transparent, [H'] will remain *) - end - end. - -Ltac specialize_by tac := repeat specialize_by' tac. - -(** [specialize_by auto] should not mean [specialize_by ltac:( auto - with * )]!!!!!!! (see - https://coq.inria.fr/bugs/show_bug.cgi?id=4966) We fix this design - flaw. *) -Tactic Notation "specialize_by" tactic3(tac) := specialize_by tac. - -(** A marginally faster version of [specialize_by assumption] *) -Ltac specialize_by_assumption := - repeat match goal with - | [ H : ?T, H' : (?T -> ?U)%type |- _ ] => specialize (H' H) - end. - (** If [tac_in H] operates in [H] and leaves side-conditions before the original goal, then [side_conditions_before_to_side_conditions_after tac_in H] does diff --git a/src/Util/Tactics/BreakMatch.v b/src/Util/Tactics/BreakMatch.v new file mode 100644 index 000000000..5ad882c6f --- /dev/null +++ b/src/Util/Tactics/BreakMatch.v @@ -0,0 +1,116 @@ +Require Export Crypto.Util.FixCoqMistakes. +Require Import Crypto.Util.Tactics.Head. + +(** destruct discriminees of [match]es in the goal *) +(* Prioritize breaking apart things in the context, then things which + don't need equations, then simple matches (which can be displayed + as [if]s), and finally matches in general. *) +Ltac set_match_refl v' only_when := + lazymatch goal with + | [ |- context G[match ?e with _ => _ end eq_refl] ] + => only_when e; + let T := fresh in + evar (T : Type); evar (v' : T); + subst T; + let vv := (eval cbv delta [v'] in v') in + let G' := context G[vv] in + let G''' := context G[v'] in + lazymatch goal with |- ?G'' => unify G' G'' end; + change G''' + end. +Ltac set_match_refl_hyp v' only_when := + lazymatch goal with + | [ H : context G[match ?e with _ => _ end eq_refl] |- _ ] + => only_when e; + let T := fresh in + evar (T : Type); evar (v' : T); + subst T; + let vv := (eval cbv delta [v'] in v') in + let G' := context G[vv] in + let G''' := context G[v'] in + let G'' := type of H in + unify G' G''; + change G''' in H + end. +Ltac destruct_by_existing_equation match_refl_hyp := + let v := (eval cbv delta [match_refl_hyp] in match_refl_hyp) in + lazymatch v with + | match ?e with _ => _ end (@eq_refl ?T ?e) + => let H := fresh in + let e' := fresh in + pose e as e'; + change e with e' in (value of match_refl_hyp) at 1; + first [ pose (@eq_refl T e : e = e') as H; + change (@eq_refl T e) with H in (value of match_refl_hyp); + clearbody H e' + | pose (@eq_refl T e : e' = e) as H; + change (@eq_refl T e) with H in (value of match_refl_hyp); + clearbody H e' ]; + destruct e'; subst match_refl_hyp + end. +Ltac destruct_rewrite_sumbool e := + let H := fresh in + destruct e as [H|H]; + try lazymatch type of H with + | ?LHS = ?RHS + => rewrite ?H; rewrite ?H in *; + repeat match goal with + | [ |- context G[LHS] ] + => let LHS' := fresh in + pose LHS as LHS'; + let G' := context G[LHS'] in + change G'; + replace LHS' with RHS by (subst LHS'; symmetry; apply H); + subst LHS' + end + end. +Ltac break_match_step only_when := + match goal with + | [ |- appcontext[match ?e with _ => _ end] ] + => only_when e; is_var e; destruct e + | [ |- appcontext[match ?e with _ => _ end] ] + => only_when e; + match type of e with + | sumbool _ _ => destruct_rewrite_sumbool e + end + | [ |- appcontext[if ?e then _ else _] ] + => only_when e; destruct e eqn:? + | [ |- appcontext[match ?e with _ => _ end] ] + => only_when e; destruct e eqn:? + | _ => let v := fresh in set_match_refl v only_when; destruct_by_existing_equation v + end. +Ltac break_match_hyps_step only_when := + match goal with + | [ H : appcontext[match ?e with _ => _ end] |- _ ] + => only_when e; is_var e; destruct e + | [ H : appcontext[match ?e with _ => _ end] |- _ ] + => only_when e; + match type of e with + | sumbool _ _ => destruct_rewrite_sumbool e + end + | [ H : appcontext[if ?e then _ else _] |- _ ] + => only_when e; destruct e eqn:? + | [ H : appcontext[match ?e with _ => _ end] |- _ ] + => only_when e; destruct e eqn:? + | _ => let v := fresh in set_match_refl_hyp v only_when; destruct_by_existing_equation v + end. +Ltac break_match := repeat break_match_step ltac:(fun _ => idtac). +Ltac break_match_hyps := repeat break_match_hyps_step ltac:(fun _ => idtac). +Ltac break_match_when_head_step T := + break_match_step + ltac:(fun e => let T' := type of e in + let T' := head T' in + constr_eq T T'). +Ltac break_match_hyps_when_head_step T := + break_match_hyps_step + ltac:(fun e => let T' := type of e in + let T' := head T' in + constr_eq T T'). +Ltac break_match_when_head T := repeat break_match_when_head_step T. +Ltac break_match_hyps_when_head T := repeat break_match_hyps_when_head_step T. +Ltac break_innermost_match_step := + break_match_step ltac:(fun v => lazymatch v with + | appcontext[match _ with _ => _ end] => fail + | _ => idtac + end). +Ltac break_innermost_match := repeat break_innermost_match_step. diff --git a/src/Util/Tactics/DestructHead.v b/src/Util/Tactics/DestructHead.v new file mode 100644 index 000000000..5620a72c9 --- /dev/null +++ b/src/Util/Tactics/DestructHead.v @@ -0,0 +1,29 @@ +Require Export Crypto.Util.FixCoqMistakes. + +Require Import Crypto.Util.Tactics.Head. +Require Import Crypto.Util.Tactics.DestructHyps. + +Ltac destruct_head_matcher T HT := + match head HT with + | T => idtac + end. +Ltac destruct_head T := destruct_all_matches ltac:(destruct_head_matcher T). +Ltac destruct_one_head T := destruct_one_match ltac:(destruct_head_matcher T). +Ltac destruct_head' T := destruct_all_matches' ltac:(destruct_head_matcher T). + +Ltac inversion_head T := inversion_all_matches ltac:(destruct_head_matcher T). +Ltac inversion_one_head T := inversion_one_match ltac:(destruct_head_matcher T). +Ltac inversion_head' T := inversion_all_matches' ltac:(destruct_head_matcher T). + + +Ltac head_hnf_matcher T HT := + match head_hnf HT with + | T => idtac + end. +Ltac destruct_head_hnf T := destruct_all_matches ltac:(head_hnf_matcher T). +Ltac destruct_one_head_hnf T := destruct_one_match ltac:(head_hnf_matcher T). +Ltac destruct_head_hnf' T := destruct_all_matches' ltac:(head_hnf_matcher T). + +Ltac inversion_head_hnf T := inversion_all_matches ltac:(head_hnf_matcher T). +Ltac inversion_one_head_hnf T := inversion_one_match ltac:(head_hnf_matcher T). +Ltac inversion_head_hnf' T := inversion_all_matches' ltac:(head_hnf_matcher T). diff --git a/src/Util/Tactics/DestructHyps.v b/src/Util/Tactics/DestructHyps.v new file mode 100644 index 000000000..8ab6215c2 --- /dev/null +++ b/src/Util/Tactics/DestructHyps.v @@ -0,0 +1,48 @@ +Require Export Crypto.Util.FixCoqMistakes. + +(** given a [matcher] that succeeds on some hypotheses and fails on + others, destruct any matching hypotheses, and then execute [tac] + after each [destruct]. + + The [tac] part exists so that you can, e.g., [simpl in *], to + speed things up. *) +Ltac do_one_match_then matcher do_tac tac := + idtac; + match goal with + | [ H : ?T |- _ ] + => matcher T; do_tac H; + try match type of H with + | T => clear H + end; + tac + end. + +Ltac do_all_matches_then matcher do_tac tac := + repeat do_one_match_then matcher do_tac tac. + +Ltac destruct_all_matches_then matcher tac := + do_all_matches_then matcher ltac:(fun H => destruct H) tac. +Ltac destruct_one_match_then matcher tac := + do_one_match_then matcher ltac:(fun H => destruct H) tac. + +Ltac inversion_all_matches_then matcher tac := + do_all_matches_then matcher ltac:(fun H => inversion H; subst) tac. +Ltac inversion_one_match_then matcher tac := + do_one_match_then matcher ltac:(fun H => inversion H; subst) tac. + +Ltac destruct_all_matches matcher := + destruct_all_matches_then matcher ltac:( simpl in * ). +Ltac destruct_one_match matcher := destruct_one_match_then matcher ltac:( simpl in * ). +Ltac destruct_all_matches' matcher := destruct_all_matches_then matcher idtac. + +Ltac inversion_all_matches matcher := inversion_all_matches_then matcher ltac:( simpl in * ). +Ltac inversion_one_match matcher := inversion_one_match_then matcher ltac:( simpl in * ). +Ltac inversion_all_matches' matcher := inversion_all_matches_then matcher idtac. + +(* matches anything whose type has a [T] in it *) +Ltac destruct_type_matcher T HT := + match HT with + | context[T] => idtac + end. +Ltac destruct_type T := destruct_all_matches ltac:(destruct_type_matcher T). +Ltac destruct_type' T := destruct_all_matches' ltac:(destruct_type_matcher T). diff --git a/src/Util/Tactics/Head.v b/src/Util/Tactics/Head.v new file mode 100644 index 000000000..fa7a301d6 --- /dev/null +++ b/src/Util/Tactics/Head.v @@ -0,0 +1,10 @@ +Require Export Crypto.Util.FixCoqMistakes. + +(** find the head of the given expression *) +Ltac head expr := + match expr with + | ?f _ => head f + | _ => expr + end. + +Ltac head_hnf expr := let expr' := eval hnf in expr in head expr'. diff --git a/src/Util/Tactics/SpecializeBy.v b/src/Util/Tactics/SpecializeBy.v new file mode 100644 index 000000000..72cf5d52f --- /dev/null +++ b/src/Util/Tactics/SpecializeBy.v @@ -0,0 +1,33 @@ +Require Export Crypto.Util.FixCoqMistakes. + +Ltac transparent_specialize_one H arg := + first [ let test := eval unfold H in H in idtac; + let H' := fresh in rename H into H'; pose (H' arg) as H; subst H' + | specialize (H arg) ]. + +(** try to specialize all non-dependent hypotheses using [tac], maintaining transparency *) +Ltac guarded_specialize_by' tac guard_tac := + idtac; + match goal with + | [ H : ?A -> ?B |- _ ] + => guard_tac H; + let H' := fresh in + assert (H' : A) by tac; + transparent_specialize_one H H'; + try clear H' (* if [H] was transparent, [H'] will remain *) + end. +Ltac specialize_by' tac := guarded_specialize_by' tac ltac:(fun _ => idtac). + +Ltac specialize_by tac := repeat specialize_by' tac. + +(** [specialize_by auto] should not mean [specialize_by ( auto + with * )]!!!!!!! (see + https://coq.inria.fr/bugs/show_bug.cgi?id=4966) We fix this design + flaw. *) +Tactic Notation "specialize_by" tactic3(tac) := specialize_by tac. + +(** A marginally faster version of [specialize_by assumption] *) +Ltac specialize_by_assumption := + repeat match goal with + | [ H : ?T, H' : (?T -> ?U)%type |- _ ] => specialize (H' H) + end. diff --git a/src/Util/Tactics/SplitInContext.v b/src/Util/Tactics/SplitInContext.v new file mode 100644 index 000000000..c2bf364a0 --- /dev/null +++ b/src/Util/Tactics/SplitInContext.v @@ -0,0 +1,22 @@ +Require Export Crypto.Util.FixCoqMistakes. + +(* Coq's build in tactics don't work so well with things like [iff] + so split them up into multiple hypotheses *) +Ltac split_in_context_by ident funl funr tac := + repeat match goal with + | [ H : context p [ident] |- _ ] => + let H0 := context p[funl] in let H0' := eval simpl in H0 in assert H0' by (tac H); + let H1 := context p[funr] in let H1' := eval simpl in H1 in assert H1' by (tac H); + clear H + end. +Ltac split_in_context ident funl funr := + split_in_context_by ident funl funr ltac:(fun H => apply H). + +Ltac split_iff := split_in_context iff (fun a b : Prop => a -> b) (fun a b : Prop => b -> a). + +Ltac split_and' := + repeat match goal with + | [ H : ?a /\ ?b |- _ ] => let H0 := fresh in let H1 := fresh in + assert (H0 := fst H); assert (H1 := snd H); clear H + end. +Ltac split_and := split_and'; split_in_context and (fun a b : Type => a) (fun a b : Type => b). diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index d1e0177f2..b8a5c2738 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -3,7 +3,9 @@ Require Import Coq.Relations.Relation_Definitions. Require Import Coq.Lists.List. Require Import Crypto.Util.Option. Require Import Crypto.Util.Prod. -Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Decidable. Require Import Crypto.Util.ListUtil. Require Export Crypto.Util.FixCoqMistakes. |