The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/22/2014 02:33 PM, Jason Gross wrote:
> I haven't really looked at the code carefully, but, a few comments:
>
> - You can use [constructor] rather than [tauto] in [smuggler] to prove your
> [JMeq] (however, note that using JMeq sets you up for contradicting
> univalence; the only way to get from JMeq to eq is by assuming that the
> universe is a set)

Note that I originally tried normal =, and it worked so long as I used 
destruct in smuggler instead of case - but the resulting equalities were 
just as unusable in the result (also, rewriting the result failed - as 
with the final rewrite or_false_r in logicalize).  I decided to use JMeq 
instead because it seemed to get further, but still hits a wall.  
Dropping all equality works - but then one loses ability to tie the 
generated hypothesis back to the original one.

> - You might want to use [cbv beta in <hypothesis>] to get rid of all the
> function applications.

If you mean on the output hypothesis of logicalize, cbv beta does 
nothing.  I have been composing some rewrite rules to get rid of the 
extraneous stuff - although it might be easier if doexistify was smarter 
about not over-complicating things, and if smuggler tried to eliminate 
false branches (either by using inversion, or proving a contradiction 
itself).

> - Your first example fails for me in Coq 8.4pl4 with
> Toplevel input, characters 0-12:
> In nested Ltac calls to "logicalize" and
> "instantiate ( 1 := False ) in (Value of P)" (expanded to
> "instantiate ( 1 := False ) in (Value of P_)"), last call failed.
> Error: Instantiate called on already-defined evar

Sorry, I'm using a trunk version.  I am addicted to its evar 
backtracking abilities.

> - To answer your comment about the failure, if you [Set Printing Implicit],
> you'll notice that the type of [y] is [Y (S m) (S n)], but the type of [Y3
> (S m)] is [Y (S m) 3].  So you first need to extract the fact that [n = 3]
> (you should be able to do this without any axioms), use that to get rid of
> [n], and then you can use [JMeq_eq] in the hypothesis.
>
> -Jason

I haven't been able to get it to work.  For instance, after Focus 3, 
inversion y0 produces
 H1 : Y (S m) (S n) = Y (S m) 3, but using that to rewrite y dies with:

Toplevel input, characters 7-23:
Error: Cannot instantiate metavariable P of type "Type -> Prop" with
abstraction "fun T : Type => T" of incompatible type
"Type -> Type".


> On Tue, Jul 22, 2014 at 3:04 PM, Jonathan 
> <jonikelee AT gmail.com>
>  wrote:
>
> > Attached is a first attempt at a general-purpose "Prop smuggling" tactic:
> > logicalize.  The point is to take a Prop hypothesis and "invert" it even
> > when the current context is not Prop - producing a disjunction of exists
> > terms, one for each constructor.
> >
> > However, the JMeq's don't work in the result, as demonstrated in the
> > second test.  Can anyone figure out what's going wrong?  If not, they can
> > just be omitted.
> >
> > Also needed is a way to simplify out false cases and factor out
> > non-dependent parts from each exists term.
> >
> > Jason: thanks for the "_ \/ _" hint!
> >
> > -- Jonathan