LP, the Larch Prover -- Sample proofs: three theorems about subset

The next three theorems in set1.lp establish some basic properties of the subset relation. They illustrate how LP's proof techniques combine to establish conjectures. The user types a few commands to select proof strategies (e.g., a proof by induction or a proof by cases). LP generates subgoals appropriate for the selected strategies and fills in most of the details automatically. Sometimes the user needs to tell LP to work a little harder near the end of a proof to fill in the remaining details.

set proof-methods normalization, =>
prove e \in x /\ x \subseteq y => e \in y by induction on x
      resume by case ec = e1c
        complete
qed

The set command directs LP to use an automatic proof technique whenever the user does not specify one explicitly. Here, it directs LP to try to prove conjectures first by rewriting, and then to assume the hypotheses of implications and try again. This setting for proof-methods is a good alternative to the standard setting, which consists of normalization alone.

A proof by induction

The user directs LP to begin the proof of the conjecture by induction on the variable x instead of by using one of the automatic proof methods. LP creates two subgoals for the proof by induction, a basis subgoal for the generator {} of sort S and an induction subgoal for the generator insert; it also formulates an induction hypothesis that can be used in the proof of the induction subgoal.

Creating subgoals for proof by structural induction on `x'
Basis subgoal:
  Subgoal 1: e \in {} /\ {} \subseteq y => e \in y
Induction constant: xc
Induction hypothesis:
  setTheoremsInductHyp.1: e \in xc /\ xc \subseteq y => e \in y
Induction subgoal:
  Subgoal 2: e \in insert(e1, xc) /\ insert(e1, xc) \subseteq y => e \in y

LP proves the basis subgoal automatically by rewriting the term e \in {} to false, but it needs further guidance to prove the induction subgoal.

A proof technique for use with implications

LP uses the automatic => proof technique to create a subgoal for the induction step:

Creating subgoals for proof of =>
New constants: e1c, ec, yc
Hypothesis:
  setTheoremsImpliesHyp.1:
     (ec = e1c \/ ec \in xc) /\ e1c \in yc /\ xc \subseteq yc
Subgoal:
  ec \in yc

The hypothesis for this subgoal is the result of reducing the hypothesis of the implication in the induction subgoal, after replacing its variables by new constants.

A proof by cases

The user must issue two more commands to finish the proof. The first directs LP to divide the proof into two cases, depending on whether the formula ec = e1c is true or not.

Creating subgoals for proof by cases 
Case hypotheses:
  setTheoremsCaseHyp.1.1: ec = e1c
  setTheoremsCaseHyp.1.2: ~(ec = e1c)
Same subgoal for all cases:
  ec \in yc

LP finishes the first case by using the case hypothesis to rewrite the subterm ec of the subgoal ec \in yc to e1c; then it rewrites e1c \in yc to true using the second conjunct of the implication hypothesis.

In the second case, LP uses the case hypothesis and its hardwired rules to rewrite the first conjunct of the implication hypothesis to ec \in xc, at which point it gets stuck. The complete command directs LP to use what it knows to finish the proof by deriving a few critical-pair equations. First, LP derives xc \subseteq y => ec \in y as critical pair between ec \in xc and the induction hypothesis . Then it obtains ec \in yc as a critical pair between this fact and the last conjunct of the implication hypothesis. This finishes the proof by cases, the proof of the implication for the induction step of the conjecture, and the proof of the conjecture itself.

Two more theorems about subset

Similar techniques can be used to prove two more basic theorems about subset. In the first, the automatic => proof technique introduces xc = yc as a subgoal. To finish the proof, the user proves a lemma (using the <=> technique) suggested by the principle of extensionality.

prove x \subseteq y /\ y \subseteq x => x = y
    prove e \in xc <=> e \in yc by <=>
        complete
        complete
    instantiate x by xc, y by yc in extensionality
qed

In the second, LP fills in all the details in a proof by induction without requiring further guidance from the user.

prove (x \union y) \subseteq z <=> x \subseteq z /\ y \subseteq z by induction on x
qed