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.
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}. Theorem add_step : forall A B C, {add A B C} -> {add A (s B) (s C)}. 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. % 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}. % 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))))}.