CODEWITHSUNDEEP
coq
Mark
Mark

Reputation: 5513

What do ellipses mean in a Coq proof?

Here is a proof that appears in this online course https://softwarefoundations.cis.upenn.edu/plf-current/StlcProp.html#lab222.

Proof with eauto.
  remember (@empty ty) as Gamma.
  intros t t' T HT. generalize dependent t'.
  induction HT;
       intros t' HE; subst Gamma; subst;
       try solve [inversion HE; subst; auto].
  - (* T_App *)
    inversion HE; subst...
    (* Most of the cases are immediate by induction,
       and [eauto] takes care of them *)
    + (* ST_AppAbs *)
      apply substitution_preserves_typing with T11...
      inversion HT1...
Qed.

What do the ellipses do in this line? apply substitution_preserves_typing with T11...

Upvotes: 6

Views: 235

Answers (1)

SCappella
SCappella

Reputation: 10464

Ellipses apply a certain predefined tactic. In this proof, it's eauto since the proof started with Proof with eauto. See the reference manual for more.

Upvotes: 8

Related Questions