I've often find myself needing to record a side condition before applying a lemma, like in the following context:
Γ: list context_decl n: nat d: context_decl cl: is_closed_context Γ ===================== nth_error Γ n = Some d -> ws_decl Γ (lift_decl (S n) 0 d)
I'd like to apply a lemma (using
move/) that uses my hypothesis cl and consumes the first hypothesis, but latter I need the fact that
n < #|Gamma|. I always first introduce the
nth hypothesis and add an appropriate
have lenGamman lemma to complete my proof, but I feel there must be a simpler way to just enrich the goal with any result that follows from the first hypothesis
nth_error Γ n = Some d
In the current version of mathcomp, you can use
/[dup] to duplicate the top assumption.
Goal forall (A B C: Prop), (A -> B) -> A -> (A -> B -> C) -> C. Proof. move=> A B C AB /[dup] /AB b a. by apply. Qed.
And dup can easily be defined as:
Notation "[dup]" := (ltac:(let H := fresh in (move=> H; generalize H; move: H))).
These are actually in Coq 8.13 but you can "backport" the thing easily since "tactics as view" were added to SSR in Coq 8.10
@Cyril Cohen added them to mathcomp first, and ported them to Coq for 8.13
I meant, you can run last mathcomp on any "recent" Coq, or no mathcomp and Coq 8.13. (or backport it yourself, as you found out)
Last updated: Feb 08 2023 at 07:02 UTC