TD du mardi 22 février

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 1 et y vaut 2, l'expression x+y s'évalue et retourne la valeur 3".

Faire la preuve Coq qui vérifie cette formule logique

Deuxième question

Ecrire le programme qui contient deux affectations, dont la première incrémente de 1 la valeur de "x" et la deuxième incrémente de 2 la valeur de "y"

Faire la preuve que ce programme peut être exécuté dans l'environnement où "x" vaut initialement 1 et "y" vaut initialement 2

Troisième question

On utilisera les théorèmes supplémentaires suivant

Lemma Z_of_nat_S_gt_0 : 
  forall n, 0 < Z_of_nat (S n).
intros n; rewrite <- (inj_lt_iff 0); apply lt_O_Sn.
Qed.

Check Zle_refl.

Lemma Z_of_nat_S : forall n, Z_of_nat (S n) = Z_of_nat n + 1.
intros n; rewrite inj_S; ring.
Qed.

On considère le programme suivant

while (blt (anum 0) (avar "x")) (assign "x" (aplus (avar "x") (anum (-1))))