1
$\begingroup$

Are there tactics in Coq that are more limited versions (subtactics?) of intros?

I'm curious if there are any specifically for forall ... and specifically for ->.

intros in Coq is capable of undoing the outermost forall as well as the outermost ->.

It introduces hypotheses with provided or arbitrary names.

I suspect the reason for this generality is the fact that coq is built on top of the calculus of inductive constructions and forall and -> really are both special cases of the dependent $\Pi$-type. (Also, now that I think about it, forall might actually be the general construction. I'm not sure.)

Here is an example from the Basics.v file from Software Foundations. This is a theorem and proof provided by authors, not a completed exercise from SF. (I mention this because the authors ask people not to post solutions to SF problems online.)

Theorem plus_id_example : forall n m:nat,
  n = m ->
  n + n = m + m.

Proof.
  (* move both quantifiers into the context: *)
  intros n m.
  (* move the hypothesis into the context: *)
  intros H.
  (* rewrite the goal using the hypothesis: *)
  rewrite -> H.
  reflexivity.  Qed.

Anyway, the generality of intros is nice in theory, but it can make tactic scripts harder to read. Are there weaker tactics than intros that can only unpack -> or only unpack forall? That would make it easier to tell at a glance what roughly what "part" of a theorem is being addressed by a tactic appearing in the middle of a tactic script.

Improve this question
$\endgroup$
4
  • 2
    $\begingroup$ forall (x : nat), 1 = 1 is equal to nat -> 1 = 1. So how would that tactic behave in this case? $\endgroup$
    – Trebor ♦
    Feb 27, 2022 at 4:55
  • $\begingroup$ @Trebor I would treat that as an instance of forall because the type of the bound variable isn't Prop. But your point is well taken. Whether a forall/->/$\Pi$ ignores its bound variable or not is completely orthogonal to what type the bound variable has. I guess this question doesn't really make sense since there's no principled way to distinguish "uses that look like $\to$ in logic" and "uses that look like $\forall$ in logic", which is what I was really trying to do. Thanks. $\endgroup$
    – Greg Nisbet
    Feb 27, 2022 at 5:33
  • 1
    $\begingroup$ Your question has two interpretations. You can make a tactic that rejects bad usages; you can also use two alias of the same tactic, and use them in a principled, but unenforced way. $\endgroup$
    – Trebor ♦
    Feb 27, 2022 at 5:41
  • $\begingroup$ Those are both interesting and I don't know how to do either. I'm primarily interested in rejecting bad usages, though. $\endgroup$
    – Greg Nisbet
    Feb 27, 2022 at 5:44

1 Answer 1

Reset to default
5
$\begingroup$

intros * only unpacks forall. Example from the reference manual:

    ============================
    forall A B : Prop, A -> B

intros *.
      
    A, B : Prop
    ============================
    A -> B
Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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