Stream: Coq users

Topic: apply tactic for type with indices


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

view this post on Zulip Guillaume Melquiond (Jun 11 2021 at 07:43):

That is plain inversion, isn't it?

view this post on Zulip Guillaume Melquiond (Jun 11 2021 at 07:44):

Ah no, sorry, misread the ordering.

view this post on Zulip Guillaume Melquiond (Jun 11 2021 at 07:44):

I think the apply tactic from CFML does that.

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

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

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

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

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

view this post on Zulip Paolo Giarrusso (Jun 15 2021 at 04:42):

@spaceloop the equalities come from replace, no?


Last updated: Feb 01 2023 at 11:04 UTC