Library AbstractSign
This file contains the abstract semantics and some example of
abstract derivations.
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
The following two are needed as we have to lattice this type.
| 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 → ℘ sign_res := fun ar r ⇒
match ar, r with
| sign_ares_top, _ ⇒ True
| sign_ares_expr ao, sign_res_expr o ⇒ gamma_aOute ao o
| sign_ares_stat ao, sign_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_prog : aEnv → sign_ast
| sign_ast_add_1 : aEnv → sign_ares → sign_ast
| sign_ast_add_2 : aVal → sign_ares → sign_ast
| sign_ast_asgn_1 : aEnv → sign_ares → sign_ast
| sign_ast_seq_1 : sign_ares → sign_ast
| sign_ast_if_1 : aEnv → sign_ares → sign_ast
| sign_ast_while_1 : sign_ares → sign_ast
| sign_ast_while_2 : aEnv → sign_ares → sign_ast
| 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 → ℘ sign_res := fun ar r ⇒
match ar, r with
| sign_ares_top, _ ⇒ True
| sign_ares_expr ao, sign_res_expr o ⇒ gamma_aOute ao o
| sign_ares_stat ao, sign_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_prog : aEnv → sign_ast
| sign_ast_add_1 : aEnv → sign_ares → sign_ast
| sign_ast_add_2 : aVal → sign_ares → sign_ast
| sign_ast_asgn_1 : aEnv → sign_ares → sign_ast
| sign_ast_seq_1 : sign_ares → sign_ast
| sign_ast_if_1 : aEnv → sign_ares → sign_ast
| sign_ast_while_1 : sign_ares → sign_ast
| sign_ast_while_2 : aEnv → sign_ares → sign_ast
The following two are needed as we have to lattice this type.
| sign_ast_top : sign_ast
| sign_ast_bot : sign_ast
.
Definition sign_ast_eq asigma1 asigma2 :=
match asigma1, asigma2 with
| sign_ast_prog E1, sign_ast_prog E2 ⇒ E1 =♯ E2
| sign_ast_add_1 E1 r1, sign_ast_add_1 E2 r2 ⇒ E1 =♯ E2 ∧ r1 =♯ r2
| sign_ast_add_2 v1 r1, sign_ast_add_2 v2 r2 ⇒ v1 =♯ v2 ∧ r1 =♯ r2
| sign_ast_asgn_1 E1 r1, sign_ast_asgn_1 E2 r2 ⇒ E1 =♯ E2 ∧ r1 =♯ r2
| sign_ast_seq_1 r1, sign_ast_seq_1 r2 ⇒ r1 =♯ r2
| sign_ast_if_1 E1 r1, sign_ast_if_1 E2 r2 ⇒ E1 =♯ E2 ∧ r1 =♯ r2
| sign_ast_while_1 r1, sign_ast_while_1 r2 ⇒ r1 =♯ r2
| sign_ast_while_2 E1 r1, sign_ast_while_2 E2 r2 ⇒ E1 =♯ E2 ∧ 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_prog E1, sign_ast_prog E2 ⇒ E1 ⊑♯ E2
| sign_ast_add_1 E1 r1, sign_ast_add_1 E2 r2 ⇒ E1 ⊑♯ E2 ∧ r1 ⊑♯ r2
| sign_ast_add_2 v1 r1, sign_ast_add_2 v2 r2 ⇒ v1 ⊑♯ v2 ∧ r1 ⊑♯ r2
| sign_ast_asgn_1 E1 r1, sign_ast_asgn_1 E2 r2 ⇒ E1 ⊑♯ E2 ∧ r1 ⊑♯ r2
| sign_ast_seq_1 r1, sign_ast_seq_1 r2 ⇒ r1 ⊑♯ r2
| sign_ast_if_1 E1 r1, sign_ast_if_1 E2 r2 ⇒ E1 ⊑♯ E2 ∧ r1 ⊑♯ r2
| sign_ast_while_1 r1, sign_ast_while_1 r2 ⇒ r1 ⊑♯ r2
| sign_ast_while_2 E1 r1, sign_ast_while_2 E2 r2 ⇒ E1 ⊑♯ E2 ∧ r1 ⊑♯ r2
| _, _ ⇒ False
end.
Definition sign_ast_join ar1 ar2 :=
match ar1, ar2 with
| sign_ast_bot, _ ⇒ ar2
| _, sign_ast_bot ⇒ ar1
| sign_ast_prog E1, sign_ast_prog E2 ⇒ sign_ast_prog (E1 ⊔♯ E2)
| sign_ast_add_1 E1 r1, sign_ast_add_1 E2 r2 ⇒ sign_ast_add_1 (E1 ⊔♯ E2) (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 E1 r1, sign_ast_asgn_1 E2 r2 ⇒ sign_ast_asgn_1 (E1 ⊔♯ E2) (r1 ⊔♯ r2)
| sign_ast_seq_1 r1, sign_ast_seq_1 r2 ⇒ sign_ast_seq_1 (r1 ⊔♯ r2)
| sign_ast_if_1 E1 r1, sign_ast_if_1 E2 r2 ⇒ sign_ast_if_1 (E1 ⊔♯ E2) (r1 ⊔♯ r2)
| sign_ast_while_1 r1, sign_ast_while_1 r2 ⇒ sign_ast_while_1 (r1 ⊔♯ r2)
| sign_ast_while_2 E1 r1, sign_ast_while_2 E2 r2 ⇒ sign_ast_while_2 (E1 ⊔♯ E2) (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_prog E1, sign_ast_prog E2 ⇒ sign_ast_prog (E1 ⊓♯ E2)
| sign_ast_add_1 E1 r1, sign_ast_add_1 E2 r2 ⇒ sign_ast_add_1 (E1 ⊓♯ E2) (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 E1 r1, sign_ast_asgn_1 E2 r2 ⇒ sign_ast_asgn_1 (E1 ⊓♯ E2) (r1 ⊓♯ r2)
| sign_ast_seq_1 r1, sign_ast_seq_1 r2 ⇒ sign_ast_seq_1 (r1 ⊓♯ r2)
| sign_ast_if_1 E1 r1, sign_ast_if_1 E2 r2 ⇒ sign_ast_if_1 (E1 ⊓♯ E2) (r1 ⊓♯ r2)
| sign_ast_while_1 r1, sign_ast_while_1 r2 ⇒ sign_ast_while_1 (r1 ⊓♯ r2)
| sign_ast_while_2 E1 r1, sign_ast_while_2 E2 r2 ⇒ sign_ast_while_2 (E1 ⊓♯ E2) (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 ];
(destruct (EquivDec.dec a a0); [| right; intro E; inverts¬ E ]);
(destruct (EquivDec.dec s s0); [| right; intro E; inverts¬ E ]);
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); splits; inverts E; apply¬ @PosetDec.refl.
introv O1 O2. destruct x; destruct y; try solve [ try inverts O1; inverts O2 ]; try exact I;
(split; forwards (O11&O12): (rm O1); forwards (O21&O22): (rm O2);
try (apply @PosetDec.antisym with (t := MapDefault.Poset _ _ _ _ _); auto~);
try (apply @PosetDec.antisym with (t := sign_ares_Poset); auto~);
try (apply @PosetDec.antisym with (t := Sign.Poset); auto~))
|| forwards¬ A: @PosetDec.antisym O1 O2.
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 ]);
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 ];
(destruct (PosetDec.dec a a0); [| right; intro E; inverts¬ E ]);
(destruct (PosetDec.dec s s0); [| right; intro E; inverts¬ E ]);
left; splits¬.
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 ]; try split;
try apply @JoinDec.bound1; try apply¬ @PosetDec.refl.
introv. destruct x; destruct y; try solve [ exact I ]; try 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; try split;
try solve [ simpls¬ ]; try apply¬ @JoinDec.least_upper_bound.
apply MeetDec.Make with (op := sign_ast_meet).
introv. destruct x; destruct y; try solve [ exact I ]; try split;
try apply @MeetDec.bound1; try apply¬ @PosetDec.refl.
introv. destruct x; destruct y; try solve [ exact I ]; try 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; try split;
try solve [ simpls¬ ]; apply¬ @MeetDec.greatest_lower_bound.
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 → ℘ sign_st := fun asigma sigma ⇒
match asigma, sigma with
| sign_ast_top, _ ⇒ True
| sign_ast_prog aE, sign_st_prog E ⇒ gamma_aEnv aE E
| sign_ast_add_1 aE ao, sign_st_add_1 E o ⇒ gamma_aEnv aE E ∧ sign_gamma_ares ao o
| sign_ast_add_2 av ao, sign_st_add_2 v o ⇒ gamma_aVal av v ∧ sign_gamma_ares ao o
| sign_ast_asgn_1 aE ao, sign_st_asgn_1 E o ⇒ gamma_aEnv aE E ∧ sign_gamma_ares ao o
| sign_ast_seq_1 ao, sign_st_seq_1 o ⇒ sign_gamma_ares ao o
| sign_ast_if_1 aE ao, sign_st_if_1 E o ⇒ gamma_aEnv aE E ∧ sign_gamma_ares ao o
| sign_ast_while_1 ao, sign_st_while_1 o ⇒ sign_gamma_ares ao o
| sign_ast_while_2 aE ao, sign_st_while_2 E o ⇒ gamma_aEnv aE E ∧ sign_gamma_ares ao o
| _, _ ⇒ False
end.
Global Instance sign_Gamma_ast : Gamma.t _ _ sign_gamma_ast.
Proof.
constructors.
introv O. destruct N1; destruct N2; tryfalse; simpls~; intros sigma G; tryfalse;
destruct sigma; tryfalse.
apply¬ (@Gamma.monotone _ _ _ _ gamma_aEnv _ _ _ O).
inverts G as GE Gr. inverts O as OE Or. splits.
apply¬ (@Gamma.monotone _ _ _ _ gamma_aEnv _ _ _ 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_aEnv _ _ _ OE).
apply¬ (@Gamma.monotone _ _ _ _ sign_gamma_ares _ _ _ Or).
apply¬ (@Gamma.monotone _ _ _ _ sign_gamma_ares _ _ _ O).
inverts G as GE Gr. inverts O as OE Or. splits.
apply¬ (@Gamma.monotone _ _ _ _ gamma_aEnv _ _ _ OE).
apply¬ (@Gamma.monotone _ _ _ _ sign_gamma_ares _ _ _ Or).
apply¬ (@Gamma.monotone _ _ _ _ sign_gamma_ares _ _ _ O).
inverts G as GE Gr. inverts O as OE Or. splits.
apply¬ (@Gamma.monotone _ _ _ _ gamma_aEnv _ _ _ OE).
apply¬ (@Gamma.monotone _ _ _ _ sign_gamma_ares _ _ _ Or).
introv. destruct N1; destruct N2; simpls~; intros sigma G; tryfalse;
destruct sigma; try solve [ false¬ G ]; try solve [ inverts¬ G ].
apply (@Gamma.meet_morph _ _ _ _ gamma_aEnv _ _ _ _). simpl. splits×.
inverts G as [GE1 Gr1] [GE2 Gr2]. splits.
apply (@Gamma.meet_morph _ _ _ _ gamma_aEnv _ _ _ _). simpl. splits×.
apply (@Gamma.meet_morph _ _ _ _ sign_gamma_ares _ _ _ _). simpl. splits×.
inverts G as [Gv1 Gr1] [Gv2 Gr2]. splits.
apply (@Gamma.meet_morph _ _ _ _ gamma_aVal _ _ _ _). simpl. splits×.
apply (@Gamma.meet_morph _ _ _ _ sign_gamma_ares _ _ _ _). simpl. splits×.
inverts G as [GE1 Gr1] [GE2 Gr2]. splits.
apply (@Gamma.meet_morph _ _ _ _ gamma_aEnv _ _ _ _). simpl. splits×.
apply (@Gamma.meet_morph _ _ _ _ sign_gamma_ares _ _ _ _). simpl. splits×.
inverts G as GE Gr.
apply (@Gamma.meet_morph _ _ _ _ sign_gamma_ares _ _ _ _). simpl. splits×.
inverts G as [GE1 Gr1] [GE2 Gr2]. splits.
apply (@Gamma.meet_morph _ _ _ _ gamma_aEnv _ _ _ _). simpl. splits×.
apply (@Gamma.meet_morph _ _ _ _ sign_gamma_ares _ _ _ _). simpl. splits×.
inverts G as GE Gr.
apply (@Gamma.meet_morph _ _ _ _ sign_gamma_ares _ _ _ _). simpl. splits×.
inverts G as [GE1 Gr1] [GE2 Gr2]. splits.
apply (@Gamma.meet_morph _ _ _ _ gamma_aEnv _ _ _ _). 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 : ∀ E r,
abort_ares r →
abort_ast (sign_ast_add_1 E r)
| abort_ast_add_2 : ∀ v r,
abort_ares r →
abort_ast (sign_ast_add_2 v r)
| abort_ast_asgn_1 : ∀ E r,
abort_ares r →
abort_ast (sign_ast_asgn_1 E r)
| abort_ast_seq_1 : ∀ r,
abort_ares r →
abort_ast (sign_ast_seq_1 r)
| abort_ast_if_1 : ∀ E r,
abort_ares r →
abort_ast (sign_ast_if_1 E r)
| abort_ast_while_1 : ∀ r,
abort_ares r →
abort_ast (sign_ast_while_1 r)
| abort_ast_while_2 : ∀ E r,
abort_ares r →
abort_ast (sign_ast_while_2 E 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_prog aE ⇒
True
| name_var x, sign_ast_prog aE ⇒
let av := read_env aE x in ¬ av =♯ (⊥♯) ∧ ¬ av =♯ aUndef
| name_varUndef x, sign_ast_prog aE ⇒
aUndef ⊑♯ read_env aE x
| name_add e1 e2, sign_ast_prog aE ⇒
True
| name_add_1 e2, sign_ast_add_1 aE ar ⇒
sign_ares_expr (⊥♯) ⊑♯ ar
| name_add_2, sign_ast_add_2 av ar ⇒
sign_ares_expr (⊥♯) ⊑♯ ar
| name_skip, sign_ast_prog aE ⇒
True
| name_throw, sign_ast_prog aE ⇒
True
| name_asgn x e, sign_ast_prog aE ⇒
True
| name_asgn_1 x, sign_ast_asgn_1 aE ar ⇒
sign_ares_expr (⊥♯) ⊑♯ ar
| name_seq s1 s2, sign_ast_prog aE ⇒
True
| name_seq_1 s2, sign_ast_seq_1 ar ⇒
sign_ares_stat (⊥♯) ⊑♯ ar
| name_if e s1 s2, sign_ast_prog aE ⇒
True
| name_if_1_true s1 s2, sign_ast_if_1 aE o ⇒
sign_ares_expr (Sign.pos, ⊥♯) ⊑♯ o ∨ sign_ares_expr (Sign.neg, ⊥♯) ⊑♯ o
| name_if_1_false s1 s2, sign_ast_if_1 aE o ⇒
sign_ares_expr (Sign.zero, ⊥♯) ⊑♯ o
| name_while e s, sign_ast_prog aE ⇒
True
| name_while_1 e s, sign_ast_while_1 ar ⇒
sign_ares_stat (⊥♯) ⊑♯ ar
| name_while_2_true e s, sign_ast_while_2 aE o ⇒
sign_ares_expr (Sign.pos, ⊥♯) ⊑♯ o ∨ sign_ares_expr (Sign.neg, ⊥♯) ⊑♯ o
| name_while_2_false e s, sign_ast_while_2 aE o ⇒
sign_ares_expr (Sign.zero, ⊥♯) ⊑♯ o
| _, _ ⇒
False
end.
| sign_ast_bot : sign_ast
.
Definition sign_ast_eq asigma1 asigma2 :=
match asigma1, asigma2 with
| sign_ast_prog E1, sign_ast_prog E2 ⇒ E1 =♯ E2
| sign_ast_add_1 E1 r1, sign_ast_add_1 E2 r2 ⇒ E1 =♯ E2 ∧ r1 =♯ r2
| sign_ast_add_2 v1 r1, sign_ast_add_2 v2 r2 ⇒ v1 =♯ v2 ∧ r1 =♯ r2
| sign_ast_asgn_1 E1 r1, sign_ast_asgn_1 E2 r2 ⇒ E1 =♯ E2 ∧ r1 =♯ r2
| sign_ast_seq_1 r1, sign_ast_seq_1 r2 ⇒ r1 =♯ r2
| sign_ast_if_1 E1 r1, sign_ast_if_1 E2 r2 ⇒ E1 =♯ E2 ∧ r1 =♯ r2
| sign_ast_while_1 r1, sign_ast_while_1 r2 ⇒ r1 =♯ r2
| sign_ast_while_2 E1 r1, sign_ast_while_2 E2 r2 ⇒ E1 =♯ E2 ∧ 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_prog E1, sign_ast_prog E2 ⇒ E1 ⊑♯ E2
| sign_ast_add_1 E1 r1, sign_ast_add_1 E2 r2 ⇒ E1 ⊑♯ E2 ∧ r1 ⊑♯ r2
| sign_ast_add_2 v1 r1, sign_ast_add_2 v2 r2 ⇒ v1 ⊑♯ v2 ∧ r1 ⊑♯ r2
| sign_ast_asgn_1 E1 r1, sign_ast_asgn_1 E2 r2 ⇒ E1 ⊑♯ E2 ∧ r1 ⊑♯ r2
| sign_ast_seq_1 r1, sign_ast_seq_1 r2 ⇒ r1 ⊑♯ r2
| sign_ast_if_1 E1 r1, sign_ast_if_1 E2 r2 ⇒ E1 ⊑♯ E2 ∧ r1 ⊑♯ r2
| sign_ast_while_1 r1, sign_ast_while_1 r2 ⇒ r1 ⊑♯ r2
| sign_ast_while_2 E1 r1, sign_ast_while_2 E2 r2 ⇒ E1 ⊑♯ E2 ∧ r1 ⊑♯ r2
| _, _ ⇒ False
end.
Definition sign_ast_join ar1 ar2 :=
match ar1, ar2 with
| sign_ast_bot, _ ⇒ ar2
| _, sign_ast_bot ⇒ ar1
| sign_ast_prog E1, sign_ast_prog E2 ⇒ sign_ast_prog (E1 ⊔♯ E2)
| sign_ast_add_1 E1 r1, sign_ast_add_1 E2 r2 ⇒ sign_ast_add_1 (E1 ⊔♯ E2) (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 E1 r1, sign_ast_asgn_1 E2 r2 ⇒ sign_ast_asgn_1 (E1 ⊔♯ E2) (r1 ⊔♯ r2)
| sign_ast_seq_1 r1, sign_ast_seq_1 r2 ⇒ sign_ast_seq_1 (r1 ⊔♯ r2)
| sign_ast_if_1 E1 r1, sign_ast_if_1 E2 r2 ⇒ sign_ast_if_1 (E1 ⊔♯ E2) (r1 ⊔♯ r2)
| sign_ast_while_1 r1, sign_ast_while_1 r2 ⇒ sign_ast_while_1 (r1 ⊔♯ r2)
| sign_ast_while_2 E1 r1, sign_ast_while_2 E2 r2 ⇒ sign_ast_while_2 (E1 ⊔♯ E2) (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_prog E1, sign_ast_prog E2 ⇒ sign_ast_prog (E1 ⊓♯ E2)
| sign_ast_add_1 E1 r1, sign_ast_add_1 E2 r2 ⇒ sign_ast_add_1 (E1 ⊓♯ E2) (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 E1 r1, sign_ast_asgn_1 E2 r2 ⇒ sign_ast_asgn_1 (E1 ⊓♯ E2) (r1 ⊓♯ r2)
| sign_ast_seq_1 r1, sign_ast_seq_1 r2 ⇒ sign_ast_seq_1 (r1 ⊓♯ r2)
| sign_ast_if_1 E1 r1, sign_ast_if_1 E2 r2 ⇒ sign_ast_if_1 (E1 ⊓♯ E2) (r1 ⊓♯ r2)
| sign_ast_while_1 r1, sign_ast_while_1 r2 ⇒ sign_ast_while_1 (r1 ⊓♯ r2)
| sign_ast_while_2 E1 r1, sign_ast_while_2 E2 r2 ⇒ sign_ast_while_2 (E1 ⊓♯ E2) (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 ];
(destruct (EquivDec.dec a a0); [| right; intro E; inverts¬ E ]);
(destruct (EquivDec.dec s s0); [| right; intro E; inverts¬ E ]);
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); splits; inverts E; apply¬ @PosetDec.refl.
introv O1 O2. destruct x; destruct y; try solve [ try inverts O1; inverts O2 ]; try exact I;
(split; forwards (O11&O12): (rm O1); forwards (O21&O22): (rm O2);
try (apply @PosetDec.antisym with (t := MapDefault.Poset _ _ _ _ _); auto~);
try (apply @PosetDec.antisym with (t := sign_ares_Poset); auto~);
try (apply @PosetDec.antisym with (t := Sign.Poset); auto~))
|| forwards¬ A: @PosetDec.antisym O1 O2.
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 ]);
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 ];
(destruct (PosetDec.dec a a0); [| right; intro E; inverts¬ E ]);
(destruct (PosetDec.dec s s0); [| right; intro E; inverts¬ E ]);
left; splits¬.
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 ]; try split;
try apply @JoinDec.bound1; try apply¬ @PosetDec.refl.
introv. destruct x; destruct y; try solve [ exact I ]; try 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; try split;
try solve [ simpls¬ ]; try apply¬ @JoinDec.least_upper_bound.
apply MeetDec.Make with (op := sign_ast_meet).
introv. destruct x; destruct y; try solve [ exact I ]; try split;
try apply @MeetDec.bound1; try apply¬ @PosetDec.refl.
introv. destruct x; destruct y; try solve [ exact I ]; try 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; try split;
try solve [ simpls¬ ]; apply¬ @MeetDec.greatest_lower_bound.
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 → ℘ sign_st := fun asigma sigma ⇒
match asigma, sigma with
| sign_ast_top, _ ⇒ True
| sign_ast_prog aE, sign_st_prog E ⇒ gamma_aEnv aE E
| sign_ast_add_1 aE ao, sign_st_add_1 E o ⇒ gamma_aEnv aE E ∧ sign_gamma_ares ao o
| sign_ast_add_2 av ao, sign_st_add_2 v o ⇒ gamma_aVal av v ∧ sign_gamma_ares ao o
| sign_ast_asgn_1 aE ao, sign_st_asgn_1 E o ⇒ gamma_aEnv aE E ∧ sign_gamma_ares ao o
| sign_ast_seq_1 ao, sign_st_seq_1 o ⇒ sign_gamma_ares ao o
| sign_ast_if_1 aE ao, sign_st_if_1 E o ⇒ gamma_aEnv aE E ∧ sign_gamma_ares ao o
| sign_ast_while_1 ao, sign_st_while_1 o ⇒ sign_gamma_ares ao o
| sign_ast_while_2 aE ao, sign_st_while_2 E o ⇒ gamma_aEnv aE E ∧ sign_gamma_ares ao o
| _, _ ⇒ False
end.
Global Instance sign_Gamma_ast : Gamma.t _ _ sign_gamma_ast.
Proof.
constructors.
introv O. destruct N1; destruct N2; tryfalse; simpls~; intros sigma G; tryfalse;
destruct sigma; tryfalse.
apply¬ (@Gamma.monotone _ _ _ _ gamma_aEnv _ _ _ O).
inverts G as GE Gr. inverts O as OE Or. splits.
apply¬ (@Gamma.monotone _ _ _ _ gamma_aEnv _ _ _ 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_aEnv _ _ _ OE).
apply¬ (@Gamma.monotone _ _ _ _ sign_gamma_ares _ _ _ Or).
apply¬ (@Gamma.monotone _ _ _ _ sign_gamma_ares _ _ _ O).
inverts G as GE Gr. inverts O as OE Or. splits.
apply¬ (@Gamma.monotone _ _ _ _ gamma_aEnv _ _ _ OE).
apply¬ (@Gamma.monotone _ _ _ _ sign_gamma_ares _ _ _ Or).
apply¬ (@Gamma.monotone _ _ _ _ sign_gamma_ares _ _ _ O).
inverts G as GE Gr. inverts O as OE Or. splits.
apply¬ (@Gamma.monotone _ _ _ _ gamma_aEnv _ _ _ OE).
apply¬ (@Gamma.monotone _ _ _ _ sign_gamma_ares _ _ _ Or).
introv. destruct N1; destruct N2; simpls~; intros sigma G; tryfalse;
destruct sigma; try solve [ false¬ G ]; try solve [ inverts¬ G ].
apply (@Gamma.meet_morph _ _ _ _ gamma_aEnv _ _ _ _). simpl. splits×.
inverts G as [GE1 Gr1] [GE2 Gr2]. splits.
apply (@Gamma.meet_morph _ _ _ _ gamma_aEnv _ _ _ _). simpl. splits×.
apply (@Gamma.meet_morph _ _ _ _ sign_gamma_ares _ _ _ _). simpl. splits×.
inverts G as [Gv1 Gr1] [Gv2 Gr2]. splits.
apply (@Gamma.meet_morph _ _ _ _ gamma_aVal _ _ _ _). simpl. splits×.
apply (@Gamma.meet_morph _ _ _ _ sign_gamma_ares _ _ _ _). simpl. splits×.
inverts G as [GE1 Gr1] [GE2 Gr2]. splits.
apply (@Gamma.meet_morph _ _ _ _ gamma_aEnv _ _ _ _). simpl. splits×.
apply (@Gamma.meet_morph _ _ _ _ sign_gamma_ares _ _ _ _). simpl. splits×.
inverts G as GE Gr.
apply (@Gamma.meet_morph _ _ _ _ sign_gamma_ares _ _ _ _). simpl. splits×.
inverts G as [GE1 Gr1] [GE2 Gr2]. splits.
apply (@Gamma.meet_morph _ _ _ _ gamma_aEnv _ _ _ _). simpl. splits×.
apply (@Gamma.meet_morph _ _ _ _ sign_gamma_ares _ _ _ _). simpl. splits×.
inverts G as GE Gr.
apply (@Gamma.meet_morph _ _ _ _ sign_gamma_ares _ _ _ _). simpl. splits×.
inverts G as [GE1 Gr1] [GE2 Gr2]. splits.
apply (@Gamma.meet_morph _ _ _ _ gamma_aEnv _ _ _ _). 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 : ∀ E r,
abort_ares r →
abort_ast (sign_ast_add_1 E r)
| abort_ast_add_2 : ∀ v r,
abort_ares r →
abort_ast (sign_ast_add_2 v r)
| abort_ast_asgn_1 : ∀ E r,
abort_ares r →
abort_ast (sign_ast_asgn_1 E r)
| abort_ast_seq_1 : ∀ r,
abort_ares r →
abort_ast (sign_ast_seq_1 r)
| abort_ast_if_1 : ∀ E r,
abort_ares r →
abort_ast (sign_ast_if_1 E r)
| abort_ast_while_1 : ∀ r,
abort_ares r →
abort_ast (sign_ast_while_1 r)
| abort_ast_while_2 : ∀ E r,
abort_ares r →
abort_ast (sign_ast_while_2 E 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_prog aE ⇒
True
| name_var x, sign_ast_prog aE ⇒
let av := read_env aE x in ¬ av =♯ (⊥♯) ∧ ¬ av =♯ aUndef
| name_varUndef x, sign_ast_prog aE ⇒
aUndef ⊑♯ read_env aE x
| name_add e1 e2, sign_ast_prog aE ⇒
True
| name_add_1 e2, sign_ast_add_1 aE ar ⇒
sign_ares_expr (⊥♯) ⊑♯ ar
| name_add_2, sign_ast_add_2 av ar ⇒
sign_ares_expr (⊥♯) ⊑♯ ar
| name_skip, sign_ast_prog aE ⇒
True
| name_throw, sign_ast_prog aE ⇒
True
| name_asgn x e, sign_ast_prog aE ⇒
True
| name_asgn_1 x, sign_ast_asgn_1 aE ar ⇒
sign_ares_expr (⊥♯) ⊑♯ ar
| name_seq s1 s2, sign_ast_prog aE ⇒
True
| name_seq_1 s2, sign_ast_seq_1 ar ⇒
sign_ares_stat (⊥♯) ⊑♯ ar
| name_if e s1 s2, sign_ast_prog aE ⇒
True
| name_if_1_true s1 s2, sign_ast_if_1 aE o ⇒
sign_ares_expr (Sign.pos, ⊥♯) ⊑♯ o ∨ sign_ares_expr (Sign.neg, ⊥♯) ⊑♯ o
| name_if_1_false s1 s2, sign_ast_if_1 aE o ⇒
sign_ares_expr (Sign.zero, ⊥♯) ⊑♯ o
| name_while e s, sign_ast_prog aE ⇒
True
| name_while_1 e s, sign_ast_while_1 ar ⇒
sign_ares_stat (⊥♯) ⊑♯ ar
| name_while_2_true e s, sign_ast_while_2 aE o ⇒
sign_ares_expr (Sign.pos, ⊥♯) ⊑♯ o ∨ sign_ares_expr (Sign.neg, ⊥♯) ⊑♯ o
| name_while_2_false e s, sign_ast_while_2 aE o ⇒
sign_ares_expr (Sign.zero, ⊥♯) ⊑♯ o
| _, _ ⇒
False
end.
Another definition of sign_acond as being the best abstraction of sign_cond.
Definition sign_acond_concr n asigma :=
∃ sigma,
sign_gamma_ast asigma sigma
∧ sign_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 →
sign_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 ].
forwards Gv: (rm G) 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.
forwards Gv: (rm G) 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. constructors×.
unfolds read_env. rewrite <- G1. constructors×.
false.
lets (o&?&Vo): (rm C). substs. lets (GE&Gr): (rm G).
destruct s0; tryfalse; constructors; simpls.
constructors.
rew_refl×.
lets (o&?&Vo): (rm C). substs. lets (GE&Gr): (rm G).
destruct s0; tryfalse.
destruct a0; tryfalse. split; simpl.
constructors.
rew_refl×.
auto×.
lets (o&?&Vo): (rm C). substs. lets (GE&Gr): (rm G).
destruct s0; tryfalse.
destruct a0; tryfalse. split; simpl.
constructors.
rew_refl×.
auto×.
lets (o&?&Vo): (rm C). substs. destruct s1; tryfalse.
destruct a; tryfalse. split; apply BotDec.prop.
auto×.
lets (o&D&Vo): (rm C). substs. inverts G as GE Gr. destruct s2; 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 Gr. destruct s2; tryfalse.
inverts Gr as Gv. constructors.
inverts Gv; tryfalse; try constructors. math.
simpl. rew_refl×.
auto×.
lets (o&?&Vo): (rm C). substs. destruct s1; tryfalse.
apply BotDec.prop.
auto×.
lets (o&D&Vo): (rm C). substs. inverts G as GE 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 Gr. destruct s1; tryfalse.
inverts Gr as Gv. constructors.
inverts Gv; tryfalse; try constructors. math.
simpl. 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) ].
forwards Ov: O v. fold (read_env a v) in Ov. fold (read_env a0 v) in Ov. lets (C1&C2): (rm C).
splits; destruct (read_env a v) as [()|]; destruct (read_env a0 v) as [()|];
inverts Ov as Ov; tryfalse; intro E; inverts E as E;
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×.
forwards Ov: O v. fold (read_env a v) in Ov. fold (read_env a0 v) in Ov.
exact (PosetDec.trans _ _ _ C Ov).
inverts O as O1 O2. exact (PosetDec.trans _ _ _ C O2).
inverts O as O1 O2. exact (PosetDec.trans _ _ _ C O2).
inverts O as O1 O2. exact (PosetDec.trans _ _ _ C O2).
exact (PosetDec.trans _ _ _ C O).
inverts C as C;[ left | right ]; inverts O as O1 O2; exact (PosetDec.trans _ _ _ C O2).
inverts O as O1 O2. exact (PosetDec.trans _ _ _ C O2).
exact (PosetDec.trans _ _ _ C O).
inverts C as C;[ left | right ]; inverts O as O1 O2; exact (PosetDec.trans _ _ _ C O2).
inverts O as O1 O2. exact (PosetDec.trans _ _ _ C O2).
Qed.
∃ sigma,
sign_gamma_ast asigma sigma
∧ sign_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 →
sign_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 ].
forwards Gv: (rm G) 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.
forwards Gv: (rm G) 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. constructors×.
unfolds read_env. rewrite <- G1. constructors×.
false.
lets (o&?&Vo): (rm C). substs. lets (GE&Gr): (rm G).
destruct s0; tryfalse; constructors; simpls.
constructors.
rew_refl×.
lets (o&?&Vo): (rm C). substs. lets (GE&Gr): (rm G).
destruct s0; tryfalse.
destruct a0; tryfalse. split; simpl.
constructors.
rew_refl×.
auto×.
lets (o&?&Vo): (rm C). substs. lets (GE&Gr): (rm G).
destruct s0; tryfalse.
destruct a0; tryfalse. split; simpl.
constructors.
rew_refl×.
auto×.
lets (o&?&Vo): (rm C). substs. destruct s1; tryfalse.
destruct a; tryfalse. split; apply BotDec.prop.
auto×.
lets (o&D&Vo): (rm C). substs. inverts G as GE Gr. destruct s2; 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 Gr. destruct s2; tryfalse.
inverts Gr as Gv. constructors.
inverts Gv; tryfalse; try constructors. math.
simpl. rew_refl×.
auto×.
lets (o&?&Vo): (rm C). substs. destruct s1; tryfalse.
apply BotDec.prop.
auto×.
lets (o&D&Vo): (rm C). substs. inverts G as GE 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 Gr. destruct s1; tryfalse.
inverts Gr as Gv. constructors.
inverts Gv; tryfalse; try constructors. math.
simpl. 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) ].
forwards Ov: O v. fold (read_env a v) in Ov. fold (read_env a0 v) in Ov. lets (C1&C2): (rm C).
splits; destruct (read_env a v) as [()|]; destruct (read_env a0 v) as [()|];
inverts Ov as Ov; tryfalse; intro E; inverts E as E;
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×.
forwards Ov: O v. fold (read_env a v) in Ov. fold (read_env a0 v) in Ov.
exact (PosetDec.trans _ _ _ C Ov).
inverts O as O1 O2. exact (PosetDec.trans _ _ _ C O2).
inverts O as O1 O2. exact (PosetDec.trans _ _ _ C O2).
inverts O as O1 O2. exact (PosetDec.trans _ _ _ C O2).
exact (PosetDec.trans _ _ _ C O).
inverts C as C;[ left | right ]; inverts O as O1 O2; exact (PosetDec.trans _ _ _ C O2).
inverts O as O1 O2. exact (PosetDec.trans _ _ _ C O2).
exact (PosetDec.trans _ _ _ C O).
inverts C as C;[ left | right ]; inverts O as O1 O2; exact (PosetDec.trans _ _ _ C O2).
inverts O as O1 O2. exact (PosetDec.trans _ _ _ C O2).
Qed.
Monads
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_prog A (f : _ → option A) asigma :=
match asigma with
| sign_ast_prog E ⇒ f E
| 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 ar ⇒ if_ares_stat f ar
| sign_ast_top ⇒ f (⊤♯) (⊤♯)
| _ ⇒ None
end.
Definition if_ast_if_1 A (f : _ → _ → _ → option A) asigma :=
match asigma with
| sign_ast_if_1 E ar ⇒ if_ares_expr (f E) ar
| sign_ast_top ⇒ f (⊤♯) (⊤♯) (⊤♯)
| _ ⇒ None
end.
Definition if_ast_while_1 A (f : _ → _ → option A) asigma :=
match asigma with
| sign_ast_while_1 ar ⇒ if_ares_stat f ar
| sign_ast_top ⇒ f (⊤♯) (⊤♯)
| _ ⇒ None
end.
Definition if_ast_while_2 A (f : _ → _ → _ → option A) asigma :=
match asigma with
| sign_ast_while_2 E ar ⇒ if_ares_expr (f E) 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_prog (fun E ⇒
Some (sign_ares_expr (get_value (read_env E x), ⊥♯))) 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_prog (fun E ⇒
Some (sign_ast_prog E)) in
let next E o :=
if_ast_prog (fun E ⇒
Some (sign_ast_add_1 E o)) E in
Rule_R2 up next
| name_add_1 e2 ⇒
let up :=
if_ast_add_1 (fun E av err ⇒
Some (sign_ast_prog 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_prog (fun E ⇒
Some (sign_ares_stat (E, ⊥♯))) in
Rule_Ax ax
| name_throw ⇒
let ax _ :=
Some (sign_ares_stat (⊥♯, ⊤♯)) in
Rule_Ax ax
| name_asgn x e ⇒
let up :=
if_ast_prog (fun E ⇒
Some (sign_ast_prog E)) in
let next E r :=
if_ast_prog (fun E ⇒
Some (sign_ast_asgn_1 E r)) E in
Rule_R2 up next
| name_asgn_1 x ⇒
let ax :=
if_ast_asgn_1 (fun E av err ⇒
Some (sign_ares_stat (write_env E x av, ⊥♯))) in
Rule_Ax ax
| name_seq s1 s2 ⇒
let up :=
if_ast_prog (fun E ⇒
Some (sign_ast_prog E)) in
let next E r :=
if_ast_prog (fun E ⇒
Some (sign_ast_seq_1 r)) E in
Rule_R2 up next
| name_seq_1 s2 ⇒
let up :=
if_ast_seq_1 (fun E err ⇒
Some (sign_ast_prog E)) in
Rule_R1 _ up
| name_if e s1 s2 ⇒
let up :=
if_ast_prog (fun E ⇒
Some (sign_ast_prog E)) in
let next E r :=
if_ast_prog (fun E ⇒
Some (sign_ast_if_1 E r)) E in
Rule_R2 up next
| name_if_1_true s1 s2 ⇒
let up :=
if_ast_if_1 (fun E av err ⇒
Some (sign_ast_prog E)) in
Rule_R1 _ up
| name_if_1_false s1 s2 ⇒
let up :=
if_ast_if_1 (fun E av err ⇒
Some (sign_ast_prog E)) in
Rule_R1 _ up
| name_while e s ⇒
let up :=
if_ast_prog (fun E ⇒
Some (sign_ast_while_1 (sign_ares_stat (E, ⊥♯)))) in
Rule_R1 _ up
| name_while_1 e s ⇒
let up :=
if_ast_while_1 (fun E err ⇒
Some (sign_ast_prog E)) in
let next asigma ar :=
if_ast_while_1 (fun E err ⇒
Some (sign_ast_while_2 E ar)) asigma in
Rule_R2 up next
| name_while_2_true e s ⇒
let up :=
if_ast_while_2 (fun E av err ⇒
Some (sign_ast_prog E)) in
let next asigma r :=
Some (sign_ast_while_1 r) in
Rule_R2 up next
| name_while_2_false e s ⇒
let ax :=
if_ast_while_2 (fun E av err ⇒
Some (sign_ares_stat (E, ⊥♯))) in
Rule_Ax ax
end.
Definition sign_asem :=
make_semantics sign_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 aC. simpls.
destruct n; destruct asigma as [aE|aE ar|aE ar|aE ar|ar|aE ar|ar|aE ar| |]; tryfalse;
try destruct ar as [[av ae]|[av ae]| |]; tryfalse; try solve [ destruct aC; tryfalse ];
try solve [ constructors; eexists; reflexivity ].
Qed.
Some lemmae for the propagation.
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_prog_out : ∀ A (f : _ → option A) sigma r,
if_st_prog f sigma = Some r →
∃ E, sigma = sign_st_prog E ∧ f E = 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) ∨
∃ E, sigma = sign_ast_prog E ∧ f E = 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 a_propagates : ∀ n,
propagates sign_asem sign_sem sign_gamma_ast sign_gamma_ares
(sign_arule n) (sign_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&Eq&E1a): if_st_prog_out (rm E1). substs.
forwards (va&Eq&E1b): option_map_out (rm E1a). substs.
forwards [(aEq&E2a)|(aE&aEq&E2a)]: if_ast_prog_out (rm E2); substs.
inverts_constr E2a. substs. unfolds.
constructors. unfolds read_env.
rewrite MapDefault.read_top. constructors.
inverts_constr E2a. substs. unfolds.
constructors. forwards¬ G': (rm G) 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. inverts E1. inverts E2. constructors. compute; auto×.
introv G E1 E2. forwards (E&Eq&E1a): if_st_prog_out (rm E1). substs. inverts E1a.
forwards [(aEq&E2a)|(aE&aEq&E2a)]: if_ast_prog_out (rm E2); substs.
inverts_constr E2a. substs. unfolds. apply gamma_aEnv_top.
inverts¬ E2a.
introv G1 G2 E1 E2. forwards (E&Eq&E1a): if_st_prog_out (rm E1). substs. inverts E1a.
forwards [(aEq&E2a)|(aE&aEq&E2a)]: if_ast_prog_out (rm E2); substs.
inverts_constr E2a. substs.
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.
unfolds. 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 (E&Eq&E1a): if_st_prog_out (rm E1). substs. inverts E1a.
forwards [(aEq&E2a)|(aE&aEq&E2a)]: if_ast_prog_out (rm E2); inverts_constr E2a; substs.
constructors. apply gamma_aEnv_top.
constructors. simpls¬.
introv G E1 E2. inverts E1. inverts E2. constructors. constructors.
introv G E1 E2. forwards (E&Eq&E1a): if_st_prog_out (rm E1). substs. inverts E1a.
forwards [(aEq&E2a)|(aE&aEq&E2a)]: if_ast_prog_out (rm E2); substs.
inverts_constr E2a. substs. unfolds. apply gamma_aEnv_top.
inverts¬ E2a.
introv G1 G2 E1 E2. forwards (E&Eq&E1a): if_st_prog_out (rm E1). substs. inverts E1a.
forwards [(aEq&E2a)|(aE&aEq&E2a)]: if_ast_prog_out (rm E2); substs.
inverts_constr E2a. substs.
splits¬. apply gamma_aEnv_top.
inverts¬ E2a. splits¬.
introv G E1 E2. destruct sigma as [| | |E r'| | | |]; tryfalse.
destruct r' as [[vr|]|]; inverts E1.
destruct asigma as [| | |aE ar'| | | | | |]; tryfalse.
destruct ar' as [[av ?]| | |]; inverts E2; lets (Ga&Gb): (rm G).
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. forwards (E&Eq&E1a): if_st_prog_out (rm E1). substs. inverts E1a.
forwards [(aEq&E2a)|(aE&aEq&E2a)]: if_ast_prog_out (rm E2); substs.
inverts_constr E2a. substs. constructors.
inverts¬ E2a.
introv G1 G2 E1 E2. forwards (E&Eq&E1a): if_st_prog_out (rm E1). substs. inverts E1a.
forwards [(aEq&E2a)|(aE&aEq&E2a)]: if_ast_prog_out (rm E2); substs.
inverts_constr E2a. substs¬.
inverts¬ E2a.
introv G E1 E2. destruct sigma as [| | | |r| | |]; tryfalse.
destruct r as [|[E|]]; inverts E1.
destruct asigma as [| | | |ar| | | | |]; tryfalse.
destruct ar as [|[aE ?]| |]; simpl in E2; inverts_constr E2; substs; inverts¬ G.
unfolds. apply gamma_aEnv_top.
simpl in E2. inverts_constr E2. substs. apply gamma_aEnv_top.
introv G E1 E2. forwards (E&Eq&E1a): if_st_prog_out (rm E1). substs. inverts E1a.
forwards [(aEq&E2a)|(aE&aEq&E2a)]: if_ast_prog_out (rm E2); substs.
inverts_constr E2a. substs. unfolds. apply gamma_aEnv_top.
inverts¬ E2a.
introv G1 G2 E1 E2. forwards (E&Eq&E1a): if_st_prog_out (rm E1). substs. inverts E1a.
forwards [(aEq&E2a)|(aE&aEq&E2a)]: if_ast_prog_out (rm E2); substs.
inverts_constr E2a. substs.
splits¬. apply gamma_aEnv_top.
inverts¬ E2a. splits¬.
introv G E1 E2. destruct sigma as [| | | | |E ?| |]; tryfalse. inverts E1.
destruct asigma as [| | | | |aE [[? ?]| | |]| | | |]; tryfalse;
simpl in E2; inverts_constr E2; substs; simpls*; apply gamma_aEnv_top.
introv G E1 E2. destruct sigma as [| | | | |E ?| |]; tryfalse. inverts E1.
destruct asigma as [| | | | |aE [[? ?]| | |]| | | |]; tryfalse;
simpl in E2; inverts_constr E2; substs; simpls*; apply gamma_aEnv_top.
introv G E1 E2. forwards (E&Eq&E1a): if_st_prog_out (rm E1). substs. inverts E1a.
forwards [(aEq&E2a)|(aE&aEq&E2a)]: if_ast_prog_out (rm E2); substs.
inverts_constr E2a. substs. constructors. apply gamma_aEnv_top.
inverts E2a. constructors¬.
introv G E1 E2. destruct sigma as [| | | | | |r|]; tryfalse.
destruct r as [|[E|]]; inverts E1.
destruct asigma as [| | | | | |ar| | |]; tryfalse.
destruct ar as [|[aE ?]| |]; simpl in E2; inverts_constr E2; substs; inverts¬ G.
unfolds. apply gamma_aEnv_top.
simpl in E2. inverts_constr E2. substs. unfolds. apply gamma_aEnv_top.
introv G1 G2 E1 E2. destruct sigma as [| | | | | |r'|]; tryfalse.
destruct r' as [|[E|]]; inverts E1.
destruct asigma as [| | | | | |ar'| | |]; tryfalse.
destruct ar' as [|[aE ?]| |]; simpl in E2; inverts_constr E2; substs; inverts G1; splits¬.
apply gamma_aEnv_top.
simpl in E2. inverts_constr E2. substs. splits¬. apply gamma_aEnv_top.
introv G E1 E2. destruct sigma as [| | | | | | |E ?]; tryfalse. inverts E1.
destruct asigma as [| | | | | | |aE [[? ?]| | |]| |]; tryfalse;
simpl in E2; inverts_constr E2; substs; simpls*; apply gamma_aEnv_top.
introv G1 G2 E1 E2. inverts E1. inverts E2. apply G2.
introv G E1 E2. destruct sigma as [| | | | | | |E ?]; tryfalse. inverts E1.
destruct asigma as [| | | | | | |aE [[? ?]| | |]| |]; tryfalse;
simpl in E2; inverts_constr E2; substs; simpls; constructors*; apply gamma_aEnv_top.
Qed.
Lemma sign_asem_correct : ∀ t asigma ar,
aeval sign_asem _ _ t asigma ar → ∀ sigma r,
sign_gamma_ast asigma sigma →
eval sign_sem t sigma r →
sign_gamma_ares ar r.
Proof.
introv aD G D.
eapply (correctness (sem := sign_sem) (asem := sign_asem) _ _ a_propagates); try typeclass.
apply sign_acond_correct.
Qed.
Lemma get_value_monotone : ∀ v1 v2,
v1 ⊑♯ v2 →
get_value v1 ⊑♯ get_value v2.
Proof. intros [[v1|]|] [[v2|]|] O; repeat (inverts O as O; auto~); constructors¬. Qed.
Lemma sign_arules_incr : ∀ n,
arules_incr _ _ _ (rule sign_asem n).
Proof.
introv. destruct n; simpl; constructors;
introv E1 E2 I; inverts E1 as E1; inverts E2 as E2; (try introv I'); auto~;
try forwards [(E1a&E1b)|(aE1&E1a&E1b)]: (if_ast_prog_out _ _ (rm E1));
try inverts E1a as E1a; try inverts E1b as E1b;
try forwards [(E2a&E2b)|(aE2&E2a&E2b)]: (if_ast_prog_out _ _ (rm E2));
try inverts E2a as E2a; try inverts E2b as E2b;
substs~; tryfalse; repeat constructors¬.
apply¬ get_value_monotone.
destruct asigma as [|aE [[av err]| | |]| | | | | | | |]; inverts E1;
destruct asigma' as [|aE' [[av' err']| | |]| | | | | | | |]; inverts E2;
tryfalse; inverts¬ I; constructors¬.
destruct asigma as [|aE [[av err]| | |]| | | | | | | |]; inverts E1;
destruct asigma' as [|aE' [[av' err']| | |]| | | | | | | |]; inverts E2;
tryfalse; constructors~; repeat inverts I as ? I; auto~; apply Sign.top_is_top.
destruct asigma as [| |av1 [[av2 err]| | |]| | | | | | |]; inverts E1;
destruct asigma' as [| |av1' [[av2' err']| | |]| | | | | | |]; inverts E2;
tryfalse; constructors~; repeat inverts I as ? I; auto~;
try apply¬ sem_add_monotone; apply¬ Sign.top_is_top.
unfolds if_ast_asgn_1. unfolds if_ares_expr.
destruct asigma as [| | |aE [[av err]| | |]| | | | | |]; inverts_constr E1;
destruct asigma' as [| | |aE' [[av' err']| | |]| | | | | |]; inverts_constr E2;
tryfalse; substs; constructors~; repeat inverts I as ? I;
unfolds write_env; apply¬ MapDefault.write_monotone;
constructors~; apply¬ Sign.top_is_top.
destruct asigma as [| | | |[|[aE err]| |]| | | | |]; inverts E1;
destruct asigma' as [| | | |[|[aE' err']| |]| | | | |]; inverts E2;
tryfalse; inverts¬ I; apply MapDefault.Top.
destruct asigma as [| | | | |aE [[av err]| | |]| | | |]; inverts E1;
destruct asigma' as [| | | | |aE' [[av' err']| | |]| | | |]; inverts E2;
tryfalse; inverts¬ I; apply MapDefault.Top.
destruct asigma as [| | | | |aE [[av err]| | |]| | | |]; inverts E1;
destruct asigma' as [| | | | |aE' [[av' err']| | |]| | | |]; inverts E2;
tryfalse; inverts¬ I; apply MapDefault.Top.
destruct asigma as [| | | | | |[|[aE err]| |]| | |]; inverts E1;
destruct asigma' as [| | | | | |[|[aE' err']| |]| | |]; inverts E2;
tryfalse; inverts¬ I; apply MapDefault.Top.
destruct asigma as [| | | | | |[|[aE err]| |]| | |]; inverts E1;
destruct asigma' as [| | | | | |[|[aE' err']| |]| | |]; inverts E2;
tryfalse; split; inverts¬ I; apply MapDefault.Top.
destruct asigma as [| | | | | | |aE [[av err]| | |]| |]; inverts E1;
destruct asigma' as [| | | | | | |aE' [[av' err']| | |]| |]; inverts E2;
tryfalse; inverts¬ I; apply MapDefault.Top.
destruct asigma as [| | | | | | |aE [[av err]| | |]| |]; inverts E1;
destruct asigma' as [| | | | | | |aE' [[av' err']| | |]| |]; inverts E2;
tryfalse; split; inverts¬ I; apply MapDefault.Top.
Qed.
Definition initial : aEnv := (aUndef, MapInterface.empty _).
Lemma prog_test1_aeffect :
aeval sign_asem _ _ prog_test1
(sign_ast_prog initial)
(sign_ares_stat (write_env initial "x"%string Sign.pos, ⊥♯)).
Proof.
apply aeval_cons. introv El C1. destruct n; simpl in × |-; inverts El.
constructors; try apply¬ @PosetDec.refl.
eapply aapply_step_R2; auto×.
apply aeval_cons. introv El C2. destruct n; simpl in × |-; inverts El.
constructors; try apply¬ @PosetDec.refl.
eapply aapply_step_Ax; auto×.
apply aeval_cons. introv El C2. destruct n; simpl in × |-; inverts El.
false. inverts C2 as C. inverts C as C; tryfalse. lets (Ca&Cb): (rm C).
forwards~: Cb Err.
constructors; try apply¬ @PosetDec.refl.
eapply aapply_step_Ax; auto×.
Qed.
End AbstractExample.