When trying to prove a phrase R, try_prove should not only look at all proven phrases P and try to substitute P to become R (that is, try to do P[P/R]), but it should also look for all proven phrases (P=>Q) and try to do (P=>Q)[Q/R].MP to prove R.
There is small potential issue of infinite loop in (P=>Q)[Q/R].MP then calling try_prove and keep on doing this, we should probably avoid that somehow.
One can use the reduce function if one knows which theorem results in the desired phrase, such as in X = Y ⇒ Y = X; 𝗦(x + y) = 𝗦x + y | reduce.MP, but it would be nice to have this happen automatically.
When trying to prove a phrase
R,try_proveshould not only look at all proven phrasesPand try to substitutePto becomeR(that is, try to doP[P/R]), but it should also look for all proven phrases(P=>Q)and try to do(P=>Q)[Q/R].MPto proveR.There is small potential issue of infinite loop in
(P=>Q)[Q/R].MPthen calling try_prove and keep on doing this, we should probably avoid that somehow.One can use the
reducefunction if one knows which theorem results in the desired phrase, such as inX = Y ⇒ Y = X; 𝗦(x + y) = 𝗦x + y | reduce.MP, but it would be nice to have this happen automatically.