Set Implicit Arguments.
Require Export ConcreteWhile.

Ltac inverts_constr H :=
  match type of H with
  | ?C ?a1 = ?C' ?a2 ⇒
    let T := fresh "T" in
    cuts T: (∀ a b, C a = C b → a = b);
    [ apply T in H; clear T
    | clear; let I := fresh "I" in introv I; solve [ inverts× I ] ]
  | _ ⇒ try solve [ inverts H ]
  end.

Ltac fexact t :=
  match goal with
  | |- ?G ⇒
    let T := type of t in
    let H := fresh in
    cuts H: (G = T); [ rewrite H; exact t |]
  end.

Section AbstractExample.

Require Export DomainsSign.

Inductive sign_ares : Type :=
  | sign_ares_expr : aOute → sign_ares
  | sign_ares_stat : aOuts → sign_ares

  

  | sign_ares_top : sign_ares
  | sign_ares_bot : sign_ares
  .

Definition sign_ares_eq ar1 ar2 :=
  match ar1, ar2 with
  | sign_ares_expr r1, sign_ares_expr r2 ⇒ r1 =♯ r2
  | sign_ares_stat r1, sign_ares_stat r2 ⇒ r1 =♯ r2
  | sign_ares_top, sign_ares_top ⇒ True
  | sign_ares_bot, sign_ares_bot ⇒ True
  | _, _ ⇒ False
  end.

Definition sign_ares_order ar1 ar2 :=
  match ar1, ar2 with
  | _, sign_ares_top ⇒ True
  | sign_ares_bot, _ ⇒ True
  | sign_ares_expr r1, sign_ares_expr r2 ⇒ r1 ⊑♯ r2
  | sign_ares_stat r1, sign_ares_stat r2 ⇒ r1 ⊑♯ r2
  | _, _ ⇒ False
  end.

Definition sign_ares_join ar1 ar2 :=
  match ar1, ar2 with
  | sign_ares_bot, _ ⇒ ar2
  | _, sign_ares_bot ⇒ ar1
  | sign_ares_expr r1, sign_ares_expr r2 ⇒ sign_ares_expr (r1 ⊔♯ r2)
  | sign_ares_stat r1, sign_ares_stat r2 ⇒ sign_ares_stat (r1 ⊔♯ r2)
  | _, _ ⇒ sign_ares_top
  end.

Definition sign_ares_meet ar1 ar2 :=
  match ar1, ar2 with
  | sign_ares_top, _ ⇒ ar2
  | _, sign_ares_top ⇒ ar1
  | sign_ares_expr r1, sign_ares_expr r2 ⇒ sign_ares_expr (r1 ⊓♯ r2)
  | sign_ares_stat r1, sign_ares_stat r2 ⇒ sign_ares_stat (r1 ⊓♯ r2)
  | _, _ ⇒ sign_ares_bot
  end.

Global Instance sign_ares_Equiv : EquivDec.t sign_ares.
  apply EquivDec.Make with (eq := sign_ares_eq).
   introv. destruct x; try apply EquivDec.refl; exact I.
   introv E. destruct x; destruct y; try (apply EquivDec.sym; apply E);
    try exact I; inverts E.
   introv E1 E2. destruct x; destruct y; destruct z; tryfalse;
    try apply (EquivDec.trans _ _ _ E1 E2); exact I.
   introv. destruct x; destruct y; try solve [ right¬ ]; try apply EquivDec.dec;
    try solve [ left; exact I ];
    (destruct (EquivDec.dec a a1); [| right; intro E; inverts¬ E ]);
    (destruct (EquivDec.dec a0 a2); [| right; intro E; inverts¬ E ]);
    left; splits¬.
Defined.

Global Instance sign_ares_Poset : PosetDec.t sign_ares.
  apply PosetDec.Make with (eq := sign_ares_Equiv) (order := sign_ares_order).
   introv E. destruct x; destruct y; try solve [ inverts E ]; try exact I;
    apply PosetDec.refl; apply E.
   introv R1 R2. destruct x; destruct y; try solve [ try inverts R1; inverts R2 ]; try exact I;
    apply¬ @PosetDec.antisym.
   introv R1 R2. destruct x; destruct y; destruct z;
    try solve [ try inverts R1; inverts R2 ]; try exact I;
    (eapply @PosetDec.trans; [ apply R1 | apply R2 ]).
   introv. destruct x; destruct y; try solve [ right¬ ]; try apply PosetDec.dec;
    try solve [ left; exact I ];
    (destruct (PosetDec.dec a a1); [| right; intro E; inverts¬ E ]);
    (destruct (PosetDec.dec a0 a2); [| right; intro E; inverts¬ E ]);
    left; splits¬.
Defined.

Global Instance sign_ares_Lat : LatticeDec.t sign_ares.
  apply LatticeDec.Make with (porder := sign_ares_Poset).
   apply JoinDec.Make with (op := sign_ares_join).
    introv. destruct x; destruct y; try solve [ exact I ];
     try apply @JoinDec.bound1; try apply¬ @PosetDec.refl.
    introv. destruct x; destruct y; try solve [ exact I ];
     try apply @JoinDec.bound2; try apply¬ @PosetDec.refl.
    introv R1 R2. destruct z; destruct y; tryfalse; destruct x;
     try solve [ exact I ]; tryfalse; try solve [ simpls¬ ];
     apply¬ @JoinDec.least_upper_bound.
   apply MeetDec.Make with (op := sign_ares_meet).
    introv. destruct x; destruct y; try solve [ exact I ];
     try apply @MeetDec.bound1; try apply¬ @PosetDec.refl.
    introv. destruct x; destruct y; try solve [ exact I ];
     try apply @MeetDec.bound2; try apply¬ @PosetDec.refl.
    introv R1 R2. destruct z; destruct y; tryfalse; destruct x;
     try solve [ exact I ]; tryfalse; try solve [ simpls¬ ];
     try apply¬ @MeetDec.greatest_lower_bound.
   apply BotDec.Make with (elem := sign_ares_bot). intros (); simpls¬.
   exact (fun _ ar ⇒ ar).
Defined.

Global Instance sign_ares_Top : TopDec.t sign_ares.
  apply TopDec.Make with (elem := sign_ares_top). intros (); simpls¬.
Defined.

Definition sign_gamma_ares : sign_ares → ℘ while_res := fun ar r ⇒
  match ar, r with
  | sign_ares_top, _ ⇒ True
  | sign_ares_expr ao, while_res_expr o ⇒ gamma_aOute ao o
  | sign_ares_stat ao, while_res_stat o ⇒ gamma_aOuts ao o
  | _, _ ⇒ False
  end.

Global Instance sign_Gamma_ares : Gamma.t _ _ sign_gamma_ares.
Proof.
  constructors.
   introv O. destruct N1 as [[av1 ae1]|[aE1 ae1]| |]; destruct N2 as [[av2 ae2]|[aE2 ae2]| |];
     tryfalse; simpls~; intros [[o|e]|[o|e]] E; tryfalse; lets (Ov&Oe): (rm O); constructors.
    inverts E. apply¬ (@Gamma.monotone _ _ _ _ _ Sign.Gamma _ _ Ov).
    inverts E as E. apply Oe. apply E.
    inverts E. apply¬ (@Gamma.monotone _ _ _ _ gamma_aEnv _ aE1 aE2 Ov).
    inverts E as E. apply Oe. apply E.
   introv. destruct N1 as [[av1 ae1]|[aE1 ae1]| |]; destruct N2 as [[av2 ae2]|[aE2 ae2]| |];
     simpls~; intros [[o|e]|[o|e]] [E1 E2]; tryfalse; constructors; inverts E1; inverts E2;
     try (unfolds gamma_aErr; unfolds PowerSet.gamma; rew_refl*).
    apply (@Gamma.meet_morph _ _ _ _ gamma_aVal _ _ _ _). simpl. splits¬.
    apply (@Gamma.meet_morph _ _ _ _ gamma_aEnv _ _ _ _). simpl. splits¬.
Qed.

Inductive sign_ast : Type :=
  | sign_ast_expr : aEnvV → sign_ast
  | sign_ast_stat : aEnvV → aEnvF → sign_ast
  | sign_ast_prog : aEnvV → aEnvF → sign_ast
  | sign_ast_add_1 : aEnvV → sign_ares → sign_ast
  | sign_ast_add_2 : aVal → sign_ares → sign_ast
  | sign_ast_asgn_1 : aEnvV → sign_ares → sign_ast
  | sign_ast_seq_1 : aCtxEnv → aEnvF → sign_ares → sign_ast
  | sign_ast_if_1 : aEnvV → aEnvF → sign_ares → sign_ast
  | sign_ast_while_1 : aCtxEnv → aEnvF → sign_ares → sign_ast
  | sign_ast_while_2 : aEnvV → aEnvF → sign_ares → sign_ast
  | sign_ast_proc_call_1 : aEnvV → aEnvF → sign_ares → sign_ast

  

  | sign_ast_top : sign_ast
  | sign_ast_bot : sign_ast
  .

Definition sign_ast_eq asigma1 asigma2 :=
  match asigma1, asigma2 with
  | sign_ast_expr Ev1, sign_ast_expr Ev2 ⇒
    Ev1 =♯ Ev2
  | sign_ast_stat Ev1 Ef1, sign_ast_stat Ev2 Ef2 ⇒
    Ev1 =♯ Ev2 ∧ Ef1 =♯ Ef2
  | sign_ast_prog Ev1 Ef1, sign_ast_prog Ev2 Ef2 ⇒
    Ev1 =♯ Ev2 ∧ Ef1 =♯ Ef2
  | sign_ast_add_1 Ev1 r1, sign_ast_add_1 Ev2 r2 ⇒
    Ev1 =♯ Ev2 ∧ r1 =♯ r2
  | sign_ast_add_2 v1 r1, sign_ast_add_2 v2 r2 ⇒
    v1 =♯ v2 ∧ r1 =♯ r2
  | sign_ast_asgn_1 Ev1 r1, sign_ast_asgn_1 Ev2 r2 ⇒
    Ev1 =♯ Ev2 ∧ r1 =♯ r2
  | sign_ast_seq_1 C1 Ef1 r1, sign_ast_seq_1 C2 Ef2 r2 ⇒
    C1 =♯ C2 ∧ Ef1 =♯ Ef2 ∧ r1 =♯ r2
  | sign_ast_if_1 Ev1 Ef1 r1, sign_ast_if_1 Ev2 Ef2 r2 ⇒
    Ev1 =♯ Ev2 ∧ Ef1 =♯ Ef2 ∧ r1 =♯ r2
  | sign_ast_while_1 C1 Ef1 r1, sign_ast_while_1 C2 Ef2 r2 ⇒
    C1 =♯ C2 ∧ Ef1 =♯ Ef2 ∧ r1 =♯ r2
  | sign_ast_while_2 Ev1 Ef1 r1, sign_ast_while_2 Ev2 Ef2 r2 ⇒
    Ev1 =♯ Ev2 ∧ Ef1 =♯ Ef2 ∧ r1 =♯ r2
  | sign_ast_proc_call_1 Ev1 Ef1 r1, sign_ast_proc_call_1 Ev2 Ef2 r2 ⇒
    Ev1 =♯ Ev2 ∧ Ef1 =♯ Ef2 ∧ r1 =♯ r2
  | sign_ast_top, sign_ast_top ⇒ True
  | sign_ast_bot, sign_ast_bot ⇒ True
  | _, _ ⇒ False
  end.

