"forall X Y" vs "forall X, forall Y"

[David Baelde]

Hi guys,

I got back to doing a small Abella development recently, and got frustrated by bad error messages on failed apply/backchain. I eventually understood that some of those surprising failures were caused by a gap between concrete and abstract syntax; at least that's how I perceived it. It's what the subject of this mail says, demonstrated in this example:

Theorem test : (forall (x:olist) y, x = y) -> (forall (x:olist) y, x = y).

intros.

backchain H1. % everything works fine

Theorem test : (forall (x:olist), forall y, x = y) -> (forall (x:olist), forall y, x = y).

intros. % just as before, good

backchain H1. % unify failure

I have never really looked at Abella's code, but it should be relatively easy to fix this: just normalize both inputs to the same synthetic AST.

Also, it's not nice that the user sees (Failure "List.iter2") when not providing the right number of arguments to apply.

Cheers,

David

[Andrew Gacek]

Thanks David. I've fixed these as you suggested.

-Andrew

> --
> You received this message because you are subscribed to the Google Groups
> "Abella" group.
> To view this discussion on the web visit
> https://groups.google.com/d/msg/abella-theorem-prover/-/9UThG77eua8J.
> To post to this group, send email to abella-the...@googlegroups.com.
> To unsubscribe from this group, send email to
> abella-theorem-p...@googlegroups.com.
> For more options, visit this group at
> http://groups.google.com/group/abella-theorem-prover?hl=en.

[David Baelde]

Thanks for the fast fix, Andrew!

David