Fix why3 tactic (WIP)

[fblanqui]

• why3_tactic.ml: many fixes (fix The why3 encoding is wrong for the quantifier and predicates #1165) and changes
• fol.ml: add fields symb_Prop and sym_Set (domains of symb_P and symb_T), and symb_eqv
• tests: merged why3_quantifiers.lp into why3.lp

As before, the why3 tactic starts by doing some assume. Then, the tactic tries to translate the environment as much as possible, and then the goal. The tactic fails if the goal cannot be translated.

A term [t:Set] is translated to a Why3 type if it is algebraic (i.e. built from function applications and variables only) and its variables are in the environment.

A term [t:T _] is translated to a Why3 term if it is algebraic and its variables are in the environment or are quantified variables.

A term [t:P _] is translated to a Why3 formula if it has the form of a formula in predicate calculus. Subterms that are not in predicate calculus are replaced by fresh propositions.

TODO:

• remove debug flags in test files
• when abstracting a subformula, compute its free variables, check that they are quantified, and replace the subterm by the application of a fresh predicate applied to those variables

[NotBad4U]

Awesome! Please ping me when I can try it.

[fblanqui]

Hi @NotBad4U . I already made quite some improvements in the why3 tactic. But it may not be sufficient for what you want though. Indeed it still does not handle quantifications on propositions, which is out of the scope of first-order logic. However, could you please try it to give me your feedback?

[fblanqui]

Precision: outer universal quantifications on propositions are fine as the why3 tactic starts by doing some assume. The problem is with existential quantifications on propositions and quantifications that are deep inside.

[NotBad4U]

I can not compile your branch. I got this error:

File "src/handle/why3_tactic.ml", line 418, characters 16-46:
418 |   and limits = {Why3.Call_provers.empty_limits
                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound value Why3.Call_provers.empty_limits
Hint: Did you mean empty_limit?

I have the version 1.7.2 of the why3 library. What about you?

[fblanqui]

You now need why3 1.8.0 (#1176).

[NotBad4U]

I did some tests and it returned nice first results.
My encoding with Alethe works with propositional extensionality, and I do not use eqv but = instead.
It would be great if we could support =. For example, it will help to prove:

symbol S : U;
symbol a: T S;
symbol p: T S → Prop;
opaque symbol test : P (all S (λ x, (or (not (a = x)) (p x)) ) = (or (not (a = a)) (p a))) ≔ begin
  why3
end;

In this test, the first one failed, but the second passed when g was passed as a parameter.

symbol ⤳ : U → U → U; notation ⤳ infix right 20;
rule T ($x ⤳ $y) ↪ T $x → T $y;
symbol g: T (S ⤳ o);

opaque symbol test_hol [x] : P (eqv (ex S (λ x, g x)) (not (all S (λ x, not (g x)))))
≔ begin
  why3 // FAIL
end; 

opaque symbol test_hol2 [x] [g: T (S ⤳ o)] : P (eqv (ex S (λ x, g x)) (not (all S (λ x, not (g x)))))
≔ begin
  why3 // PASS
end;