Substitution failure for a complex expression

[Jinxu Zhao]

Dear professionals,

I encountered the following problem:

H46 : Exp1 n3 n2 = L3 (arrow n2 n3)

H47 : subal (FxE n3 n2) (subt A2 n2 :: subt n3 A3 :: Exp1 n3 n2)

============================

 subal (FxE n3 n2) (subt A2 n2 :: subt n3 A3 :: L3 (arrow n2 n3))

Proving such a goal should be easy: just plug H46 into H47 and the form matches. However, when I perform a `case H46`, Abella gives me

H47 : subal (FxE n3 n2) (subt A2 n2 :: subt n3 A3 :: Exp1 n3 n2)

H48 : Exp1 n3 n2 = L3 (arrow n2 n3)

============================

 subal (FxE n3 n2) (subt A2 n2 :: subt n3 A3 :: L3 (arrow n2 n3))

and nothing actually changes. The search tactic does not help, either.

Currently a workaround for me is to define a theorem with simpler form so that Abella understands how to substitute:

Theorem wtf_subal : forall (f : ty -> ty -> olist -> olist) g h (a : ty -> ty -> ty) e,

nabla x y, subal (e x y) (f x y (g x y)) -> g x y = h (a y x) -> subal (e x y) (f x y (h (a y x))).

intros. case H2. search.

which is really easy to prove, and applying that to H47 H46 works.

I am eager to know what happened and how to solve the problem by not defining an auxiliary theorem. Thanks in advance.

[Kaustuv Chaudhuri]

This is because H46 is a non-pattern equation, which is something Abella currently does not handle. A workaround to deal with such equations that is slightly simpler than your lemma is shown here:

https://github.com/abella-prover/abella/issues/11

Doing much better than this requires non-trivial effort, which is why the issue has been open for a while. Maybe someone has some new ideas?

Kaustuv

--
You received this message because you are subscribed to the Google Groups "Abella" group.
To unsubscribe from this group and stop receiving emails from it, send an email to abella-theorem-prover+unsub...@googlegroups.com.
To post to this group, send email to abella-theorem-prover@googlegroups.com.
Visit this group at https://groups.google.com/group/abella-theorem-prover.
For more options, visit https://groups.google.com/d/optout.

[Todd Wilson]

This is similar to the situation I wrote about in another thread with the title "nominal extensionality". My thought there was that an equation like

H46 : Exp1 n3 n2 = L3 (arrow n2 n3)

could be solved in favor of Exp1 as

Exp1 = x\ y\ L3 (arrow y x)

which would have rendered H47 and your goal identical. I'm still unsure why, when one of the two sides of a non-pattern equation is in fact a pattern, it can't be solved for the variable on that side.

To post to this group, send email to abella-the...@googlegroups.com.

[Kaustuv Chaudhuri]

Going from

X n1 n2 ... nk = t

to

X = x1\ x2 \ ... xk \ [x1/n1, ..., xk/nk] t

is fine. It's just an application of eta-contraction modulo the equivalence between the nominal form and the implicit lambda-prefixed form of the equation. We could probably implement this special case without too much trouble.

Kaustuv (in discussion with Dale)

[Roberto Blanco]

I recently did this to have Abella use full higher-order unification and the pattern generalization of functions-as-constructors (which, alas, does not cover the problem case in this thread directly).

That was not problematic, although I have not modified Abella's unification module, which in my opinion needs to be vastly improved in terms of documentation or replaced with something better. While the modification you propose sounds simple, I would not be surprised if implementing it turned out to be delicate.

Best,

Rob

--

You received this message because you are subscribed to the Google Groups "Abella" group.
To unsubscribe from this group and stop receiving emails from it, send an email to abella-theorem-prover+unsub...@googlegroups.com.

To post to this group, send email to abella-theorem-prover@googlegroups.com.

[Jinxu Zhao]

Looking forward to that feature :)

Recently I also encountered similar problems:

1) I want to unify

L n1 = L1 n1 A

, or even prove

L m = L1 m A (for any m of the right type)

2) I have got

L = L1 n1 A

