<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
(* 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.