The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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)

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

- 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

- 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

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