fix_IF_NONE_EQUALS_OPTION

[ordinarymath]

This change removes IF_NONE_EQUALS_OPTION from the srw_ss and adds if_option_eq which has the last 2
conjuncts + 2 more other useful case splits.

[ordinarymath]

I'm skeptical of the usefulness of the first 2 rewrites so removing them for now.

[ordinarymath]

It seems that otknl is some how not terminating. Can someone with permission to kill jobs kill it. Also to prevent this from happening again @mn200 can I please get permission to kill jobs as it seems like this is happening frequently enough.

[ordinarymath]

Oh it finished running.

[ordinarymath]

@mn200 ping on this?

[binghe]

The name y' was available here, and it's supposed to correspond to y. In my name design, y is the head variable of M0, and y' is the head variable of M0', which is perfect. Now this bad y''' jump out, because somehow y' and y'' occurred from nowhere but changed simplification rules. Shit.

[ordinarymath]

Another slightly less obvious change is Overload subterm' = “\X M p r. FST (THE (subterm X M p r))”
does not print as often as
subterm X M p r <> NONE before would be simplified in some cases to.
subterm X M p r = SOME y
and i get
FST y appearing instead

[binghe]

Both NONE and SOME are primitive constants provided by optionTheory. I think it's very rude to automatically rewrite all a <> NONE to a = SOME y with a new, fixed name y introduced. I keep those _ <> NONE terms only because I don't care which SOME y it equals to.

[binghe]

I actually have a blacklist of simplification rules in front of my boehmTheory. Some are specific to the related work to lambda-calculus, some are general for all my proofs:

(* These theorems usually give unexpected results, should be applied manually *)
val _ = temp_delsimps [
   "lift_disj_eq", "lift_imp_disj",
   "IN_UNION",     (* |- !s t x. x IN s UNION t <=> x IN s \/ x IN t *)
   "APPEND_ASSOC", (* |- !l1 l2 l3. l1 ++ (l2 ++ l3) = l1 ++ l2 ++ l3 *)
   "SNOC_APPEND"   (* |- !x l. SNOC x l = l ++ [x] *)
];

If this PR were merged, I will later revert the changed proofs by putting if_option_eq and if_option_neq into this list, instead. So I give up, just do whatever you feel like.

[mn200]

As per Zulip discussion, I think the best way forward is to avoid automatic simps that generate (existentially-quantified) names, so that (?y. x = SOME y) gets replaced with x <> NONE (in the option_neq rewrite).

[mn200]

Thanks for negotiating the long back-and-forth with this PR!

The total impact now looks quite minimal and the failing checks in the latest regression are not your problem so I'm happy to merge.