The Coq mailing list

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

Hi Matthieu,

many thanks for the quick answer.

> If you redefine the notation like this it works:
>
> Tactic Notation "dependent" "destruction" hyp(H) :=
>  do_depelim' ltac:(fun hyp => do_case hyp) H.

Is "do_depelim'" included in the Coq 8.3?
(In Coq 8.2pl1, it doesn't seem to be.)

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

Sorry, understanding tacticals is still a hard work for me.

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

Thanks for hints.


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

I meant "matching on the goal".