The Coq mailing list

[Gyesik Lee <gslee AT ropas.snu.ac.kr>]

Hi,

I would like to write some tactics using dependent destruction.
(I'm using Coq8.2pl1)

1) Writing a tactic using dependent destruction is not possible?

Let me first introduce an example:

================

Parameter A B : Type.

Inductive P : A -> B -> Prop :=
  | All : forall a b, P a b.

Ltac toto :=
  match goal with
    | H : P _ _ |- _ => dependent destruction H
  end.

Ltac toto1 := intros; toto.

Lemma titi : forall a b c d,
  P a b -> P c d.
Proof.
intros. toto.

=================

Applying the tactic "toto" triggers the following error message:

Error: No matching clauses for match goal
       (use "Set Ltac Debug" for more info).

However, if you replace "dependent destruction H" with "assert False",
for example,
in the definition of toto, then it behaves as expected.

I am wondering why.

2) Is there a way to use "dependent destruction" with "as" like
"inversion H as ..." or "destruct H as ... "?

3) (not relevant to dependent destruction)

Suppose, during a proof, you have assumptions as follows

H : forall (x : A), Q x -> P x x
a : A
H0 : Q a

How would you write a tactic which generates a new assumption (H1 : P a a)?

Gyesik