CODEWITHSUNDEEP
coq
Jakub Arnold
Jakub Arnold

Reputation: 87220

How can I do intros in a different order without using generalize dependent in Coq?

Given that I have forall n m, is there a way to this:

intros n m. generalize dependent n.

But in a single step, by only applying intros (or an alternative tactic) just to m?

Upvotes: 1

Views: 106

Answers (2)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23592

Unfortunately, the basic Coq tactic language is not very good for this sort of bookkeeping steps. I personally prefer to use the SSReflect ones for this, since they are much more economical. Compare

intros n m. generalize dependent n.

with the SSR equivalent

move=> n m; move: n.

Notice that if your theorem is a universally quantified fact, you can also put n and m directly before the colon, thus saving the first intros step, e.g.

Lemma my_lemma n m : P n m.
Proof.
move: n.
(* Rest of proof *)
Qed.

or, even better, if you're doing induction right after generalizing,

Lemma my_lemma n m : P n m.
Proof.
elim: n.
(* Rest of proof *)
Qed.

Upvotes: 0

gallais
gallais

Reputation: 12103

You probably want something along those lines (but with an heterogeneous list in order to be able to apply the tactics to multi-sorted telescopes):

Require Import ListTactics.

Ltac introNthAcc n acc := match constr:n with
  | 0    => intro ; list_iter ltac:(fun x => generalize dependent x) acc
  | S ?n =>
     let H := fresh "H" in
     intro H ; introNthAcc n (cons H acc)
end.

Ltac introNth n := introNthAcc n (@nil Prop).

Goal forall a b c, a /\ b /\ c.

 introNth 1.

Upvotes: 1

Related Questions