Require Import Coqlib.
Require Import Errors.
Require Import Maps.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import AST.
Require Import Csyntax.
Require Cstrategy.
Require Import Clight.
Require Import SimplExpr.

Section SPEC.

Local Open Scope gensym_monad_scope.

Relational specification of the translation.

Translation of expressions

Definition final (dst: destination) (a: expr) : list statement :=
  match dst with
  | For_val => nil
  | For_effects => nil
  | For_test tyl s1 s2 => makeif (fold_left Ecast tyl a) s1 s2 :: nil
  end.

Inductive tr_rvalof: type -> expr -> list statement -> expr -> list ident -> Prop :=
  | tr_rvalof_nonvol: forall ty a tmp,
      type_is_volatile ty = false ->
      tr_rvalof ty a nil a tmp
  | tr_rvalof_vol: forall ty a t tmp,
      type_is_volatile ty = true -> In t tmp ->
      tr_rvalof ty a (Svolread t a :: nil) (Etempvar t ty) tmp.

Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr -> list ident -> Prop :=
  | tr_var: forall le dst id ty tmp,
      tr_expr le dst (C.Evar id ty)
              (final dst (Evar id ty)) (Evar id ty) tmp
  | tr_deref: forall le dst e1 ty sl1 a1 tmp,
      tr_expr le For_val e1 sl1 a1 tmp ->
      tr_expr le dst (C.Ederef e1 ty)
              (sl1 ++ final dst (Ederef a1 ty)) (Ederef a1 ty) tmp
  | tr_field: forall le dst e1 f ty sl1 a1 tmp,
      tr_expr le For_val e1 sl1 a1 tmp ->
      tr_expr le dst (C.Efield e1 f ty)
              (sl1 ++ final dst (Efield a1 f ty)) (Efield a1 f ty) tmp
  | tr_val_effect: forall le v ty any tmp,
      tr_expr le For_effects (C.Eval v ty) nil any tmp
  | tr_val_value: forall le v ty a tmp,
      typeof a = ty ->
      (forall tge e le' m,
         (forall id, In id tmp -> le'!id = le!id) ->
         eval_expr tge e le' m a v) ->
      tr_expr le For_val (C.Eval v ty)
                           nil a tmp
  | tr_val_test: forall le tyl s1 s2 v ty a any tmp,
      typeof a = ty ->
      (forall tge e le' m,
         (forall id, In id tmp -> le'!id = le!id) ->
         eval_expr tge e le' m a v) ->
      tr_expr le (For_test tyl s1 s2) (C.Eval v ty)
                   (makeif (fold_left Ecast tyl a) s1 s2 :: nil) any tmp
  | tr_sizeof: forall le dst ty' ty tmp,
      tr_expr le dst (C.Esizeof ty' ty)
                   (final dst (Esizeof ty' ty))
                   (Esizeof ty' ty) tmp
  | tr_alignof: forall le dst ty' ty tmp,
      tr_expr le dst (C.Ealignof ty' ty)
                   (final dst (Ealignof ty' ty))
                   (Ealignof ty' ty) tmp
  | tr_valof: forall le dst e1 ty tmp sl1 a1 tmp1 sl2 a2 tmp2,
      tr_expr le For_val e1 sl1 a1 tmp1 ->
      tr_rvalof (C.typeof e1) a1 sl2 a2 tmp2 ->
      list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp ->
      tr_expr le dst (C.Evalof e1 ty)
                    (sl1 ++ sl2 ++ final dst a2)
                    a2 tmp
  | tr_addrof: forall le dst e1 ty tmp sl1 a1,
      tr_expr le For_val e1 sl1 a1 tmp ->
      tr_expr le dst (C.Eaddrof e1 ty)
                   (sl1 ++ final dst (Eaddrof a1 ty))
                   (Eaddrof a1 ty) tmp
  | tr_unop: forall le dst op e1 ty tmp sl1 a1,
      tr_expr le For_val e1 sl1 a1 tmp ->
      tr_expr le dst (C.Eunop op e1 ty)
                   (sl1 ++ final dst (Eunop op a1 ty))
                   (Eunop op a1 ty) tmp
  | tr_binop: forall le dst op e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 tmp,
      tr_expr le For_val e1 sl1 a1 tmp1 ->
      tr_expr le For_val e2 sl2 a2 tmp2 ->
      list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp ->
      tr_expr le dst (C.Ebinop op e1 e2 ty)
                   (sl1 ++ sl2 ++ final dst (Ebinop op a1 a2 ty))
                   (Ebinop op a1 a2 ty) tmp
  | tr_cast: forall le dst e1 ty sl1 a1 tmp,
      tr_expr le For_val e1 sl1 a1 tmp ->
      tr_expr le dst (C.Ecast e1 ty)
                   (sl1 ++ final dst (Ecast a1 ty))
                   (Ecast a1 ty) tmp
  | tr_condition_simple: forall le dst e1 e2 e3 ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 tmp,
      Cstrategy.simple e2 = true -> Cstrategy.simple e3 = true ->
      tr_expr le For_val e1 sl1 a1 tmp1 ->
      tr_expr le For_val e2 sl2 a2 tmp2 ->
      tr_expr le For_val e3 sl3 a3 tmp3 ->
      list_disjoint tmp1 tmp2 ->
      list_disjoint tmp1 tmp3 ->
      incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp ->
      tr_expr le dst (C.Econdition e1 e2 e3 ty)
                       (sl1 ++ final dst (Econdition a1 a2 a3 ty))
                       (Econdition a1 a2 a3 ty) tmp
  | tr_condition_val: forall le e1 e2 e3 ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 t tmp,
      Cstrategy.simple e2 = false \/ Cstrategy.simple e3 = false ->
      tr_expr le For_val e1 sl1 a1 tmp1 ->
      tr_expr le For_val e2 sl2 a2 tmp2 ->
      tr_expr le For_val e3 sl3 a3 tmp3 ->
      list_disjoint tmp1 tmp2 ->
      list_disjoint tmp1 tmp3 ->
      incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp ->
      In t tmp -> ~In t tmp1 ->
      tr_expr le For_val (C.Econdition e1 e2 e3 ty)
                      (sl1 ++ makeif a1
                                (Ssequence (makeseq sl2) (Sset t (Ecast a2 ty)))
                                (Ssequence (makeseq sl3) (Sset t (Ecast a3 ty))) :: nil)
                      (Etempvar t ty) tmp
  | tr_condition_effects: forall le dst e1 e2 e3 ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp,
      Cstrategy.simple e2 = false \/ Cstrategy.simple e3 = false ->
      dst <> For_val ->
      tr_expr le For_val e1 sl1 a1 tmp1 ->
      tr_expr le (cast_destination ty dst) e2 sl2 a2 tmp2 ->
      tr_expr le (cast_destination ty dst) e3 sl3 a3 tmp3 ->
      list_disjoint tmp1 tmp2 ->
      list_disjoint tmp1 tmp3 ->
      incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp ->
      tr_expr le dst (C.Econdition e1 e2 e3 ty)
                       (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil)
                       any tmp
  | tr_assign_effects: forall le e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 any tmp,
      tr_expr le For_val e1 sl1 a1 tmp1 ->
      tr_expr le For_val e2 sl2 a2 tmp2 ->
      list_disjoint tmp1 tmp2 ->
      incl tmp1 tmp -> incl tmp2 tmp ->
      tr_expr le For_effects (C.Eassign e1 e2 ty)
                      (sl1 ++ sl2 ++ Sassign a1 a2 :: nil)
                      any tmp
  | tr_assign_val: forall le dst e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 t tmp ty1 ty2,
      tr_expr le For_val e1 sl1 a1 tmp1 ->
      tr_expr le For_val e2 sl2 a2 tmp2 ->
      incl tmp1 tmp -> incl tmp2 tmp ->
      list_disjoint tmp1 tmp2 ->
      In t tmp -> ~In t tmp1 -> ~In t tmp2 ->
      ty1 = C.typeof e1 ->
      ty2 = C.typeof e2 ->
      tr_expr le dst (C.Eassign e1 e2 ty)
                   (sl1 ++ sl2 ++
                    Sset t a2 ::
                    Sassign a1 (Etempvar t ty2) ::
                    final dst (Ecast (Etempvar t ty2) ty1))
                   (Ecast (Etempvar t ty2) ty1) tmp
  | tr_assignop_effects: forall le op e1 e2 tyres ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp,
      tr_expr le For_val e1 sl1 a1 tmp1 ->
      tr_expr le For_val e2 sl2 a2 tmp2 ->
      ty1 = C.typeof e1 ->
      tr_rvalof ty1 a1 sl3 a3 tmp3 ->
      list_disjoint tmp1 tmp2 -> list_disjoint tmp1 tmp3 -> list_disjoint tmp2 tmp3 ->
      incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp ->
      tr_expr le For_effects (C.Eassignop op e1 e2 tyres ty)
                      (sl1 ++ sl2 ++ sl3 ++ Sassign a1 (Ebinop op a3 a2 tyres) :: nil)
                      any tmp
  | tr_assignop_val: forall le dst op e1 e2 tyres ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 t tmp ty1,
      tr_expr le For_val e1 sl1 a1 tmp1 ->
      tr_expr le For_val e2 sl2 a2 tmp2 ->
      tr_rvalof ty1 a1 sl3 a3 tmp3 ->
      list_disjoint tmp1 tmp2 -> list_disjoint tmp1 tmp3 -> list_disjoint tmp2 tmp3 ->
      incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp ->
      In t tmp -> ~In t tmp1 -> ~In t tmp2 -> ~In t tmp3 ->
      ty1 = C.typeof e1 ->
      tr_expr le dst (C.Eassignop op e1 e2 tyres ty)
                   (sl1 ++ sl2 ++ sl3 ++
                    Sset t (Ebinop op a3 a2 tyres) ::
                    Sassign a1 (Etempvar t tyres) ::
                    final dst (Ecast (Etempvar t tyres) ty1))
                   (Ecast (Etempvar t tyres) ty1) tmp
  | tr_postincr_effects: forall le id e1 ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 any tmp,
      tr_expr le For_val e1 sl1 a1 tmp1 ->
      tr_rvalof ty1 a1 sl2 a2 tmp2 ->
      ty1 = C.typeof e1 ->
      incl tmp1 tmp -> incl tmp2 tmp ->
      list_disjoint tmp1 tmp2 ->
      tr_expr le For_effects (C.Epostincr id e1 ty)
                      (sl1 ++ sl2 ++ Sassign a1 (transl_incrdecr id a2 ty1) :: nil)
                      any tmp
  | tr_postincr_val: forall le dst id e1 ty sl1 a1 tmp1 t ty1 tmp,
      tr_expr le For_val e1 sl1 a1 tmp1 ->
      incl tmp1 tmp -> In t tmp -> ~In t tmp1 ->
      ty1 = C.typeof e1 ->
      tr_expr le dst (C.Epostincr id e1 ty)
                   (sl1 ++ make_set t a1 ::
                    Sassign a1 (transl_incrdecr id (Etempvar t ty1) ty1) ::
                    final dst (Etempvar t ty1))
                   (Etempvar t ty1) tmp
  | tr_comma: forall le dst e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 tmp,
      tr_expr le For_effects e1 sl1 a1 tmp1 ->
      tr_expr le dst e2 sl2 a2 tmp2 ->
      list_disjoint tmp1 tmp2 ->
      incl tmp1 tmp -> incl tmp2 tmp ->
      tr_expr le dst (C.Ecomma e1 e2 ty) (sl1 ++ sl2) a2 tmp
  | tr_call_effects: forall le e1 el2 ty sl1 a1 tmp1 sl2 al2 tmp2 any tmp,
      tr_expr le For_val e1 sl1 a1 tmp1 ->
      tr_exprlist le el2 sl2 al2 tmp2 ->
      list_disjoint tmp1 tmp2 ->
      incl tmp1 tmp -> incl tmp2 tmp ->
      tr_expr le For_effects (C.Ecall e1 el2 ty)
                   (sl1 ++ sl2 ++ Scall None a1 al2 :: nil)
                   any tmp
  | tr_call_val: forall le dst e1 el2 ty sl1 a1 tmp1 sl2 al2 tmp2 t tmp,
      dst <> For_effects ->
      tr_expr le For_val e1 sl1 a1 tmp1 ->
      tr_exprlist le el2 sl2 al2 tmp2 ->
      list_disjoint tmp1 tmp2 -> In t tmp ->
      incl tmp1 tmp -> incl tmp2 tmp ->
      tr_expr le dst (C.Ecall e1 el2 ty)
                   (sl1 ++ sl2 ++ Scall (Some t) a1 al2 :: final dst (Etempvar t ty))
                   (Etempvar t ty) tmp
  | tr_paren_val: forall le e1 ty sl1 a1 tmp1 t tmp,
      tr_expr le For_val e1 sl1 a1 tmp1 ->
      incl tmp1 tmp -> In t tmp ->
      tr_expr le For_val (C.Eparen e1 ty)
                       (sl1 ++ Sset t (Ecast a1 ty) :: nil)
                       (Etempvar t ty) tmp
  | tr_paren_effects: forall le dst e1 ty sl1 a1 tmp any,
      dst <> For_val ->
      tr_expr le (cast_destination ty dst) e1 sl1 a1 tmp ->
      tr_expr le dst (C.Eparen e1 ty) sl1 any tmp

with tr_exprlist: temp_env -> C.exprlist -> list statement -> list expr -> list ident -> Prop :=
  | tr_nil: forall le tmp,
      tr_exprlist le C.Enil nil nil tmp
  | tr_cons: forall le e1 el2 sl1 a1 tmp1 sl2 al2 tmp2 tmp,
      tr_expr le For_val e1 sl1 a1 tmp1 ->
      tr_exprlist le el2 sl2 al2 tmp2 ->
      list_disjoint tmp1 tmp2 ->
      incl tmp1 tmp -> incl tmp2 tmp ->
      tr_exprlist le (C.Econs e1 el2) (sl1 ++ sl2) (a1 :: al2) tmp.

Scheme tr_expr_ind2 := Minimality for tr_expr Sort Prop
  with tr_exprlist_ind2 := Minimality for tr_exprlist Sort Prop.
Combined Scheme tr_expr_exprlist from tr_expr_ind2, tr_exprlist_ind2.


Lemma tr_expr_invariant:
  forall le dst r sl a tmps, tr_expr le dst r sl a tmps ->
  forall le', (forall x, In x tmps -> le'!x = le!x) ->
  tr_expr le' dst r sl a tmps
with tr_exprlist_invariant:
  forall le rl sl al tmps, tr_exprlist le rl sl al tmps ->
  forall le', (forall x, In x tmps -> le'!x = le!x) ->
  tr_exprlist le' rl sl al tmps.

Lemma tr_rvalof_monotone:
  forall ty a sl b tmps, tr_rvalof ty a sl b tmps ->
  forall tmps', incl tmps tmps' -> tr_rvalof ty a sl b tmps'.

Lemma tr_expr_monotone:
  forall le dst r sl a tmps, tr_expr le dst r sl a tmps ->
  forall tmps', incl tmps tmps' -> tr_expr le dst r sl a tmps'
with tr_exprlist_monotone:
  forall le rl sl al tmps, tr_exprlist le rl sl al tmps ->
  forall tmps', incl tmps tmps' -> tr_exprlist le rl sl al tmps'.

Top-level translation

Section TR_TOP.

Variable ge: genv.
Variable e: env.
Variable le: temp_env.
Variable m: mem.

Inductive tr_top: destination -> C.expr -> list statement -> expr -> list ident -> Prop :=
  | tr_top_val_val: forall v ty a tmp,
      typeof a = ty -> eval_expr ge e le m a v ->
      tr_top For_val (C.Eval v ty) nil a tmp
  | tr_top_val_test: forall tyl s1 s2 v ty a any tmp,
      typeof a = ty -> eval_expr ge e le m a v ->
      tr_top (For_test tyl s1 s2) (C.Eval v ty) (makeif (fold_left Ecast tyl a) s1 s2 :: nil) any tmp
  | tr_top_base: forall dst r sl a tmp,
      tr_expr le dst r sl a tmp ->
      tr_top dst r sl a tmp
  | tr_top_paren_test: forall tyl s1 s2 r ty sl a tmp,
      tr_top (For_test (ty :: tyl) s1 s2) r sl a tmp ->
      tr_top (For_test tyl s1 s2) (C.Eparen r ty) sl a tmp.

End TR_TOP.

Translation of statements

Inductive tr_expression: C.expr -> statement -> expr -> Prop :=
  | tr_expression_intro: forall r sl a tmps,
      (forall ge e le m, tr_top ge e le m For_val r sl a tmps) ->
      tr_expression r (makeseq sl) a.

Inductive tr_expr_stmt: C.expr -> statement -> Prop :=
  | tr_expr_stmt_intro: forall r sl a tmps,
      (forall ge e le m, tr_top ge e le m For_effects r sl a tmps) ->
      tr_expr_stmt r (makeseq sl).

Inductive tr_if: C.expr -> statement -> statement -> statement -> Prop :=
  | tr_if_intro: forall r s1 s2 sl a tmps,
      (forall ge e le m, tr_top ge e le m (For_test nil s1 s2) r sl a tmps) ->
      tr_if r s1 s2 (makeseq sl).

Inductive tr_stmt: C.statement -> statement -> Prop :=
  | tr_skip:
      tr_stmt C.Sskip Sskip
  | tr_do: forall r s,
      tr_expr_stmt r s ->
      tr_stmt (C.Sdo r) s
  | tr_seq: forall s1 s2 ts1 ts2,
      tr_stmt s1 ts1 -> tr_stmt s2 ts2 ->
      tr_stmt (C.Ssequence s1 s2) (Ssequence ts1 ts2)
  | tr_ifthenelse_big: forall r s1 s2 s' a ts1 ts2,
      tr_expression r s' a ->
      tr_stmt s1 ts1 -> tr_stmt s2 ts2 ->
      tr_stmt (C.Sifthenelse r s1 s2) (Ssequence s' (Sifthenelse a ts1 ts2))
  | tr_ifthenelse_small: forall r s1 s2 ts1 ts2 ts,
      tr_stmt s1 ts1 -> tr_stmt s2 ts2 ->
      small_stmt ts1 = true -> small_stmt ts2 = true ->
      tr_if r ts1 ts2 ts ->
      tr_stmt (C.Sifthenelse r s1 s2) ts
  | tr_while: forall r s1 s' ts1,
      tr_if r Sskip Sbreak s' ->
      tr_stmt s1 ts1 ->
      tr_stmt (C.Swhile r s1)
              (Swhile expr_true (Ssequence s' ts1))
  | tr_dowhile: forall r s1 s' ts1,
      tr_if r Sskip Sbreak s' ->
      tr_stmt s1 ts1 ->
      tr_stmt (C.Sdowhile r s1)
              (Sfor' expr_true s' ts1)
  | tr_for_1: forall r s3 s4 s' ts3 ts4,
      tr_if r Sskip Sbreak s' ->
      tr_stmt s3 ts3 ->
      tr_stmt s4 ts4 ->
      tr_stmt (C.Sfor C.Sskip r s3 s4)
              (Sfor' expr_true ts3 (Ssequence s' ts4))
  | tr_for_2: forall s1 r s3 s4 s' ts1 ts3 ts4,
      tr_if r Sskip Sbreak s' ->
      s1 <> C.Sskip ->
      tr_stmt s1 ts1 ->
      tr_stmt s3 ts3 ->
      tr_stmt s4 ts4 ->
      tr_stmt (C.Sfor s1 r s3 s4)
              (Ssequence ts1 (Sfor' expr_true ts3 (Ssequence s' ts4)))
  | tr_break:
      tr_stmt C.Sbreak Sbreak
  | tr_continue:
      tr_stmt C.Scontinue Scontinue
  | tr_return_none:
      tr_stmt (C.Sreturn None) (Sreturn None)
  | tr_return_some: forall r s' a,
      tr_expression r s' a ->
      tr_stmt (C.Sreturn (Some r)) (Ssequence s' (Sreturn (Some a)))
  | tr_switch: forall r ls s' a tls,
      tr_expression r s' a ->
      tr_lblstmts ls tls ->
      tr_stmt (C.Sswitch r ls) (Ssequence s' (Sswitch a tls))
  | tr_label: forall lbl s ts,
      tr_stmt s ts ->
      tr_stmt (C.Slabel lbl s) (Slabel lbl ts)
  | tr_goto: forall lbl,
      tr_stmt (C.Sgoto lbl) (Sgoto lbl)

with tr_lblstmts: C.labeled_statements -> labeled_statements -> Prop :=
  | tr_default: forall s ts,
      tr_stmt s ts ->
      tr_lblstmts (C.LSdefault s) (LSdefault ts)
  | tr_case: forall n s ls ts tls,
      tr_stmt s ts ->
      tr_lblstmts ls tls ->
      tr_lblstmts (C.LScase n s ls) (LScase n ts tls).

Correctness proof with respect to the specification.

Properties of the monad

Remark bind_inversion:
  forall (A B: Type) (f: mon A) (g: A -> mon B) (y: B) (z1 z3: generator) I,
  bind f g z1 = Res y z3 I ->
  exists x, exists z2, exists I1, exists I2,
  f z1 = Res x z2 I1 /\ g x z2 = Res y z3 I2.

Remark bind2_inversion:
  forall (A B C: Type) (f: mon (A*B)) (g: A -> B -> mon C) (y: C) (z1 z3: generator) I,
  bind2 f g z1 = Res y z3 I ->
  exists x1, exists x2, exists z2, exists I1, exists I2,
  f z1 = Res (x1,x2) z2 I1 /\ g x1 x2 z2 = Res y z3 I2.

Ltac monadInv1 H :=
  match type of H with
  | (Res _ _ _ = Res _ _ _) =>
      inversion H; clear H; try subst
  | (@ret _ _ _ = Res _ _ _) =>
      inversion H; clear H; try subst
  | (@error _ _ _ = Res _ _ _) =>
      inversion H
  | (bind ?F ?G ?Z = Res ?X ?Z' ?I) =>
      let x := fresh "x" in (
      let z := fresh "z" in (
      let I1 := fresh "I" in (
      let I2 := fresh "I" in (
      let EQ1 := fresh "EQ" in (
      let EQ2 := fresh "EQ" in (
      destruct (bind_inversion _ _ F G X Z Z' I H) as [x [z [I1 [I2 [EQ1 EQ2]]]]];
      clear H;
      try (monadInv1 EQ2)))))))
   | (bind2 ?F ?G ?Z = Res ?X ?Z' ?I) =>
      let x := fresh "x" in (
      let y := fresh "y" in (
      let z := fresh "z" in (
      let I1 := fresh "I" in (
      let I2 := fresh "I" in (
      let EQ1 := fresh "EQ" in (
      let EQ2 := fresh "EQ" in (
      destruct (bind2_inversion _ _ _ F G X Z Z' I H) as [x [y [z [I1 [I2 [EQ1 EQ2]]]]]];
      clear H;
      try (monadInv1 EQ2))))))))
 end.

Ltac monadInv H :=
  match type of H with
  | (@ret _ _ _ = Res _ _ _) => monadInv1 H
  | (@error _ _ _ = Res _ _ _) => monadInv1 H
  | (bind ?F ?G ?Z = Res ?X ?Z' ?I) => monadInv1 H
  | (bind2 ?F ?G ?Z = Res ?X ?Z' ?I) => monadInv1 H
  | (?F _ _ _ _ _ _ _ _ = Res _ _ _) =>
      ((progress simpl in H) || unfold F in H); monadInv1 H
  | (?F _ _ _ _ _ _ _ = Res _ _ _) =>
      ((progress simpl in H) || unfold F in H); monadInv1 H
  | (?F _ _ _ _ _ _ = Res _ _ _) =>
      ((progress simpl in H) || unfold F in H); monadInv1 H
  | (?F _ _ _ _ _ = Res _ _ _) =>
      ((progress simpl in H) || unfold F in H); monadInv1 H
  | (?F _ _ _ _ = Res _ _ _) =>
      ((progress simpl in H) || unfold F in H); monadInv1 H
  | (?F _ _ _ = Res _ _ _) =>
      ((progress simpl in H) || unfold F in H); monadInv1 H
  | (?F _ _ = Res _ _ _) =>
      ((progress simpl in H) || unfold F in H); monadInv1 H
  | (?F _ = Res _ _ _) =>
      ((progress simpl in H) || unfold F in H); monadInv1 H
  end.

Freshness and separation properties.

Definition within (id: ident) (g1 g2: generator) : Prop :=
  Ple (gen_next g1) id /\ Plt id (gen_next g2).

Lemma gensym_within:
  forall ty g1 id g2 I,
  gensym ty g1 = Res id g2 I -> within id g1 g2.

Lemma within_widen:
  forall id g1 g2 g1' g2',
  within id g1 g2 ->
  Ple (gen_next g1') (gen_next g1) ->
  Ple (gen_next g2) (gen_next g2') ->
  within id g1' g2'.

Definition contained (l: list ident) (g1 g2: generator) : Prop :=
  forall id, In id l -> within id g1 g2.

Lemma contained_nil:
  forall g1 g2, contained nil g1 g2.

Lemma contained_widen:
  forall l g1 g2 g1' g2',
  contained l g1 g2 ->
  Ple (gen_next g1') (gen_next g1) ->
  Ple (gen_next g2) (gen_next g2') ->
  contained l g1' g2'.

Lemma contained_cons:
  forall id l g1 g2,
  within id g1 g2 -> contained l g1 g2 -> contained (id :: l) g1 g2.

Lemma contained_app:
  forall l1 l2 g1 g2,
  contained l1 g1 g2 -> contained l2 g1 g2 -> contained (l1 ++ l2) g1 g2.

Lemma contained_disjoint:
  forall g1 l1 g2 l2 g3,
  contained l1 g1 g2 -> contained l2 g2 g3 -> list_disjoint l1 l2.

Lemma contained_notin:
  forall g1 l g2 id g3,
  contained l g1 g2 -> within id g2 g3 -> ~In id l.

Hint Resolve gensym_within within_widen contained_widen
             contained_cons contained_app contained_disjoint
             contained_notin contained_nil
             incl_refl incl_tl incl_app incl_appl incl_appr
             in_eq in_cons
             Ple_trans Ple_refl: gensym.

Correctness of the translation functions

Lemma finish_meets_spec_1:
  forall dst sl a sl' a',
  finish dst sl a = (sl', a') -> sl' = sl ++ final dst a.

Lemma finish_meets_spec_2:
  forall dst sl a sl' a',
  finish dst sl a = (sl', a') -> a' = a.

Ltac UseFinish :=
  match goal with
  | [ H: finish _ _ _ = (_, _) |- _ ] =>
      try (rewrite (finish_meets_spec_2 _ _ _ _ _ H));
      try (rewrite (finish_meets_spec_1 _ _ _ _ _ H));
      repeat rewrite app_ass
  end.

Lemma transl_valof_meets_spec:
  forall ty a g sl b g' I,
  transl_valof ty a g = Res (sl, b) g' I ->
  exists tmps, tr_rvalof ty a sl b tmps /\ contained tmps g g'.

Scheme expr_ind2 := Induction for C.expr Sort Prop
  with exprlist_ind2 := Induction for C.exprlist Sort Prop.
Combined Scheme expr_exprlist_ind from expr_ind2, exprlist_ind2.

Lemma transl_meets_spec:
   (forall r dst g sl a g' I,
    transl_expr dst r g = Res (sl, a) g' I ->
    exists tmps, (forall le, tr_expr le dst r sl a tmps) /\ contained tmps g g')
  /\
   (forall rl g sl al g' I,
    transl_exprlist rl g = Res (sl, al) g' I ->
    exists tmps, (forall le, tr_exprlist le rl sl al tmps) /\ contained tmps g g').

Lemma transl_expr_meets_spec:
   forall r dst g sl a g' I,
   transl_expr dst r g = Res (sl, a) g' I ->
   exists tmps, forall ge e le m, tr_top ge e le m dst r sl a tmps.

Lemma transl_expression_meets_spec:
  forall r g s a g' I,
  transl_expression r g = Res (s, a) g' I ->
  tr_expression r s a.

Lemma transl_expr_stmt_meets_spec:
  forall r g s g' I,
  transl_expr_stmt r g = Res s g' I ->
  tr_expr_stmt r s.

Lemma transl_if_meets_spec:
  forall r s1 s2 g s g' I,
  transl_if r s1 s2 g = Res s g' I ->
  tr_if r s1 s2 s.

Lemma transl_stmt_meets_spec:
  forall s g ts g' I, transl_stmt s g = Res ts g' I -> tr_stmt s ts
with transl_lblstmt_meets_spec:
  forall s g ts g' I, transl_lblstmt s g = Res ts g' I -> tr_lblstmts s ts.

Theorem transl_function_spec:
  forall f tf,
  transl_function f = OK tf ->
  tr_stmt f.(C.fn_body) tf.(fn_body)
  /\ fn_return tf = C.fn_return f
  /\ fn_params tf = C.fn_params f
  /\ fn_vars tf = C.fn_vars f.

End SPEC.