• Andrei Paskevich's avatar
    Split_goal: make introduce_premises less aggressige · 8b809621
    Andrei Paskevich authored
    Prevent introduce_premises from splitting too aggressively
    on the left-hand side:
    - under quantifiers:
        "forall x. P /\ Q" =/=> "(forall x. P) /\ (forall x. Q)"
    - match-with:
        "match t with A -> P | B -> Q" =/=> "(t = A -> P) /\ (t = B -> Q)"
    - if-then-else:
        "if f then P else Q" =/=> "(f -> P) /\ (not f -> Q)"
    - equivalence:
        "P <-> Q" =/=> "(P -> Q) /\ (Q -> P)"
    Those splits duplicate formulas, hinder readability and do not
    really simplify anything. Moreover, in case of a split under
    a quantifier, they create several universal premises for provers
    to instantiate, instead of just one.
    TODO: introduce_premises should be able to split under
    a single-branch match. However, this requires special
    treatment in Introduce.dequant, since the pattern
    should be rather skolemized than used as a condition.