Commit 1553cd8e authored by charguer's avatar charguer

seq_encoding

parent fcad5dc2
......@@ -23,6 +23,7 @@ Open Scope string_scope.
(* ---------------------------------------------------------------------- *)
(** Representation of variables and locations *)
Definition tag := nat.
Definition var := string.
Definition loc := nat.
Definition null : loc := 0%nat.
......@@ -61,11 +62,12 @@ with trm : Type :=
| trm_fun : var -> trm -> trm
| trm_fix : var -> var -> trm -> trm
| trm_if : trm -> trm -> trm -> trm
| trm_seq : trm -> trm -> trm
| 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_tag : tag -> trm -> trm
| trm_protect : var -> trm -> trm.
(** The type of values is inhabited *)
......@@ -85,6 +87,25 @@ Coercion trm_var : var >-> trm.
Coercion trm_app : trm >-> Funclass.
(* ---------------------------------------------------------------------- *)
(** Encoded constructs *)
(** Reserved variables begin with character [$] *)
Definition is_reserved_var (x:var) : bool :=
match x with
| String h _ => if Ascii.ascii_dec h "$" then true else false
| _ => false
end.
(** Encoding of sequences *)
Definition tag_seq : tag := 1%nat.
Definition trm_seq (t1:trm) (t2:trm) : trm :=
trm_tag tag_seq (trm_let "$_" t1 (trm_protect "$_" t2)).
(* ********************************************************************** *)
(* * Source language semantics *)
......@@ -101,11 +122,12 @@ Fixpoint subst (y:var) (w:val) (t:trm) : trm :=
| 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)
| trm_tag g t1 => trm_tag g (aux t1)
| trm_protect x t1 => if eq_var_dec x y then t else trm_protect x (aux t1)
end.
......@@ -126,6 +148,12 @@ Implicit Types b : bool.
Implicit Types n : int.
Inductive red : state -> trm -> state -> val -> Prop :=
| red_tag : forall g t1 m1 m2 v,
red m1 t1 m2 v ->
red m1 (trm_tag g t1) m2 v
| red_protect : forall x t1 m1 m2 v,
red m1 t1 m2 v ->
red m1 (trm_protect x t1) m2 v
| red_val : forall m v,
red m v m v
| red_fun : forall m x t1,
......@@ -136,10 +164,6 @@ Inductive red : state -> trm -> state -> val -> Prop :=
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 ->
......@@ -213,6 +237,15 @@ Inductive red : state -> trm -> state -> val -> Prop :=
(* ---------------------------------------------------------------------- *)
(* ** Derived rules *)
Lemma 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.
Proof using.
introv M1 M2. applys red_tag. applys* red_let.
simpl. applys* red_protect.
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.
......@@ -516,17 +549,18 @@ 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_protect 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
......@@ -555,7 +589,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~. }
{ repeat case_if; simpl; repeat case_if~. fequals. }
Qed. (* LATER: simplify *)
(** Substituting for a variable that has just been substituted
......@@ -565,7 +600,7 @@ 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 ].
repeat case_if; simpl; repeat case_if; auto; fequals ].
Qed.
......@@ -755,7 +790,7 @@ 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'. }
......
......@@ -170,6 +170,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]).
......@@ -225,13 +227,20 @@ 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_tag g t1 => wp_tag g (aux t1)
| trm_protect x t1 => wp (ctx_rem x E) t1
end.
(* match
| trm_tag g (trm_let x t1 (trm_protect y t2)) =>
if eq_nat_dec g tag_seq && eq_var_dec x y
then wp_seq (aux t1) (aux t2)
else ...
*)
(* ********************************************************************** *)
......@@ -309,7 +318,8 @@ 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 ].
Qed.
(** [remove_local] applies to goal of the form [triple t (local F Q) Q]
......@@ -319,6 +329,43 @@ Ltac remove_local :=
match goal with |- triple _ _ ?Q =>
applys triple_local_pre; try (clear Q; intros Q); xpull end.
(* TODO move *)
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_protect : forall E x t1,
substs E (trm_protect x t1)
= trm_protect x (substs (ctx_rem x E) t1).
Proof using. substs_simpl_proof. case_if; rewrite~ IH. Qed.
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_tag : forall g 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.
Lemma triple_wp : forall t E Q,
triple (substs E t) (wp E t Q) Q.
Proof using.
......@@ -342,16 +389,14 @@ 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_tag. applys rule_tag. unfold wp_tag. applys IHt. }
{ rewrite substs_protect. applys rule_protect. applys IHt. }
Qed.
Lemma triple_substs_of_wp : forall t E H Q,
......@@ -368,44 +413,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 +536,8 @@ Qed.
End WP2.
*)
(* ********************************************************************** *)
(* * Practical proofs using characteristic formulae *)
......@@ -546,6 +562,12 @@ Notation "'`Seq' F1 ;;; F2" :=
(at level 68, right associativity,
format "'[v' '`Seq' '[' F1 ']' ;;; '/' '[' F2 ']' ']'") : charac.
Notation "'`Seq' x F1 ;;; F2" :=
(wp_tag tag_seq (wp_let F1 (fun x => F2)))
(at level 68, right associativity, x ident,
format "'[v' '`Seq' x '[' F1 ']' ;;; '/' '[' F2 ']' ']'") : charac.
(* LATER: how to remove x ? specific CF for tagged-let with a sequence-tag *)
Notation "'`Let' x ':=' F1 'in' F2" :=
((wp_let F1 (fun x => F2)))
(at level 69, x ident, right associativity,
......@@ -603,7 +625,7 @@ Qed.
(*
Module WP2Aux.
Import WP2.
......@@ -635,6 +657,7 @@ Qed.
End LemmasCf.
End WP2Aux.
*)
(* ---------------------------------------------------------------------- *)
(** ** Database of lemmas *)
......
......@@ -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
......
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