2
$\begingroup$

I'm self-studying the Semantics course, and met the following proof script in the warmup directory:

 Lemma step_deterministic e e' e'' :
   step e e' → step e e'' → e' = e''.
 Proof.
   intros Hstep1 Hstep2.
   induction Hstep1 as [ ??? H IH | ??? H IH | | ??? H IH | ??? H IH | ] in e'', Hstep2 |- *.
   { inversion Hstep2; subst.
     + f_equal. by apply IH.
     + exfalso; by eapply no_step_const.
     + exfalso; by eapply no_step_const.
   }
   { inversion Hstep2; subst.
     + exfalso; by eapply no_step_const.
     + f_equal. by apply IH.
     + exfalso; by eapply no_step_const.
   }
   (* you get the idea, let's apply some automation... *)
   (* [naive_solver] is a clever automation tactic by [stdpp] that can solve many simple things. *)
   all: inversion Hstep2; subst; first [ try exfalso; by eapply no_step_const | naive_solver].
 Qed.

What does the part in e'' in induction Hstep1 ... in e'' do? I can understand that we are applying a rule induction on step, and with in e'' the number of the goals reduces down to the number of the rules rather than the square of it.

I also have another small question---what does ??? do, and what is the intention of putting the trailing |- * which seems useless?

EDIT: I now understand that induction Hstep1 ... in e'', Hstep2 |- * is not parsed as induction (Hstep1 ... in e''), Hstep2 |- * but as induction Hstep1 ... in (e'', Hstep2 |- *). Also, I found that

  generalize dependent e''.
  induction H_step1; intros.

works as well. What I still don't understand is the purpose of the |- * in this specific example.

Improve this question
$\endgroup$
4
  • 1
    $\begingroup$ The |- is a special token used to indicate the premises (before this token) and goals (after this token) in Coq. So e'', Hstep2 |- * selects the premises e'' and Hstep2 and all goals. $\endgroup$
    – Hiroki Chen
    Commented Apr 28 at 19:09
  • 1
    $\begingroup$ Also the question mark is used to let Coq generate fresh names for the newly introduced variables and premises. ??? lets Coq pick three arbitrary names for the things you have introduced in the induction pattern. $\endgroup$
    – Hiroki Chen
    Commented Apr 28 at 19:17
  • $\begingroup$ @HirokiChen Ohh, so is the above parsed as induction Hstep1 as ... in (e'', Hstep2 |- *)? $\endgroup$
    – Jay Lee
    Commented Apr 29 at 3:31
  • $\begingroup$ Yes, you are right. So induction a in b means doing induction in b where in your case b is (e'', Hstep 2 |- *), i.e., doing induction within e'' and Hstep2 as well as all goals. $\endgroup$
    – Hiroki Chen
    Commented Apr 29 at 15:03

1 Answer 1

Reset to default
1
$\begingroup$

Since you have added a follow-up question, I think wrapping all the comments in this answer might be clearer.

What does the part in e'' in induction Hstep1 ... in e'' do?

I also have another small question---what does ??? do, and what is the intention of putting the trailing |- * which seems useless?

This statement should rather read as induction Hstep1 as [...] in (e'', Hstep2 |- *), i.e., doing induction on Hstep within (e'', Hstep2 |- *). |- is an interesting token in Coq used to select both hypotheses and goals. There is a more detailed documentation in Coq's reference manual (https://coq.inria.fr/doc/V8.19.0/refman/proof-engine/tactics.html#occurrence-clauses). In short, a |- b selects hypothesis a and goal b, and you can use the asterisk to select all.

I also have another small question---what does ??? do?

This is called introduction pattern in Coq. It is used to tell Coq that you do not care what names of the fresh variables the induction tactic might introduce, Coq will figure it out itself. Each question mark stands for one fresh variable.

Also, I found that

 generalize dependent e''.
 induction H_step1; intros.

works as well.

Since your proof does not depend on a specific instance of e'', introducing e'' in the forall will mess up the proof and you want to revert it to a universal quantifier. The induction ... in e'', Hstep1 |- * does the trick for you. If variables or hypotheses not mentioning the Hstep are selected, those are also generalized in the statement to prove.

Improve this answer
$\endgroup$
3
  • $\begingroup$ Thank you for providing the relevant part of the manual! But I can't seem to search (or found a keyword to look for) introduction pattern and the in part for induction tactic is explained online... $\endgroup$
    – Jay Lee
    Commented Apr 29 at 17:26
  • 1
    $\begingroup$ @JayLee See coq.inria.fr/doc/V8.19.0/refman/proof-engine/… and coq.inria.fr/doc/V8.19.0/refman/proofs/writing-proofs/… (the in is defined as another language term named induction clause.) $\endgroup$
    – Hiroki Chen
    Commented Apr 29 at 18:28
  • $\begingroup$ Thank you! From what I see in the first link, "naming_intropattern" a single ? can be used for the same purpose, right? $\endgroup$
    – Jay Lee
    Commented Apr 30 at 3:39

Not the answer you're looking for? Browse other questions tagged or ask your own question.