(* Exercise coq_nat_11 *)
(* Do you know that having stamps of nominals 3 and 5 you can
pay any value greater or equal than 8?
Below is a Coq specification of this statemant - can you
prove it? *)
Require Import Arith.
(* Hint: for arithmetical reasoning you may try to use the
'lia' tactic.
This is one of the powerful automated Coq tactics, that
solves problems in linear arithmetic.
In the first exercises we did, I advised you to not use
too much automation, because it is good to understand the
underlying principles. In general, and also for the assignment,
it is ok to use lia.
Remark: if afterwards you decide to try to prove it without
the use of lia, it should give you a good idea
of how helpful such automated tactics can be!
*)
Require Import Lia.
Lemma stamps : forall i, exists v3, exists v5, i + 8 = 3*v3 + 5*v5.
Proof.
induction i.
- exists 1.
exists 1.
auto.
- destruct IHi.
destruct H.
destruct x0. (* distinguishing cases x0 = 0 or x0 = S x1 *)
* destruct x. (* distinguishing cases x = 0 or x = S x2 *)
+ simpl in H.
(* it can be shown that the context is inconsistent using
some simple arithmetic, and we can prove that using "lia"
lia can solve simple arithmetic goals that have no quantifiers
so we proceed as follows
one could also do
assert (~(i+8 = 0)).
lia.
contradiction.
*)
lia.
+ destruct x. (* distinguishing cases x = 0 or x = S x2 *)
-- simpl in H.
(* we are in a similar situation as before, the context is
inconsistent using some simple arithmetic *)
lia.
-- destruct x.
** simpl in H.
lia.
(* Now the real choices have to be made! *)
** exists x.
exists 2.
lia.
* exists (x+2).
exists x0.
lia.
Qed.