%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Illustrating the use of the `compute` tactic
Specification "nat".
Define $nat : nat -> prop by
; $nat z
; $nat (s X) := $nat X.
%% declare that `compute` must suspend on `$nat X` if `X` is flex.
Suspend $nat X.
%% can also say:
%%
%% Suspend $nat X := X.
%%
%% If the := part is omitted, then *all* the variables in the head
%% must be flex.
Theorem ten : forall X, $nat (s^10 X) -> $nat X.
intros. compute H1. search.
% can also say `compute *H1` to get rid of H1
Define leq : nat -> nat -> prop by
; leq z X
; leq (s X) (s Y) := leq X Y.
Suspend leq X _.
%% Equivalently: Suspend leq X Y := X.
Theorem filter : forall X L, member X (s^10 z :: s^9 z :: s^8 z :: L) -> leq X (s^5 z) -> member X L.
/* Built-in: Suspend member E L := L. */
intros. compute H1 H2. search.
Theorem filter_alt : forall X L, member X (s^10 z :: s^9 z :: s^8 z :: L) -> leq X (s^5 z) -> member X L.
% the "compute (all)" form tries compute on all hypotheses
intros. compute (*all). search.
Define plus : nat -> nat -> nat -> prop by
; plus z X X := $nat X
; plus (s X) Y (s Z) := plus X Y Z.
Suspend plus X _ Z.
%% Equivalently: plus X Y Z := X, Z.
Theorem eight : forall X, plus (s^3 z) X (s^8 z) -> X = s^5 z.
intros. compute (*all). search.
Theorem nine : forall X Y, plus (s^3 z) X (s^8 z) -> plus Y (s^4 z) (s^9 z) -> X = Y.
intros. compute (all). search.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Some other minor uses of compute
Theorem plus_invert : forall M N K, plus M N K -> $nat M /\ $nat N /\ $nat K.
induction on 1. intros. case H1.
search.
apply IH to H2. search.
Theorem plus_zero : forall N, $nat N -> plus N z N.
induction on 1. intros. case H1.
search.
apply IH to H2. search.
Theorem plus_succ : forall M N K, plus M N K -> plus M (s N) (s K).
induction on 1. intros. case H1.
search.
apply IH to H2. search.
Theorem plus_comm : forall M N K, $nat K -> plus M N K -> plus N M K.
induction on 2. intros. case H2.
apply plus_zero to H1. search.
compute *H1. apply IH to H4 H3. apply plus_succ to H5. search.
Theorem plus_assoc : forall A B C AB ABC,
plus A B AB -> plus AB C ABC -> exists BC, plus B C BC /\ plus A BC ABC.
induction on 1. intros. case H1.
apply plus_invert to H2. search.
compute *H2. apply IH to H3 H4. search.
Theorem plus_det : forall M N J K, plus M N J -> plus M N K -> J = K.
induction on 1. intros. case H1.
case H2. search.
case H2. apply IH to H3 H4. search.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Fibonacci
Define fib : nat -> nat -> prop by
; fib z z
; fib (s z) (s z)
; fib (s (s X)) F := exists A B, fib (s X) A /\ fib X B /\ plus A B F.
Suspend fib (s X) _.
Suspend fib X _.
%% The order matters only insofar as it may change the order of subgoals
%% produced by compute.
Theorem fib_three : forall F, fib (s^3 z) F -> F = s^2 z.
intros. compute *H1. search.
Theorem fib_four : forall F, fib (s^4 z) F -> F = s^3 z.
intros. compute *H1. search.
Theorem fib_five : forall F, fib (s^5 z) F -> F = s^5 z.
intros. compute *H1. search.
Theorem fib_six : forall F, fib (s^6 z) F -> F = s^8 z.
intros. compute *H1. search.
Theorem fib_seven : forall F, fib (s^7 z) F -> F = s^13 z.
intros. compute *H1. search.
Theorem fib_det : forall A B C, fib A B -> fib A C -> B = C.
induction on 1. intros. case H1.
compute *H2. search.
compute *H2. search.
compute *H2.
apply IH to H4 H7. apply IH to H3 H8.
apply plus_det to H5 H6. search.
Theorem three_solutions : forall N, (N = z \/ N = s z \/ N = s^5 z) -> fib N N.
intros. compute H1. search. search. search 10.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Spec logic
Type p nat -> o.
% Suspend p X.
%% if you suspend p, then the following won't work
Theorem p_cases : forall X Y Z, {p X, p Y |- p Z} -> Z = X \/ Z = Y.
intros.
compute H1. search. search.
%% suspension of spec predicates is allowed
Suspend is_nat X.
Theorem spec_ten : forall X, {is_nat (s^10 X)} -> {is_nat X}.
intros.
compute H1. search.
Theorem no_progress : forall X Y, {is_nat X |- is_nat Y} -> false.
intros. compute H1. % no progress is possible because is_nat Y is suspended
abort.
Theorem no_progress_nabla : nabla X Y, {is_nat X |- is_nat Y} -> false.
intros. compute H1. % this will work because nominal constants are not eigenvariables
