Laurent Voisin

Require Java 17 for build

Document the deactivation of Resources auto-update

There is already the manual rule DEF_IN_ID which manually rewrites E ↦ F ∈ id to E = F, but it needs some user interaction to be applied. I propose to name SIMP_SPECIAL_IN_ID the rule that rewrites E ↦ E ∈ id to ⊤, and SIMP_SPECIAL_IN_SETMINUS_ID for the rule that rewrites E ↦ E ∈ r ∖ id to ⊥. The rule SIMP_SPECIAL_IN_DOMRES_IDrewrites E ↦ E ∈ S ◁ id to E ∈ S. Similarly, we could add the rule SIMP_SPECIAL_IN_SETMINUS_DOMRES_ID that rewrites E ↦ E ∈ r ∖ (S ◁ id) to E ↦ E ∈ S ⩤ r.

The last case could also be part of the generalized modus ponens reasoner, as it is quite necessary to perform inductive proofs.

Add a test on datatype induction

Loosen WD condition on exponent

The proposed change is indeed compatible with Atelier B provers. However, if we change the WD condition, then we may introduce regressions in proofs. Currently, the WD condition ensures that e^n is non-negative. If we allow for negative bases, this will no longer be true (need to check that either base is non-negative or exponent is even). Therefore introducing such a change should be studied with care.

Fix FR#385: Better message for syntax errors in set comprehension