Commit 14b96621 authored by charguer's avatar charguer

testvar_end_of_test

parent 5603c811
......@@ -365,6 +365,10 @@ Notation "'$' x" := (var_special x) (at level 6, format "'$' x").
Definition val_fun x t :=
val_fix (var_special "_") x (trm_unbind (var_special "_") t).
Lemma red_fun : forall m x t1,
red m (trm_fun x t1) m (val_fun x t1).
Proof using. intros. applys red_fun_encoded. applys red_fix. Qed.
Lemma red_app_fun : forall m1 m2 v1 v2 x t r,
v1 = val_fun x t ->
x <> var_special "_" ->
......@@ -768,10 +772,11 @@ Fixpoint trm_size (t:trm) : nat :=
| trm_fun x t1 => 1 + trm_size t1
| trm_fix f x t1 => 1 + trm_size t1
| 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 t1 t2 => 1 + trm_size t1 + trm_size t2
| trm_while t1 t2 => 1 + trm_size t1 + trm_size t2
| trm_for x t1 t2 t3 => 1 + trm_size t1 + trm_size t2 + trm_size t3
| trm_tag g t1 => 1 + trm_size t1
| trm_unbind x t1 => 1 + trm_size t1
end.
......@@ -808,7 +813,7 @@ Definition vars : Type := list var.
Fixpoint var_fresh (y:var) (xs:vars) : bool :=
match xs with
| nil => true
| x::xs' => if eq_var_dec x y then false else var_fresh y xs'
| x::xs' => if var_eq x y then false else var_fresh y xs'
end.
(** [var_distinct xs] asserts that [xs] consists of a list of distinct variables. *)
......@@ -844,7 +849,7 @@ Fixpoint ctx_rem (x:var) (E:ctx) : ctx :=
| nil => nil
| (y,v)::E' =>
let E'' := ctx_rem x E' in
if eq_var_dec x y then E'' else (y,v)::E''
if var_eq x y then E'' else (y,v)::E''
end.
(** [ctx_lookup x E] returns
......@@ -854,7 +859,7 @@ Fixpoint ctx_rem (x:var) (E:ctx) : ctx :=
Fixpoint ctx_lookup (x:var) (E:ctx) : option val :=
match E with
| nil => None
| (y,v)::E' => if eq_var_dec x y
| (y,v)::E' => if var_eq x y
then Some v
else ctx_lookup x E'
end.
......@@ -896,7 +901,7 @@ Lemma subst_substs_ctx_rem_same : forall E x v t,
Proof using.
intros E. induction E as [|(y,w) E']; simpl; intros.
{ auto. }
{ case_if.
{ rewrite var_eq_spec. case_if.
{ subst. rewrite IHE'. rewrite~ subst_subst_same. }
{ simpl. rewrite IHE'. rewrite~ subst_subst_neq. } }
Qed.
......@@ -919,11 +924,6 @@ Ltac substs_simpl_proof :=
intros E; induction E as [|(x,w) E' IH]; intros; simpl;
[ | try rewrite IH ]; auto.
Lemma substs_tag : forall E g t1,
substs E (trm_tag g t1)
= trm_tag g (substs E t1).
Proof using. substs_simpl_proof. Qed.
Lemma substs_unbind : forall E x t1,
substs E (trm_unbind x t1)
= trm_unbind x (substs (ctx_rem x E) t1).
......@@ -995,7 +995,7 @@ Proof using.
induction ys as [|y ys']; simpl; intros [|v vs] M L;
rew_list in *; try solve [ false; math ].
{ auto. }
{ simpl. do 2 case_if. rewrite~ IHys'. }
{ simpl. rewrite var_eq_spec in *. do 2 case_if. rewrite~ IHys'. }
Qed.
(* Permutation lemma for substitution and n-ary substitution *)
......@@ -1153,22 +1153,43 @@ Proof using.
{ case_if. rewrite~ IHxs'. }
Qed.
Lemma red_app_arg_l : forall m1 tf (v:val) x t m2 r,
red m1 tf m1 (val_fun x t) ->
red m1 ((val_fun x t) v) m2 r ->
red m1 (tf v) m2 r.
Proof using.
introv M1 M2. tests C: (trm_is_val tf).
{ destruct tf; tryfalse. inverts M1. applys M2. }
{ applys* red_app_arg M1. applys red_val. }
Qed.
(* todo move *)
Definition names := list name.
Coercion names_to_vars (xs:names) :=
List.map var_name xs.
Hint Resolve var_neq_of_var_eq.
Lemma red_app_funs_val_ind : forall xs vs m1 m2 tf t r,
red m1 tf m1 (val_funs xs t) ->
red m1 (substn xs vs t) m2 r ->
var_funs (length vs) xs ->
LibList.Forall (<> var_special "_") xs -> (* todo: executable version *)
red m1 (trm_apps tf vs) m2 r.
Proof using.
hint red_val.
intros xs. induction xs as [|x xs']; introv R M (N&L&P).
{ false. } clear P.
intros xs. induction xs as [|x xs']; introv R M (N&L&P) S.
{ false*. } clear P.
{ destruct vs as [|v vs']; rew_list in *. { false; math. }
simpls. tests C: (xs' = nil).
{ rew_list in *. asserts: (vs' = nil).
{ rew_list in *. inverts S as S1 _. asserts: (vs' = nil).
{ applys length_zero_inv. math. } subst vs'. clear L.
simpls. applys~ red_app_arg R. applys~ red_app_fun. }
{ rew_istrue in N. destruct N as [F N']. applys~ IHxs' M.
applys~ red_app_arg R. applys~ red_app_fun.
simpls. applys~ red_app_arg_l R. applys~ red_app_fun. }
{ rew_istrue in N. inverts S as S1 SN.
destruct N as [F N']. applys~ IHxs' M.
applys~ red_app_arg_l R. applys~ red_app_fun.
rewrite~ subst_trm_funs. applys~ red_funs. splits~. } }
Qed.
......@@ -1176,9 +1197,10 @@ Lemma red_app_funs_val : forall xs vs m1 m2 vf t r,
vf = val_funs xs t ->
red m1 (substn xs vs t) m2 r ->
var_funs (length vs) xs ->
LibList.Forall (<> var_special "_") xs -> (* todo: executable version *)
red m1 (trm_apps vf vs) m2 r.
Proof using.
introv R M N. applys* red_app_funs_val_ind.
introv R M N S. applys* red_app_funs_val_ind.
{ subst. apply~ red_val. }
Qed.
......@@ -1207,20 +1229,22 @@ Lemma red_app_fixs_val : forall xs vs m1 m2 vf f t r,
vf = val_fixs f xs t ->
red m1 (subst f vf (substn xs vs t)) m2 r ->
var_fixs f (length vs) xs ->
LibList.Forall (fun x => x <> f /\ x <> var_special "_") xs -> (* todo: executable version *)
red m1 (trm_apps vf vs) m2 r.
Proof using.
introv E M (N&L&P). destruct xs as [|x xs']. { false. }
introv E M (N&L&P) S. destruct xs as [|x xs']. { false. }
{ destruct vs as [|v vs']; rew_list in *. { false; math. } clear P.
simpls. case_if*. rew_istrue in *. destruct N as (N1&N2&N3).
tests C':(xs' = nil).
{ rew_list in *. asserts: (vs' = nil).
{ applys length_zero_inv. math. } subst vs'. clear L.
simpls. applys* red_app_fix. }
{ applys~ red_app_funs_val_ind.
{ inverts S as (S1&S1') SN. applys~ red_app_funs_val_ind.
{ applys* red_app_fix. do 2 rewrite~ subst_trm_funs. applys~ red_funs. }
{ rewrite~ subst_substn in M. { rewrite~ substn_cons in M.
rewrite~ subst_subst_neq. } { simpl. case_if~. } }
{ splits*. } } }
{ splits*. }
{ applys Forall_pred_incl SN. hnfs*. } } }
Qed.
......@@ -1329,13 +1353,13 @@ Proof using. intros. rew_nary. Abort.
Definition dummy_char := Ascii.ascii_of_nat 0%nat.
Fixpoint nat_to_var (n:nat) : var :=
Fixpoint nat_to_name (n:nat) : name :=
match n with
| O => String.EmptyString
| S n' => String.String dummy_char (nat_to_var n')
| S n' => String.String dummy_char (nat_to_name n')
end.
Lemma injective_nat_to_var : injective nat_to_var.
Lemma injective_nat_to_name : injective nat_to_name.
Proof using.
intros n. induction n as [|n']; intros m E; destruct m as [|m']; tryfalse.
{ auto. }
......@@ -1349,7 +1373,7 @@ Qed.
Fixpoint var_seq (start:nat) (nb:nat) : vars :=
match nb with
| O => nil
| S nb' => (nat_to_var start) :: var_seq (S start) nb'
| S nb' => (var_name (nat_to_name start)) :: var_seq (S start) nb'
end.
Section Var_seq.
......@@ -1357,23 +1381,25 @@ Implicit Types start nb : nat.
Lemma var_fresh_var_seq_lt : forall x start nb,
(x < start)%nat ->
var_fresh (nat_to_var x) (var_seq start nb).
var_fresh (nat_to_name x) (var_seq start nb).
Proof using.
intros. gen start. induction nb; intros.
{ auto. }
{ simpl. case_if.
{ lets: injective_nat_to_var C. math. }
{ rewrite name_eq_spec in C. rew_bool_eq in C.
lets: injective_nat_to_name C. math. }
{ applys IHnb. math. } }
Qed.
Lemma var_fresh_var_seq_ge : forall x start nb,
(x >= start+nb)%nat ->
var_fresh (nat_to_var x) (var_seq start nb).
var_fresh (nat_to_name x) (var_seq start nb).
Proof using.
intros. gen start. induction nb; intros.
{ auto. }
{ simpl. case_if.
{ lets: injective_nat_to_var C. math. }
{ rewrite name_eq_spec in C. rew_bool_eq in C.
lets: injective_nat_to_name C. math. }
{ applys IHnb. math. } }
Qed.
......@@ -1424,6 +1450,7 @@ Ltac fmap_red_base tt ::=
(* ** Tactic [var_neq] for proving two concrete variables distinct;
also registered as hint for [auto] *)
(*
Ltac var_neq :=
match goal with |- ?x <> ?y :> var =>
solve [ let E := fresh in
......@@ -1431,4 +1458,4 @@ Ltac var_neq :=
[ false | apply E ] ] end.
Hint Extern 1 (?x <> ?y) => var_neq.
*)
......@@ -538,16 +538,10 @@ Proof using.
exists h' v. splits~.
Qed.
Lemma rule_tag : forall g t1 H Q,
Lemma rule_unbind : forall x t1 H Q,
triple t1 H Q ->
triple (trm_tag g t1) H Q.
Proof using. introv M. applys rule_red M. applys red_tag. Qed.
Lemma rule_protect : forall x t1 H Q,
triple t1 H Q ->
triple (trm_protect x t1) H Q.
Proof using. introv M. applys rule_red M. applys red_protect. Qed.
triple (trm_unbind x t1) H Q.
Proof using. introv M. applys rule_red M. applys red_unbind. Qed.
Lemma rule_val : forall v H Q,
......@@ -608,7 +602,7 @@ Proof using.
{ intros v' N. hpull. intros E. inverts~ E. false N. hnfs*. }
Qed.
(* todo: deprecated *)
(* todo: deprecated
Lemma rule_seq_unit : forall t1 t2 H Q Q1,
triple t1 H Q1 ->
(forall v, ~ is_val_unit v -> (Q1 v) ==> \[False]) ->
......@@ -629,13 +623,15 @@ Proof using.
{ applys~ red_seq_unit R2. }
{ rewrite <- htop_hstar_htop. hhsimpl. }
Qed.
*)
Lemma rule_let : forall x t1 t2 H Q Q1,
Lemma rule_let_general : forall x t1 t2 H Q Q1,
x <> var_special "_" ->
triple t1 H Q1 ->
(forall (X:val), triple (subst x X t2) (Q1 X) Q) ->
triple (trm_let x t1 t2) H Q.
Proof using.
introv M1 M2. intros HF h N.
introv F M1 M2. intros HF h N.
lets~ (h1'&v1&R1&K1): (rm M1) HF h.
forwards* (h2'&v2&R2&K2): (rm M2) (\Top \* HF) h1'.
exists h2' v2. splits~.
......@@ -643,14 +639,22 @@ Proof using.
{ rewrite <- htop_hstar_htop. hhsimpl. }
Qed.
Lemma rule_let : forall (x:name) t1 t2 H Q Q1,
triple t1 H Q1 ->
(forall (X:val), triple (subst x X t2) (Q1 X) Q) ->
triple (trm_let x t1 t2) H Q.
Proof using. intros. applys* rule_let_general. auto. Qed.
Lemma rule_seq : forall t1 t2 H Q Q1,
triple t1 H Q1 ->
(forall (X:val), triple t2 (Q1 X) Q) ->
triple (trm_seq t1 t2) H Q.
Proof using.
introv M1 M2. unfold trm_seq. apply rule_tag. applys rule_let.
introv M1 M2. applys rule_red. applys red_seq_encoded.
applys rule_let_general.
{ auto. }
{ applys M1. }
{ simpl. intros. applys rule_protect. applys M2. }
{ simpl. intros. applys rule_unbind. applys M2. }
Qed.
Lemma rule_apps_funs : forall xs F (Vs:vals) t1 H Q,
......@@ -660,7 +664,7 @@ Lemma rule_apps_funs : forall xs F (Vs:vals) t1 H Q,
triple (trm_apps F Vs) H Q.
Proof using.
introv E N M. intros H' h Hf. forwards (h'&v&R&K): (rm M) Hf.
exists h' v. splits~. { subst. applys* red_app_funs_val. }
exists h' v. splits~. { subst. applys* red_app_funs_val. admit. (*todo side*) }
Qed.
Lemma rule_apps_fixs : forall xs f F (Vs:vals) t1 H Q,
......@@ -670,7 +674,7 @@ Lemma rule_apps_fixs : forall xs f F (Vs:vals) t1 H Q,
triple (trm_apps F Vs) H Q.
Proof using.
introv E N M. intros H' h Hf. forwards (h'&v&R&K): (rm M) Hf.
exists h' v. splits~. { subst. applys* red_app_fixs_val. }
exists h' v. splits~. { subst. applys* red_app_fixs_val. admit. (*todo side*) }
Qed.
......@@ -695,6 +699,18 @@ Proof using.
introv M. applys M. introv K. applys rule_while_raw. applys K.
Qed.
(* todo: investigate
Lemma rule_while' : forall t1 t2 H Q,
(forall t,
(forall H' Q', triple (trm_if t1 (trm_seq t2 t) val_unit) H' Q' ->
triple t H' Q') ->
triple t H Q) ->
triple (trm_while t1 t2) H Q.
Proof using.
introv M. applys rule_red.
Qed.
*)
Lemma rule_while_inv : forall (A:Type) (I:bool->A->hprop) (R:A->A->Prop) t1 t2 H,
let Q := (fun r => \[r = val_unit] \* Hexists Y, I false Y) in
wf R ->
......@@ -1057,6 +1073,7 @@ Qed.
(** Combination of [rule_let] and [rule_val] *)
(** todo fix
Lemma rule_let_val : forall x v1 t2 H Q,
(forall (X:val), X = v1 -> triple (subst x X t2) H Q) ->
triple (trm_let x (trm_val v1) t2) H Q.
......@@ -1066,6 +1083,7 @@ Proof using.
{ applys rule_val. hsimpl~. }
{ intros X. applys rule_extract_hprop. intro_subst. applys M'. }
Qed.
*)
(** A rule of conditionals with case analysis already done *)
......@@ -1099,7 +1117,7 @@ Proof using.
Qed.
(** An alternative statement for [rule_seq_unit] -- deprecated *)
(* todo fix
Lemma rule_seq_unit' : forall t1 t2 H Q H1,
triple t1 H (fun r => \[r = val_unit] \* H1) ->
triple t2 H1 Q ->
......@@ -1110,7 +1128,7 @@ Proof using.
{ intros v E. hpull; false. }
{ applys rule_extract_hprop. intros. applys M2. }
Qed.
*)
(* ---------------------------------------------------------------------- *)
(** Reformulation of the rule for N-ary functions *)
......
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