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

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

(* Nous encoderons les environnements par des listes de paires. *)

Definition env := list (string*Z).

(* Voici l'encodage en Coq des règles d'évaluation pour les expressions
  arithmétiques. *)

Inductive aeval : env -> aexpr -> Z -> Prop :=
  ae_int : 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 bexpr := blt (e1 e2 : aexpr).

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

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

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.


(* Ecrivez une fonction booléenne sur les instruction qui indique
   si une variable fixee est affectée dans une instruction.

   Vous devez obtenir une fonction de type

   modified : string -> instr -> bool

*)


(* Démontrez que lors qu'un programme ne modifie pas une variable
  et que ce programme s'exécute et termine, alors la valeur finale
  de cette variable est inchangé par rapport à la valeur initiale. *)



Lemma not_modified_unchanged:
  forall x v r i r', exec r i r' -> modified x i = false ->
     aeval r (avar x) v -> aeval r' (avar x) v.

(* La preuve fait une quarantaine de lignes et peut faire appel à un
  deuxième lemme.  Deux preuves par récurrences sur des propriétés inductives
  sont à prévoir. *)