...
 
Commits (6)
......@@ -4195,4 +4195,70 @@ Ltac xwhile_core xwhile_tactic ::=
*)
*)
\ No newline at end of file
*)
(** Encoding of sequences *)
Definition trm_seq (t1:trm) (t2:trm) : trm :=
trm_tag tag_seq (trm_let "$_" t1 (trm_unbind "$_" t2)).
(** Encoding of while loops *)
Definition trm_while (t1:trm) (t2:trm) : trm :=
let F : var := "$f" in
let U : var := "$_" in
let P t := trm_unbind F (trm_unbind U t) in
let X : val := val_fix F U (trm_if (P t1) (trm_seq (P t2) (F val_unit)) val_unit) in
trm_tag tag_while (X val_unit).
(*
Lemma red_app_fun : forall m1 m2 v1 v2 x t r,
var_special x = false ->
v1 = val_fun x t ->
red m1 (subst x v2 t) m2 r ->
red m1 (trm_app v1 v2) m2 r.
Proof using. intros. applys* red_app_fun_precise. Qed.
*)
(* todo: deprecated
Lemma red_seq_unit : forall m1 m2 m3 t1 t2 r,
red m1 t1 m2 val_unit ->
red m2 t2 m3 r ->
red m1 (trm_seq t1 t2) m3 r.
Proof using.
introv M1 M2. applys* red_let.
simpl. applys* red_unbind.
Qed.
*)
(* todo: deprecated
Lemma red_seq' : forall m1 m2 t1 t2 r,
let x : var := "$_" 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. inverts M as. intros m3 r1 M1 M2.
inverts M2 as. intros M3. applys* red_seq.
Qed.
*)
(* todo: deprecated
Lemma red_while' : forall t1 t2 m1 m2 r,
let F : var := "$f" in
let U : var := "$_" 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.
Proof using.
introv M1. applys red_while. ...
Qed.
*)
(*
Inductive test : nat -> Prop :=
| test_intro : forall m,
let n := 3 in
test (m + n) ->
test m.
Lemma test_inv : test 5 -> True.
intros M. inversion M.
*)
(**
This file describes the syntax and semantics of a lambda calculus
......@@ -23,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.
(* ---------------------------------------------------------------------- *)
......@@ -52,7 +66,7 @@ Inductive val : Type :=
| val_int : int -> val
| val_loc : loc -> val
| val_prim : prim -> val
| val_fun : var -> trm -> val
(*| val_fun : var -> trm -> val*)
| val_fix : var -> var -> trm -> val
with trm : Type :=
......@@ -65,7 +79,8 @@ with trm : Type :=
| trm_let : var -> trm -> trm -> trm
| trm_app : trm -> trm -> trm
| trm_while : trm -> trm -> trm
| trm_for : var -> trm -> trm -> trm -> trm.
| trm_for : var -> trm -> trm -> trm -> trm
| trm_unbind : var -> trm -> trm.
(** The type of values is inhabited *)
......@@ -83,6 +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.
Definition name_eq (x y:name) :=
if eq_name_dec x y then true else false.
Lemma var_neq_of_name_dec : forall x y,
name_eq x y = false ->
x <> y.
Proof using. unfolds name_eq. introv M. case_if~. Qed.
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_var_eq : forall x y,
var_eq x y = false ->
x <> y.
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.
(* ********************************************************************** *)
......@@ -93,19 +166,76 @@ Coercion trm_app : trm >-> Funclass.
Fixpoint subst (y:var) (w:val) (t:trm) : trm :=
let aux t := subst y w t in
let aux_no_capture 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_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_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 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)
| trm_let x t1 t2 => trm_let x (aux t1) (aux_no_capture x t2)
| trm_let x t1 t2 => trm_let x (aux t1) (aux_unbind 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)
| trm_for x t1 t2 t3 => trm_for x (aux t1) (aux t2) (aux_unbind x t3)
| trm_unbind x t1 => if var_eq x y then t else trm_unbind x (aux t1)
end.
(* ---------------------------------------------------------------------- *)
(** Properties of substitution *)
(** Substitutions for two distinct variables commute. *)
Lemma subst_subst_neq : forall x1 x2 v1 v2 t,
x1 <> x2 ->
subst x2 v2 (subst x1 v1 t) = subst x1 v1 (subst x2 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~.
rewrite var_eq_spec in *. rew_bool_eq in *. subst*. }
{ repeat case_if; simpl; repeat case_if~. fequals. }
Qed. (* LATER: simplify *)
(** Substituting for a variable that has just been substituted
does not further modify the term. *)
Lemma subst_subst_same : forall x v1 v2 t,
subst x v2 (subst x v1 t) = subst x v1 t.
Proof using.
intros. induction t; simpl; try solve [ fequals;
repeat case_if; simpl; repeat case_if; auto; fequals ].
Qed.
(** Substitution commutes with [unbind] for a distinct name. *)
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~.
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~.
rewrite var_eq_spec in *. rew_bool_eq in *. subst*.
Qed.
(* ---------------------------------------------------------------------- *)
(** Characterization of values *)
Definition trm_is_val (t:trm) : Prop :=
match t with
| trm_val v => True
| _ => False
end.
......@@ -126,37 +256,44 @@ Implicit Types b : bool.
Implicit Types n : int.
Inductive red : state -> trm -> state -> val -> Prop :=
| red_unbind : forall x t1 m1 m2 v,
red m1 t1 m2 v ->
red m1 (trm_unbind x t1) m2 v
| red_val : forall m v,
red m v m v
| red_fun : forall m x t1,
red m (trm_fun x t1) m (val_fun x t1)
| red_fun_encoded : forall m1 m2 x t1 r,
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,
red m (trm_fun x t1) m (val_fun x t1)*)
| red_fix : forall m f x t1,
red m (trm_fix f x t1) m (val_fix f x t1)
| red_if : forall m1 m2 m3 b r t0 t1 t2,
red m1 t0 m2 (val_bool b) ->
red m2 (if b then t1 else t2) m3 r ->
red m1 (trm_if t0 t1 t2) m3 r
| red_seq : forall m1 m2 m3 t1 t2 r,
red m1 t1 m2 val_unit ->
red m2 t2 m3 r ->
red m1 (trm_seq t1 t2) m3 r
| red_let : forall m1 m2 m3 x 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
| red_let_encoded : forall m1 m2 x t1 t2 r,
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 := 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,
(* LATER: add [not_is_val t1 \/ not_is_val t2] *)
(~ trm_is_val t1 \/ ~ trm_is_val t2) ->
red m1 t1 m2 v1 ->
red m2 t2 m3 v2 ->
red m3 (trm_app v1 v2) m4 r ->
red m1 (trm_app t1 t2) m4 r
| red_app_fun : forall m1 m2 v1 v2 x t r,
(*| red_app_fun : forall m1 m2 v1 v2 x t r,
v1 = val_fun x t ->
red m1 (subst x v2 t) m2 r ->
red m1 (trm_app v1 v2) m2 r
red m1 (trm_app v1 v2) m2 r*)
| red_app_fix : forall m1 m2 v1 v2 f x t r,
v1 = val_fix f x t ->
red m1 (subst f v1 (subst x v2 t)) m2 r ->
(* red m1 (subst x v2 (subst f v1 t)) m2 r -> todo: remove *)
red m1 (trm_app v1 v2) m2 r
| red_ref : forall ma mb v l,
mb = (fmap_single l v) ->
......@@ -186,8 +323,11 @@ Inductive red : state -> trm -> state -> val -> Prop :=
red m (val_ptr_add (val_loc l) (val_int n)) m (val_loc l')
| red_eq : forall m v1 v2,
red m (val_eq v1 v2) m (val_bool (isTrue (v1 = v2)))
| red_while : forall m1 m2 t1 t2 r,
red m1 (trm_if t1 (trm_seq t2 (trm_while t1 t2)) val_unit) m2 r ->
| red_while_encoded : forall t1 t2 m1 m2 r,
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
| red_for_arg : forall m1 m2 m3 m4 v1 v2 x t1 t2 t3 r,
(* LATER: add [not_is_val t1 \/ not_is_val t2] *)
......@@ -213,6 +353,121 @@ 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 (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 "_" ->
red m1 (subst x v2 t) m2 r ->
red m1 (trm_app v1 v2) m2 r.
Proof using.
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 <> var_special "_" ->
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 N M1 M2. applys red_let_encoded. applys* red_app_arg.
{ applys* red_fun_encoded. applys red_fix. }
{ 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 ->
red m1 (trm_seq t1 t2) m3 r.
Proof using.
introv M1 M2. applys red_seq_encoded. applys* red_let.
simpl. applys* red_unbind.
Qed.
Lemma red_let_inv : forall m1 m3 x t1 t2 r,
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.
introv N1 M. inverts M as. introv M. inverts M as. introv N2 M1 M2 M3.
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. 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.
Proof using.
introv M. inversions M. rename H4 into M. subst x.
forwards~ (m2&v1&M1&M2): red_let_inv M. simpls. inverts* M2.
Qed.
Lemma red_while : forall m1 m2 t1 t2 r,
red m1 (trm_if t1 (trm_seq t2 (trm_while t1 t2)) val_unit) m2 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.
{ lets (m'&r'&M2'&M3'): red_seq_inv (rm M2). applys red_seq.
{ do 2 applys* red_unbind. }
{ inversion M3'; subst. rename H4 into M4. applys M4. } }
{ auto. } }
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.
......@@ -242,6 +497,7 @@ Proof using.
{ applys red_val. }
Qed.
End Derived.
End Red.
......@@ -521,12 +777,13 @@ Fixpoint trm_size (t:trm) : nat :=
| 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_unbind x t1 => 1 + trm_size t1
end.
Lemma trm_size_subst : forall t x v,
trm_size (subst x v t) = trm_size t.
Proof using.
intros. induction t; simpl; repeat case_if; auto.
intros. induction t; simpl; repeat case_if; auto. { simpl. math. }
Qed.
(** Hint for induction on size. Proves subgoals of the form
......@@ -542,32 +799,7 @@ Hint Extern 1 (measure trm_size _ _) => solve_measure_trm_size tt.
(* ********************************************************************** *)
(* * More on substitutions *)
(* ---------------------------------------------------------------------- *)
(** Properties of substitution *)
(** Substitutions for two distinct variables commute. *)
Lemma subst_subst_neq : forall x1 x2 v1 v2 t,
x1 <> x2 ->
subst x2 v2 (subst x1 v1 t) = subst x1 v1 (subst x2 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~.
Qed. (* LATER: simplify *)
(** Substituting for a variable that has just been substituted
does not further modify the term. *)
Lemma subst_subst_same : forall x v1 v2 t,
subst x v2 (subst x v1 t) = subst x v1 t.
Proof using.
intros. induction t; simpl; try solve [ fequals;
repeat case_if; simpl; repeat case_if; auto ].
Qed.
(* * Iterated substitutions *)
(* ---------------------------------------------------------------------- *)
(** Distinct variables *)
......@@ -581,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. *)
......@@ -617,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
......@@ -627,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.
......@@ -669,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.
......@@ -692,6 +924,11 @@ Ltac substs_simpl_proof :=
intros E; induction E as [|(x,w) E' IH]; intros; simpl;
[ | try rewrite IH ]; auto.
Lemma substs_unbind : forall E x t1,
substs E (trm_unbind x t1)
= trm_unbind x (substs (ctx_rem x E) t1).
Proof using. substs_simpl_proof. case_if; rewrite~ IH. Qed.
Lemma substs_val : forall E v,
substs E (trm_val v) = v.
Proof using. substs_simpl_proof. Qed.
......@@ -755,10 +992,10 @@ Lemma ctx_fresh_combine : forall x ys vs,
ctx_fresh x (LibList.combine ys vs).
Proof using.
intros x ys. unfold ctx_fresh.
induction ys as [|y ys']; simpl; intros [|v vs] M L;
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 *)
......@@ -916,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.
......@@ -939,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.
......@@ -970,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.
......@@ -1092,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. }
......@@ -1112,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.
......@@ -1120,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.
......@@ -1187,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
......@@ -1194,4 +1458,4 @@ Ltac var_neq :=
[ false | apply E ] ] end.
Hint Extern 1 (?x <> ?y) => var_neq.
*)
......@@ -529,6 +529,21 @@ Qed.
(* ---------------------------------------------------------------------- *)
(* ** Term rules *)
Lemma rule_red : forall t1 t2 H Q,
(forall m m' r, red m t1 m' r -> red m t2 m' r) ->
triple t1 H Q ->
triple t2 H Q.
Proof using.
introv T M. intros Hf h N. lets~ (h'&v&R&K): (rm M) Hf h.
exists h' v. splits~.
Qed.
Lemma rule_unbind : forall x t1 H Q,
triple t1 H Q ->
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,
H ==> Q v ->
triple (trm_val v) H Q.
......@@ -587,7 +602,8 @@ Proof using.
{ intros v' N. hpull. intros E. inverts~ E. false N. hnfs*. }
Qed.
Lemma rule_seq : forall t1 t2 H Q Q1,
(* 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]) ->
triple t2 (Q1 val_unit) Q ->
......@@ -604,16 +620,18 @@ Proof using.
(* LATER: shorten this, and factorize with rule_if *)
subst. forwards* (h2'&v2&R2&K2): (rm M3) (\Top \* HF) h1'.
exists h2' v2. splits~.
{ applys~ red_seq R2. }
{ 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~.
......@@ -621,6 +639,24 @@ 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. applys rule_red. applys red_seq_encoded.
applys rule_let_general.
{ auto. }
{ applys M1. }
{ simpl. intros. applys rule_unbind. applys M2. }
Qed.
Lemma rule_apps_funs : forall xs F (Vs:vals) t1 H Q,
F = (val_funs xs t1) ->
var_funs (length Vs) xs ->
......@@ -628,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,
......@@ -638,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.
......@@ -663,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 ->
......@@ -1025,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.
......@@ -1034,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 *)
......@@ -1066,19 +1116,19 @@ Proof using.
{ applys* red_if_bool. } }
Qed.
(** An alternative statement for [rule_seq] *)
Lemma rule_seq' : forall t1 t2 H Q H1,
(** 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 ->
triple (trm_seq t1 t2) H Q.
Proof using.
introv M1 M2. applys rule_seq.
introv M1 M2. applys rule_seq_unit.
{ applys M1. }
{ intros v E. hpull; false. }
{ applys rule_extract_hprop. intros. applys M2. }
Qed.
*)
(* ---------------------------------------------------------------------- *)
(** Reformulation of the rule for N-ary functions *)
......
......@@ -18,6 +18,7 @@ Implicit Types t : trm.
(* ********************************************************************** *)
(* * WP generator *)
......@@ -170,6 +171,8 @@ Proof using. intros. unfolds. rewrite~ local_local. Qed.
(** These auxiliary definitions give the characteristic formula
associated with each term construct. *)
Definition wp_tag (g:tag) (F:formula) : formula := F.
Definition wp_fail : formula := local (fun Q =>
\[False]).
......@@ -179,6 +182,9 @@ Definition wp_val (v:val) : formula := local (fun Q =>
Definition wp_seq (F1 F2:formula) : formula := local (fun Q =>
F1 (fun r => \[r = val_unit] \* F2 Q)).
Definition wp_seq' (F1 F2:formula) : formula := local (fun Q =>
F1 (fun r => F2 Q)).
Definition wp_let (F1:formula) (F2of:val->formula) : formula := local (fun Q =>
F1 (fun X => F2of X Q)).
......@@ -217,6 +223,7 @@ Definition wp_var (E:ctx) (x:var) : formula :=
| Some v => (fun Q => Q v)
end).
Fixpoint wp (E:ctx) (t:trm) : formula :=
let aux := wp E in
match t with
......@@ -225,15 +232,30 @@ Fixpoint wp (E:ctx) (t:trm) : formula :=
| trm_fun x t1 => wp_val (val_fun x (substs E t1)) (* todo remove x from E *)
| trm_fix f x t1 => wp_val (val_fix f x (substs E t1)) (* todo remove x,f from E *)
| trm_if t0 t1 t2 => wp_if (aux t0) (aux t1) (aux t2)
| trm_seq t1 t2 => wp_seq (aux t1) (aux t2)
| trm_let x t1 t2 => wp_let (aux t1) (fun X => wp (ctx_add x X E) t2)
| trm_app t1 t2 => local (weakestpre (triple (substs E t)))
| trm_while t1 t2 => wp_while (aux t1) (aux t2)
| trm_for x t1 t2 t3 => wp_for' (aux t1) (aux t2) (fun X => wp (ctx_add x X E) t3)
| trm_protect x t1 => wp (ctx_rem x E) t1
| trm_tag g t0 =>
match g, t0 with
(*| tag_seq, trm_let "$_" t1 (trm_protect "$_" t2) =>
wp_seq' (aux t1) (wp (ctx_rem "$_" E) t2) *)
| tag_seq, trm_let x t1 (trm_protect y t2) =>
if eq_var_dec x y
then wp_seq' (aux t1) (wp (ctx_rem x E) t2)
else wp_fail
(*
| tag_while, trm_app (val_fix "$f" "$_" (trm_if (trm_protect "$f" (trm_protect "$_" t1))
(trm_let "$_" (trm_protect "$f" (trm_protect U t2))
((trm_protect "$_" t2 (trm_app "$f" val_unit)))
val_unit)) val_unit =>
let aux := wp (ctx_rem "$_" (ctx_rem "$f" E)) in
wp_while (aux t1) (aux t2)*)
| _,_ => wp_fail
end
end.
(* ********************************************************************** *)
(* * Soundness proof *)
......@@ -309,9 +331,18 @@ Qed. (* TODO: simplify proof? *)
Lemma is_local_cf : forall E t,
is_local (wp E t).
Proof.
intros. destruct t; try solve [ apply is_local_local ].
intros. gen E. induction t; intros;
try solve [ apply is_local_local | eauto ].
{ simpl. rename t into g.
destruct g; try apply is_local_local.
destruct t0; try applys is_local_local.
destruct t0_2; try applys is_local_local.
case_if; try applys is_local_local. }
Qed.
(** [remove_local] applies to goal of the form [triple t (local F Q) Q]
and turns it into [triple t (F Q) Q] for a fresh [Q], then calls [xpull] *)
......@@ -319,6 +350,13 @@ Ltac remove_local :=
match goal with |- triple _ _ ?Q =>
applys triple_local_pre; try (clear Q; intros Q); xpull end.
(** Triples with [wp_fail] as precondition are always valid. *)
Lemma triple_wp_fail : forall t Q,
triple t (wp_fail Q) Q.
Proof using. intros. remove_local. intros. false. Qed.
Lemma triple_wp : forall t E Q,
triple (substs E t) (wp E t Q) Q.
Proof using.
......@@ -342,16 +380,21 @@ Proof using.
{ applys* IHt2. }
{ applys* IHt3. } }
{ intros. applys~ wp_if_val_false. } }
admit.
(** will be handled differently
{ remove_local. applys rule_seq'. { applys* IH. } { applys* IH. } }
*)
{ remove_local. rewrite substs_let. applys rule_let.
{ applys* IHt1. }
{ intros X. simpl. rewrite subst_substs_ctx_rem_same. applys IHt2. } }
{ remove_local. rewrite substs_app. apply triple_weakestpre_pre. }
{ admit. } (** will be handled differently *)
{ admit. }
{ rewrite substs_protect. applys rule_protect. applys IHt. }
{ rename t into g. destruct g; try apply triple_wp_fail.
destruct t0; try apply triple_wp_fail.
destruct t0_2; try apply triple_wp_fail.
case_if; try apply triple_wp_fail. subst.
renames v0 to x, t0_1 to t1, t0_2 to t2.
rewrite substs_tag. applys rule_tag.
simpl in IHt. case_if. unfolds wp_let.
unfold wp_seq'. apply IHt. }
Qed.
Lemma triple_substs_of_wp : forall t E H Q,
......@@ -368,44 +411,13 @@ Proof using. introv M. xchanges M. applys triple_wp. Qed.
(* ********************************************************************** *)
(* * Alternative definition of the CF generator *)
(*
Module WP2.
(* ********************************************************************** *)
(* * Size of a term *)
(* ---------------------------------------------------------------------- *)
(** Size of a term, where all values counting for one unit. *)
Fixpoint trm_size (t:trm) : nat :=
match t with
| trm_var x => 1
| trm_val v => 1
| 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
end.
Lemma trm_size_subst : forall t x v,
trm_size (subst x v t) = trm_size t.
Proof using.
intros. induction t; simpl; repeat case_if; auto.
Qed.
(** Hint for induction on size. Proves subgoals of the form
[measure trm_size t1 t2], when [t1] and [t2] may have some
structure or involve substitutions. *)
Ltac solve_measure_trm_size tt :=
unfold measure in *; simpls; repeat rewrite trm_size_subst; math.
Hint Extern 1 (measure trm_size _ _) => solve_measure_trm_size tt.
(** The CF generator is a recursive function, defined using the
optimal fixed point combinator (from TLC). [wp_def] gives the
function, and [cf] is then defined as the fixpoint of [wp_def].
......@@ -522,6 +534,8 @@ Qed.
End WP2.
*)
(* ********************************************************************** *)
(* * Practical proofs using characteristic formulae *)
......@@ -542,7 +556,7 @@ Notation "'`If' v 'Then' F1 'Else' F2" :=
(at level 69) : charac.
Notation "'`Seq' F1 ;;; F2" :=
((wp_seq F1 F2))
((wp_seq' F1 F2))
(at level 68, right associativity,
format "'[v' '`Seq' '[' F1 ']' ;;; '/' '[' F2 ']' ']'") : charac.
......@@ -603,7 +617,7 @@ Qed.
(*
Module WP2Aux.
Import WP2.
......@@ -635,6 +649,7 @@ Qed.
End LemmasCf.
End WP2Aux.
*)
(* ---------------------------------------------------------------------- *)
(** ** Database of lemmas *)
......@@ -771,15 +786,56 @@ Definition val_incr :=
Lemma rule_incr : forall (p:loc) (n:int),
triple (val_incr p)
(p ~~~> n)
(fun r => \[r = val_unit] \* (p ~~~> (n+1))).
(fun r => (p ~~~> (n+1))).
Proof using.
intros. xcf.
xlet. { xapp. xapplys rule_get. }
intros x. hpull ;=> E. subst.
xlet. { xapp. xapplys rule_add. }
intros y. hpull ;=> E. subst.
xapp. xapplys rule_set. auto.
Qed.
xapp. xapplys rule_set.
Qed.
Definition val_incr2 :=
ValFun 'p :=
val_incr 'p ;;;
val_incr 'p.
Lemma rule_incr2 : forall (p:loc) (n:int),
triple (val_incr2 p)
(p ~~~> n)
(fun r => (p ~~~> (n+2))).
Proof using.
intros. xcf.
xlet. { xapp. xapplys rule_incr. }
hnf. intros _.
xapp. xapplys rule_incr.
hnf. intros _.
math_rewrite (n+2 = n+1+1). hsimpl.
Qed.
......
......@@ -14,7 +14,7 @@ COQFLAGS:=-w -notation-overridden,-implicits-in-term
# Compilation.
# Note: double space below is important for export.sh
SRC := TLCbuffer Fmap SepFunctor LambdaSemantics LambdaSep SepGPM LambdaSepProofMode LambdaCF LambdaCFTactics LambdaWP LambdaStruct LambdaSepRO LambdaSepROProofMode ExampleROProofMode ExampleListProofMode LambdaSepCredits LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleQueueNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder ExampleList LambdaCFCredits ExampleRO ExampleListProofMode
SRC := TLCbuffer Fmap SepFunctor LambdaSemantics LambdaSep LambdaCFTactics LambdaWP SepGPM LambdaSepProofMode LambdaCF LambdaStruct LambdaSepRO LambdaSepROProofMode ExampleROProofMode ExampleListProofMode LambdaSepCredits LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleQueueNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder ExampleList LambdaCFCredits ExampleRO ExampleListProofMode
# LambdaCFRO
......