Definition sign_ast_order asigma1 asigma2 :=
  match asigma1, asigma2 with
  | _, sign_ast_top ⇒ True
  | sign_ast_bot, _ ⇒ True
  | sign_ast_expr Ev1, sign_ast_expr Ev2 ⇒
    Ev1 ⊑♯ Ev2
  | sign_ast_stat Ev1 Ef1, sign_ast_stat Ev2 Ef2 ⇒
    Ev1 ⊑♯ Ev2 ∧ Ef1 ⊑♯ Ef2
  | sign_ast_prog Ev1 Ef1, sign_ast_prog Ev2 Ef2 ⇒
    Ev1 ⊑♯ Ev2 ∧ Ef1 ⊑♯ Ef2
  | sign_ast_add_1 Ev1 r1, sign_ast_add_1 Ev2 r2 ⇒
    Ev1 ⊑♯ Ev2 ∧ r1 ⊑♯ r2
  | sign_ast_add_2 v1 r1, sign_ast_add_2 v2 r2 ⇒
    v1 ⊑♯ v2 ∧ r1 ⊑♯ r2
  | sign_ast_asgn_1 Ev1 r1, sign_ast_asgn_1 Ev2 r2 ⇒
    Ev1 ⊑♯ Ev2 ∧ r1 ⊑♯ r2
  | sign_ast_seq_1 C1 Ef1 r1, sign_ast_seq_1 C2 Ef2 r2 ⇒
    C1 ⊑♯ C2 ∧ Ef1 ⊑♯ Ef2 ∧ r1 ⊑♯ r2
  | sign_ast_if_1 Ev1 Ef1 r1, sign_ast_if_1 Ev2 Ef2 r2 ⇒
    Ev1 ⊑♯ Ev2 ∧ Ef1 ⊑♯ Ef2 ∧ r1 ⊑♯ r2
  | sign_ast_while_1 C1 Ef1 r1, sign_ast_while_1 C2 Ef2 r2 ⇒
    C1 ⊑♯ C2 ∧ Ef1 ⊑♯ Ef2 ∧ r1 ⊑♯ r2
  | sign_ast_while_2 Ev1 Ef1 r1, sign_ast_while_2 Ev2 Ef2 r2 ⇒
    Ev1 ⊑♯ Ev2 ∧ Ef1 ⊑♯ Ef2 ∧ r1 ⊑♯ r2
  | sign_ast_proc_call_1 Ev1 Ef1 r1, sign_ast_proc_call_1 Ev2 Ef2 r2 ⇒
    Ev1 ⊑♯ Ev2 ∧ Ef1 ⊑♯ Ef2 ∧ r1 ⊑♯ r2
  | _, _ ⇒ False
  end.

Definition sign_ast_join ar1 ar2 :=
  match ar1, ar2 with
  | sign_ast_bot, _ ⇒ ar2
  | _, sign_ast_bot ⇒ ar1
  | sign_ast_expr Ev1, sign_ast_expr Ev2 ⇒
    sign_ast_expr (Ev1 ⊔♯ Ev2)
  | sign_ast_stat Ev1 Ef1, sign_ast_stat Ev2 Ef2 ⇒
    sign_ast_stat (Ev1 ⊔♯ Ev2) (Ef1 ⊔♯ Ef2)
  | sign_ast_prog Ev1 Ef1, sign_ast_prog Ev2 Ef2 ⇒
    sign_ast_prog (Ev1 ⊔♯ Ev2) (Ef1 ⊔♯ Ef2)
  | sign_ast_add_1 Ev1 r1, sign_ast_add_1 Ev2 r2 ⇒
    sign_ast_add_1 (Ev1 ⊔♯ Ev2) (r1 ⊔♯ r2)
  | sign_ast_add_2 v1 r1, sign_ast_add_2 v2 r2 ⇒
    sign_ast_add_2 (v1 ⊔♯ v2) (r1 ⊔♯ r2)
  | sign_ast_asgn_1 Ev1 r1, sign_ast_asgn_1 Ev2 r2 ⇒
    sign_ast_asgn_1 (Ev1 ⊔♯ Ev2) (r1 ⊔♯ r2)
  | sign_ast_seq_1 C1 Ef1 r1, sign_ast_seq_1 C2 Ef2 r2 ⇒
    sign_ast_seq_1 (C1 ⊔♯ C2) (Ef1 ⊔♯ Ef2) (r1 ⊔♯ r2)
  | sign_ast_if_1 Ev1 Ef1 r1, sign_ast_if_1 Ev2 Ef2 r2 ⇒
    sign_ast_if_1 (Ev1 ⊔♯ Ev2) (Ef1 ⊔♯ Ef2) (r1 ⊔♯ r2)
  | sign_ast_while_1 C1 Ef1 r1, sign_ast_while_1 C2 Ef2 r2 ⇒
    sign_ast_while_1 (C1 ⊔♯ C2) (Ef1 ⊔♯ Ef2) (r1 ⊔♯ r2)
  | sign_ast_while_2 Ev1 Ef1 r1, sign_ast_while_2 Ev2 Ef2 r2 ⇒
    sign_ast_while_2 (Ev1 ⊔♯ Ev2) (Ef1 ⊔♯ Ef2) (r1 ⊔♯ r2)
  | sign_ast_proc_call_1 Ev1 Ef1 r1, sign_ast_proc_call_1 Ev2 Ef2 r2 ⇒
    sign_ast_proc_call_1 (Ev1 ⊔♯ Ev2) (Ef1 ⊔♯ Ef2) (r1 ⊔♯ r2)
  | _, _ ⇒ sign_ast_top
  end.

Definition sign_ast_meet ar1 ar2 :=
  match ar1, ar2 with
  | sign_ast_top, _ ⇒ ar2
  | _, sign_ast_top ⇒ ar1
  | sign_ast_expr Ev1, sign_ast_expr Ev2 ⇒
    sign_ast_expr (Ev1 ⊓♯ Ev2)
  | sign_ast_stat Ev1 Ef1, sign_ast_stat Ev2 Ef2 ⇒
    sign_ast_stat (Ev1 ⊓♯ Ev2) (Ef1 ⊓♯ Ef2)
  | sign_ast_prog Ev1 Ef1, sign_ast_prog Ev2 Ef2 ⇒
    sign_ast_prog (Ev1 ⊓♯ Ev2) (Ef1 ⊓♯ Ef2)
  | sign_ast_add_1 Ev1 r1, sign_ast_add_1 Ev2 r2 ⇒
    sign_ast_add_1 (Ev1 ⊓♯ Ev2) (r1 ⊓♯ r2)
  | sign_ast_add_2 v1 r1, sign_ast_add_2 v2 r2 ⇒
    sign_ast_add_2 (v1 ⊓♯ v2) (r1 ⊓♯ r2)
  | sign_ast_asgn_1 Ev1 r1, sign_ast_asgn_1 Ev2 r2 ⇒
    sign_ast_asgn_1 (Ev1 ⊓♯ Ev2) (r1 ⊓♯ r2)
  | sign_ast_seq_1 C1 Ef1 r1, sign_ast_seq_1 C2 Ef2 r2 ⇒
    sign_ast_seq_1 (C1 ⊓♯ C2) (Ef1 ⊓♯ Ef2) (r1 ⊓♯ r2)
  | sign_ast_if_1 Ev1 Ef1 r1, sign_ast_if_1 Ev2 Ef2 r2 ⇒
    sign_ast_if_1 (Ev1 ⊓♯ Ev2) (Ef1 ⊓♯ Ef2) (r1 ⊓♯ r2)
  | sign_ast_while_1 C1 Ef1 r1, sign_ast_while_1 C2 Ef2 r2 ⇒
    sign_ast_while_1 (C1 ⊓♯ C2) (Ef1 ⊓♯ Ef2) (r1 ⊓♯ r2)
  | sign_ast_while_2 Ev1 Ef1 r1, sign_ast_while_2 Ev2 Ef2 r2 ⇒
    sign_ast_while_2 (Ev1 ⊓♯ Ev2) (Ef1 ⊓♯ Ef2) (r1 ⊓♯ r2)
  | sign_ast_proc_call_1 Ev1 Ef1 r1, sign_ast_proc_call_1 Ev2 Ef2 r2 ⇒
    sign_ast_proc_call_1 (Ev1 ⊓♯ Ev2) (Ef1 ⊓♯ Ef2) (r1 ⊓♯ r2)
  | _, _ ⇒ sign_ast_bot
  end.

Global Instance sign_ast_Equiv : EquivDec.t sign_ast.
  apply EquivDec.Make with (eq := sign_ast_eq).
   introv. destruct x; try apply EquivDec.refl; try exact I; splits; apply EquivDec.refl.
   introv E. destruct x; destruct y; try (apply EquivDec.sym; apply E);
    try exact I; try solve [ inverts E ]; splits; apply EquivDec.sym; apply E.
   introv E1 E2. destruct x; destruct y; destruct z; tryfalse;
    try apply (EquivDec.trans _ _ _ E1 E2); try exact I; splits;
    (eapply EquivDec.trans; [ apply E1 | apply E2 ]).
   introv. destruct x; destruct y; try solve [ right¬ ]; try apply EquivDec.dec;
    try solve [ left; exact I ];
    try (destruct (EquivDec.dec a a0); [| right; intro E; inverts¬ E ]);
    try (destruct (EquivDec.dec a a1); [| right; intro E; inverts¬ E ]);
    try (destruct (EquivDec.dec a0 a2); [| right; intro E; inverts¬ E ]);
    try (destruct (EquivDec.dec s s0); [| right; intro E; inverts¬ E ]);
    intuit; tryfalse;
    try solve [ left; splits¬ ].
Defined.

Global Instance sign_ast_Poset : PosetDec.t sign_ast.
  apply PosetDec.Make with (eq := sign_ast_Equiv) (order := sign_ast_order).
   introv E. destruct x; destruct y; try solve [ inverts E ]; try exact I;
    try (apply PosetDec.refl; apply E); inverts E; intuit; splits; apply¬ @PosetDec.refl.
   introv O1 O2. destruct x; destruct y;
     try solve [ try inverts O1; inverts O2 ]; try exact I;
     try exact (@PosetDec.antisym _ _ _ _ O1 O2);
     forwards (O11&O12): (rm O1); forwards (O21&O22): (rm O2); intuit; substs;
     repeat match goal with
     | a : aEnvV |- _ ⇒ destruct a as [? ?]
     | a : aCtxEnv |- _ ⇒ destruct a as [[[[? ?]|]|]|]
     end; simpls; intuit; substs; repeat split;
     match goal with
     | H : False |- _ ⇒ false H
     | |- _ _ _ _ _ ?a1 ?a2 ⇒ change (a1 =♯ a2)
     | |- _ _ _ ?a1 ?a2 ⇒ change (a1 =♯ a2)
     | |- _ ?a1 ?a2 ⇒ change (a1 =♯ a2)
     | _ ⇒ idtac
     end;
     try (apply @PosetDec.antisym with (t := Sign.Poset); auto~);
     try (apply @PosetDec.antisym with (t := sign_ares_Poset); auto~);
     try (apply @PosetDec.antisym with (t := @FlatLatticeDec.tPoset EnvF _); auto~);
     try (apply @PosetDec.antisym with (t := MapDefault.Poset _ _ _ _ _); auto~).
   introv O1 O2. destruct x; destruct y; destruct z;
    try solve [ try inverts O1; inverts O2 ]; try exact I;
    try (eapply @PosetDec.trans; [ apply O1 | apply O2 ]);
    repeat split; try (eapply @PosetDec.trans; [ apply O1 | apply O2 ]).
   introv. destruct x; destruct y; try solve [ right¬ ]; try apply PosetDec.dec;
    try solve [ left; exact I ];
    try (destruct (PosetDec.dec a a0); [| right; intro E; inverts¬ E ]);
    try (destruct (PosetDec.dec a a1); [| right; intro E; inverts¬ E ]);
    try (destruct (PosetDec.dec a0 a2); [| right; intro E; inverts¬ E ]);
    try (destruct (PosetDec.dec s s0); [| right; intro E; inverts¬ E ]);
    solve [ left; splits¬ ] || (intuit; false*).
Defined.

Global Instance sign_ast_Lat : LatticeDec.t sign_ast.
  apply LatticeDec.Make with (porder := sign_ast_Poset).
   apply JoinDec.Make with (op := sign_ast_join).
    introv. destruct x; destruct y; try solve [ exact I ]; repeat split;
     try apply @JoinDec.bound1; try apply¬ @PosetDec.refl.
    introv. destruct x; destruct y; try solve [ exact I ]; repeat split;
     try apply @JoinDec.bound2; try apply¬ @PosetDec.refl.
    introv R1 R2. destruct z; destruct y; tryfalse; destruct x;
     try solve [ exact I ]; tryfalse; try inverts R1; try inverts R2;
     intuit; repeat split; try solve [ simpls¬ ];
     try (apply @JoinDec.least_upper_bound; try assumption);
     try match goal with
     | |- (_ _ _ ?a1) ⊑♯ (_ _ _ ?a2) ⇒
       asserts (?&?): (a1 ⊑♯ a2); assumption
     end.
   apply MeetDec.Make with (op := sign_ast_meet).
    introv. destruct x; destruct y; try solve [ exact I ]; repeat split;
     try apply @MeetDec.bound1; try apply¬ @PosetDec.refl.
    introv. destruct x; destruct y; try solve [ exact I ]; repeat split;
     try apply @MeetDec.bound2; try apply¬ @PosetDec.refl.
    introv R1 R2. destruct z; destruct y; tryfalse; destruct x;
     try solve [ exact I ]; tryfalse; try inverts R1; try inverts R2;
     intuit; repeat split; try solve [ simpls¬ ];
     try (apply @MeetDec.greatest_lower_bound; try assumption);
     try match goal with
     | |- (_ _ _ ?a1) ⊑♯ (_ _ _ ?a2) ⇒
       asserts (?&?): (a1 ⊑♯ a2); assumption
     end.
   apply BotDec.Make with (elem := sign_ast_bot). intros (); simpls¬.
   exact (fun _ ar ⇒ ar).
Defined.

Global Instance sign_ast_Top : TopDec.t sign_ast.
  apply TopDec.Make with (elem := sign_ast_top). intros (); simpls¬.
Defined.

Definition sign_gamma_ast : sign_ast → ℘ while_st := fun asigma sigma ⇒
  match asigma, sigma with
  | sign_ast_top, _ ⇒ True
  | sign_ast_expr Ev1, while_st_expr Ev2 ⇒
    gamma_aEnvV Ev1 Ev2
  | sign_ast_stat Ev1 Ef1, while_st_stat Ev2 Ef2 ⇒
    gamma_aEnvV Ev1 Ev2 ∧ gamma_aEnvF Ef1 Ef2
  | sign_ast_prog Ev1 Ef1, while_st_prog Ev2 Ef2 ⇒
    gamma_aEnvV Ev1 Ev2 ∧ gamma_aEnvF Ef1 Ef2
  | sign_ast_add_1 Ev1 r1, while_st_add_1 Ev2 r2 ⇒
    gamma_aEnvV Ev1 Ev2 ∧ sign_gamma_ares r1 r2
  | sign_ast_add_2 v1 r1, while_st_add_2 v2 r2 ⇒
    gamma_aVal v1 v2 ∧ sign_gamma_ares r1 r2
  | sign_ast_asgn_1 Ev1 r1, while_st_asgn_1 Ev2 r2 ⇒
    gamma_aEnvV Ev1 Ev2 ∧ sign_gamma_ares r1 r2
  | sign_ast_seq_1 C1 Ef1 r1, while_st_seq_1 C2 Ef2 r2 ⇒
    gamma_aCtxEnv C1 C2 ∧ gamma_aEnvF Ef1 Ef2 ∧ sign_gamma_ares r1 r2
  | sign_ast_if_1 Ev1 Ef1 r1, while_st_if_1 Ev2 Ef2 r2 ⇒
    gamma_aEnvV Ev1 Ev2 ∧ gamma_aEnvF Ef1 Ef2 ∧ sign_gamma_ares r1 r2
  | sign_ast_while_1 C1 Ef1 r1, while_st_while_1 C2 Ef2 r2 ⇒
    gamma_aCtxEnv C1 C2 ∧ gamma_aEnvF Ef1 Ef2 ∧ sign_gamma_ares r1 r2
  | sign_ast_while_2 Ev1 Ef1 r1, while_st_while_2 Ev2 Ef2 r2 ⇒
    gamma_aEnvV Ev1 Ev2 ∧ gamma_aEnvF Ef1 Ef2 ∧ sign_gamma_ares r1 r2
  | sign_ast_proc_call_1 Ev1 Ef1 r1, while_st_proc_call_1 Ev2 Ef2 r2 ⇒
    gamma_aEnvV Ev1 Ev2 ∧ gamma_aEnvF Ef1 Ef2 ∧ sign_gamma_ares r1 r2
  | _, _ ⇒ False
  end.

