Stream: math-comp users

Topic: Idiom with nth_error

Matthieu Sozeau (Mar 12 2021 at 11:46):

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

Christian Doczkal (Mar 12 2021 at 12:48):

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.

Matthieu Sozeau (Mar 12 2021 at 17:53):

Cool, thanks!

Matthieu Sozeau (Mar 12 2021 at 17:55):

And dup can easily be defined as:
Notation "[dup]" := (ltac:(let H := fresh in (move=> H; generalize H; move: H))).

Enrico Tassi (Mar 12 2021 at 18:42):

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

Enrico Tassi (Mar 12 2021 at 18:43):

@Cyril Cohen added them to mathcomp first, and ported them to Coq for 8.13

Enrico Tassi (Mar 12 2021 at 18:45):

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