(* 
Fragment of the Coq encoding described in the paper
"Theorem proving support in programming language smenatics"

Prog.Lang. syntax + Natural Semantics + Axiomatic Semantics
correctness proof of the Axiomatic Semantics wrt. Natural Semantics

Author: Yves Bertot
*)


Require Import ZArith List.

Set Implicit Arguments.

Open Scope Z_scope.


Parameter string : Set.

Parameter string_dec : forall a b:string, {a=b}+{a<>b}.
Parameter false_cst : string.
Parameter true_cst : string.
Parameter between_cst : string.
Parameter ge_cst : string.
Parameter le_cst : string.
Parameter lt : string -> string -> Prop.

Axiom lt_irrefl : forall x, ~lt x  x.
Axiom lt_trans : forall x y z, lt x y -> lt y z -> lt x z.

Axiom all_distinct :
  lt between_cst false_cst /\ lt false_cst ge_cst /\ 
  lt ge_cst le_cst /\ lt le_cst true_cst.


(* ************** Prog.Lang. Syntax ************** *)

Inductive aexpr : Set := 
    avar : string -> aexpr
  | anum : Z -> aexpr
  | aplus : aexpr -> aexpr -> aexpr.

Inductive bexpr : Set :=  
    blt :  aexpr -> aexpr -> bexpr.

Inductive instr : Set :=
    assign : string -> aexpr -> instr 
  | sequence : instr -> instr -> instr
  | while : bexpr -> instr -> instr
  | skip : instr.

Inductive assert : Set :=
    a_b : bexpr -> assert
  | a_not : assert -> assert
  | a_conj : assert -> assert -> assert
  | pred : string -> list aexpr -> assert.

Inductive condition : Set :=
    c_imp : assert -> assert -> condition.



(* ************** Natural Semantics ************** *)

Definition env := list(string*Z).

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

