Commit b8db9790 authored by charguer's avatar charguer

lambda_wp_linear

parent b2ae7c5d
......@@ -3817,3 +3817,121 @@ Parameter hexists : forall A (J:A->hprop), hprop.
(* ---------------------------------------------------------------------- *)
(** Definition of substitution of a set of bindings *)
Section LinearWp.
Definition ctx := list (var*val).
Definition ctx_empty : ctx :=
nil.
Definition ctx_add (E:ctx) (x:var) (v:val) :=
(x,v)::E.
Fixpoint ctx_lookup (x:var) (E:ctx) : option val :=
match E with
| nil => None
| (y,v)::E' => if eq_var_dec x y
then Some v
else ctx_lookup x E'
end.
(*
Fixpoint ctx_subst (E:ctx) (t:trm) : trm :=
let aux t := subst E t in
match t with
| trm_val v => trm_val v
| trm_var x => match ctx_lookup x E with
| None => t
| Some v => trm_val v
end
| trm_fun x t1 => trm_fun x (aux_no_capture x t1)
| trm_fix f x t1 => trm_fix f x (if eq_var_dec f y then t1 else
aux_no_capture x t1)
| trm_if t0 t1 t2 => trm_if (aux t0) (aux t1) (aux t2)
| trm_seq t1 t2 => trm_seq (aux t1) (aux t2)
| trm_let x t1 t2 => trm_let x (aux t1) (aux_no_capture x t2)
| trm_app t1 t2 => trm_app (aux t1) (aux t2)
| trm_while t1 t2 => trm_while (aux t1) (aux t2)
| trm_for x t1 t2 t3 => trm_for x (aux t1) (aux t2) (aux_no_capture x t3)
end.
*)
Definition wp_def' wp (E:ctx) (t:trm) :=
let w := wp E in
match t with
| trm_val v => wp_val v
| trm_var x => match ctx_lookup x E with
| None => wp_fail
| Some v => wp_val v
end
| trm_fun x t1 => wp_val (val_fun x t1)
| trm_fix f x t1 => wp_val (val_fix f x t1)
| trm_if t0 t1 t2 => wp_if (w t0) (w t1) (w t2)
| trm_seq t1 t2 => wp_seq (w t1) (w t2)
| trm_let x t1 t2 => wp_let (w t1) (fun X => wp (ctx_add E x X) t2)
| trm_app t1 t2 => local (weakestpre (triple t))
| trm_while t1 t2 => wp_while (w t1) (w t2)
| trm_for x t1 t2 t3 => wp_for' (w t1) (w t2) (fun X => wp (ctx_add E x X) t3)
end.
Definition wp' := FixFun2 wp_def'.
(*
Lemma wp'_unfold_iter : forall n t,
wp' t = func_iter n wp_def' wp' t.
Proof using.
applys~ (FixFun_fix_iter (measure trm_size)). auto with wf.
intros f1 f2 t IH. unfold wp_def.
destruct t; try solve [ fequals~ | fequals~; applys~ fun_ext_1 ].
Qed.
*)
Hint Extern 1 (measure2 _ _ _) => simpl; math.
Lemma wp'_unfold : forall E t,
wp' E t = wp_def' wp' E t.
Proof using. (*applys (wp_unfold_iter 1). *)
applys~ (FixFun2_fix (measure2 (fun (E:ctx) (t:trm) => trm_size t))). auto with wf.
intros E t f1 f2 IH. unfold wp_def'. (* TODO inconsistent order of args with before *)
destruct t; try solve [ fequals~ | fequals~; applys~ fun_ext_1 ].
Qed.
(*
Lemma wp'_eq_wp_ind : forall E t,
wp' E t = wp (ctx_subst E t).
Proof using.
admit.
Qed.
*)
Lemma wp_eq_wp' :
wp = wp' ctx_empty.
Proof using.
admit.
Qed.
End LinearWp.
(*
Lemma ctx_subst_add_rem : forall E x v t,
ctx_subst (ctx_add x v (ctx_rem x E)) t
= ctx_subst (ctx_add x v E) t.
Proof using.
intros E. induction E as [|(y,w) E']; intros.
{ auto. }
{ simpl ctx_rem. unfold ctx_add. case_if.
{ subst y. admit. }
{ simpls. rewrite subst_subst_cross; [|auto]. apply IHE'. } }
Qed.
*)
\ No newline at end of file
This diff is collapsed.
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