The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/20/2014 04:34 PM, Jason Gross wrote:
> If your goal is an evar in Prop, I think you can split it in to two evars
> via [refine (_ : _ \/ _)].  Does this work (I'm not in fromt of a computer
> at the moment), and if so, does it let you write the fully general tactic
> you want?
>
> -Jason

That's a nice trick!  I wonder how it can be used here?  One problem is 
that the inversion of the targeted Prop is going to do subgoal splitting 
itself.  The other problem is that it is hard to know in advance how 
many subgoals are going to get created.

Maybe [instantiate (1:=_\/_) in (Value of P)] is a better choice - since 
it does the same evar splitting without splitting off subgoals - so that 
the inversion of the targeted Prop would be the only thing creating new 
subgoals.

Hmmm.... Maybe this CAN be turned into a general version...

> On Jul 20, 2014 3:06 PM, "Jonathan" 
> <jonikelee AT gmail.com>
>  wrote:
>
> > 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