case fails to normalize object sequents

[silene]

Consider the following proof of false (derived from my weak understanding of the JFR paper). Is there some criteria to help me detect such inconsistent signatures / modules? (For example, in Coq, I would look for Axiom and Admitted, but what about Abella?)

sig test.
type foo o.

module test.
/* empty */

Specification "test".
Theorem bar : false.
assert { foo => foo }.
case H1.
/* Proof completed. */

By the way, the "cut" example shipped with Abella suffers from the exact same inconsistency.

[chaudhuri]

Very odd. Thanks for the report.

[chaudhuri]

Potentially fixed in 5216bc5345b8db535132c70. Needs a little bit more testing.

[silene]

While this solves the simplified script, my original script unfortunately still goes through:

Theorem baz : forall L, { L |- foo } -> false.
induction on 1.
intros.
case H1.
monotone H2 with L.
apply IH to H4.

Theorem bar : false.
apply baz to _ with L = foo :: nil.
/* Proof completed. */

[chaudhuri]

Interesting. I didn't know monotone was even allowed for focused sequents and anyhow the implementation of it in this case seems to have a huge bug. I'll need to do a little pen-and-paper work to make sure that the fix I have in mind is sound.

@yvting -- maybe this will be interesting to you as well since this goes back to the stuff you did in your internship.

[chaudhuri]

As of now I can't think of any reason why the fix in 45d4954 would be unsound, so I'm closing this issue.