The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/20/2014 06:06 AM, Kirill Taran wrote:
> > If you are instead asking for a tactic to replace the above assertion
> such that it determines the type of H' for you, I agree that such a tactic
> would be nice to have.
>
> This and plus that with some matches we need more than one destruct (when
> patterns have variables e.g.), but the latter can be fixed with plain repeat
> .
>
> Maybe there are other difficulties with complex pattern matches, yesterday
> I had some specific notes, but I have forgotten them already =/
>
> Sincerely,
> Kirill Taran

I don't mind having to compose destructs.  But, there is one variant of 
the assert X as H' by (destruct P...) that would be very useful to have 
as a tactic - which is when P is a Prop but the current goal is not (and 
so P cannot be case analyzed in the current goal at all), and the type X 
one would get by destructing P is too complex to determine by hand prior 
to interactively destructing P.  In such a case, a workaround is to do 
something like exfalso (producing a goal in Prop), then destruct P, then 
copy out the result, then undo to before the exfalso, then assert 
(pasted result) as H' by (destruct P...).  I call this "Prop 
smuggling",  and it is something I do often enough that I have attempted 
to automated it, but it is exceedingly difficult to automate in a 
general way.  The closest I have come is a tactic that uses an evar (R : 
Prop), then asserts the evar, then destructs P and instantiates R's 
value as the resulting logical type obtained from P.  I can get this to 
work when P either destructs (or inverts) into a single subgoal, or into 
several such that all but one can be eliminated due to a contradiction.  
But, if P produces more than one non-contradictory subgoal, as in your 
case, and you want the result to be a disjunction of the types produced 
in each subgoal, then it's back to exfalso/destruct/copy/undo/paste by hand.

-- Jonathan