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).

Fixpoint lookup (l:list (string*Z)) (x:string) {struct l} : option Z :=
  match l with nil =>
    None
  | (y,n)::tl => if string_dec x y then Some n else lookup tl x
  end.

Definition o_add (ov1 ov2 : option Z) : option Z :=
  match ov1 with
    Some v1 => match ov2 with Some v2 => Some (v1 + v2) | None => None end
  | None => None
  end.

Fixpoint af (l:list (string * Z)) (e:aexpr) {struct e} : option Z :=
  match e with
    avar x => lookup l x
  | anum n => Some n
  | aplus e1 e2 =>
    o_add (af l e1) (af l e2)
  end.

Lemma lookup_complete : forall l e v, aeval l e v ->
  forall x, e = avar x -> lookup l x = Some v.
intros l e v H; induction H.
      intros x h.
      discriminate.
    intros x' q.
    injection q.
    intros xx'.
    simpl.
    case (string_dec x' x).
      intros x'x; reflexivity.
    intros x'nx.
    case x'nx.
    rewrite xx'.
    reflexivity.
  intros x' q.
  injection q.
  intros xx'.
  rewrite <- xx'.
  simpl.
  case (string_dec x y).
    intros xy.
    case H.
    assumption.
  intros _.
  apply IHaeval.
  reflexivity.
intros x abs.
discriminate.
Qed.

Lemma af_complete : forall l e v, aeval l e v -> af l e = Some v.
intros l e v H; induction H.
      reflexivity.
    apply lookup_complete with (e := avar x).
      apply ae_var1.
    reflexivity.
  apply lookup_complete with (e := avar x).
    apply ae_var2.
      assumption.
    assumption.
  reflexivity.
simpl.
rewrite IHaeval1.
rewrite IHaeval2.
simpl.
reflexivity.
Qed.

Lemma lookup_correct : forall l x v, lookup l x = Some v -> aeval l (avar x) v.
induction l.
  simpl. 
  intros x v abs; discriminate.
simpl.
intros x v.
destruct a as [y n].
case (string_dec x y).
intros xy nv.
injection nv.
intros nv'; rewrite nv'.
rewrite xy.
apply ae_var1.
intros xny h.
apply ae_var2.
assumption.
apply IHl.
assumption.
Qed.

Lemma af_correct : forall l e v, af l e = Some v -> aeval l e v.
intros l e; induction e.
    simpl.
    intros v lk.
    apply lookup_correct.
    assumption.
  simpl. 
  intros v h.
  injection h.
  intros nv.
  rewrite nv.
  apply ae_int.
simpl.
intros v.
destruct (af l e1).
  destruct (af l e2).
    intros h; injection h.
    intros hv.
    rewrite <- hv.
    apply ae_plus.
      apply IHe1.
      reflexivity.
    apply IHe2.
    reflexivity.
  intros abs.
  discriminate.
intros abs.
discriminate.
Qed.

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.

Definition bf (r:env)(b:bexpr) : option bool :=
  match b with
    blt e1 e2 =>
    match af r e1 with
      Some v1 =>
      match af r e2 with
        Some v2 => if Zlt_bool v1 v2 then Some true else Some false
      | None => None
      end
    | None => None
    end
  end.

Lemma bf_correct : forall r e v, bf r e = Some v -> beval r e v.
intros r e v.
destruct e as [e1 e2].
simpl.
assert (t1: forall v1, af r e1 = Some v1 -> aeval r e1 v1).
  apply af_correct.
destruct (af r e1) as [v1 | ].
  assert (t2 : forall v2, af r e2  = Some v2 -> aeval r e2 v2).
    apply af_correct.
  destruct (af r e2) as [v2 | ].
    assert (t3 : if Zlt_bool v1 v2 then v1 < v2 else v1 >= v2).
      apply Zlt_cases.
    destruct (Zlt_bool v1 v2).
      intros q.
      injection q.
      intros q'.
      rewrite <- q'.
      apply b_true with (v1:= v1) (v2 := v2).
          apply t1.
          reflexivity.
        apply t2.
        reflexivity.
      assumption.
    intros q.
    injection q.
    intros q'.
    rewrite <- q'.
    apply b_false with (v1:= v1) (v2 := v2).
        apply t1.
        reflexivity.
      apply t2.
      reflexivity.
    omega.
  discriminate.
discriminate.
Qed.

Lemma bf_complete : forall r b v, beval r b v -> bf r b = Some v.
intros r b v H; induction H.
  simpl.
  rewrite (af_complete r e1 v1).
    rewrite (af_complete r e2 v2).
      assert (t3 : if Zlt_bool v1 v2 then v1 < v2 else v1 >= v2).
        apply Zlt_cases.
      destruct (Zlt_bool v1 v2).
        reflexivity.
      assert (abs : False).
        omega.
      case abs.
    assumption.
  assumption.
simpl.
rewrite (af_complete r e1 v1).
  rewrite (af_complete r e2 v2).
    assert (t3 : if Zlt_bool v1 v2 then v1 < v2 else v1 >= v2).
      apply Zlt_cases.
    destruct (Zlt_bool v1 v2).
      assert (abs : False).
        omega.
      case abs.
    reflexivity.
  assumption.
assumption.
Qed.

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').

Fixpoint uf (r:env)(x:string)(v:Z) : option env :=
  match r with
    nil => None
  | (y, v')::r' => 
    if string_dec x y then Some ((y,v)::r')
    else match uf r' x v with
           Some r'' => Some ((y, v')::r'')
         | None => None
         end
  end.

Lemma uf_correct : forall r x v r', uf r x v = Some r' -> update r x v r'.
induction r; intros x v r'.
  simpl.
  discriminate.
destruct a as (y, v').
simpl.
  case (string_dec x y).
  intros xy.
  rewrite xy.
  intros q.
  injection q.
  intros q'.
  rewrite <- q'.
  apply s_up1.
intros xny q.
  assert (t1: forall r'', uf r x v = Some r'' -> update r x v r'').
    apply IHr.
  destruct (uf r x v).
  injection q.
  intros q'.
  rewrite <- q'.
  apply s_up2.
    apply t1.
    reflexivity.
  assumption.
discriminate.
Qed.

Lemma uf_complete :
  forall r x v r', update r x v r' -> uf r x v = Some r'.
intros r x v r' H; induction H.
  simpl.
  case (string_dec x x).
    intros; reflexivity.
  intros abs; case abs.
  reflexivity.
simpl.
case (string_dec x y).
  intros abs; case H0; exact abs.
intros _.
rewrite IHupdate.
reflexivity.
Qed.

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

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.

Fixpoint ef (n:nat)(r:env)(i:instr) : option env :=
  match n with
    0%nat => None
  | S p =>
    match i with 
      assign x e =>
      match af r e with Some v => uf r x v | None => None end
    | sequence i1 i2 =>
      match ef p r i1 with Some r' => ef p r' i2 | None => None end
    | skip => Some r
    | while b i =>
      match bf r b with
        Some true =>
        match ef p r i with Some r' => ef p r' (while b i) | None => None end
      | Some false => Some r
      | None => None
      end
    end
  end.

(* A votre tour : prouvez les lemmes suivants! *)

Lemma ef_correct :
  forall n r i r', ef n r i = Some r' -> exec r i r'.
Admitted.

(* Si vous avez le premier en TD, c'est bien!  Vous pouvez faire les
  lemmes suivant comme travail personnel. *)

Lemma ef_monotonic :
  forall n m r i r', ef n r i = Some r' -> (n <= m)%nat -> ef m r i = Some r'.
Admitted.

Lemma ef_complete :
  forall r i r', exec r i r' -> exists n, ef n r i = Some r'.
Admitted.