(* 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.