(* 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.
Fixpoint rcons (A : Type)(a : A)(l : list A) : list A :=
match l with
|nil => a :: nil
|hd :: tl => hd :: (rcons A a tl)
end.
(* Use an inductive predicate to characterize lists of natural numbers *)
(*that are palindromes *)
Inductive palindrome : list nat -> Prop :=
|Empty : palindrome nil
|Single : forall n, palindrome (n :: nil)
|Rcons : forall (n : nat)(l : list nat), palindrome (n :: (rcons nat n l)).
(* 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.
*)
Require Import Relations.
Section perms.
Variable A : Set.
Inductive transpose : list A -> list A -> Prop :=
| transpose_hd :
forall (a b:A) (l:list A), transpose (a :: b :: l) (b :: a :: l)
| transpose_tl :
forall (a:A) (l l':list A),
transpose l l' -> transpose (a :: l) (a :: l').
Inductive perm (l:list A) : list A -> Prop :=
| perm_id : perm l l
| perm_tr :
forall l' l'':list A, perm l l' -> transpose l' l'' -> perm l l''.
Lemma perm_refl : reflexive _ perm.
Proof.
unfold reflexive; left.
Qed.
Lemma perm_intro_r :
forall l l1 l2:list A, transpose l l1 -> perm l1 l2 -> perm l l2.
Proof.
intros l l1 l2 H H0; elim H0.
eapply perm_tr; eauto.
left.
intros l' l''; intros; right with l'; auto.
Qed.
Lemma perm_trans : transitive _ perm.
Proof.
unfold transitive; intros l l' l'' H; generalize l''.
elim H.
trivial.
intros l'0 l''0 H0 H1; intros.
apply H1;eapply perm_intro_r; eauto.
Qed.
Lemma transpose_sym : forall l l':list A, transpose l l' -> transpose l' l.
Proof.
intros l l' H;elim H; [ left | right; auto ].
Qed.
Lemma perm_sym : symmetric _ perm.
Proof.
unfold symmetric; intros l l' H; elim H.
left.
intros; eapply perm_intro_r.
eapply transpose_sym; eauto.
auto.
Qed.
Theorem equiv_perm : equiv _ perm.
Proof.
repeat split.
apply perm_refl.
apply perm_trans.
apply perm_sym.
Qed.
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.
intros t1 t1' t2 h12; revert t2.
induction h12; intros t3; simpl.
constructor.
constructor.
constructor.
trivial.
constructor.
constructor.
trivial.
Qed.
(* Prove that evaluation is deterministic: *)
Lemma eval_det : forall t n1 n2, eval t n1 -> eval t n2 -> n1 = n2.
Proof.
intros t n1 n2 h1 h2.
revert n2 h2.
induction h1.
intros n2; simpl.
inversion 1.
trivial.
intros n3 h3.
inversion_clear h3.
rewrite (IHh1_1 n0 H).
rewrite (IHh1_2 n4 H0).
trivial.
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.
intros t t1 t2 Ht1 Ht2.
revert t2 Ht2.
induction Ht1.
intros t3 ht3.
inversion ht3.
reflexivity.
inversion H2.
inversion H2.
intros t3 Ht3.
inversion Ht3.
rewrite <- H0 in Ht1.
inversion Ht1.
rewrite <- (IHHt1 t1'0); trivial.
rewrite <- H in Ht1.
inversion Ht1.
intros t3 Ht3.
inversion Ht3.
rewrite <- H1 in Ht1.
inversion Ht1.
inversion H2.
rewrite <- (IHHt1 t2'0); trivial.
Qed.