Uvar issue with apply/unification

[jldodds]

I'm not sure if this is supposed to work, but I think it is related to a problem I'm having with my set lemma

Axiom bad_ax : forall A, A /\ A.

Definition bad_ax_lemma : my_lemma.
reify_lemma reify_vst bad_ax.
Defined.

Definition EAPPLY_bad_ax :=
EAPPLY typ func bad_ax_lemma.

Goal exists A, A.
reify_expr_tac.
Eval vm_compute in run_tac (THEN INTROS (EAPPLY_bad_ax)) e.

the run_tac at the end is failing, presumably because it is "splitting" the uvar the INTROS works but the apply fails. I'll try to work on a case that better explains the problem I'm having with my lemma

[jldodds]

Here's a better example:

Lemma bad_ax : forall A: Prop, A -> A /\ (True /\ A).
auto.
Qed.

Definition bad_ax_lemma : my_lemma.
reify_lemma reify_vst bad_ax.
Defined.

Definition EAPPLY_bad_ax :=
EAPPLY typ func bad_ax_lemma.

Goal exists A, True /\ A.
reify_expr_tac.
Eval vm_compute in run_tac (THEN INTROS (EAPPLY_bad_ax)) e.

also fails. If the lemma is changed to

Lemma bad_ax : forall A: Prop, A -> A /\ (A).

it will work fine

[gmalecha]

It seems like you are saying that True /\ ?1 does not unify with ?2 /\ (True /\ ?2) but it does unify with ?2 /\ ?2. I think this is currently a limitation of Rtac, one that I'm not certain that I know how to fix. The issue is that the solution to the instantiation is [?1 = True /\ ?2] which leads to a forward pointer in the unification. In theory this is fine because there are no [forall]s between the two, but recognizing this is a little bit hairy.

I will keep it in mind and see if I can come up with a way to solve it when I look more into Rtac this week.

[jldodds]

This is a problem that is preventing symbolic execution from working for my set lemma which (simplified) is something like this:

msubst e = Some vl ->
{assertD nil (localD ls vs) R}
      (Sset id e)
{normal_ret_assert (assertD nil (localD (my_set id vl ls) vs) R)}

when I apply this to a triple with an existential for the post condition it won't work, I think for the reasons above

[gmalecha]

Yes, that sound reasonable. Essentially, what you would need to do is solve vl before doing unification. Then the expression that you are instantiating the unification variable with would contain no unification variables and everything would work out.

Question: When you are running this tactic, do you introduce any universal quantifiers between the unification variable in the goal and applying this lemma?

[jldodds]

Even R is a problem there though. a postcondition of

{normal_ret_assert (assertD nil nil R)}

also can't be applied. The tactic is pretty much intros and apply that lemma

[jesper-bengtson]

No, this is one single EAPPLY failing, so no new variables are introduced.

/Jesper

On 25 Nov 2014, at 10:19, Gregory Malecha notifications@github.com<mailto:notifications@github.com> wrote:

Yes, that sound reasonable. Essentially, what you would need to do is solve vl before doing unification. Then the expression that you are instantiating the unification variable with would contain no unification variables and everything would work out.

Question: When you are running this tactic, do you introduce any universal quantifiers between the unification variable in the goal and applying this lemma?

— Reply to this email directly or view it on GitHubhttps://github.com/gmalecha/mirror-core/issues/55#issuecomment-64415014.

[gmalecha]

I think that we could avoid [R] as a problem because it must already have been unified because it exists in the pre-condition. The bug fix for that would be something like performing the occurs check after doing the instantiate rather than before.

[jldodds]

It looks like it might work to rewrite as:

msubst e = Some vl ->
(assertD nil (localD (my_set id vl ls) vs) R) = P ->
{assertD nil (localD ls vs) R}
      (Sset id e)
{normal_ret_assert P}

and instantiate before calling the unifier on the subgoals. This is close to what @jesper-bengtson is doing and is why he hasn't run into this issue yet.