but I cannot prune the nabla variable from W.

I believe these relate to the problem in the discussion. But I can not find any workaround without admitting things like L = x\ L1 x A.

I understand that full higher-order unification might be challenging, but only this limited form helps a lot for my situation.

[Yuting Wang]

I found out that the function "make_non_llambda_subst" in "unify.ml" already does something like eta-contraction when unifying flexible terms.

I have tweaked the code of "make_non_llambda_subst" a bit to make the following example work:

Kind i type.

Type arrow  i -> i -> i.

Theorem foo: forall Exp1 (L3: i -> i), nabla x y,

 Exp1 x y = L3 (arrow y x) -> Exp1 = x\ y\ L3 (arrow y x).

intros. case H1. search.

You can find the updated unification algorithm at the branch 'fix-non-pattern-unif'.

I would not consider this as a fix since I do not fully understand what "make_non_llambda_subst" is supposed to do. I think we need to check with Gopalan or Andrew to understand the logic behind it before we apply a fix.

- Yuting

--

You received this message because you are subscribed to the Google Groups "Abella" group.

To unsubscribe from this group and stop receiving emails from it, send an email to abella-theorem-p...@googlegroups.com.

[Yuting Wang]

Hi Jinxu,

I don't quite get your example. The equation (L n1 = L1 n1 A) is actually solvable (by the "make_non_llambda_subst" function I mentioned in another reply) in Abella, as manifested by the following theorem:

Kind i type.

Theorem foo: forall L (L1: i -> i -> i) A, nabla (x:i),

  L x = L1 x A -> L = x\L1 x A.

intros. case H1. search.

What is the theorem you are trying to prove? Could you write it down?

- Yuting

--

You received this message because you are subscribed to the Google Groups "Abella" group.

To unsubscribe from this group and stop receiving emails from it, send an email to abella-theorem-p...@googlegroups.com.

[Jinxu Zhao]

Hi Yuting,

Thanks for the replies.

I understand the Theorem you shown.

But the actual point of my confusion was that I would like Abella to substitute all occurrences of L in the hypothesis list properly.

Currently if I managed to prove a similar lemma (or just make use of assert for an automatic proof), a hypothesis like this will be generated:

Hxx: z2\L z2 = z2\W z2 A

and no L will be substituted. Since some of the expressions does not match the shape of IH without performing a proper substitution, the proof got stuck.

I am also interested in the second question, or how to prove (I am not 100% sure that the theorem is what I want)

forall (L A : i) L1, nabla (x : i), L = L1 x A -> exists L0, L1 = x\ L0.

or maybe

forall (L A : i) L1, nabla (x : i), L = L1 A x -> exists L0, L1 = a\ x\ L0 a.

Thanks anyway for the reply!

Jinxu

To unsubscribe from this group and stop receiving emails from it, send an email to abella-theorem-prover+unsub...@googlegroups.com.

[Yuting Wang]

Hi all,

I have committed a fix of a bug in the unification engine of Abella described at https://github.com/abella-prover/abella/issues/110. With this fix, the following theorem is now provable in Abella:

Type arrow   i -> i -> i.

Theorem bug: forall E (L:i -> i), nabla (x y: i),
  E y x = L (arrow x y) -> E = y\x\ L (arrow x y).
intros. case H1. search.

I believe this fixes most of the problems mentioned in this thread.

BTW, the master branch of Abella now supports polymorphism. We are working on releasing a new version with this feature, which should be available soon. You can also test it out now by consulting the tutorial at http://abella-prover.org/schm-poly/. Let me know if you have any questions.

Cheers,

- Yuting

To unsubscribe from this group and stop receiving emails from it, send an email to abella-theorem-p...@googlegroups.com.

To post to this group, send email to abella-the...@googlegroups.com.
Visit this group at https://groups.google.com/group/abella-theorem-prover.
For more options, visit https://groups.google.com/d/optout.

--

You received this message because you are subscribed to the Google Groups "Abella" group.

To unsubscribe from this group and stop receiving emails from it, send an email to abella-theorem-p...@googlegroups.com.