Properties of addition

Executable Specification

[View add.mod]

add z N N.
add (s A) B (s C) :- add A B C.

nat z.
nat (s N) :- nat N.

Reasoning

[View add.thm] [Show All Proofs] [Hide All Proofs]

Click on a command or tactic to see a detailed view of its use.

%% Properties of addition
%%
%% We turn the type nat into a predicate so that we can induct on it.

% Add is commutative

Theorem add_base : forall N, {nat N} -> {add N z N}. [Show Proof][Hide Proof]
induction on 1. intros. case H1. search.
  apply IH to H2. search.

Theorem add_step : forall A B C, {add A B C} -> {add A (s B) (s C)}. [Show Proof][Hide Proof]
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.

Theorem add_comm : forall A B C, {nat B} -> {add A B C} -> {add B A C}. [Show Proof][Hide Proof]
induction on 2. intros. case H2.
  apply add_base to H1. search.
  apply IH to H1 H3. apply add_step to H4. search.

% Add is deterministic

Theorem add_det : forall A B C D,
  {add A B C} -> {add A B D} -> C = D. [Show Proof][Hide Proof]
induction on 1. intros. case H1.
  case H2. search.
  case H2. apply IH to H3 H4. search.

% Add is associative

Theorem add_assoc : forall A B C AB BC ABC,
  {add A B AB} -> {add AB C ABC} -> {add B C BC} -> {add A BC ABC}. [Show Proof][Hide Proof]
induction on 1. intros. case H1.
  apply add_det to H2 H3. search.
  case H2. apply IH to H4 H5 H3. search.