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
.
This should be a new level of the auto-rewriter.
There is already the manual rule
DEF_IN_ID
which manually rewritesE ↦ F ∈ id
toE = F
, but it needs some user interaction to be applied.I propose to name
SIMP_SPECIAL_IN_ID
the rule that rewritesE ↦ E ∈ id
to⊤
, andSIMP_SPECIAL_IN_SETMINUS_ID
for the rule that rewritesE ↦ E ∈ r ∖ id
to⊥
.The rule
SIMP_SPECIAL_IN_DOMRES_ID
rewritesE ↦ E ∈ S ◁ id
toE ∈ S
.Similarly, we could add the rule
SIMP_SPECIAL_IN_SETMINUS_DOMRES_ID
that rewritesE ↦ E ∈ r ∖ (S ◁ id)
toE ↦ E ∈ S ⩤ r
.The requested rules have been implemented in commit [8b2820].
Related
Commit: [8b2820]