Add simplification for bool_equality stuff.

Open ordinarymath opened this issue 9 months ago • 5 comments

Simplify stuff like this. (A ==> B) <=> (A ==> C) (A /\ B) <=> (A /\ C) There some discord discussion here https://discord.com/channels/1171421764379742258/1171423803553878117/1323470362805145653. Where @mn200 wants to use a custom conversion to deal with bool permutations.

Mar 23 '25 06:03 ordinarymath

Another pattern to consider. (A ==> B) ==> ~A ~= (A ==>B) ==> (A ==> F)

May 09 '25 08:05 ordinarymath

Why is this a good idea? If anything, I'd prefer to simplify the LHS above into B ==> ~A.

May 12 '25 01:05 mn200

(Which we could do by extending the implication congruence rule to assume the negation of the r.h.s. of the arrow while simplifying the left.)

May 12 '25 01:05 mn200

How much of this is already existing in src/1/BoolExtractShared.sml?

Sep 17 '25 16:09 ordinarymath

Lots of it, it would appear! I'd be tempted to put BOOL_EQ_IMP_CONV into bool_ss.

Sep 18 '25 02:09 mn200