Commit 4cb81bd7 authored by charguer's avatar charguer

encoding

parent b5fe6d16
......@@ -691,7 +691,7 @@ Proof using.
rewrite heap_union_empty_r. applys* M.
Qed.
Lemma rule_extract_exists : forall t (J:val->hprop) Q,
Lemma rule_extract_exists : forall t A (J:A->hprop) Q,
(forall x, triple t (J x) Q) ->
triple t (hprop_exists J) Q.
Proof using. introv M D (x&Jx). applys* M. Qed.
......
......@@ -880,7 +880,7 @@ Proof using.
rew_heap in R2. subst h12. applys* M.
Qed.
Lemma rule_extract_exists : forall t (J:val->hprop) Q,
Lemma rule_extract_exists : forall t A (J:A->hprop) Q,
(forall x, triple t (J x) Q) ->
triple t (hprop_exists J) Q.
Proof using. introv M D (x&Jx). applys* M. Qed.
......
......@@ -330,7 +330,7 @@ Proof using.
subst h22 h1. rewrite heap_union_empty_r. applys* M.
Qed.
Lemma rule_extract_exists : forall t (J:val->hprop) Q,
Lemma rule_extract_exists : forall t A (J:A->hprop) Q,
(forall x, triple t (J x) Q) ->
triple t (hprop_exists J) Q.
Proof using. introv M D (x&Jx). applys* M. Qed.
......@@ -543,7 +543,7 @@ Proof using.
subst h22 h1. rewrite heap_union_empty_r. applys* M.
Qed.
Lemma rule_extract_exists : forall t (J:val->hprop) Q,
Lemma rule_extract_exists : forall t (A:Type) (J:A->hprop) Q,
(forall x, triple t (J x) Q) ->
triple t (hprop_exists J) Q.
Proof using. introv M D (x&Jx). applys* M. Qed.
......@@ -690,3 +690,171 @@ Qed.
End TripleWithGC.
(********************************************************************)
(********************************************************************)
(********************************************************************)
(** * Triples with lifting *)
Module TripleWithGCAndLifting.
Import TripleWithGC.
Generalizable Variables A B.
Definition func := val.
Class Enc (A:Type) :=
make_Enc { enc : A -> val }.
Instance Enc_int : Enc int.
Proof using. constructor. applys val_int. Defined.
Instance Enc_func : Enc func.
Proof using. constructor. applys (fun x:func => x). Defined.
Definition Subst_trm (x:var) `{Enc A} (X:A) (t:trm) : trm :=
subst_trm x (enc X) t.
Definition PostEnc `{Enc A} (Q:A->hprop) : val->hprop :=
fun v => Hexists V, \[v = enc V] \* Q V.
Definition Triple (t:trm) (H:hprop) `{EA:Enc A} (Q:A->hprop) :=
triple t H (PostEnc Q).
Lemma Rule_val : forall `{EA:Enc A} (V:A) v H (Q:A->hprop),
v = enc V ->
H ==> Q V ->
Triple (trm_val v) H Q.
Proof using.
introv E M. applys rule_val.
unfold PostEnc. subst.
applys himpl_inst_exists V.
applys~ himpl_inst_prop.
Qed.
Lemma Rule_if : forall (V:int) v t1 t2 H `{EA:Enc A} (Q:A->hprop),
v = enc V ->
Triple (If V = 0 then t2 else t1) H Q ->
Triple (trm_if v t1 t2) H Q.
Proof using.
introv E M. applys rule_if. subst.
applys_eq (rm M) 3. tests: (V = 0); simpl; case_if~.
Qed.
Lemma Rule_let : forall x t1 t2 H,
forall `{EA:Enc A} (Q:A->hprop) `{EA1:Enc A1} (Q1:A1->hprop),
Triple t1 H Q1 ->
(forall (X:A1), Triple (Subst_trm x X t2) (Q1 X) Q) ->
Triple (trm_let x t1 t2) H Q.
Proof using.
introv M1 M2. applys rule_let M1.
intros v. unfold PostEnc.
applys rule_extract_exists. intros V.
rewrite hprop_star_comm. applys rule_extract_prop.
introv E. subst. applys M2.
(* TODO: why notation for hprop_exists shows hexists? *)
Qed.
Lemma Rule_let_val_enc : forall `{Enc A1} (V1:A1) x v1 t2 H A `{EA: Enc A} (Q:A->hprop),
v1 = enc V1 ->
(forall X, X = V1 -> Triple (Subst_trm x X t2) H Q) ->
Triple (trm_let x (trm_val v1) t2) H Q.
Proof using.
introv E M. applys rule_let_val. intros X EX. subst. applys~ M.
Qed.
(*
Lemma Rule_let_val : forall x v1 t2 H A `{EA: Enc A} (Q:A->hprop),
(forall `{Enc A1} (X:A1), v1 = enc X -> Triple (Subst_trm x X t2) H Q) ->
Triple (trm_let x (trm_val v1) t2) H Q.
=> true by exploiting the fact that every value is the encoding of another.
*)
Lemma Rule_app : forall f x (F:func) V t1 H A `{EA:Enc A} (Q:A->hprop),
F = (val_fix f x t1) ->
Triple (subst_trm f F (subst_trm x V t1)) H Q ->
Triple (trm_app F V) H Q.
Proof using.
introv EF M. applys* rule_app.
Qed.
Lemma enc_val_fix_eq : forall F f x t1,
F = val_fix f x t1 ->
enc F = F.
Proof using. intros. subst~. Qed.
Lemma Rule_let_fix : forall f x t1 t2 H A `{EA:Enc A} (Q:A->hprop),
(forall (F:func),
(forall `{EA1:Enc A1} `{EA2:Enc A2} (X:A1) H' (Q':A2->hprop),
Triple (Subst_trm f F (Subst_trm x X t1)) H' Q' ->
Triple (trm_app F (enc X)) H' Q') ->
Triple (Subst_trm f F t2) H Q) ->
Triple (trm_let f (trm_val (val_fix f x t1)) t2) H Q.
Proof using.
introv M. applys (@Rule_let_val_enc _ _ (val_fix f x t1)).
{ symmetry. applys* enc_val_fix_eq. }
intros F EF. applys (rm M). clears H Q.
intros A2 EA2 A3 EA3 X H Q M.
applys~ Rule_app EF.
Qed.
Definition hprop_single_enc `{EA:Enc A} r V :=
hprop_single r (enc V).
Notation "r '~~~>' V" := (hprop_single_enc r V)
(at level 32, no associativity) : heap_scope.
Instance Enc_loc : Enc loc.
Proof using. constructor. applys val_loc. Defined.
Lemma Rule_new : forall `{EA:Enc A} (V:A) v,
v = enc V ->
Triple (trm_new v) \[] (fun l => l ~~~> V).
Proof using.
introv E. applys_eq rule_new 1. subst~.
Qed.
Lemma Rule_get : forall `{EA:Enc A} (V:A) l,
Triple (trm_get (val_loc l)) (l ~~~> V) (fun x => \[x = V] \* (l ~~~> V)).
Proof using.
introv. applys rule_consequence. { auto. } { applys rule_get. }
{ intros v. unfold PostEnc.
applys himpl_extract_prop. intro_subst.
applys himpl_inst_exists V.
applys~ himpl_inst_prop.
applys~ himpl_inst_prop. }
Qed.
Instance Enc_unit : Enc unit.
Proof using. constructor. applys (fun x:unit => val_unit). Defined.
Lemma Rule_set : forall `{EA1:Enc A1} (V1:A1) `{EA2:Enc A2} (V2:A2) l v2,
v2 = enc V2 ->
Triple (trm_set (val_loc l) v2) (l ~~~> V1) (fun (r:unit) => l ~~~> V2).
Proof using.
introv E. applys rule_consequence. { auto. } { applys rule_set. }
{ subst. intros v. unfold PostEnc.
applys himpl_extract_prop. intro_subst.
applys himpl_inst_exists tt.
applys~ himpl_inst_prop. }
Qed.
End TripleWithGCAndLifting.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment