Stream: math-comp users

Topic: Idiom with nth_error


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Mar 12 2021 at 17:53):

Cool, thanks!

view this post on Zulip 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))).

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Mar 12 2021 at 18:43):

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

view this post on Zulip 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