Require Import little_w_string axiom List ZArith parser.
Import str syntax AB A D L.
Notation skip := (@skip str.string).
Definition parse s := un_annot (parse_instr' s).
Close Scope a_scope.


Definition eq_list (l:list Z) :=  
  match l with n1::n2::nil => n1 = n2 | _ => False end.

Definition meanings := ("eq", eq_list)::nil.

Ltac parse_them := unfold parse; parse_it.

Print ax_sem.

Definition ex_i :=
  sequence (assign "x" (aplus (avar "x")(avar "y")))
       (assign "y" (aplus (avar "y") (aplus (avar "x") (avar "x")))).

Definition ex_a :=
  pred "eq" (avar "y"::aplus (avar "x") (aplus (avar "x") (avar "x"))::nil).

(* Exemple de preuve.  A cannibaliser pour votre exercice. *)
Lemma tdax1 :
    exists P, ax_sem meanings P ex_i ex_a.
exists (parse_assert' "eq(x,0)").
apply ax5 with (P':= parse_assert' "eq(y+((x+y)+(x+y)),(x+y)+((x+y)+(x+y)))")
  (Q' := parse_assert' "eq(y,x+(x+x))").
parse_them.
unfold valid, meanings; compute_vcg; expand_semantics; unfold eq_list.
intros g; generalize (g "x") (g "y"); intros x y.
intros x0; rewrite x0; ring.
unfold ex_i.
apply ax3 with (Q:= parse_assert' "eq(y+(x+x),x+(x+x))").
Check ax2.
parse_them.
apply (ax2 meanings 
        (pred "eq" ((aplus (avar "y")(aplus (avar "x")(avar "x")))::aplus (avar "x") (aplus (avar "x")(avar "x"))::nil)) "x" (aplus (avar "x")(avar "y"))).
apply (ax2 meanings 
        (pred "eq"
           (avar "y"::aplus (avar "x") (aplus (avar "x")(avar "x"))::nil))
         "y" (aplus (avar "y") (aplus (avar "x")(avar "x")))).
unfold ex_a.
intros g H; exact H.
Qed.

Definition ex_i2 := Eval vm_compute in parse "x:=1".
Definition ex_a2 := Eval vm_compute in parse_assert' "eq(x,2)".
Print ex_i2.

(* Your turn: try to do this one. *)
Lemma tdax2 :
  exists P, ax_sem meanings P ex_i2 ex_a2.
unfold ex_i2, ex_a2.

(* you should be able to replace this command by Qed. *)
Admitted.

(* Slightly harder. *)

Definition pp (l:list Z) :=
  match l with n1::n2::nil => 2*n1= n2*(n2+1) | _ => False end.
Definition le' (l:list Z) :=
  match l with n1::n2::nil => n1 <= n2 | _ => False end.

Definition ex_i3 := Eval vm_compute in 
  parse "while x < 10 do [ pp(y,x) /\ le(x,10) ] x:=x+1; y:=y+x done".
Print ex_i3.
Definition ex_a3 := Eval vm_compute in parse_assert' "eq(y,55)".
Definition ex_a4 := Eval vm_compute in parse_assert' "eq(x,0)".
Definition m := ("pp", pp)::("le",le')::("eq",eq_list)::nil.

Lemma tdax3 : ax_sem m ex_a4 ex_i3 ex_a3.
unfold ex_a4, ex_a3, ex_i3.
Admitted.