Global Instance sign_Gamma_ast : Gamma.t _ _ sign_gamma_ast.
Proof.
  constructors.
   introv O. destruct N1; destruct N2; tryfalse; try solve [ simpls¬ ];
     intros sigma G; tryfalse; destruct sigma; tryfalse;
     repeat match goal with
     | e : aEnvV |- _ ⇒ destruct e as [? ?]
     end.
    inverts G as GE GC. inverts O as OE OC. split.
     apply¬ (@Gamma.monotone _ _ _ _ gamma_aEnv _ _ _ OE).
     apply¬ (@Gamma.monotone _ _ _ _ gamma_aCtxEnv _ _ _ OC).
    inverts G as GE Gr. inverts O as OE Or. splits.
     apply¬ (@Gamma.monotone _ _ _ _ gamma_aEnvV _ _ _ OE).
     apply¬ (@Gamma.monotone _ _ _ _ gamma_aEnvF _ _ _ Or).
    inverts G as Gv Gr. inverts O as Ov Or. splits.
     apply¬ (@Gamma.monotone _ _ _ _ gamma_aEnvV _ _ _ Ov).
     apply¬ (@Gamma.monotone _ _ _ _ gamma_aEnvF _ _ _ Or).
    inverts G as GE Gr. inverts O as OE Or. splits.
     apply¬ (@Gamma.monotone _ _ _ _ gamma_aEnvV _ _ _ OE).
     apply¬ (@Gamma.monotone _ _ _ _ sign_gamma_ares _ _ _ Or).
    inverts G as Gv Gr. inverts O as Ov Or. splits.
     apply¬ (@Gamma.monotone _ _ _ _ gamma_aVal _ _ _ Ov).
     apply¬ (@Gamma.monotone _ _ _ _ sign_gamma_ares _ _ _ Or).
    inverts G as GE Gr. inverts O as OE Or. splits.
     apply¬ (@Gamma.monotone _ _ _ _ gamma_aEnvV _ _ _ OE).
     apply¬ (@Gamma.monotone _ _ _ _ sign_gamma_ares _ _ _ Or).
    inverts G as GC [GE Gr]. inverts O as OC [OE Or]. splits.
     apply¬ (@Gamma.monotone _ _ _ _ gamma_aCtxEnv _ _ _ OC).
     apply¬ (@Gamma.monotone _ _ _ _ gamma_aEnvF _ _ _ OE).
     apply¬ (@Gamma.monotone _ _ _ _ sign_gamma_ares _ _ _ Or).
    inverts G as GEv [GEf Gr]. inverts O as OEv [OEf Or]. splits.
     apply¬ (@Gamma.monotone _ _ _ _ gamma_aEnvV _ _ _ OEv).
     apply¬ (@Gamma.monotone _ _ _ _ gamma_aEnvF _ _ _ OEf).
     apply¬ (@Gamma.monotone _ _ _ _ sign_gamma_ares _ _ _ Or).
    inverts G as GC [GE Gr]. inverts O as OC [OE Or]. splits.
     apply¬ (@Gamma.monotone _ _ _ _ gamma_aCtxEnv _ _ _ OC).
     apply¬ (@Gamma.monotone _ _ _ _ gamma_aEnvF _ _ _ OE).
     apply¬ (@Gamma.monotone _ _ _ _ sign_gamma_ares _ _ _ Or).
    inverts G as GEv [GEf Gr]. inverts O as OEv [OEf Or]. splits.
     apply¬ (@Gamma.monotone _ _ _ _ gamma_aEnvV _ _ _ OEv).
     apply¬ (@Gamma.monotone _ _ _ _ gamma_aEnvF _ _ _ OEf).
     apply¬ (@Gamma.monotone _ _ _ _ sign_gamma_ares _ _ _ Or).
    inverts G as GEv [GEf Gr]. inverts O as OEv [OEf Or]. splits.
     apply¬ (@Gamma.monotone _ _ _ _ gamma_aEnvV _ _ _ OEv).
     apply¬ (@Gamma.monotone _ _ _ _ gamma_aEnvF _ _ _ OEf).
     apply¬ (@Gamma.monotone _ _ _ _ sign_gamma_ares _ _ _ Or).
   introv. destruct N1; destruct N2; tryfalse; try solve [ simpls¬ ];
     intros sigma G; tryfalse; destruct sigma;
     try solve [ false¬ G ]; try solve [ inverts¬ G ];
     repeat match goal with
     | e : aEnvV |- _ ⇒ destruct e as [? ?]
     end.
    inverts G as [GE1 Gr1] [GE2 Gr2]. split.
     apply (@Gamma.meet_morph _ _ _ _ gamma_aEnv _ _ _ _). simpl. splits×.
     apply (@Gamma.meet_morph _ _ _ _ gamma_aCtxEnv _ _ _ _). simpl. splits×.
    inverts G as [GE1 Gr1] [GE2 Gr2]. split.
     apply (@Gamma.meet_morph _ _ _ _ gamma_aEnvV _ _ _ _). simpl. splits×.
     apply (@Gamma.meet_morph _ _ _ _ gamma_aEnvF _ _ _ _). simpl. splits×.
    inverts G as [GE1 Gr1] [GE2 Gr2]. split.
     apply (@Gamma.meet_morph _ _ _ _ gamma_aEnvV _ _ _ _). simpl. splits×.
     apply (@Gamma.meet_morph _ _ _ _ gamma_aEnvF _ _ _ _). simpl. splits×.
    inverts G as [Gv1 Gr1] [Gv2 Gr2]. split.
     apply (@Gamma.meet_morph _ _ _ _ gamma_aEnvV _ _ _ _). simpl. splits×.
     apply (@Gamma.meet_morph _ _ _ _ sign_gamma_ares _ _ _ _). simpl. splits×.
    inverts G as [GE1 Gr1] [GE2 Gr2]. split.
     apply (@Gamma.meet_morph _ _ _ _ gamma_aVal _ _ _ _). simpl. splits×.
     apply (@Gamma.meet_morph _ _ _ _ sign_gamma_ares _ _ _ _). simpl. splits×.
    inverts G as [GE1 Gr1] [GE2 Gr2]. split.
     apply (@Gamma.meet_morph _ _ _ _ gamma_aEnvV _ _ _ _). simpl. splits×.
     apply (@Gamma.meet_morph _ _ _ _ sign_gamma_ares _ _ _ _). simpl. splits×.
    inverts G as [GE1 Gr1] [GE2 Gr2]. repeat split.
     apply (@Gamma.meet_morph _ _ _ _ gamma_aCtxEnv _ _ _ _). simpl. splits×.
     apply (@Gamma.meet_morph _ _ _ _ gamma_aEnvF _ _ _ _). simpl. splits×.
     apply (@Gamma.meet_morph _ _ _ _ sign_gamma_ares _ _ _ _). simpl. splits×.
    inverts G as [GE1 Gr1] [GE2 Gr2]. split; [|split].
     apply (@Gamma.meet_morph _ _ _ _ gamma_aEnvV _ _ _ _). simpl. splits×.
     apply (@Gamma.meet_morph _ _ _ _ gamma_aEnvF _ _ _ _). simpl. splits×.
     apply (@Gamma.meet_morph _ _ _ _ sign_gamma_ares _ _ _ _). simpl. splits×.
    inverts G as [GE1 [GF1 Gr1]] [GE2 [GF2 Gr2]]. split; [|split].
     apply (@Gamma.meet_morph _ _ _ _ gamma_aCtxEnv _ _ _ _). simpl. splits×.
     apply (@Gamma.meet_morph _ _ _ _ gamma_aEnvF _ _ _ _). simpl. splits×.
     apply (@Gamma.meet_morph _ _ _ _ sign_gamma_ares _ _ _ _). simpl. splits×.
    inverts G as [GE1 [GF1 Gr1]] [GE2 [GF2 Gr2]]. split; [|split].
     apply (@Gamma.meet_morph _ _ _ _ gamma_aEnvV _ _ _ _). simpl. splits×.
     apply (@Gamma.meet_morph _ _ _ _ gamma_aEnvF _ _ _ _). simpl. splits×.
     apply (@Gamma.meet_morph _ _ _ _ sign_gamma_ares _ _ _ _). simpl. splits×.
    inverts G as [GE1 [GF1 Gr1]] [GE2 [GF2 Gr2]]. split; [|split].
     apply (@Gamma.meet_morph _ _ _ _ gamma_aEnvV _ _ _ _). simpl. splits×.
     apply (@Gamma.meet_morph _ _ _ _ gamma_aEnvF _ _ _ _). simpl. splits×.
     apply (@Gamma.meet_morph _ _ _ _ sign_gamma_ares _ _ _ _). simpl. splits×.
Qed.

Inductive abort_ares : sign_ares → Prop :=
  | abort_ares_expr : ∀ ar,
    sign_ares_expr (⊥♯, ⊤♯) ⊑♯ ar →
    abort_ares ar
  | abort_ares_stat : ∀ ar,
    sign_ares_stat (⊥♯, ⊤♯) ⊑♯ ar →
    abort_ares ar
  .

Inductive abort_ast : sign_ast → Prop :=
  | abort_ast_add_1 : ∀ Ev r,
    abort_ares r →
    abort_ast (sign_ast_add_1 Ev r)
  | abort_ast_add_2 : ∀ v r,
    abort_ares r →
    abort_ast (sign_ast_add_2 v r)
  | abort_ast_asgn_1 : ∀ Ev r,
    abort_ares r →
    abort_ast (sign_ast_asgn_1 Ev r)
  | abort_ast_seq_1 : ∀ C Ef r,
    abort_ares r →
    abort_ast (sign_ast_seq_1 C Ef r)
  | abort_ast_if_1 : ∀ Ev Ef r,
    abort_ares r →
    abort_ast (sign_ast_if_1 Ev Ef r)
  | abort_ast_while_1 : ∀ C Ef r,
    abort_ares r →
    abort_ast (sign_ast_while_1 C Ef r)
  | abort_ast_while_2 : ∀ Ev Ef r,
    abort_ares r →
    abort_ast (sign_ast_while_2 Ev Ef r)
  | abort_ast_proc_call_1 : ∀ Ev Ef r,
    abort_ares r →
    abort_ast (sign_ast_proc_call_1 Ev Ef r)
  .

Definition sign_acond n asigma : Prop :=
  match n, asigma with
  | _, sign_ast_top ⇒
      True
  | name_abort_ext_expr e, sigma ⇒
      abort_ast sigma
  | name_abort_ext_stat s, sigma ⇒
      abort_ast sigma
  | name_cst c, sign_ast_expr aEv ⇒
      True
  | name_var x, sign_ast_expr (aE, aC) ⇒
      let av := read_env aE x in ¬ av =♯ (⊥♯) ∧ ¬ av =♯ aUndef
  | name_varCxt x, sign_ast_expr (aE, aC) ⇒
      ∃ v, Some (Some (Some (x, v))) ⊑♯ aC
  | name_varUndef x, sign_ast_expr (aE, aC) ⇒
      (∀ v, ¬ aC ⊑♯ Some (Some (Some (x, v)))) ∧
      aUndef ⊑♯ read_env aE x
  | name_add e1 e2, sign_ast_expr aEv ⇒
      True
  | name_add_1 e2, sign_ast_add_1 aEv ar ⇒
      sign_ares_expr (⊥♯) ⊑♯ ar
  | name_add_2, sign_ast_add_2 av ar ⇒
      sign_ares_expr (⊥♯) ⊑♯ ar
  | name_skip, sign_ast_stat aEv aEf ⇒
      True
  | name_throw, sign_ast_stat aEv aEf ⇒
      True
  | name_asgn x e, sign_ast_stat aEv aEf ⇒
      True
  | name_asgn_1 x, sign_ast_asgn_1 (aE, aC) ar ⇒
      (~ ∃ v, aC ⊑♯ Some (Some (Some (x, v)))) ∧
      sign_ares_expr (⊥♯) ⊑♯ ar
  | name_asgn_1_immutable x, sign_ast_asgn_1 (aE, aC) ar ⇒
      (∃ v, Some (Some (Some (x, v))) ⊑♯ aC) ∧
      sign_ares_expr (⊥♯) ⊑♯ ar
  | name_seq s1 s2, sign_ast_stat aEv aEf ⇒
      True
  | name_seq_1 s2, sign_ast_seq_1 aC aEf ar ⇒
      sign_ares_stat (⊥♯) ⊑♯ ar
  | name_if e s1 s2, sign_ast_stat aEv aEf ⇒
      True
  | name_if_1_true s1 s2, sign_ast_if_1 aEv aEf o ⇒
      sign_ares_expr (Sign.pos, ⊥♯) ⊑♯ o ∨ sign_ares_expr (Sign.neg, ⊥♯) ⊑♯ o
  | name_if_1_false s1 s2, sign_ast_if_1 aEv aEf o ⇒
      sign_ares_expr (Sign.zero, ⊥♯) ⊑♯ o
  | name_while e s, sign_ast_stat aEv aEf ⇒
      True
  | name_while_1 e s, sign_ast_while_1 aC aEf ar ⇒
      sign_ares_stat (⊥♯) ⊑♯ ar
  | name_while_2_true e s, sign_ast_while_2 aEv aEf o ⇒
      sign_ares_expr (Sign.pos, ⊥♯) ⊑♯ o ∨ sign_ares_expr (Sign.neg, ⊥♯) ⊑♯ o
  | name_while_2_false e s, sign_ast_while_2 aEv aEf o ⇒
      sign_ares_expr (Sign.zero, ⊥♯) ⊑♯ o
  | name_proc_call f e, sign_ast_stat aEv aEf ⇒
      True
  | name_proc_call_1 f x s, sign_ast_proc_call_1 aEv aEf ar ⇒
      FlatLatticeDec.TB_Elem (Some (x, s)) ⊑♯ readF_env aEf f ∧
      sign_ares_expr (⊥♯) ⊑♯ ar
  | name_proc_call_1_undef f, sign_ast_proc_call_1 aEv aEf ar ⇒
      FlatLatticeDec.TB_Elem None ⊑♯ readF_env aEf f ∧
      sign_ares_expr (⊥♯) ⊑♯ ar
  | name_proc_decl f x s p, sign_ast_prog aEv aEf ⇒
      True
  | name_prog_stat s, sign_ast_prog Ev Ef ⇒
      True
  | _, _ ⇒
      False
  end.

Definition sign_acond_concr n asigma :=
  ∃ sigma,
    sign_gamma_ast asigma sigma
    ∧ while_cond n sigma.

Lemma gamma_ares_abort : ∀ ar r,
  sign_gamma_ares ar r →
  abort_res r →
  abort_ares ar.
Proof.
  introv G A. inverts A; destruct ar as [[av ae]|[aE ae]| |]; simpls; tryfalse;
    inverts G as G; try solve [ constructors; apply (@TopDec.prop _ _ sign_ares_Top) ];
    inverts G as G.
   apply abort_ares_expr. repeat constructors. intro er. destruct¬ er.
   apply abort_ares_stat. constructors.
    apply BotDec.prop.
    intro er. destruct¬ er.
Qed.

Lemma sign_acond_correct : ∀ n asigma sigma,
  sign_gamma_ast asigma sigma →
  while_cond n sigma →
  sign_acond n asigma.
Proof.
  introv G C. destruct n; destruct sigma; unfolds in C; tryfalse;
    destruct asigma; unfolds in G; tryfalse; unfolds; try exact I;
    try solve [ inverts C as C; try constructors; applys× gamma_ares_abort C; inverts¬ G ];
    try solve [ inverts C as C; try constructors; applys× gamma_ares_abort; inverts¬ G ].
   destruct e as [E c]. destruct a as [aE ac]. inverts G as GE Gc.
   forwards Gv: (rm GE) v. rewrite read_option_def in Gv.
   cases_if as I; try solve [ false¬ I ]. inverts Gv as G1 G2.
    unfolds read_env. rewrite <- G2. splits; intro A; inverts A as A A'.
     clear - A G1. forwards G': gamma_eq A G1; try typeclass. applys¬ Sign.bottom_empty G'.
     inverts A'.
    unfolds read_env. rewrite <- G1. splits; intro A; inverts A as A A'.
    false. unfolds in G1. applys¬ Sign.bottom_empty G1.
   destruct e as [E [[y vy]|]]; tryfalse. substs. destruct a as [aE ac]. inverts G as GE Gc.
   compute in Gc. destruct ac as [[[[x av]|]|]|]; tryfalse.
    inverts Gc as ? Gv. eexists. apply PosetDec.refl. auto×.
    ∃ (Sign.top). auto×.
   destruct e as [E c]. destruct a as [aE ac]. inverts G as GE Gc.
   forwards Gv: (rm GE) v. rewrite read_option_def in Gv. simpl in Gc. lets (C1&C2): (rm C).
   cases_if as I; try solve [ false¬ I ]; inverts Gv as G1 G2 G3.
    unfolds read_env. rewrite <- G2. splits.
     introv A. destruct c as [[x v']|]; destruct ac as [[[[ax av']|]|]|]; tryfalse.
      inverts A. simpls. intuit. substs×.
     constructors×.
    unfolds read_env. rewrite <- G1. splits.
     introv A. destruct c as [[x v']|]; destruct ac as [[[[ax av']|]|]|]; tryfalse.
      inverts A. simpls. intuit. substs×.
     constructors×.
    false.
   lets (o&?&Vo): (rm C). substs. lets (GE&Gr): (rm G).
   destruct s; tryfalse; constructors; simpls.
    constructors.
    rew_refl×.
   lets (o&?&Vo): (rm C). substs. lets (GE&Gr): (rm G).
   destruct s; tryfalse.
    destruct a0; tryfalse. split; simpl.
     constructors.
     rew_refl×.
    auto×.
   destruct e as [E c]. destruct a as [aE ac]. inverts G as GE Gr. inverts C as CE Cr.
   lets (o&?&Vo): (rm Cr). substs. inverts GE as GE GC. splits.
    introv (v'&C). destruct ac as [[[[? ?]|]|]|]; inverts C; simpls; substs; tryfalse.
     destruct c as [?|]; false. simpl in GC. intuit. substs. apply CE.
     destruct p. constructors¬.
    destruct s; tryfalse.
     destruct a; tryfalse. split; simpl.
      constructors.
      rew_refl×.
     auto×.
   destruct e as [E c]. destruct a as [aE ac]. inverts G as GE Gr. inverts C as CE Cr.
   lets (o&?&Vo): (rm Cr). substs. inverts GE as GE GC. splits.
    destruct ac as [[[[? ?]|]|]|]; simpl in GC; tryfalse;
      [| | ∃ (Sign.top); auto× ]; destruct c; simpl in GC;
      tryfalse; intuit; substs; inverts CE.
     eexists. auto×.
    destruct s; tryfalse.
     destruct a; tryfalse. split; simpl.
      constructors.
      rew_refl×.
     auto×.
   lets (o&?&Vo): (rm C). substs. lets (GC&Gf&Gr): (rm G).
   destruct s0; tryfalse.
    destruct a1; tryfalse. split; apply BotDec.prop.
    auto×.
   lets (o&D&Vo): (rm C). substs. inverts G as GE [Gf Gr]. destruct s1; tryfalse.
    inverts Gr as Gv. inverts Gv; let t := constructors; [ constructors | simpl; rew_refl× ] in
     (left; t) || (right; t) || (false D; math).
    auto×.
   substs. inverts G as GE [Gf Gr]. destruct s1; tryfalse.
    inverts Gr as Gv. constructors.
     inverts Gv; tryfalse; try constructors. math.
     simpl. rew_refl×.
    auto×.
   lets (o&?&Vo): (rm C). substs. lets (GC&Gf&Gr): (rm G).
   destruct s0; tryfalse.
    apply BotDec.prop.
    auto×.
   lets (o&D&Vo): (rm C). substs. inverts G as GE [Gf Gr]. destruct s0; tryfalse.
    inverts Gr as Gv. inverts Gv; let t := constructors; [ constructors | simpl; rew_refl× ] in
     (left; t) || (right; t) || (false D; math).
    auto×.
   substs. inverts G as GE [Gf Gr]. destruct s0; tryfalse.
    inverts Gr as Gv. constructors.
     inverts Gv; tryfalse; try constructors. math.
     simpl. rew_refl×.
    auto×.
   lets (R&o&?&Vo): (rm C). substs. lets (GC&Gf&Gr): (rm G). splits.
    destruct a0; tryfalse; simpls¬. substs.
      symmetry. apply¬ @binds_read_option.
    destruct s0; tryfalse.
     destruct a1; tryfalse. split; simpl.
      constructors.
      rew_refl×.
     auto×.
   lets (R&o&?&Vo): (rm C). substs. lets (GC&Gf&Gr): (rm G). splits.
    destruct a0; tryfalse; simpls¬. substs.
      symmetry. apply¬ @not_indom_read_option.
    destruct s; tryfalse.
     destruct a1; tryfalse. split; simpl.
      constructors.
      rew_refl×.
     auto×.
Qed.

Lemma sign_acond_monotone : ∀ n (sigma sigma' : sign_ast),
   sigma' ⊑♯ sigma →
   sign_acond n sigma' → sign_acond n sigma.
Proof.
  introv O C. destruct n; destruct sigma'; tryfalse;
    destruct sigma; tryfalse; trivial;
    try solve [
      do 2 inverts C as C; constructors;
      constructor (refine (PosetDec.trans _ _ _ C _); simpls~; inverts× O) ];
    try solve [
      inverts C as C; inverts H1 as C; constructors;
      constructor (refine (PosetDec.trans _ _ _ C _); simpls~; inverts× O) ].
  destruct a as [E c]. destruct a0 as [E' c']. inverts O as OE OC.
  forwards Ov: OE v. fold (read_env E v) in Ov. fold (read_env E' v) in Ov.
  lets (C1&C2): (rm C).
  splits; destruct (read_env E v) as [()|]; destruct (read_env E' v) as [()|];
    inverts Ov as Ov; tryfalse; intro Eq; inverts Eq as Eq;
    try (inverts Ov as Ov; false C1; constructors; try apply EquivDec.refl; apply¬ Ov);
    try (false C1; constructors; try apply EquivDec.refl; applys¬ inf_bot Ov).
   destruct u as [()|]; destruct u0 as [()|]; tryfalse.
    false¬ C2.
    false C1. constructors×.
  destruct a as [E c]. destruct a0 as [E' c']. inverts O as OE OC.
  forwards Ov: OE v. fold (read_env E v) in Ov. fold (read_env E' v) in Ov.
  lets (av&C'): (rm C).
  destruct c' as [[[[? ?]|]|]|]; tryfalse; simpl;
    try solve [ destruct c as [[[[? ?]|]|]|]; false ].
   destruct c as [[[[? ?]|]|]|]; tryfalse. simpl in OC. simpl in C'. intuit. substs.
    eexists; splits×.
    ∃ Sign.top. auto¬.
  destruct a as [E c]. destruct a0 as [E' c']. inverts O as OE OC.
  forwards Ov: OE v. fold (read_env E v) in Ov. fold (read_env E' v) in Ov.
  lets (C1&C2): (rm C). splits.
   introv A. destruct c' as [[[[? ?]|]|]|]; tryfalse;
     destruct c as [[[[? ?]|]|]|]; tryfalse.
    inverts A as A1 A2. simpl in A2. simpl in OC. intuit. substs. false× C1.
    destruct¬ (C1 Sign.zero).
    destruct¬ (C1 Sign.zero).
   exact (PosetDec.trans _ _ _ C2 Ov).
  inverts O as O1 O2. exact (PosetDec.trans _ _ _ C O2).
  inverts O as O1 O2. exact (PosetDec.trans _ _ _ C O2).
  destruct a as [E c]. destruct a0 as [E' c'].
  inverts O as O1 O2. lets (NC&Cr): (rm C). split.
   introv (v'&Eq). destruct c' as [[[[? ?]|]|]|]; tryfalse.
    simpl in Eq. intuit. substs.
     destruct c as [[[[? ?]|]|]|]; simpl in O1; intuit; substs; tryfalse.
      apply NC. eexists. auto×.
      apply NC. ∃ Sign.bot. auto×.
    destruct c as [[[[? ?]|]|]|]; simpl in O1; intuit; substs; tryfalse.
     apply NC. ∃ Sign.bot. auto×.
   exact (PosetDec.trans _ _ _ Cr O2).
  destruct a as [E c]. destruct a0 as [E' c'].
  inverts O as [? O1] O2. lets ((v'&Hv')&Cr): (rm C). split.
   ∃ v'. exact (PosetDec.trans _ _ _ Hv' O1).
   exact (PosetDec.trans _ _ _ Cr O2).
  inverts O as [? O1] O2. destruct s0; tryfalse; destruct s1; tryfalse; try exact I.
  inverts O1 as O1 O2. inverts C as C1 C2. split.
   exact (PosetDec.trans _ _ _ C1 O1).
   exact (PosetDec.trans _ _ _ C2 O2).
  inverts C as C; [ left | right ]; inverts O as O1 [O2 O3];
    exact (PosetDec.trans _ _ _ C O3).
  inverts O as O1 [O2 O3]. exact (PosetDec.trans _ _ _ C O3).
  inverts O as O1 [O2 O3]. exact (PosetDec.trans _ _ _ C O3).
  inverts C as C; [ left | right ]; inverts O as O1 [O2 O3];
    exact (PosetDec.trans _ _ _ C O3).
  inverts O as O1 [O2 O3]. exact (PosetDec.trans _ _ _ C O3).
  destruct a as [E c]. destruct a1 as [E' c'].
  inverts O as [O1 O2] [O3 O4]. inverts C as C1 C2. split.
   apply (PosetDec.trans _ _ _ C1). clear - O3.
    destruct a0 as [| |E]; try exact I; destruct a2 as [| |E']; try exact I; tryfalse.
    simpls. substs¬.
   exact (PosetDec.trans _ _ _ C2 O4).
  destruct a as [E c]. destruct a1 as [E' c'].
  inverts O as [O1 O2] [O3 O4]. inverts C as C1 C2. split.
   apply (PosetDec.trans _ _ _ C1). clear - O3.
    destruct a0 as [| |E]; try exact I; destruct a2 as [| |E']; try exact I; tryfalse.
    simpls. substs¬.
   exact (PosetDec.trans _ _ _ C2 O4).
Qed.

Definition if_ares_expr A (f : _ → _ → option A) ar :=
  match ar with
  | sign_ares_expr (av, err) ⇒ f av err
  | sign_ares_top ⇒ f (⊤♯) (⊤♯)
  | _ ⇒ None
  end.

Definition if_ares_stat A (f : _ → _ → option A) ar :=
  match ar with
  | sign_ares_stat (E, err) ⇒ f E err
  | sign_ares_top ⇒ f (⊤♯) (⊤♯)
  | _ ⇒ None
  end.

Definition if_ast_expr A (f : _ → _ → option A) asigma :=
  match asigma with
  | sign_ast_expr (E, C) ⇒ f E C
  | sign_ast_top ⇒ f (⊤♯) (⊤♯)
  | _ ⇒ None
  end.

Definition if_ast_stat A (f : _ → _ → option A) asigma :=
  match asigma with
  | sign_ast_stat Ev Ef ⇒ f Ev Ef
  | sign_ast_top ⇒ f (⊤♯) (⊤♯)
  | _ ⇒ None
  end.

Definition if_ast_prog A (f : _ → _ → option A) asigma :=
  match asigma with
  | sign_ast_prog Ev Ef ⇒ f Ev Ef
  | sign_ast_top ⇒ f (⊤♯) (⊤♯)
  | _ ⇒ None
  end.

Definition if_ast_add_1 A (f : _ → _ → _ → option A) asigma :=
  match asigma with
  | sign_ast_add_1 E ar ⇒ if_ares_expr (f E) ar
  | sign_ast_top ⇒ f (⊤♯) (⊤♯) (⊤♯)
  | _ ⇒ None
  end.

Definition if_ast_add_2 A (f : _ → _ → _ → option A) asigma :=
  match asigma with
  | sign_ast_add_2 av1 ar ⇒ if_ares_expr (f av1) ar
  | sign_ast_top ⇒ f (⊤♯) (⊤♯) (⊤♯)
  | _ ⇒ None
  end.

Definition if_ast_asgn_1 A (f : _ → _ → _ → option A) asigma :=
  match asigma with
  | sign_ast_asgn_1 E ar ⇒ if_ares_expr (f E) ar
  | sign_ast_top ⇒ f (⊤♯) (⊤♯) (⊤♯)
  | _ ⇒ None
  end.

Definition if_ast_seq_1 A (f : _ → _ → _ → _ → option A) asigma :=
  match asigma with
  | sign_ast_seq_1 aC aEf ar ⇒ if_ares_stat (f aC aEf) ar
  | sign_ast_top ⇒ f (⊤♯) (⊤♯) (⊤♯) (⊤♯)
  | _ ⇒ None
  end.

Definition if_ast_if_1 A (f : _ → _ → _ → _ → option A) asigma :=
  match asigma with
  | sign_ast_if_1 Ev Ef ar ⇒ if_ares_expr (f Ev Ef) ar
  | sign_ast_top ⇒ f (⊤♯) (⊤♯) (⊤♯) (⊤♯)
  | _ ⇒ None
  end.

Definition if_ast_while_1 A (f : _ → _ → _ → _ → option A) asigma :=
  match asigma with
  | sign_ast_while_1 C Ef ar ⇒ if_ares_stat (f C Ef) ar
  | sign_ast_top ⇒ f (⊤♯) (⊤♯) (⊤♯) (⊤♯)
  | _ ⇒ None
  end.

Definition if_ast_while_2 A (f : _ → _ → _ → _ → option A) asigma :=
  match asigma with
  | sign_ast_while_2 Ev Ef ar ⇒ if_ares_expr (f Ev Ef) ar
  | sign_ast_top ⇒ f (⊤♯) (⊤♯) (⊤♯) (⊤♯)
  | _ ⇒ None
  end.

Definition if_ast_proc_call_1 A (f : _ → _ → _ → _ → option A) asigma :=
  match asigma with
  | sign_ast_proc_call_1 Ev Ef ar ⇒ if_ares_expr (f Ev Ef) ar
  | sign_ast_top ⇒ f (⊤♯) (⊤♯) (⊤♯) (⊤♯)
  | _ ⇒ None
  end.

Definition sign_arule n : Rule sign_ast sign_ares :=
  match n with
  | name_abort_ext_expr e ⇒
    let ax _ :=
      Some (sign_ares_expr (⊥♯, ⊤♯)) in
    Rule_Ax ax
  | name_abort_ext_stat s ⇒
    let ax _ :=
      Some (sign_ares_stat (⊥♯, ⊤♯)) in
    Rule_Ax ax
  | name_cst c ⇒
    let ax _ :=
      Some (sign_ares_expr (Sign.const c, ⊥♯)) in
    Rule_Ax ax
  | name_var x ⇒
    let ax :=
      if_ast_expr (fun E C ⇒
        Some (sign_ares_expr (get_value (read_env E x), ⊥♯))) in
    Rule_Ax ax
  | name_varCxt x ⇒
    let ax :=
      if_ast_expr (fun E C ⇒
        match C with
        | Some (Some (Some (x, v))) ⇒ Some (sign_ares_expr (v, ⊥♯))
        | None ⇒ Some (sign_ares_expr (⊤♯))
        | _ ⇒ None
        end) in
    Rule_Ax ax
  | name_varUndef x ⇒
    let ax _ :=
      Some (sign_ares_expr (⊥♯, ⊤♯)) in
    Rule_Ax ax
  | name_add e1 e2 ⇒
    let up :=
      if_ast_expr (fun E C ⇒
        Some (sign_ast_expr (E, C))) in
    let next E o :=
      if_ast_expr (fun E C ⇒
        Some (sign_ast_add_1 (E, C) o)) E in
    Rule_R2 up next
  | name_add_1 e2 ⇒
    let up :=
      if_ast_add_1 (fun E av err ⇒
        Some (sign_ast_expr E)) in
    let next asigma ar :=
      if_ast_add_1 (fun E av err ⇒
        Some (sign_ast_add_2 av ar)) asigma in
    Rule_R2 up next
  | name_add_2 ⇒
    let ax :=
      if_ast_add_2 (fun av1 av2 err ⇒
        Some (sign_ares_expr (Sign.sem_add av1 av2, ⊥♯))) in
    Rule_Ax ax
  | name_skip ⇒
    let ax :=
      if_ast_stat (fun Ev Ef ⇒
        Some (sign_ares_stat (fst Ev, ⊥♯))) in
    Rule_Ax ax
  | name_throw ⇒
    let ax _ :=
      Some (sign_ares_stat (⊥♯, ⊤♯)) in
    Rule_Ax ax
  | name_asgn x e ⇒
    let up :=
      if_ast_stat (fun Ev Ef ⇒
        Some (sign_ast_expr Ev)) in
    let next asigma r :=
      if_ast_stat (fun Ev Ef ⇒
        Some (sign_ast_asgn_1 Ev r)) asigma in
    Rule_R2 up next
  | name_asgn_1 x ⇒
    let ax :=
      if_ast_asgn_1 (fun Ev av err ⇒
        Some (sign_ares_stat (write_env (fst Ev) x av, ⊥♯))) in
    Rule_Ax ax
  | name_asgn_1_immutable x ⇒
    let ax _ :=
      Some (sign_ares_stat (⊥♯, ⊤♯)) in
    Rule_Ax ax
  | name_seq s1 s2 ⇒
    let up :=
      if_ast_stat (fun Ev Ef ⇒
        Some (sign_ast_stat Ev Ef)) in
    let next sigma r :=
      if_ast_stat (fun Ev Ef ⇒
        Some (sign_ast_seq_1 (snd Ev) Ef r)) sigma in
    Rule_R2 up next
  | name_seq_1 s2 ⇒
    let up :=
      if_ast_seq_1 (fun C Ef E err ⇒
        Some (sign_ast_stat (E, C) Ef)) in
    Rule_R1 _ up
  | name_if e s1 s2 ⇒
    let up :=
      if_ast_stat (fun Ev Ef ⇒
        Some (sign_ast_expr Ev)) in
    let next sigma r :=
      if_ast_stat (fun Ev Ef ⇒
        Some (sign_ast_if_1 Ev Ef r)) sigma in
    Rule_R2 up next
  | name_if_1_true s1 s2 ⇒
    let up :=
      if_ast_if_1 (fun Ev Ef av err ⇒
        Some (sign_ast_stat Ev Ef)) in
    Rule_R1 _ up
  | name_if_1_false s1 s2 ⇒
    let up :=
      if_ast_if_1 (fun Ev Ef av err ⇒
        Some (sign_ast_stat Ev Ef)) in
    Rule_R1 _ up
  | name_while e s ⇒
    let up :=
      if_ast_stat (fun Ev Ef ⇒
        let (E, C) := Ev in
        Some (sign_ast_while_1 C Ef (sign_ares_stat (E, ⊥♯)))) in
    Rule_R1 _ up
  | name_while_1 e s ⇒
    let up :=
      if_ast_while_1 (fun C Ef E err ⇒
        Some (sign_ast_expr (E, C))) in
    let next asigma ar :=
      if_ast_while_1 (fun C Ef E err ⇒
        Some (sign_ast_while_2 (E, C) Ef ar)) asigma in
    Rule_R2 up next
  | name_while_2_true e s ⇒
    let up :=
      if_ast_while_2 (fun Ev Ef av err ⇒
        Some (sign_ast_stat Ev Ef)) in
    let next asigma r :=
      if_ast_while_2 (fun Ev Ef av err ⇒
        Some (sign_ast_while_1 (snd Ev) Ef r)) asigma in
    Rule_R2 up next
  | name_while_2_false e s ⇒
    let ax :=
      if_ast_while_2 (fun Ev Ef av err ⇒
        Some (sign_ares_stat (fst Ev, ⊥♯))) in
    Rule_Ax ax
  | name_proc_call f e ⇒
    let up :=
      if_ast_stat (fun Ev Ef ⇒
        Some (sign_ast_expr Ev)) in
    let next sigma r :=
      if_ast_stat (fun Ev Ef ⇒
        Some (sign_ast_proc_call_1 Ev Ef r)) sigma in
    Rule_R2 up next
  | name_proc_call_1 f x s ⇒
    let up :=
      if_ast_proc_call_1 (fun Ev Ef av err ⇒
        let C := Some (Some (Some (x, av))) in
        Some (sign_ast_stat (fst Ev, C) Ef)) in
    Rule_R1 _ up
  | name_proc_call_1_undef f ⇒
    let ax _ :=
      Some (sign_ares_stat (⊥♯, ⊤♯)) in
    Rule_Ax ax
  | name_proc_decl f x s p ⇒
    let up :=
      if_ast_prog (fun Ev Ef ⇒
        let Ef := writeF_env Ef f x s in
        Some (sign_ast_prog Ev Ef)) in
    Rule_R1 _ up
  | name_prog_stat s ⇒
    let up :=
      if_ast_prog (fun Ev Ef ⇒
        Some (sign_ast_stat Ev Ef)) in
    Rule_R1 _ up
  end.

Definition sign_asem :=
  make_semantics while_str sign_acond sign_arule.

Lemma sign_arule_format_correct : rule_format_correct_all sign_asem.
Proof. intro n. destruct n; constructors. Qed.

Lemma sign_asemantics_full : semantics_full sign_asem.
Proof.
  intros n asigma C. simpls.
  destruct n; destruct asigma as [aEv|aEv aEf|aEv aEf|aEv ar|av ar|aEv ar|aC aEv ar
                                 |aEv aEf ar|aC aEf ar|aEv aEf ar|aEv aEf ar| |];
    tryfalse;
    try destruct aC as [[[[? ?]|]|]|]; tryfalse;
    try destruct aEv as [aE [[[[? ?]|]|]|]]; tryfalse;
    try destruct ar as [[av' ae]|[av' ae]| |]; tryfalse;
    try solve [ destruct C; tryfalse ];
    try solve [ constructors; eexists; reflexivity ].
Qed.

Lemma option_map_out : ∀ A B (f : A → B) o r,
  option_map f o = Some r →
  ∃ c, o = Some c ∧ f c = r.
Proof. introv Eq. destruct o; inverts× Eq. Qed.

Lemma if_st_expr_out : ∀ A (f : _ → _ → option A) sigma r,
  if_st_expr f sigma = Some r →
  ∃ E C, sigma = while_st_expr (E, C) ∧ f E C = Some r.
Proof. introv Eq. destruct sigma; try destruct e; inverts× Eq. Qed.

Lemma if_ast_expr_out : ∀ A (f : _ → _ → option A) sigma r,
  if_ast_expr f sigma = Some r →
  (sigma = sign_ast_top ∧ f (⊤♯) (⊤♯) = Some r) ∨
  ∃ E C, sigma = sign_ast_expr (E, C) ∧ f E C = Some r.
Proof. introv Eq. destruct sigma; solve [ inverts× Eq ] || (destruct a; inverts× Eq). Qed.

Lemma if_st_stat_out : ∀ A (f : _ → _ → option A) sigma r,
  if_st_stat f sigma = Some r →
  ∃ Ev Ef, sigma = while_st_stat Ev Ef ∧ f Ev Ef = Some r.
Proof. introv Eq. destruct sigma; inverts× Eq. Qed.

Lemma if_ast_stat_out : ∀ A (f : _ → _ → option A) sigma r,
  if_ast_stat f sigma = Some r →
  (sigma = sign_ast_top ∧ f (⊤♯) (⊤♯) = Some r) ∨
  ∃ Ev Ef, sigma = sign_ast_stat Ev Ef ∧ f Ev Ef = Some r.
Proof. introv Eq. destruct sigma; inverts× Eq. Qed.

Lemma if_st_prog_out : ∀ A (f : _ → _ → option A) sigma r,
  if_st_prog f sigma = Some r →
  ∃ Ev Ef, sigma = while_st_prog Ev Ef ∧ f Ev Ef = Some r.
Proof. introv Eq. destruct sigma; inverts× Eq. Qed.

Lemma if_ast_prog_out : ∀ A (f : _ → _ → option A) sigma r,
  if_ast_prog f sigma = Some r →
  (sigma = sign_ast_top ∧ f (⊤♯) (⊤♯) = Some r) ∨
  ∃ Ev Ef, sigma = sign_ast_prog Ev Ef ∧ f Ev Ef = Some r.
Proof. introv Eq. destruct sigma; inverts× Eq. Qed.

Lemma gamma_aEnv_top : ∀ E,
   gamma_aEnv (⊤♯) E.
Proof. intros E x. rewrite MapDefault.read_top. constructors. Qed.

Lemma gamma_aEnv_write : ∀ E aE x v av,
  gamma_aEnv aE E →
  gamma_aVal av v →
  gamma_aEnv (write_env aE x av) (write E x v).
Proof.
  introv G1 G2. intro y. unfolds write_env.
  tests T: (x = y); eapply gamma_eq.
   typeclass.
   apply EquivDec.sym. apply MapDefault.read_write_eq; try typeclass.
   rewrite read_option_write_eq; typeclass.
   typeclass.
   apply EquivDec.sym. apply MapDefault.read_write_neq.
    introv T'. apply T. apply¬ var_eq_eq.
    intro A. inverts A as A'. forwards G: gamma_eq A' G2; try typeclass. inverts G.
   rewrite¬ read_option_write_neq; typeclass.
Qed.

Lemma gamma_aEnvF_write : ∀ Ef aEf f x s,
  gamma_aEnvF aEf Ef →
  gamma_aEnvF (writeF_env aEf f x s) (writeF Ef f x s).
Proof. introv G. destruct aEf; simpls~; tryfalse. substs¬. Qed.

Lemma a_propagates : ∀ n,
  propagates sign_asem while_sem sign_gamma_ast sign_gamma_ares
    (sign_arule n) (while_rule n).
Proof.
  introv. destruct n; constructors.
   introv G E1 E2. inverts E1. inverts E2. constructors. constructors.
   introv G E1 E2. inverts E1. inverts E2. constructors. constructors.
   introv G E1 E2. inverts E1; inverts E2. constructors. apply Sign.const_correct.
   introv G E1 E2. forwards (E&C&Eq&E1a): if_st_expr_out (rm E1). substs.
   forwards (va&Eq&E1b): option_map_out (rm E1a). substs.
   forwards [(aEq&E2a)|(aE&aC&aEq&E2a)]: if_ast_expr_out (rm E2); substs.
    inverts_constr E2a. substs. unfolds.
     constructors. unfolds read_env.
     rewrite MapDefault.read_top. constructors.
    inverts_constr E2a. substs. unfolds.
     constructors. lets (G1&G2): (rm G). forwards¬ G': (rm G1) v. rewrite Eq in G'.
     inverts G' as G1' G2'.
      unfold read_env. rewrite <- G2'. apply G1'.
      unfold read_env. rewrite <- G1'. constructors.
      inverts G1'.
   introv G E1 E2. forwards (E&C&Eq&E1a): if_st_expr_out (rm E1). substs.
   forwards (va&Eq&E1b): option_map_out (rm E1a). substs.
   forwards [(aEq&E2a)|(aE&aC&aEq&E2a)]: if_ast_expr_out (rm E2); substs.
    simpl in E2a. inverts_constr E2a. substs¬. constructors. apply Sign.gamma_top.
    destruct aC as [[[[? ?]|]|]|]; inverts E2a; simpls¬.
     constructors. lets¬ (G1&G2&G3): (rm G).
     constructors. apply Sign.gamma_top.
   introv G E1 E2. inverts E1. inverts E2. constructors. compute; auto×.
   introv G E1 E2. forwards (E&C&Eq&E1a): if_st_expr_out (rm E1). substs. inverts E1a.
   forwards [(aEq&E2a)|(aE&aC&aEq&E2a)]: if_ast_expr_out (rm E2); substs.
    inverts_constr E2a. substs. unfolds. splits¬. apply gamma_aEnv_top.
    inverts¬ E2a.
   introv G1 G2 E1 E2. forwards (E&C&Eq&E1a): if_st_expr_out (rm E1). substs. inverts E1a.
   forwards [(aEq&E2a)|(aE&aC&aEq&E2a)]: if_ast_expr_out (rm E2); substs.
    inverts_constr E2a. substs.
     do 2 splits¬. apply gamma_aEnv_top.
    inverts¬ E2a. splits¬.
   introv G E1 E2. destruct sigma; tryfalse. inverts E1.
   destruct asigma as [| | |E [[av err]| | |]| | | | | | | | |]; simpl in E2;
     tryfalse; inverts_constr E2; substs.
    simpls×.
    unfolds× sign_gamma_ast.
    splits¬. apply gamma_aEnv_top.
   introv G1 G2 E1 E2. destruct sigma as [| | |E r'| | | | | | |]; tryfalse.
   destruct r' as [[v|]|]; inverts E1.
   destruct asigma as [| | |aE ar'| | | | | | | | |]; tryfalse.
    destruct ar' as [[av ?]| | |]; inverts E2; lets (G1a&G1b): (rm G1).
     splits¬. inverts¬ G1b.
     splits¬. constructors.
    inverts E2. splits¬. constructors.
   introv G E1 E2. destruct sigma as [| | | |E r'| | | | | |]; tryfalse.
   destruct r' as [[v2|]|]; inverts E1.
   destruct asigma as [| | | |av ar'| | | | | | | |]; tryfalse. simpl in E2.
    destruct ar' as [[av' ?]| | |]; inverts E2; lets (Ga&Gb): (rm G).
     constructors. eapply Sign.sem_add_correct; auto×. inverts¬ Gb.
     constructors. destruct av; try apply Sign.gamma_top. inverts Ga.
    inverts E2. constructors. apply Sign.gamma_top.
   introv G E1 E2. forwards (Ev&Ef&Eq&E1a): if_st_stat_out (rm E1). substs. inverts E1a.
   forwards [(aEq&E2a)|(aEv&aEf&aEq&E2a)]: if_ast_stat_out (rm E2); inverts_constr E2a; substs.
    constructors. apply gamma_aEnv_top.
    constructors. inverts G as [G1 G2] G3. simpls¬.
   introv G E1 E2. inverts E1. inverts E2. constructors. constructors.
   introv G E1 E2. forwards (E&C&Eq&E1a): if_st_stat_out (rm E1). substs. inverts E1a.
   forwards [(aEq&E2a)|(aE&aC&aEq&E2a)]: if_ast_stat_out (rm E2); substs.
    inverts_constr E2a. substs. unfolds. splits¬. apply gamma_aEnv_top.
    inverts¬ E2a. simpls×.
   introv G1 G2 E1 E2. forwards (Ev&Ef&Eq&E1a): if_st_stat_out (rm E1). substs. inverts E1a.
   forwards [(aEq&E2a)|(aEv&aEf&aEq&E2a)]: if_ast_stat_out (rm E2); substs.
    inverts_constr E2a. substs.
     do 2 splits¬. apply gamma_aEnv_top.
    inverts¬ E2a. simpls. splits×.
   introv G E1 E2. destruct sigma as [| | | | |[E C] r'| | | | |]; tryfalse.
   destruct r' as [[vr|]|]; inverts E1.
   destruct asigma as [| | | | |aE ar'| | | | | | |]; tryfalse.
    destruct ar' as [[av ?]| | |]; inverts E2;
      lets ((G1&G2)&Gb): (rm G); do 2 unfolds in G1; simpls.
     constructors. unfold write_env. eapply MapDefault.gammaf_write; try typeclass.
       intro Eq. inverts Eq as Eq. inverts Gb as G. inverts G; tryfalse.
       introv D. asserts: (v ≠ k').
         intro_subst. apply D. apply Equivalence_Reflexive.
        simpl. repeat rewrite read_option_def. erewrite If_eq.
         reflexivity.
         iff; [ apply¬ @indom_write | eapply @indom_write_inv; auto× ].
         introv I. unfolds write. rewrite¬ @read_write_neq.
         auto×.
       introv S. asserts: (v = k').
         applys var_eq_eq S.
        substs. repeat rewrite read_option_def. cases_if as I.
         constructors. unfolds write. rewrite read_write_eq. inverts¬ Gb.
         false I. apply indom_write_eq.
     constructors. unfold write_env. eapply MapDefault.gammaf_write; try typeclass.
      intro Eq. inverts Eq as Eq. inverts Eq.
      introv D. asserts: (v ≠ k').
        intro_subst. apply D. apply Equivalence_Reflexive.
       simpl. repeat rewrite read_option_def. erewrite If_eq.
        reflexivity.
        iff; [ apply¬ @indom_write | eapply @indom_write_inv; auto× ].
        introv I. unfolds write. rewrite¬ @read_write_neq.
        auto×.
      introv S. asserts: (v = k').
        applys var_eq_eq S.
       substs. repeat rewrite read_option_def. cases_if as I.
        constructors. unfolds write. rewrite read_write_eq. inverts¬ Gb.
         constructors.
        false I. apply indom_write_eq.
      unfolds in E2. inverts_constr E2. subst. constructors.
       apply gamma_aEnv_write.
        apply gamma_aEnv_top.
        apply Sign.gamma_top.
   introv G E1 E2. inverts E1. inverts E2. constructors. constructors.
   introv G E1 E2. forwards (Ev&Ef&Eq&E1a): if_st_stat_out (rm E1). substs. inverts E1a.
   forwards [(aEq&E2a)|(aEv&aEf&aEq&E2a)]: if_ast_stat_out (rm E2); substs.
    inverts_constr E2a. substs. constructors¬. splits¬. apply gamma_aEnv_top.
    inverts¬ E2a.
   introv G1 G2 E1 E2. forwards (Ev&Ef&Eq&E1a): if_st_stat_out (rm E1). substs. inverts E1a.
   forwards [(aEq&E2a)|(aEv&aEf&aEq&E2a)]: if_ast_stat_out (rm E2); substs.
    inverts_constr E2a. substs. splits¬.
    inverts¬ E2a. lets ((Ga&Gb)&Gc): (rm G1). splits¬.
   introv G E1 E2. destruct sigma as [| | | | | |C Ef r| | | |]; tryfalse.
   destruct r as [|[E|]]; inverts E1.
   destruct asigma as [| | | | | |aC aEf ar| | | | | |]; tryfalse.
    destruct ar as [|[aE ?]| |]; simpl in E2; inverts_constr E2; substs;
      inverts G as G1 [G2 G3].
     do 2 splits¬. simpls. inverts¬ G3.
     do 2 splits¬. apply gamma_aEnv_top.
    simpl in E2. inverts_constr E2. substs. do 2 splits¬. apply gamma_aEnv_top.
   introv G E1 E2. forwards (Ev&Ef&Eq&E1a): if_st_stat_out (rm E1). substs. inverts E1a.
   forwards [(aEq&E2a)|(aEv&aEf&aEq&E2a)]: if_ast_stat_out (rm E2); substs.
    inverts_constr E2a. substs. unfolds. splits¬. apply gamma_aEnv_top.
    inverts E2a. simpls. intuit. auto¬.
   introv G1 G2 E1 E2. forwards (Ev&Ef&Eq&E1a): if_st_stat_out (rm E1). substs. inverts E1a.
   forwards [(aEq&E2a)|(aEv&aEf&aEq&E2a)]: if_ast_stat_out (rm E2); substs.
    inverts_constr E2a. substs.
     do 2 splits¬. apply gamma_aEnv_top.
    inverts¬ E2a. simpls. intuit. splits¬.
   introv G E1 E2. destruct sigma as [| | | | | | |Ev Ef ?| | |]; tryfalse. inverts E1.
   destruct asigma as [| | | | | | |aEv aEf [[? ?]| | |]| | | | |]; tryfalse;
     simpl in E2; inverts_constr E2; substs; simpls×.
    do 2 splits¬. apply gamma_aEnv_top.
   introv G E1 E2. destruct sigma as [| | | | | | |Ev Ef ?| | |]; tryfalse. inverts E1.
   destruct asigma as [| | | | | | |aEv aEf [[? ?]| | |]| | | | |]; tryfalse;
     simpl in E2; inverts_constr E2; substs; simpls×.
    do 2 splits¬. apply gamma_aEnv_top.
   introv G E1 E2. forwards ([E C]&Ef&Eq&E1a): if_st_stat_out (rm E1). substs. inverts E1a.
   forwards [(aEq&E2a)|([aE aC]&aEf&aEq&E2a)]: if_ast_stat_out (rm E2); substs.
    simpls. inverts_constr E2a. substs. constructors¬. splits¬.
     simpl. constructors. apply gamma_aEnv_top.
    inverts E2a. inverts G as [G1 G2] G3. splits¬. constructors¬.
   introv G E1 E2. destruct sigma as [| | | | | | | |C Ef r| |]; tryfalse.
   destruct r as [|[E|]]; inverts E1.
   destruct asigma as [| | | | | | | |aC aEf ar| | | |]; tryfalse.
    destruct ar as [|[aE ?]| |]; simpl in E2;
      inverts_constr E2; substs; inverts G as G1 [G2 G3].
     splits¬. inverts¬ G3.
     splits¬. apply gamma_aEnv_top.
    simpl in E2. inverts_constr E2. substs. unfolds. splits¬. apply gamma_aEnv_top.
   introv G1 G2 E1 E2. destruct sigma as [| | | | | | | |C Ef r'| |]; tryfalse.
   destruct r' as [|[E|]]; inverts E1.
   destruct asigma as [| | | | | | | |aC aEf ar'| | | |]; tryfalse.
    destruct ar' as [|[aE ?]| |]; simpl in E2;
      inverts_constr E2; substs; inverts G1 as G1 [G3 G4]; splits¬.
     splits¬. inverts¬ G4.
     splits¬. apply gamma_aEnv_top.
    simpl in E2. inverts_constr E2. substs. do 2 splits¬. apply gamma_aEnv_top.
   introv G E1 E2. destruct sigma as [| | | | | | | | |Ev Ef ?| ]; tryfalse. inverts E1.
   destruct asigma as [| | | | | | | | |aEv aEf [[? ?]| | |]| | |]; tryfalse;
     simpl in E2; inverts_constr E2; substs; simpls×.
    do 2 splits¬. apply gamma_aEnv_top.
   introv G1 G2 E1 E2. destruct sigma as [| | | | | | | | |Ev Ef ?| ]; tryfalse. inverts E1.
   destruct asigma as [| | | | | | | | |aEv aEf [[? ?]| | |]| | |]; tryfalse;
     simpl in E2; inverts_constr E2; substs; simpls*;
     lets ([? ?]&?&?): (rm G1); splits¬.
   introv G E1 E2. destruct sigma as [| | | | | | | | |[E C] Ef ?| ]; tryfalse. inverts E1.
   destruct asigma as [| | | | | | | | |aEv aEf [[? ?]| | |]| | |]; tryfalse;
     simpl in E2; inverts_constr E2; substs; simpls; constructors×.
    lets¬ ([? ?]&?&?): (rm G).
    lets¬ ([? ?]&?&?): (rm G).
    apply gamma_aEnv_top.
   introv G E1 E2. forwards ([E C]&Ef&Eq&E1a): if_st_stat_out (rm E1). substs. inverts E1a.
   forwards [(aEq&E2a)|([aE aC]&aEf&aEq&E2a)]: if_ast_stat_out (rm E2);
     substs; inverts E2a; substs.
    constructors¬. simpl. apply gamma_aEnv_top.
    inverts G as [G1 G2] G3. splits¬.
   introv G1 G2 E1 E2. forwards (Ev&Ef&Eq&E1a): if_st_stat_out (rm E1). substs. inverts E1a.
   forwards [(aEq&E2a)|(aEv&aEf&aEq&E2a)]: if_ast_stat_out (rm E2);
     substs; inverts E2a; substs.
    do 2 splits¬. apply gamma_aEnv_top.
    simpls. intuit. splits¬.
   introv G E1 E2. destruct sigma as [| | | | | | | | | |[E C] Ef r]; tryfalse.
   destruct r as [[v'|]|]; inverts E1.
   destruct asigma as [| | | | | | | | | |aEv aEf [[? ?]| | |]| |]; tryfalse;
     simpl in E2; inverts_constr E2; substs; simpls*;
     try lets¬ ([G1 G2]&G3&G4): (rm G); repeat (splits~; simpl).
    inverts¬ G4.
    constructors¬.
    apply gamma_aEnv_top.
    constructors¬.
   introv G E1 E2. inverts E1. inverts E2. constructors. constructors.
   introv G E1 E2. forwards ([E C]&Ef&Eq&E1a): if_st_prog_out (rm E1). substs. inverts E1a.
   forwards [(aEq&E2a)|([aE aC]&aEf&aEq&E2a)]: if_ast_prog_out (rm E2);
     substs; inverts E2a; substs.
    constructors¬. splits¬. apply gamma_aEnv_top.
    inverts G as [G1 G2] G3. repeat splits¬.
     apply¬ gamma_aEnvF_write.
   introv G E1 E2. forwards (Ev&Ef&Eq&E1a): if_st_prog_out (rm E1). substs. inverts E1a.
   forwards [(aEq&E2a)|(aEv&aEf&aEq&E2a)]: if_ast_prog_out (rm E2); substs.
    inverts_constr E2a. substs. simpls. do 2 splits¬. apply gamma_aEnv_top.
    inverts¬ E2a.
Qed.

Lemma sign_asem_correct : ∀ t asigma ar,
  aeval sign_asem _ _ t asigma ar → ∀ sigma r,
  sign_gamma_ast asigma sigma →
  eval while_sem t sigma r →
  sign_gamma_ares ar r.
Proof.
  introv aD G D.
  eapply (correctness (sem := while_sem) (asem := sign_asem) _ _ a_propagates); try typeclass.
  apply sign_acond_correct.
Qed.