Require Import syntax parser extracted_io boxes Zwf.

(* La syntaxe du langage est définie dans le fichier syntax.v *)
(* Un analyseur syntaxique est fourni dans le fichier parser.v *)

Eval vm_compute in  parse_i "while x < 10 do x := x + 1 done".

Eval vm_compute in parse_e "x + (y + 1)".

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

(* Voici quelques fonctions pour afficher les dérivations.  Il n'est
  pas nécessaire de comprendre tout ce qui se passe ici. *)

Definition ae_sequent (r : env) (e:aexpr) (v : Z) : string :=
  env_to_string r ++ " |- " ++ aexpr_to_string e ++ " -> " ++ Z_to_string v.

Fixpoint ae_to_box r e v (t : aeval r e v) {struct t} : box :=
  match t with
    ae_var1 r x n  => mkrule0 (text (ae_sequent ((x,n)::r) (avar x) n))
  | ae_var2 tl x y n m _ t' => (mkrule2 (text (x ++ "<>" ++ y)) 
                             (ae_to_box tl (avar x) m t')
                             (text (ae_sequent ((y,n)::tl) (avar x) m)))
  | ae_int r n => (mkrule0 (text (ae_sequent r (anum n) n)))
  | ae_plus r e1 e2 n1 n2 t1 t2 =>
    mkrule2 (ae_to_box _ _ _ t1) (ae_to_box _ _ _ t2)
      (text (ae_sequent r (aplus e1 e2) (n1 + n2)))
  end.

Definition ae_display r e v (t : aeval r e v) : string :=
  display (ae_to_box _ _ _ t).

Implicit Arguments ae_display [r e v].

(* C'est la fin du code d'affichage. *)

(* exemple de preuve d'évaluation.  *)

Lemma ex1 : aeval (("x",3)::("y", 5)::nil) (aplus (avar "x")(avar "y")) 8.
apply ae_plus with (v1:=3) (v2:=5).
apply ae_var1.
apply ae_var2.
discriminate.
apply ae_var1.
Defined.

(* Pour afficher cette dérivation correctement, il faut choisir une police
  de largeur fixe. *)
Eval vm_compute in ae_display ex1.

Lemma ex2 : aeval (("x", 2)::("y", 4)::("z", 7)::nil)
                (aplus (aplus (anum 1) (avar "y")) 
                       (aplus (avar "x") (aplus (anum 2) (avar "z"))))
                16.
(* C'est votre tour. *)


Defined.

(* Voici la description du jugement d'évaluation des expressions booléennes. *)
Inductive beval : env -> bexpr -> bool -> prop :=
  blt_true : forall r e1 e2 v1 v2,
    aeval r e1 v1 -> aeval r e2 v2 -> v1 < v2 ->
    beval r (blt e1 e2) true
| blt_false : forall r e1 e2 v1 v2,
    aeval r e1 v1 -> aeval r e2 v2 -> v2 <= v1 ->
    beval r (blt e1 e2) false.

(* Voici la description du jugement de mise à jour. *)

Inductive update : env->string->Z->env->prop :=
| up1 : forall r x v v', update ((x,v)::r) x v' ((x,v')::r)
| up2 : forall r r' x y v v', update r x v' r' ->
            x <> y -> update ((y,v)::r) x v' ((y,v)::r').

(* Maintenant c'est à nouveau votre tour, complétez la définition suivante. *)

Inductive exec : env -> instr -> env -> prop :=


(* La directive "Eval vm_compute in" dans la définition suivante impose que
 l'analyse syntaxique soit faite au moment de la définition, pas au moment
 de chaque utilisation. *)
Definition i_ex := Eval vm_compute in
   match parse_i "while x < 1 do x := x + 1 done" with
   Some i => i | _ => assign "x" (anum 0) end.

Eval vm_compute in i_ex.

Lemma ex3 : exec (("x", 0)::nil) i_ex (("x", 1)::nil).

Defined.

(* Exercice très difficile!
   Nous allons maintenant nous intéresser à l'énoncé suivant. *)

Definition ex4_statement := 
   forall m n, 0 <= m -> 
      exec (("x", n)::nil) 
           (while (blt (avar "x") (anum (n+m)))
                      (assign "x" (aplus (avar "x") (anum 1))))
           (("x", n+m)::nil).

(* Nous prouverons cet énoncé par récurrence sur m.  Pour cela, nous
  allons utiliser un principe de récurrence sur les entiers positifs.
  Lisez bien l'énoncé du lemme suivant, il permet de faire des preuves
  par récurrence sur les entiers. *)

Lemma pos_well_founded_induction :
  forall P : Z -> prop,
       (forall x : Z, (forall y : Z, 0 <= x /\ y < x -> P y) -> P x) ->
       forall x : Z, P x.
exact (Fix (Zwf_well_founded 0)).
Defined.

(* C'est votre tour ! *)
Lemma ex4 : ex4_statement.
unfold ex4_statement.
intros m; induction m using pos_well_founded_induction.

(* Il y a deux cas: soit m = 0 soit m <> 0. Utilisez Zeq_bool et
  Zeq_cases pour distinguer entre ces deux cas et pour faire les preuves. *)