From 33661a3f6d77fb8ae4ea269f3a2a50c2a93ee163 Mon Sep 17 00:00:00 2001 From: Michael Sammler <noreply@sammler.me> Date: Tue, 26 Jul 2022 16:17:50 +0200 Subject: [PATCH] Add the feed generalizef, efeed generalize, efeed inversion, and efeed destruct tactics --- theories/tactics.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/theories/tactics.v b/theories/tactics.v index d4c143a6..ad120b58 100644 --- a/theories/tactics.v +++ b/theories/tactics.v @@ -548,15 +548,30 @@ Tactic Notation "feed" "specialize" hyp(H) := Tactic Notation "efeed" "specialize" hyp(H) := efeed H using (fun p => specialize p). +Tactic Notation "feed" "generalize" constr(H) := + feed (fun p => let H':=fresh in pose proof p as H'; generalize H') H. +Tactic Notation "efeed" "generalize" constr(H) := + efeed H using (fun p => let H':=fresh in pose proof p as H'; generalize H'). + Tactic Notation "feed" "inversion" constr(H) := feed (fun p => let H':=fresh in pose proof p as H'; inversion H') H. +Tactic Notation "efeed" "inversion" constr(H) := + efeed H using (fun p => let H':=fresh in pose proof p as H'; inversion H'). + Tactic Notation "feed" "inversion" constr(H) "as" simple_intropattern(IP) := feed (fun p => let H':=fresh in pose proof p as H'; inversion H' as IP) H. +Tactic Notation "efeed" "inversion" constr(H) "as" simple_intropattern(IP) := + efeed H using (fun p => let H':=fresh in pose proof p as H'; inversion H' as IP). Tactic Notation "feed" "destruct" constr(H) := feed (fun p => let H':=fresh in pose proof p as H'; destruct H') H. +Tactic Notation "efeed" "destruct" constr(H) := + efeed H using (fun p => let H':=fresh in pose proof p as H'; destruct H'). + Tactic Notation "feed" "destruct" constr(H) "as" simple_intropattern(IP) := feed (fun p => let H':=fresh in pose proof p as H'; destruct H' as IP) H. +Tactic Notation "efeed" "destruct" constr(H) "as" simple_intropattern(IP) := + efeed H using (fun p => let H':=fresh in pose proof p as H'; destruct H' as IP). (** The block definitions are taken from [Coq.Program.Equality] and can be used by tactics to separate their goal from hypotheses they generalize over. *) -- GitLab