From 250412bbacb2bf013d94b0b2458120e18c07c8fe Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Tue, 26 Sep 2023 21:47:59 +0200 Subject: [PATCH] clarify efeed a bit and add some tests --- stdpp/tactics.v | 2 +- tests/tactics.ref | 2 ++ tests/tactics.v | 21 +++++++++++++++++++++ 3 files changed, 24 insertions(+), 1 deletion(-) diff --git a/stdpp/tactics.v b/stdpp/tactics.v index 65d7ab7a..cdb7488f 100644 --- a/stdpp/tactics.v +++ b/stdpp/tactics.v @@ -545,7 +545,7 @@ Tactic Notation "efeed_core" constr(H) "using" tactic3(tac) := | ?T1 → ?T2 => let HT1 := fresh "feed" in assert T1 as HT1; [| go (H HT1); clear HT1 ] - | ?T1 → _ => + | ∀ x : ?T1, _ => let e := mk_evar T1 in go (H e) | ?T1 => tac H diff --git a/tests/tactics.ref b/tests/tactics.ref index be6d2967..21ef6edc 100644 --- a/tests/tactics.ref +++ b/tests/tactics.ref @@ -4,3 +4,5 @@ The command has indeed failed with message: Failed to progress. The command has indeed failed with message: Failed to progress. +The command has indeed failed with message: +Failed to progress. diff --git a/tests/tactics.v b/tests/tactics.v index 8272a640..bb2e4680 100644 --- a/tests/tactics.v +++ b/tests/tactics.v @@ -116,3 +116,24 @@ Proof. let f' := get_head (f 0 1 2) in unify f f'. let f' := get_head f in unify f f'. Abort. + +(** (e)feed tests *) +Lemma feed1 (P Q R : Prop) : + P → Q → (P → Q → R) → R. +Proof. + intros HP HQ HR. + feed specialize HR; [exact HP|exact HQ|exact HR]. +Restart. + intros HP HQ HR. + feed pose proof HR as HR'; [exact HP|exact HQ|exact HR']. +Qed. +Lemma efeed1 (P Q R : nat → Prop) : + P 1 → Q 1 → (∀ n, P n → Q n → R n) → R 1. +Proof. + intros HP HQ HR. + Fail progress feed specialize HR. + efeed specialize HR; [exact HP|exact HQ|exact HR]. +Restart. + intros HP HQ HR. + efeed pose proof HR as HR'; [exact HP|exact HQ|exact HR']. +Qed. -- GitLab