Commit 5603c811 authored by charguer's avatar charguer

special_vars_constr

parent 0169d014
......@@ -34,14 +34,17 @@ Open Scope string_scope.
(* ---------------------------------------------------------------------- *)
(** Representation of variables and locations *)
Definition var := string.
Definition name := string.
Inductive var :=
| var_name : name -> var
| var_special : name -> var.
Definition loc := nat.
Definition null : loc := 0%nat.
Definition field := nat.
Definition eq_var_dec := String.string_dec.
Global Opaque field var loc.
Global Opaque field name loc.
(* ---------------------------------------------------------------------- *)
......@@ -95,33 +98,64 @@ Coercion val_loc : loc >-> val.
Coercion trm_val : val >-> trm.
Coercion trm_var : var >-> trm.
Coercion trm_app : trm >-> Funclass.
Coercion var_name : name >-> var.
(* ---------------------------------------------------------------------- *)
(** Encoded constructs *)
(*
Definition var_special (x:var) : bool :=
match x with
| String h _ => if Ascii.ascii_dec h "$" then true else false
| _ => false
end.
*)
Definition eq_name_dec := String.string_dec.
(** A special variable is always distinct from a non-special one *)
Definition name_eq (x y:name) :=
if eq_name_dec x y then true else false.
Lemma var_neq_of_special : forall x y,
var_special x = false ->
var_special y = true ->
Lemma var_neq_of_name_dec : forall x y,
name_eq x y = false ->
x <> y.
Proof using. introv E1 E2 N. unfolds var_special.
destruct x as [|x1 xs]; destruct y as [|y1 ys]; inverts N; try false.
Qed.
Proof using. unfolds name_eq. introv M. case_if~. Qed.
(** Computable comparison of two distinct variables. *)
Definition var_eq (x y:var) :=
match x, y with
| var_name a, var_name b => name_eq a b
| var_special a, var_special b => name_eq a b
| _, _ => false
end.
Lemma var_neq_of_string_dec : forall x y,
(if string_dec x y then true else false) = false ->
Lemma var_neq_of_var_eq : forall x y,
var_eq x y = false ->
x <> y.
Proof using. introv M. case_if~. Qed.
Proof using.
introv M N. unfolds var_eq.
destruct x as [a|a]; destruct y as [b|b]; inverts N;
try applys* var_neq_of_name_dec.
Qed.
(* todo: use decide *)
Lemma name_eq_spec : forall (x y:name),
name_eq x y = isTrue (x = y).
Proof using.
intros. unfold name_eq. case_if; rew_bool_eq~.
Qed.
Lemma var_eq_spec : forall (x y:var),
var_eq x y = isTrue (x = y).
Proof using.
intros. unfold var_eq. destruct x as [a|a]; destruct y as [b|b];
try rewrite name_eq_spec; rew_bool_eq.
{ iff M; inverts* M. }
{ introv M; inverts* M. }
{ introv M; inverts* M. }
{ iff M; inverts* M. }
Qed.
(* ********************************************************************** *)
......@@ -132,12 +166,12 @@ Proof using. introv M. case_if~. Qed.
Fixpoint subst (y:var) (w:val) (t:trm) : trm :=
let aux t := subst y w t in
let aux_unbind x t := if eq_var_dec x y then t else aux t in
let aux_unbind x t := if var_eq x y then t else aux t in
match t with
| trm_val v => trm_val v
| trm_var x => if eq_var_dec x y then trm_val w else t
| trm_var x => if var_eq x y then trm_val w else t
| trm_fun x t1 => trm_fun x (aux_unbind x t1)
| trm_fix f x t1 => trm_fix f x (if eq_var_dec f y then t1 else
| trm_fix f x t1 => trm_fix f x (if var_eq f y then t1 else
aux_unbind 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)
......@@ -145,7 +179,7 @@ Fixpoint subst (y:var) (w:val) (t:trm) : trm :=
| 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_unbind x t3)
| trm_unbind x t1 => if eq_var_dec x y then t else trm_unbind x (aux t1)
| trm_unbind x t1 => if var_eq x y then t else trm_unbind x (aux t1)
end.
......@@ -160,7 +194,8 @@ Lemma subst_subst_neq : forall x1 x2 v1 v2 t,
Proof using.
introv N. induction t; simpl; try solve [ fequals;
repeat case_if; simpl; repeat case_if; auto ].
{ repeat case_if; simpl; repeat case_if~. }
{ repeat case_if; simpl; repeat case_if~.
rewrite var_eq_spec in *. rew_bool_eq in *. subst*. }
{ repeat case_if; simpl; repeat case_if~. fequals. }
Qed. (* LATER: simplify *)
......@@ -179,13 +214,19 @@ Qed.
Lemma subst_unbind_neq : forall x y v t,
x <> y ->
subst x v (trm_unbind y t) = trm_unbind y (subst x v t).
Proof using. intros. simpl. case_if~. Qed.
Proof using.
intros. simpl. case_if~.
rewrite var_eq_spec in *. rew_bool_eq in *. subst*.
Qed.
(** Substitution cancels out on [unbind] for a same name. *)
Lemma subst_unbind_same : forall x v t,
subst x v (trm_unbind x t) = trm_unbind x t.
Proof using. intros. simpl. case_if~. Qed.
Proof using.
intros. simpl. case_if~.
rewrite var_eq_spec in *. rew_bool_eq in *. subst*.
Qed.
(* ---------------------------------------------------------------------- *)
......@@ -221,7 +262,7 @@ Inductive red : state -> trm -> state -> val -> Prop :=
| red_val : forall m v,
red m v m v
| red_fun_encoded : forall m1 m2 x t1 r,
let f : var := "$_" in
let f : var := var_special "_" in
red m1 (trm_fix f x (trm_unbind f t1)) m2 r ->
red m1 (trm_fun x t1) m2 r
(*| red_fun : forall m x t1,
......@@ -236,7 +277,7 @@ Inductive red : state -> trm -> state -> val -> Prop :=
red m1 (trm_app (trm_fun x t2) t1) m2 r ->
red m1 (trm_let x t1 t2) m2 r
| red_seq_encoded : forall t1 t2 m1 m2 r,
let x : var := "$u" in
let x : var := var_special "u" in
red m1 (trm_let x t1 (trm_unbind x t2)) m2 r ->
red m1 (trm_seq t1 t2) m2 r
| red_app_arg : forall m1 m2 m3 m4 t1 t2 v1 v2 r,
......@@ -283,8 +324,8 @@ Inductive red : state -> trm -> state -> val -> Prop :=
| red_eq : forall m v1 v2,
red m (val_eq v1 v2) m (val_bool (isTrue (v1 = v2)))
| red_while_encoded : forall t1 t2 m1 m2 r,
let F : var := "$f" in
let U : var := "$_" in
let F : var := var_special "f" in
let U : var := var_special "i" in
let P t := trm_unbind F (trm_unbind U t) in
red m1 ((val_fix F U (trm_if (P t1) (trm_seq (P t2) (F val_unit)) val_unit)) val_unit) m2 r ->
red m1 (trm_while t1 t2) m2 r
......@@ -312,24 +353,37 @@ Inductive red : state -> trm -> state -> val -> Prop :=
(* ---------------------------------------------------------------------- *)
(* ** Derived rules *)
(*
Hint Resolve var_neq_of_special var_neq_of_string_dec.
*)
Section Derived.
Hint Resolve var_neq_of_var_eq.
Notation "'$' x" := (var_special x) (at level 6, format "'$' x").
Definition val_fun x t :=
val_fix "$_" x (trm_unbind "$_" t).
val_fix (var_special "_") x (trm_unbind (var_special "_") t).
Lemma red_app_fun : forall m1 m2 v1 v2 x t r,
x <> "$_" ->
v1 = val_fun x t ->
x <> var_special "_" ->
red m1 (subst x v2 t) m2 r ->
red m1 (trm_app v1 v2) m2 r.
Proof using.
introv N E M1. applys red_app_fix E.
introv E N M1. applys red_app_fix E.
rewrite~ subst_subst_neq. rewrite subst_unbind_same.
rewrite~ subst_unbind_neq. applys~ red_unbind.
Qed.
Lemma red_app_fun' : forall m1 m2 v1 v2 (x:name) t r,
v1 = val_fun x t ->
red m1 (subst x v2 t) m2 r ->
red m1 (trm_app v1 v2) m2 r.
Proof using. introv E M1. applys* red_app_fun. Qed.
Lemma red_let : forall m1 m2 m3 x t1 t2 v1 r,
x <> "$_" ->
x <> var_special "_" ->
red m1 t1 m2 v1 ->
red m2 (subst x v1 t2) m3 r ->
red m1 (trm_let x t1 t2) m3 r.
......@@ -339,6 +393,12 @@ Proof using.
{ applys* red_app_fun. }
Qed.
Lemma red_let' : forall m1 m2 m3 (x:name) t1 t2 v1 r,
red m1 t1 m2 v1 ->
red m2 (subst x v1 t2) m3 r ->
red m1 (trm_let x t1 t2) m3 r.
Proof using. introv M1 M2. applys* red_let. Qed.
Lemma red_seq : forall m1 m2 m3 t1 t2 r1 r,
red m1 t1 m2 r1 ->
red m2 t2 m3 r ->
......@@ -349,7 +409,7 @@ Proof using.
Qed.
Lemma red_let_inv : forall m1 m3 x t1 t2 r,
x <> "$_" ->
x <> var_special "_" ->
red m1 (trm_let x t1 t2) m3 r ->
exists m2 v1, red m1 t1 m2 v1 /\ red m2 (subst x v1 t2) m3 r.
Proof using.
......@@ -357,10 +417,24 @@ Proof using.
inversions M1. rename H4 into M1. inverts M1.
exists___. split. applys M2.
inverts M3 as. { introv N3. false. destruct* N3. } introv E M4.
subst f. inverts E. simpls. case_if. (* temp: slow! *)
{ simpls. inverts M4. auto. }
subst f. inverts E. rewrite~ subst_unbind_neq in M4.
simpls. inverts M4. auto.
Qed.
(** Note: assuming the semantics of [seq], one can show that [seq]
(* has the same semantics has its [let]-based encoding. *) *)
Lemma red_seq' : forall m1 m2 t1 t2 r,
let x : var := var_special "u" in
red m1 (trm_let x t1 (trm_unbind x t2)) m2 r ->
red m1 (trm_seq t1 t2) m2 r.
Proof using.
introv M. lets~ (m3&r1&M1&M2): red_let_inv M.
inverts M2 as. intros M3. applys* red_seq.
Qed.
Lemma red_seq_inv : forall m1 m3 t1 t2 r,
red m1 (trm_seq t1 t2) m3 r ->
exists m2 r1, red m1 t1 m2 r1 /\ red m2 t2 m3 r.
......@@ -374,6 +448,7 @@ Lemma red_while : forall m1 m2 t1 t2 r,
red m1 (trm_while t1 t2) m2 r.
Proof using.
introv M1. applys red_while_encoded. applys* red_app_fix.
match goal with |- context [val_fix ?f ?x ?t] => set (F:=val_fix f x t) end.
simpl. inverts M1 as. introv M1 M2. applys red_if.
{ do 2 applys* red_unbind. }
{ case_if.
......@@ -384,6 +459,11 @@ Proof using.
Qed.
Lemma red_ptr_add_nat : forall m l (f : nat),
red m (val_ptr_add (val_loc l) (val_int f)) m (val_loc (l+f)%nat).
Proof using. intros. applys* red_ptr_add. math. Qed.
......@@ -413,6 +493,7 @@ Proof using.
{ applys red_val. }
Qed.
End Derived.
End Red.
......
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