Abella logo (small)

add.thm

%% Properties of addition %% %% 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))))}.