## 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.
``````

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: Jul 15 2024 at 20:02 UTC