Stream: Coq users

Topic: apply tactic for type with indices

spaceloop (Jun 11 2021 at 07:30):

Suppose I have an inductive type

Inductive T : nat -> nat -> Type :=
  | T1 : T 0 1
  .

Now I have a value t : T x y. I'd like to have a tactic tac T1, which like apply tries to apply T1, and leaves the goals x = 0 and y = 1. Does this exist?

Guillaume Melquiond (Jun 11 2021 at 07:43):

That is plain inversion, isn't it?

Guillaume Melquiond (Jun 11 2021 at 07:44):

Ah no, sorry, misread the ordering.

Guillaume Melquiond (Jun 11 2021 at 07:44):

I think the apply tactic from CFML does that.

Théo Winterhalter (Jun 11 2021 at 07:51):

Otherwise you can write something by hand that can do the job in at least a few cases.

From Coq Require Import Utf8.

Inductive T : nat → nat → Type :=
| T1 : T 0 1
.

Inductive bar : nat → nat → Type :=
| C : bar 2 2
| D : ∀ x, bar x x
.

Ltac replace_args g :=
  lazymatch g with
  | ?f ?x =>
    let x' := fresh x in
    let t := type of x in
    evar (x' : t) ;
    replace x with x' ; [
      replace_args f ; subst x'
    | subst x'
    ]
  | _ => idtac
  end.

Ltac eqapply ff :=
  lazymatch goal with
  | |- ?g =>
    replace_args g ; [
      eapply ff
    | try reflexivity ..
    ]
  end.

Lemma foo : ∀ x y, T x y.
Proof.
  intros x y.
  eqapply T1.
Abort.

Lemma foo : ∀ x y, bar x y.
Proof.
  intros x y.
  Fail Fail eqapply D. (* Asks for x = y *)
  eqapply C. (* Asks for 2 = x and 2 = y *)
Abort.

Gaëtan Gilbert (Jun 11 2021 at 08:08):

instead of

    evar (x' : t) ;
    replace x with x' ; [
      replace_args f ; subst x'
    | subst x'
    ]

I would do

    let x' := open_constr:(_ : t) in
    replace x with x' ; [replace_args f |]

Yannick Forster (Jun 11 2021 at 10:06):

We used this as an example how to implement tactics using MetaCoq for last year's Coq WS: https://arxiv.org/abs/2006.15135 Usage example: https://github.com/uds-psl/metacoq-examples-coqws/blob/master/test.v

Yannick Forster (Jun 11 2021 at 10:07):

But for your use case, using MetaCoq for this might be overkill and Théo's solution is easier

spaceloop (Jun 14 2021 at 09:21):

Thanks for the responses, I don't completely understand how the ltac approach works yet (what actually introduces the equality types here?). The MetaCoq approach looks good, that's exactly what I've been doing by hand for now.

Paolo Giarrusso (Jun 15 2021 at 04:42):

@spaceloop the equalities come from replace, no?

Last updated: Oct 13 2024 at 01:02 UTC