Documentation out of dateLearn more

Solution: plus is commutative

This page is part of the introduction to proving metatheorems with STELF.

Exercise 1 from the part 1 exercises: State and prove a metatheorem showing that plus is commutative.

Starting with the preliminaries:

%sort nat %.
%term z nat %.
%term s %pi nat %-> nat %.
%sort plus {_ nat} {_ nat} {_ nat} %.
%term plus-z plus z N2 N2 %.
%term plus-s %pi (plus (s N1) N2 (s N3)) %<- (plus N1 N2 N3) %.

The theorem may be stated:

%sort plus-commutes {_ plus N1 N2 N3} {_ plus N2 N1 N3} %.
%mode plus-commutes %in %out %.

However, before we prove this theorem, we first prove two lemmas. The first says that for any natural number $x$$n$ , $x$$n+0=n$ . This is similar to the constant plus-z, but the order of the arguments to plus has been changed:

%sort plus-zero-id {N1 nat} {_ plus N1 z N1} %.
%mode plus-zero-id %in %out %.
%term pzidz plus-zero-id z plus-z %.
%term pzids
  %pi (plus-zero-id (s N) (%the (plus (s N) z (s N)) (plus-s D)))
  %<- (plus-zero-id N D) %.
%worlds () (plus-zero-id _ _) %.
%total N (plus-zero-id N _) %.

Our second lemma states that if $x$$\mathsf{plus}(n_1,n_2,n_3)$ then $x$$\mathsf{plus}(n_1, \mathsf{succ}(n_2), \mathsf{succ}(n_3))$ . This lemma is similar to the constant plus-s, but the order of the arguments to plus has been changed:

%sort plus-flip {_ plus N1 N2 N3} {_ plus N1 (s N2) (s N3)} %.
%mode plus-flip %in %out %.
%term pfz plus-flip _ plus-z %.
%term pfs
  %pi (plus-flip (%the (plus (s N1) N2 (s N3)) (plus-s Dplus)) (%the (plus (s N1) (s N2) (s (s N3))) (plus-s DIH)))
  %<- (plus-flip Dplus DIH) %.
%worlds () (plus-flip _ _) %.
%total D (plus-flip D _) %.

Finally, using these two lemmas, we may prove the theorem itself:

%sort plus-commutes {_ plus N1 N2 N3} {_ plus N2 N1 N3} %.
%mode plus-commutes %in %out %.
%term pcz %pi (plus-commutes _ D) %<- (plus-zero-id N1 D) %.
%term pcs
  %pi (plus-commutes (%the (plus (s N1') N2 (s N3')) (plus-s Dplus)) D)
  %<- (plus-commutes Dplus DIH)
  %<- (plus-flip DIH D) %.

The theorem checks: given a derivation of plus N1 N2 N3, there exists a derivation of plus N2 N1 N3.

%worlds () (plus-commutes _ _) %.
%total D (plus-commutes D _) %.