(* Exercise 1 *)
(* Program a function rcons : forall A, A -> list A -> list A which *)
(*add an element at the end of a list *)
Require Import List.
(* Use an inductive predicate to characterize lists of natural numbers *)
(*that are palindromes *)
(* Exercise 2 *)
(* Define inductively the following binary relations on types
(list A):
- the list l' is obtained form l by transposing two consecutive
elements
- the list l' is obtained form l by applying the above operation a
finite number of times. Here we say that l' is a permutation of l.
Show that the second relation is an equivalence relation : reflexive,
symmetric, and transitive.
Require Import Relations.
Section perms.
Variable A : Set.
Lemma perm_refl : reflexive _ perm.
Lemma perm_trans : transitive _ perm.
Lemma perm_sym : symmetric _ perm.
Theorem equiv_perm : equiv _ perm.
End perms.
*)
(* Exercise 3 : borrowed and adapted from B. Pierce 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).
Proof.
...
Qed.
(* Prove that evaluation is deterministic: *)
Lemma eval_det : forall t n1 n2, eval t n1 -> eval t n2 -> n1 = n2.
Proof.
...
Qed.
(* 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.
Proof.
...
Qed.