Hint Resolve ae_int ae_var1 ae_var2 ae_plus.

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 s_update : env->string->Z->env->Prop :=
| s_up1 : forall r x v v', s_update ((x,v)::r) x v' ((x,v')::r)
| s_up2 : forall r r' x y v v', s_update r x v' r' ->
            x <> y -> s_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 -> s_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.


Hint Resolve be_lt1 be_lt2 s_up1 s_up2 SN1 SN2 SN3 SN4 SN5.




(* ************** Axiomatic Semantics ************** *)

Fixpoint subst (e:aexpr)(s:string)(v:aexpr) {struct e} : aexpr :=
  match e with
    avar s' =>
      if string_dec s s' then v else e
  | anum n => anum n
  | aplus e1 e2 => aplus (subst e1 s v) (subst e2 s v)
  end.

Definition b_subst (b:bexpr) (s:string) (v:aexpr) : bexpr :=
  match b with blt e1 e2 => blt (subst e1 s v)(subst e2 s v) end.

Fixpoint l_subst (l:list aexpr)(s:string)(v:aexpr) {struct l} : list aexpr :=
  match l with 
    nil => nil
  | a::tl => subst a s v::l_subst tl s v
  end.

Fixpoint a_subst (a:assert)(s:string)(v:aexpr) {struct a} :assert :=
  match a with
    a_b e => a_b (b_subst e s v)
  | a_not a => a_not (a_subst a s v)
  | pred p l => pred p (l_subst l s v)
  | a_conj a1 a2 => a_conj(a_subst a1 s v)(a_subst a2 s v)
  end.


Fixpoint af' (g:string->Z)(a:aexpr) {struct a} : Z :=
  match a with
    avar s => g s
  | anum n => n
  | aplus e1 e2 => af' g e1 + af' g e2
  end.

Fixpoint lf' (g:string->Z)(l:list aexpr){struct l} : 
   list Z :=
   match l with
     nil => nil
   | e::tl => af' g e::lf' g tl
   end.


Definition p_env := list(string*(list Z->Prop)).

Fixpoint f_p (preds : p_env)
  (s:string) (args:list Z) {struct preds} : Prop :=
  match preds with
    (a,m)::tl =>
    if string_dec a s then m args else f_p tl s args
  | nil => True
  end.

Definition bf' (g:string->Z)(b:bexpr) : Prop :=
 match b with
   blt e1 e2 => af' g e1 < af' g e2
 end.

Fixpoint i_a 
  (preds: p_env) (g:string->Z)(a:assert) {struct a}: Prop :=
  match a with
    a_b e => bf' g e
  | a_not a => ~ i_a preds g a
  | pred p l => f_p preds p (lf' g l)
  | a_conj a1 a2 =>
    i_a preds g a1 /\ i_a preds g a2
  end.

Definition i_c (m: p_env) (g:string->Z)(c:condition) :=
match c with
  c_imp a1 a2 => i_a m g a1 -> i_a m g a2
end.

Definition valid (preds: p_env) (c:condition) :=
  forall g, i_c preds g c.


Inductive ax_sem (preds : p_env) :
      assert -> instr -> assert -> Prop :=
  ax1 : forall P, ax_sem preds P skip P
| ax2 : forall P x e, ax_sem preds (a_subst P x e) (assign x e) P
| ax3 : forall P Q R i1 i2, 
          ax_sem preds P i1 Q -> ax_sem preds Q i2 R ->
          ax_sem preds P (sequence i1 i2) R
| ax4 : forall P b i,
          ax_sem preds (a_conj (a_b b) P) i P ->
          ax_sem preds P (while b i) (a_conj (a_not (a_b b)) P)
| ax5 : forall P P' Q' Q i,
        valid preds (c_imp P P') -> ax_sem preds P' i Q' ->
        valid preds (c_imp Q' Q) ->
        ax_sem preds P i Q.

Inductive nax (preds: p_env) :
  assert -> instr -> assert -> Prop :=
  nax1 : forall P Q, valid preds (c_imp P Q) ->
      nax preds P skip Q
| nax2 : forall P P' Q x e,
    valid preds (c_imp P (a_subst P' x e)) ->
    valid preds (c_imp P' Q) ->
    nax preds P (assign x e) Q
| nax3 : forall P P' Q' R' R i1 i2,
    valid preds (c_imp P P') ->
    valid preds (c_imp R' R) ->
    nax preds P' i1 Q' -> nax preds Q' i2 R' ->
    nax preds P (sequence i1 i2) R
| nax4 : forall P P' Q b i,
    valid preds (c_imp P P') ->
    valid preds (c_imp (a_conj (a_not (a_b b)) P') Q) ->
    nax preds (a_conj (a_b b) P') i P' ->
    nax preds P (while b i) Q.

Fixpoint i_lc (preds: list (string*(list Z->Prop)))
  (g:string->Z)(l:list condition) {struct l}: Prop :=
  match l with
    nil => True
  | c::tl => i_c preds g c /\ i_lc preds g tl
  end.

Fixpoint e_to_f(r:list(string*Z))(g:string->Z)(var:string):Z :=
  match r with
    nil => g var
  | (s,v)::tl =>
    if string_dec s var then v else e_to_f tl g var
  end.

Notation "r @ g" := (e_to_f r g) (at level 30, right associativity): a_scope.
Delimit Scope a_scope with A.
Open Scope a_scope.


(* Correctness proofs: axiomatic semantics is correct. *)


Lemma af'_correct : forall r1 e v g,
  aeval r1 e v -> af' (r1@g) e = v.
intros r1 e v g H; induction H; simpl; auto.
case (string_dec x x); auto.
intros Habs; elim Habs; auto.
simpl in IHaeval; case (string_dec y x); auto.
intros Hxy ; assert (Habs:x<>y) by auto; elim Habs; auto.
rewrite IHaeval1; rewrite IHaeval2; auto.
Qed.


Lemma update_af' : forall x v r1 r2 g,
  s_update r1 x v r2 -> af' (r2@g) (avar x) = v.
intros x v r1 r2 g H; induction H.
simpl; case (string_dec x x); auto.
intros Habs; case Habs; auto.
simpl; case (string_dec y x).
intros Hxy.
assert (Hnxy : x<> y) by assumption; case Hnxy; auto.
intros _; simpl in IHs_update; apply IHs_update.
Qed.

Lemma update_af'_diff : forall x v r1 r2 g s,
  s_update r1 x v r2 -> x <> s -> 
  af' (r2@g)(avar s) = af' (r1@g) (avar s).
intros x v r1 r2 g s H; induction H; intros Hnxs.
simpl; case (string_dec x s).
intros Hxs; elim Hnxs; auto.
auto.
simpl; case (string_dec y s); auto.
Qed.


Lemma update_af'_var_subst : forall r1 x v r2 e g s,
  s_update r1 x v r2 -> aeval r1 e v ->
  af' (r2@g) (avar s) = af' (r1@g) (subst (avar s) x e).
intros r1 x v r2 e g s H He; simpl subst.
case (string_dec x s).
intros; subst s; rewrite (@af'_correct r1 e v); auto.
apply update_af' with (1:= H).
intros Hnxs; apply update_af'_diff with (1:= H); auto.
Qed.

    
Lemma update_af'_subst : forall r1 x v r2 e' g e, 
  s_update r1 x v r2 -> aeval r1 e' v ->
  af' (r2@g) e = af' (r1@g) (subst e x e').
intros r1 x v r2 e' g e Hup He'; induction e.
apply update_af'_var_subst with (1:= Hup); auto.
trivial.
simpl; rewrite IHe1; rewrite IHe2; auto.
Qed.

Lemma update_lf'_subst :
  forall r1 x v r2 e' g l, s_update r1 x v r2 -> aeval r1 e' v ->
  lf' (r2@g) l = lf' (r1@g) (l_subst l x e').
intros r1 x v r2 e' g l Hu He'; induction l.
simpl; auto.
simpl; rewrite update_af'_subst with (1:= Hu)(2:= He').
rewrite IHl; auto.
Qed.


Lemma update_f_p_subst :
  forall r1 x v r2 e' m g s l, s_update r1 x v r2 -> aeval r1 e' v ->
  (f_p m s (lf' (r1@g) (l_subst l x e')) <-> f_p m s (lf' (r2@g) l)).
intros r1 x v r2 e' m g s l Hu He'; induction m.
simpl; intros; split; auto.
destruct a as [p1 P]; simpl; case (string_dec p1 s).
rewrite update_lf'_subst with (1:= Hu) (2:= He').
intros; split; auto.
intros; apply IHm.
Qed.

Lemma a_subst_correct :
  forall a r1 e v m g r2 x,
    aeval r1 e v ->
    s_update r1 x v r2 ->
    (i_a m (r1@g) (a_subst a x e)<->
    i_a m (r2@g) a).
induction a; simpl; intros r1 e v m g r2 x H Hu.
destruct b as [e1 e2]; unfold bf', b_subst.
repeat rewrite update_af'_subst with (1:= Hu) (2:=H); split; auto.
split; intros H1 Habs; case H1; 
elim (IHa r1 e v m g r2 x H Hu); auto.
split; intros [H1 H2]; (split; [elim (IHa1 r1 e v m g r2 x H Hu)|
                               elim (IHa2 r1 e v m g r2 x H Hu)]); auto.
apply update_f_p_subst with (1:=Hu)(2:=H).
Qed.

Lemma beval_true_interpret :
  forall r b g, beval r b true -> bf' (r@g) b.
intros r b g H; inversion H; simpl.
rewrite (@af'_correct r e1 v1);
 try rewrite (@af'_correct r e2 v2); auto.
Qed.

Lemma beval_false_interpret :
  forall r b g, beval r b false -> ~ bf' (r@g) b.
intros r b g H; inversion H; simpl.
rewrite (@af'_correct r e1 v1);
 try rewrite (@af'_correct r e2 v2); auto with zarith.
Qed.

Hint Resolve beval_true_interpret beval_false_interpret.

Lemma ax_sem_nax :
  forall m P i Q, ax_sem m P i Q -> nax m P i Q.
induction 1.
apply nax1; red; simpl; auto.
apply nax2 with P; red; simpl; auto.
apply nax3 with P Q R; try red; simpl; auto.
apply nax4 with P; try red; simpl; auto.
inversion_clear IHax_sem.
apply nax1; unfold valid in *; simpl in *; auto.
apply nax2 with P'0; unfold valid in *; simpl in *; auto.
apply nax3 with P'0 Q'0 R'; unfold valid in *; simpl in *; auto.
apply nax4 with P'0; unfold valid in *; simpl in *; auto.
Qed.

Hint Resolve ax1 ax2 ax3 ax4.

Lemma nax_ax_sem :
  forall m P i Q, nax m P i Q -> ax_sem m P i Q.
induction 1.
apply ax5 with Q Q; unfold valid in *; simpl in *; eauto.
apply ax5 with (a_subst P' x e) P'; simpl in *; eauto.
apply ax5 with P' R'; simpl in *; eauto.
apply ax5 with P' (a_conj (a_not (a_b b)) P'); simpl in *; eauto.
Qed.

Theorem nax_sound :
  forall m r i r' g, exec r i r' -> 
  forall P Q, nax m P i Q ->
  i_a m (r@g) P -> i_a m (r'@g) Q.
Proof.
intros m r i r' g H; induction H; intros P Q Ha; inversion Ha;
unfold valid in *; simpl in *; intros; subst; clear Ha; eauto.
match goal with
 H: aeval _ _ _, G: s_update _ _ _ _ |- _ =>
 destruct (@a_subst_correct P' _ _ _ m g _ _ H G) as [Hs1 _]
end; auto.
match goal with
  H:nax m (a_conj _ ?P') ?i1 ?Q',G:exec _ (while ?b _) ?r'',
  K: _ |- _ => assert (Ha := H); apply K;
  change (i_a m (r''@g) (a_conj (a_not (a_b b)) P'));
  apply IHexec2 with (P:=P')
end.
apply nax4 with (3:= Ha); unfold valid; simpl; auto.
apply IHexec1 with (1:= Ha); simpl; auto.
Qed.

Theorem ax_sem_sound :
  forall m r i r' g P Q, exec r i r' -> ax_sem m P i Q ->
  i_a m (r@g) P -> i_a m (r'@g) Q.
intros; eapply nax_sound; eauto.
apply ax_sem_nax; auto.
Qed.