# Executable Specification

[View add.sig] [View add.mod]
```sig add.

kind     nat      type.

type     z        nat.
type     s        nat -> nat.

type     nat      nat -> o.
type     add      nat -> nat -> nat -> o.

```
```module add.

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]

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

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

Specification "add".

% Add is commutative

Theorem add_base : forall N, {nat N} -> {add N z N}.
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)}.
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}.
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.
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 ABC,
{add A B AB} -> {add AB C ABC} ->
exists BC, {add B C BC} /\ {add A BC ABC}.
induction on 1. intros. case H1.
search.
case H2. apply IH to H3 H4. search.
% We can use Query to "run add in reverse"

Query {add A B (s (s (s (s z))))}.

Query {add A A (s (s (s (s z))))}.
```