The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 19 juin 2010 à 12:02, Gyesik Lee a écrit :

> Hi,

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.

There seems to be a bug in the interpretation of tactics. "dependent 
destuction" is
defined as a tactic notation expecting an ident(H), while H is an hypothesis 
(bound) name here.
If you redefine the notation like this it works:

Tactic Notation "dependent" "destruction" hyp(H) := 
  do_depelim' ltac:(fun hyp => do_case hyp) H.

In any case, you can use the underlying tactical directly which has no such 
problems.

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

By customizing the tactical I suppose yes. Have a look at the end of 
Program.Equality for ideas (e.g. the [using] variants).

> 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)?

assert(H1:=H _ H0)? Or you mean how to match on the goal?

Hope this helps,
-- Matthieu