#368 Better simplification of identity

[Laurent Voisin]

It would be nice if the prover would rewrite predicates of the form E ↦ E ∈ id to ⊤ and E ↦ E ∈ F ∖ id to ⊥.

This can be particularly useful when these predicates occur in hypotheses.

This request comes from a suggestion by Dominique Cansell who encountered these predicates several times when working with strict partial orders. Usually, a hypothesis containing such predicates shall be detected as false by the PP prover, but it does not happen in all cases.

We could also imagine rewriting E ↦ E ∈ S ◁ id to E ∈ S.

[Laurent Voisin]

This should be a new level of the auto-rewriter.

[Laurent Voisin]

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.

[Guillaume Verdier]

The requested rules have been implemented in commit [8b2820].