Commit 7ba728ec authored by charguer's avatar charguer

model_subst_progress

parent 32b11f4f
......@@ -24,7 +24,7 @@ Proof.
introv L M. rewrite L. intros m Hm.
exists (= m) \[] Q. splits~.
{ exists~ m state_empty. }
{ intros h. applys himpl_cancel_r. intros h' Hh'. applys~ hprop_gc_prove. }
{ intros h. applys himpl_cancel_r. intros h' Hh'. applys~ hprop_gc_intro. }
Qed.
Lemma cf_name : forall T (H:hprop) (Q:val->hprop),
......
......@@ -114,7 +114,7 @@ Hint Extern 1 (\# _ _ _) => state_disjoint_pre.
(*------------------------------------------------------------------*)
(* ** Properties of empty *)
Lemma hprop_empty_prove :
Lemma hprop_empty_intro :
\[] heap_empty.
Proof using. hnfs~. Qed.
......@@ -129,7 +129,7 @@ Proof using. auto. Qed.
Section Properties.
Hint Resolve hprop_empty_prove.
Hint Resolve hprop_empty_intro.
Lemma hprop_star_empty_l : forall H,
hprop_empty \* H = H.
......@@ -429,7 +429,7 @@ Definition triple' t H Q :=
Lemma triple_eq_triple' : triple = triple'.
Proof using.
hint hprop_gc_prove.
hint hprop_gc_intro.
applys prop_ext_3. intros t H Q.
unfold triple, triple'. iff M.
{ introv D P1.
......
......@@ -326,7 +326,7 @@ Ltac heap_eq :=
(*------------------------------------------------------------------*)
(* ** Properties of empty *)
Lemma hprop_empty_prove :
Lemma hprop_empty_intro :
\[] heap_empty.
Proof using. hnfs~. Qed.
......@@ -341,7 +341,7 @@ Proof using. auto. Qed.
Section Properties.
Hint Resolve hprop_empty_prove.
Hint Resolve hprop_empty_intro.
Lemma hprop_star_empty_l : forall H,
hprop_empty \* H = H.
......@@ -764,7 +764,7 @@ Definition triple'' t H Q :=
Lemma triple_eq_triple'' : triple = triple''.
Proof using.
hint hprop_gc_prove.
hint hprop_gc_intro.
applys prop_ext_3. intros t H Q.
rewrite triple_eq_triple'.
unfold triple', triple''. iff M.
......
......@@ -478,7 +478,7 @@ Qed.
(*------------------------------------------------------------------*)
(* ** Properties of empty *)
Lemma hprop_empty_prove :
Lemma hprop_empty_intro :
\[] heap_empty.
Proof using. hnfs~. Qed.
......@@ -493,7 +493,7 @@ Proof using. introv M. applys~ heap_eq. Qed.
Section Properties.
Hint Resolve hprop_empty_prove
Hint Resolve hprop_empty_intro
heap_compat_empty_l heap_compat_empty_r
heap_union_empty_l heap_union_empty_r.
......@@ -1136,7 +1136,7 @@ Proof using.
{ exists heap_empty h1. splits~.
{ applys~ heap_compat_empty_l. }
{ heap_eq. }
{ applys~ hprop_pure_prove. applys hprop_empty_prove. } }
{ applys~ hprop_pure_intro. applys hprop_empty_intro. } }
Qed.
Lemma rule_set : forall w l v,
......
......@@ -457,7 +457,7 @@ Tactic Notation "xif" :=
applys local_erase; unfold Cf_if;
try esplit; split; [ reflexivity | split ].
Lemma Cf_let_prove : forall A1 (EA1:id Enc A1) (Q1:A1->hprop) (F1 : formula) (F2of : forall A1 `{EA1:Enc A1}, A1 -> formula),
Lemma Cf_let_intro : forall A1 (EA1:id Enc A1) (Q1:A1->hprop) (F1 : formula) (F2of : forall A1 `{EA1:Enc A1}, A1 -> formula),
forall A (EA:id Enc A) H (Q:A->hprop),
F1 A1 EA1 H Q1 ->
(forall (X:A1), (@F2of A1 EA1 X) A EA (Q1 X) Q) ->
......@@ -465,7 +465,7 @@ Lemma Cf_let_prove : forall A1 (EA1:id Enc A1) (Q1:A1->hprop) (F1 : formula) (F2
Proof using. intros. hnf. exists A1 EA1 Q1. auto. Qed.
Tactic Notation "xlet" :=
applys local_erase; eapply @Cf_let_prove.
applys local_erase; eapply @Cf_let_intro.
(* TODO: why does not work?
applys local_erase;
let A := fresh "A" in let EA := fresh "E" A in
......
......@@ -141,15 +141,25 @@ Definition mlist_length : val :=
(** Helper for simplifying substitutions *)
Parameter mlist_length_closed : forall E,
subst_val E mlist_length = mlist_length.
(* todo: prove *)
Lemma mlist_length_closed :
closed_val mlist_length.
Proof using. reflexivity. Qed.
Hint Rewrite mlist_length_closed : rew_subst.
Lemma subst_val_mlist_length : forall E,
subst_val E mlist_length = mlist_length.
Proof using. intros. applys subst_val_closed. applys mlist_length_closed. Qed.
Ltac simpl_subst := simpl; autorewrite with rew_subst.
Hint Rewrite subst_val_mlist_length : rew_subst.
(* short version to avoid stating the two lemmas above:
Lemma subst_val_closed' : forall v, closed_val v -> forall E,
subst_val E v = v.
Proof using. intros. applys subst_val_closed. Qed.
Hint Rewrite (@subst_val_closed' mlist_length (refl_equal _)) : rew_subst.
*)
Ltac simpl_subst :=
simpl; autorewrite with rew_subst.
(** Temporary auxiliary specification *)
......
......@@ -99,37 +99,79 @@ Coercion trm_app : val >-> Funclass.
(*------------------------------------------------------------------*)
(** Definition of capture-avoiding substitution *)
(** Computable version of list operations *)
Section Lists.
Fixpoint list_mem (y:var) (L:vars) :=
match L with
| nil => false
| x::L' => if eq_var_dec x y then true else list_mem y L'
end.
(** Remove [L] from [L'] *)
Fixpoint list_remove (L:vars) (L':vars) : vars :=
match L' with
| nil => nil
| x::Q => let Q' := list_remove L Q in
if list_mem x L then Q' else x::Q'
end.
Fixpoint list_app (L:vars) (L':vars) : vars :=
match L with
| nil => L'
| x::Q => x::(list_app Q L')
end.
Local Infix "++" := list_app.
Fixpoint list_concat (Ls:list vars) : vars :=
match Ls with
| nil => nil
| L::Ls' => L ++ (list_concat Ls')
end.
End Lists.
Infix "++" := list_app : vars_scope.
(*------------------------------------------------------------------*)
(** Computable version of association list operations *)
Definition ctx := list (var*val).
Fixpoint ctx_lookup (y : var) (E : ctx) : option val :=
Fixpoint ctx_lookup (y:var) (E:ctx) : option val :=
match E with
| nil => None
| (x,v)::E' => if eq_var_dec x y then Some v else ctx_lookup y E'
end.
Fixpoint list_mem (y : var) (L : vars) :=
match L with
| nil => false
| x::L' => if eq_var_dec x y then true else list_mem y L'
end.
Fixpoint ctx_remove (L : list var) (E : ctx) : ctx :=
Fixpoint ctx_remove (L:vars) (E:ctx) : ctx :=
match E with
| nil => nil
| (x,v)::E' => let E'' := ctx_remove L E' in
if list_mem x L then E'' else (x,v)::E''
end.
Fixpoint subst_val E (v : val) : val :=
(*------------------------------------------------------------------*)
(** Definition of capture-avoiding substitution *)
Fixpoint subst_val (E:ctx) (v:val) : val :=
match v with
| val_var x => match ctx_lookup x E with None => v | Some w => w end
| val_fix f xs t => let E' := ctx_remove (f::xs) E in val_fix f xs (subst_trm E' t)
| val_var x =>
match ctx_lookup x E with
| None => v
| Some w => w
end
| val_fix f xs t =>
let E' := ctx_remove (f::xs) E in
val_fix f xs (subst_trm E' t)
| _ => v
end
with subst_trm (E : ctx) (t : trm) : trm :=
with subst_trm (E:ctx) (t:trm) : trm :=
match t with
| trm_val v => trm_val (subst_val E v)
| trm_if t0 t1 t2 => trm_if (subst_trm E t0) (subst_trm E t1) (subst_trm E t2)
......@@ -140,6 +182,109 @@ with subst_trm (E : ctx) (t : trm) : trm :=
end.
(*------------------------------------------------------------------*)
(** Free variables *)
Section Freevars.
Open Scope vars_scope.
Fixpoint freevars_val (v:val) : vars :=
match v with
| val_var x => x::nil
| val_fix f xs t => list_remove (f::xs) (freevars_trm t)
| _ => nil
end
with freevars_trm (t:trm) : vars :=
match t with
| trm_val v => freevars_val v
| trm_if t0 t1 t2 => freevars_trm t0 ++ freevars_trm t1 ++ freevars_trm t2
| trm_seq t1 t2 => freevars_trm t1 ++ freevars_trm t2
| trm_let x t1 t2 => freevars_trm t1 ++ (list_remove (x::nil) (freevars_trm t2))
| trm_app v1 v2s => freevars_val v1 ++ list_concat (List.map freevars_val v2s)
| trm_while t1 t2 => freevars_trm t1 ++ freevars_trm t2
end.
End Freevars.
Definition closed_val (v:val) :=
freevars_val v = nil.
Definition closed_trm (t:trm) :=
freevars_trm t = nil.
Fixpoint val_size (v:val) : nat :=
match v with
| val_fix f xs t => 1 + trm_size t
| _ => 1
end
with trm_size (t:trm) : nat :=
match t with
| trm_val v => val_size v
| trm_if t0 t1 t2 => 1 + trm_size t0 + trm_size t1 + trm_size t2
| trm_seq t1 t2 => 1 + trm_size t1 + trm_size t2
| trm_let x t1 t2 => 1 + trm_size t1 + trm_size t2
| trm_app v1 v2s => 1 + val_size v1 + (List.fold_right (fun v n => (n + val_size v)%nat) O v2s)
| trm_while t1 t2 => 1 + trm_size t1 + trm_size t2
end.
Ltac simpl_meas :=
match goal with |- measure _ _ _ => hnf; simpl; math end.
Ltac simpl_IH :=
simpl;
match goal with H: context [subst_trm _ _ = _] |- _ =>
repeat rewrite H;
try simpl_meas end;
try fequals.
Lemma ctx_lookup_remove : forall x L E,
ctx_lookup x E = None ->
ctx_lookup x (ctx_remove L E) = None.
Proof using.
intros. induction E as [| [a v] E']; simpls.
{ auto. }
{ do 2 case_if. { applys* IHE'. } { simpl. case_if. applys* IHE'. } }
Qed.
(* todo: mixed induction with subst_val *)
Lemma subst_trm_closed_ind : forall E t,
(forall x, list_mem x (freevars_trm t) -> ctx_lookup x E = None) ->
subst_trm E t = t.
Proof using.
intros E t. gen E. induction_wf IH: trm_size t.
introv N. destruct t; simpls.
{ destruct v; simpls; auto.
{ specializes N v. destruct (ctx_lookup v E). { false* N. case_if~. } { auto. } }
{ do 2 fequals. simpl_IH. intros x K. tests: (list_mem x (v::v0)).
{ admit. }
{ applys ctx_lookup_remove.
(* skip_rewrite (ctx_lookup x (ctx_remove (v :: v0) E) = ctx_lookup x E). *)
applys* N. admit. (* list_mem_remove *) } } }
{ skip. }
{ simpl_IH.
{ introv K. applys N. skip. } (* list_mem_app *)
{ introv K. applys N. skip. } (* list_mem_app *) }
{ skip. }
{ skip. }
{ skip. }
Qed.
(* TODO: rename remove to removes *)
(* TODO: ListExec library *)
Axiom subst_val_closed : forall E v,
closed_val v ->
subst_val E v = v.
Lemma subst_trm_closed : forall E t,
closed_trm t ->
subst_trm E t = t.
Proof using.
introv N. applys subst_trm_closed_ind. rewrite N. auto_false.
Qed.
(************************************************************)
(* * Source language semantics *)
......
......@@ -109,7 +109,7 @@ Hint Extern 1 (\# _ _ _) => state_disjoint_pre.
(*------------------------------------------------------------------*)
(* ** Properties of empty *)
Lemma hprop_empty_prove :
Lemma hprop_empty_intro :
\[] heap_empty.
Proof using. hnfs~. Qed.
......@@ -124,7 +124,7 @@ Proof using. auto. Qed.
Section Properties.
Hint Resolve hprop_empty_prove.
Hint Resolve hprop_empty_intro.
Lemma hprop_star_empty_l : forall H,
hprop_empty \* H = H.
......@@ -210,8 +210,8 @@ Lemma hprop_single_not_null : forall (l:loc) (f:field) (v:val),
(l `.` f ~> v) ==> (l `.` f ~> v) \* \[l <> null].
Proof using.
intros. unfold hprop_single. intros h (Hh&Nl).
exists h heap_empty. splits~. applys~ hprop_pure_prove.
applys~ hprop_empty_prove.
exists h heap_empty. splits~. applys~ hprop_pure_intro.
applys~ hprop_empty_intro.
Qed.
Implicit Arguments hprop_single_not_null [].
......
......@@ -271,7 +271,7 @@ Proof using.
iff (p&M) (p&M). { split~. } { exists~ p. }
Qed.
Lemma hprop_pure_prove : forall (P:Prop) h,
Lemma hprop_pure_intro : forall (P:Prop) h,
\[] h ->
P ->
\[P] h.
......@@ -292,7 +292,7 @@ Lemma hprop_empty_def :
\[] = \[True].
Proof using.
applys prop_ext_1. intros h. iff M.
{ applys* hprop_pure_prove. }
{ applys* hprop_pure_intro. }
{ forwards*: hprop_pure_inv M. }
Qed.
......@@ -300,7 +300,7 @@ Lemma hprop_pure_def : forall (P:Prop),
\[P] = (Hexists (p:P), \[]).
Proof using. auto. Qed.
Lemma hprop_gc_prove : forall h,
Lemma hprop_gc_intro : forall h,
\GC h.
Proof using. intros. exists~ (=h). Qed.
......@@ -1482,7 +1482,7 @@ Qed.
(** A introduction rule to establish [is_local] *)
Lemma is_local_prove : forall B (F:~~B),
Lemma is_local_intro : forall B (F:~~B),
(forall H Q, F H Q <-> local F H Q) -> is_local F.
Proof using.
intros. unfold is_local. apply func_ext_2.
......
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