(* Exercise 1 *)
(* Consider the following definitions *)
(* Note: any theorem --- either proven or admitted --- can be used for proving the following
ones *)
Require Import Omega.
Inductive Even : nat -> Prop :=
| Ev0: Even 0
| Ev2 : forall n, Even n -> Even (S (S n)).
Definition Odd n := Even (S n).
(* Prove the following lemmas (remove the Admitted) *)
Lemma E6: Even 6.
Admitted.
Lemma O7 : Odd 5.
Admitted.
Lemma E_double : forall n:nat, Even (2*n).
Admitted.
Lemma not_E1 : ~ Even 1.
Admitted.
Lemma Even_SS_inv : forall n, Even (S (S n)) -> Even n.
Admitted.
Lemma Odd_not_Even : forall n, Odd n -> ~ Even n.
Admitted.
Lemma Even_not_Odd : forall n, Even n -> ~ Odd n.
Admitted.
Lemma Even_double : forall n, Even n -> exists p:nat, n = p + p.
Admitted.
Lemma Odd_S_double : forall n, Odd n -> exists p:nat, n = S( p + p).
Admitted.
(* Consider the following function *)
Fixpoint evenb (n: nat): bool :=
match n with O => true
| 1 => false
| S (S p) => evenb p
end.
Lemma evenb_Sn : forall n:nat, evenb (S n) = negb (evenb n).
Admitted.
Lemma evenb_if : forall n:nat, if evenb n then Even n else Odd n.
Admitted.
Lemma evenb_iff : forall n, evenb n = true <-> Even n.
Admitted.
Goal Even 560.
rewrite <- evenb_iff.
reflexivity.
Qed.
(* Exercise 2 *)
(* Consider the following definitions *)
Require Import Arith.
Definition Le (n p : nat) : Prop := exists q:nat, q + n = p.
Fixpoint LE (n p: nat): Prop :=
match n, p with 0, _ => True
| S _, 0 => False
| S n', S p' => LE n' p'
end.
(* Prove the following theorems
Note: any theorem --- either proven or admitted --- can be used for proving the following
ones *)
Lemma le_Le : forall n p, n <= p -> Le n p.
Admitted.
Lemma Le_le : forall n p, Le n p -> n <= p.
Admitted.
Lemma LE_n : forall n, LE n n.
Admitted.
Lemma LE_S : forall n p, LE n p -> LE n (S p).
Admitted.
Lemma le_LE : forall n p, n <= p -> LE n p.
Admitted.
Lemma LE_Le : forall n p, LE n p -> Le n p.
Admitted.
Require Import Max.
Lemma le_leb_iff : forall n p, n <= p <-> leb n p = true.
Lemma lt_lb_iff : forall n p, p < n <-> leb n p = false
Use these lemmas for proving :
Lemma leb_max : forall n p, max n p = if leb n p then p else n.
(*
Hint : execute the command
SearchAbout [le max].
*)
(* Exercise 3 *)
(* Consider the following declarations : *)
Require Import List.
Section On_index.
Variable A : Type.
Variable eqAb : A -> A -> bool.
Inductive eqA_spec (a b:A):bool -> Prop :=
eqA_eq : forall Heq :a = b, eqA_spec a b true
|eqA_diff : forall Hdiff: a <> b , eqA_spec a b false.
Hypothesis eqAbP : forall a b, eqA_spec a b (eqAb a b).
(* Give an inductive definition of the predicate
is_nth a n l : Prop
the maeaning of which is "a is the i-th element of the list l" *)
(* We now consider the following specification *)
Inductive index_spec (a:A)(l:list A):(option nat)->Prop :=
| success : forall i (Hsuccess:is_nth a i l), index_spec a l (Some i)
| failure : forall (Hfail : forall i, ~ is_nth a i l), index_spec a l None.
Definition index_ok (idx : A -> list A -> option nat) :=
forall a l, index_spec a l (idx a l).
(* Define a recursive function
index (a:A)(l:list A) : option nat
and prove your function is correct *)
(* Prove the following lemmas *)
Lemma index_is_nth: forall a l i, index a l = Some i -> is_nth a i l.
Lemma is_nth_index: forall a l i, is_nth a i l -> exists j, index a l = Some j.
(* Exercise 4 : borrowed and adapted from B. Pierce's
course "Software Foundations"*)
(* We define the following toy language: *)
Inductive tm : Type :=
| tm_const : nat -> tm
| tm_plus : tm -> tm -> tm.
(* Here is a big step evaluator for this language *)
Inductive eval : tm -> nat -> Prop :=
| E_Const : forall n,
eval (tm_const n) n
| E_Plus : forall t1 t2 n1 n2,
eval t1 n1 ->
eval t2 n2 ->
eval (tm_plus t1 t2) (plus n1 n2).
(* Here is a small step evaluator for this language *)
Inductive step : tm -> tm -> Prop :=
| ST_PlusConstConst : forall n1 n2,
step (tm_plus (tm_const n1) (tm_const n2))
(tm_const (plus n1 n2))
| ST_Plus1 : forall t1 t1' t2,
(step t1 t1')
-> step (tm_plus t1 t2)
(tm_plus t1' t2)
| ST_Plus2 : forall n1 t2 t2',
(step t2 t2')
-> step (tm_plus (tm_const n1) t2)
(tm_plus (tm_const n1) t2').
(*A few things to notice:
* We are defining just a single reduction step, in which one
tm_plus node is replaced by its value.
* Each step finds the leftmost tm_plus node that is "ready to go"
(both of its operands are constants) and reduces it. The first
rule tells how to reduce this tm_plus node itself; the other two
rules tell how to find it.
* A term that is just a constant cannot take a step.
*)
(* Prove that: *)
Lemma step_plus_l : forall t1 t1' t2, step t1 t1' ->
step (tm_plus t1 t2) (tm_plus t1' t2).
(* Prove that evaluation is deterministic: *)
Lemma eval_det : forall t n1 n2, eval t n1 -> eval t n2 -> n1 = n2.
(* We can also prove that step is deterministic :
We must show that if x steps to both y1 and y2 then y1 and y2 are *)
(*equal. Consider the last rules used in the derivations of step x y1 *)
(*and step x y2.
* If both are ST_PlusConstConst, the result is immediate.
* It cannot happen that one is ST_PlusConstConst and the other is
ST_Plus1 or ST_Plus2, since this would imply that x has the form
tm_plus t1 t2 where both t1 and t2 are constants (by
ST_PlusConstConst) AND one of t1 or t2 has the form tm_plus ....
* Similarly, it cannot happen that one is ST_Plus1 and the other
is ST_Plus2, since this would imply that x has the form tm_plus
t1 t2 where t1 has both the form tm_plus t1 t2 and the form
tm_const n.
* The cases when both derivations end with ST_Plus1 or ST_Plus2
follow by the induction hypothesis.
*)
Theorem step_deterministic :
forall t t1 t2, step t t1 -> step t t2 -> t1 = t2.
Admitted.