TD du mardi 6 mars 2012 (TD noté : envoyer le fichier final à 12:15 à Yves.Bertot@inria.fr)

On devra travailler avec les définitions suivantes:

Require Export ZArith String.
Require Export List.
Open Scope Z_scope.
Open Scope string_scope.

Inductive aexpr : Type :=
  avar (s:string) | anum (x:Z) | aplus (e1 e2 : aexpr).

Inductive bexpr : Set :=
  blt (e1 e2 : aexpr).

Inductive instr : Type:=
  skip | assign (s:string) (e:aexpr) 
| sequence (i1 i2 : instr) | while (b : bexpr) (i:instr).

Definition env := list (string * Z).

Inductive aeval : env -> aexpr -> Z -> Prop :=
  ae_num : forall r n, aeval r (anum n) n
| ae_var1 : forall r x v, aeval ((x,v)::r) (avar x) v
| ae_var2 : forall r x y v v' , x <> y -> aeval r (avar x) v' ->
              aeval ((y,v)::r) (avar x) v'
| ae_plus : forall r e1 e2 v1 v2,
              aeval r e1 v1 -> aeval r e2 v2 ->
              aeval r (aplus e1 e2) (v1 + v2).

Inductive beval : env -> bexpr -> bool -> Prop :=
| be_lt1 : forall r e1 e2 v1 v2,
            aeval r e1 v1 -> aeval r e2 v2 ->
            v1 < v2 -> beval r (blt e1 e2) true
| be_lt2 : forall r e1 e2 v1 v2,
            aeval r e1 v1 -> aeval r e2 v2 ->
            v2 <= v1 -> beval r (blt e1 e2) false.

Inductive update : env->string->Z->env->Prop :=
| s_up1 : forall r x v v', update ((x,v)::r) x v' ((x,v')::r)
| s_up2 : forall r r' x y v v', update r x v' r' ->
            x <> y -> update ((y,v)::r) x v' ((y,v)::r').

Inductive exec : env->instr->env->Prop :=
| SN1 : forall r, exec r skip r
| SN2 : forall r r' x e v,
   aeval r e v -> update r x v r' -> exec r (assign x e) r'
| SN3 : forall r r' r'' i1 i2,
    exec r i1 r' -> exec r' i2 r'' ->
    exec r (sequence i1 i2) r''
| SN4 : forall r r' r'' b i,
    beval r b true -> exec r i r' -> 
    exec r' (while b i) r'' ->
    exec r (while b i) r''
| SN5 : forall r b i,
    beval r b false -> exec r (while b i) r.

Première question

Ecrire un énoncé Coq qui correspond à la phrase "Dans l'environnement où x vaut 13 et y vaut 4, l'expression y+38 s'évalue et retourne la valeur 42".

Faire la preuve Coq qui vérifie cette formule logique

Deuxième question

Montrer que si l'on dispose de 4 variables x, y, z et t, pour n'importe quel environnement s, les évaluations des expressions

(x + y) + (z + t)

x + (y + (z + t))

Troisième question

Prouvez l'énoncé suivant:

Lemma update_dif_eval :
  forall s x v1 s', update  s x v1 s' ->
   forall y v2, x <> y -> aeval s (avar y) v2 -> aeval s' (avar y) v2.