Commit 111fd3e9 authored by charguer's avatar charguer

modelproof

parent 52671c29
......@@ -12,9 +12,6 @@ include $(CFML)/Makefile.common
PWD := $(shell pwd)
V := $(V_TLC) $(wildcard $(PWD)/*.v)
test:
echo $(VIO)
# The line "-R $(TLC) TLC" is required only if we wish to write just
# "LibFoo", as opposed to "TLC.LibFoo". In the long run, I believe it
# would be preferable to explicitly use the TLC prefix.
......
##############################################################
# Parameters
##############################################################################
# CFML setup.
CFML := ..
-include $(CFML)/settings.sh
include $(CFML)/Makefile.common
##############################################################
# Files
# We compile only a subset of the files present in the folder
##############################################################################
# Compilation.
SRC :=\
ModelLambda \
ModelSep \
ModelRO
V := $(SRC:=.v)
PWD := $(shell pwd)
# V := $(wildcard $(PWD)/*.v)
V := $(CFML)/lib/coq/Shared.v $(SRC:=.v)
test:
echo $(VIO)
##############################################################
# Rules
# $(V_TLC)
all: proof
# The line "-R $(TLC) TLC" is required only if we wish to write just
# "LibFoo", as opposed to "TLC.LibFoo". In the long run, I believe it
# would be preferable to explicitly use the TLC prefix.
COQINCLUDE := -R $(CFML)/lib/tlc TLC -R $(CFML)/lib/coq CFML -R . MODEL
COQINCLUDE := \
-R $(TLC) TLC \
-R $(CFML)/lib/coq CFML \
-R . MODEL
include $(CFML)/lib/make/Makefile.coq
quick_cf: CFHeader.vio
include $(TLC)/Makefile.coq
#####################################################################
......@@ -61,7 +61,7 @@ Definition heap_is_star (H1 H2 : hprop) : hprop :=
(** Lifting of existentials *)
Definition heap_is_pack A (Hof : A -> hprop) : hprop :=
Definition heap_is_exists A (Hof : A -> hprop) : hprop :=
fun h => exists x, Hof x h.
(** Lifting of predicates *)
......@@ -72,7 +72,7 @@ Definition heap_is_empty_st (H:Prop) : hprop :=
(** Garbage collection predicate: [Hexists H, H]. *)
Definition heap_is_gc : hprop :=
heap_is_pack (fun H => H).
heap_is_exists (fun H => H).
(** Hprop is inhabited *)
......@@ -83,6 +83,7 @@ Proof using. intros. apply (prove_Inhab heap_is_empty). Qed.
(*------------------------------------------------------------------*)
(* ** Notation for heap predicates *)
Notation "\# h1 h2" := (heap_disjoint h1 h2)
(at level 40, h1 at level 0, h2 at level 0, no associativity) : heap_scope.
......@@ -108,7 +109,7 @@ Notation "H1 '\*' H2" := (heap_is_star H1 H2)
Notation "\GC" := (heap_is_gc) : heap_scope.
Notation "'Hexists' x1 , H" := (heap_is_pack (fun x1 => H))
Notation "'Hexists' x1 , H" := (heap_is_exists (fun x1 => H))
(at level 39, x1 ident, H at level 50) : heap_scope.
Notation "'Hexists' x1 x2 , H" := (Hexists x1, Hexists x2, H)
(at level 39, x1 ident, x2 ident, H at level 50) : heap_scope.
......@@ -121,7 +122,7 @@ Notation "'Hexists' x1 x2 x3 x4 x5 , H" :=
(Hexists x1, Hexists x2, Hexists x3, Hexists x4, Hexists x5, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50) : heap_scope.
Notation "'Hexists' x1 : T1 , H" := (heap_is_pack (fun x1:T1 => H))
Notation "'Hexists' x1 : T1 , H" := (heap_is_exists (fun x1:T1 => H))
(at level 39, x1 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) , H" := (Hexists x1:T1,H)
(at level 39, x1 ident, H at level 50, only parsing) : heap_scope.
......@@ -169,12 +170,17 @@ Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) x4 x5 , H" :=
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50, only parsing) : heap_scope.
Notation "r '~~>' v" := (heap_is_single r v)
(at level 32, no associativity) : heap_scope.
Notation "Q \*+ H" :=
(fun x => heap_is_star (Q x) H)
(at level 40) : heap_scope.
(*
Notation "# H" := (fun (_:unit) => (H:hprop))
(at level 39, H at level 99) : heap_scope.
*)
Notation "\[= v ]" := (fun x => \[x = v])
(at level 0) : heap_scope.
......@@ -194,6 +200,8 @@ Definition triple t H Q :=
/\ Q r h1'.
Definition app f v H Q :=
triple (trm_app f v) H Q.
(********************************************************************)
......@@ -422,7 +430,7 @@ Lemma heap_extract_prop : forall (P:Prop) H H',
Proof using. introv W Hh. applys_to Hh heap_star_prop_elim. autos*. Qed.
Lemma heap_weaken_pack : forall A (x:A) H J,
H ==> J x -> H ==> (heap_is_pack J).
H ==> J x -> H ==> (heap_is_exists J).
Proof using. introv W h. exists x. apply~ W. Qed.
......@@ -463,30 +471,36 @@ Tactic Notation "rew_heap" "*" "in" hyp(H) :=
(********************************************************************)
(* ** Soundness *)
(* ** Rules *)
Implicit Types H : hprop.
Implicit Types Q : val -> hprop.
Lemma seq_rule : forall x t1 t2 H Q Q1,
triple t1 H Q1 ->
(forall (X:val), triple (subst_trm x X t2) (Q1 X) Q) ->
triple (trm_let x t1 t2) H Q.
Proof using.
introv M1 M2. intros h1 h2 D1 H1.
lets (h1'a&h3a&ra&Da&Ra&Qa): M1 D1 H1.
rew_disjoint.
forwards (h1'b&h3b&rb&Db&Rb&Qb): M2 ra h1'a (h2 \+ h3a).
{ rew_disjoint. jauto. }
{ auto. }
{ exists h1'b (h3a \+ h3b) rb. splits.
{ rew_disjoint. jauto. }
{ rewrite <- heap_union_assoc in Rb. constructors*. }
{ auto. } }
(** Structural *)
Lemma rule_extract_prop : forall t (P:Prop) H Q,
(P -> triple t H Q) ->
triple t (H \* \[P]) Q.
Proof using.
introv M D (h21&h22&N1&(HE&HP)&N3&N4).
subst h22 h1. rewrite state_union_neutral_r.
forwards (h1'&h3&r&R1&R2&R3): M HP h2 N1.
{ subst. rew_disjoint. jauto. }
exists~ h1' h3 r.
Qed.
Lemma frame_rule : forall t H Q H',
Lemma rule_extract_exists : forall t (J:val->hprop) Q,
(forall x, triple t (J x) Q) ->
triple t (heap_is_exists J) Q.
Proof using.
introv M D (x&Jx).
forwards (h1'&h3&r&R1&R2&R3): M D Jx.
exists~ h1' h3 r.
Qed.
Lemma rule_frame : forall t H Q H',
triple t H Q ->
triple t (H \* H') (Q \*+ H').
Proof using.
......@@ -503,20 +517,110 @@ Qed.
(* TODO: add to hint extern "rew_disjoint" the jauto_set. *)
(** Terms *)
Lemma rule_val : forall v H Q,
H ==> Q v ->
triple (trm_val v) H Q.
Proof using.
introv M D H1.
exists h1 heap_empty v. rewrite state_union_neutral_r.
splits.
{ rew_disjoint; jauto. }
{ applys red_val. }
{ auto. }
Qed.
Lemma rule_if_true : forall v t1 t2 H Q,
triple (If v = val_int 0 then t2 else t1) H Q ->
triple (trm_if v t1 t2) H Q.
Proof using.
introv M D H1.
forwards (h1'&h3&r&R1&R2&R3): M D H1.
exists h1' h3 r. splits.
{ rew_disjoint; jauto. }
{ applys~ red_if. }
{ auto. }
Qed.
Lemma let_rule : forall x t1 t2 H Q Q1,
triple t1 H Q1 ->
(forall (X:val), triple (subst_trm x X t2) (Q1 X) Q) ->
triple (trm_let x t1 t2) H Q.
Proof using.
introv M1 M2. intros h1 h2 D1 H1.
lets (h1'a&h3a&ra&Da&Ra&Qa): M1 D1 H1.
rew_disjoint.
forwards (h1'b&h3b&rb&Db&Rb&Qb): M2 ra h1'a (h2 \+ h3a).
{ rew_disjoint. jauto. }
{ auto. }
{ exists h1'b (h3a \+ h3b) rb. splits.
{ rew_disjoint. jauto. }
{ rewrite <- heap_union_assoc in Rb. constructors*. }
{ auto. } }
Qed.
Lemma rule_app : forall f v H Q,
app f v H Q ->
triple (trm_app f v) H Q.
Proof using.
auto.
Qed.
Lemma rule_fix : forall f x t1 t2 H Q,
(forall (F:val),
(forall X H' Q', triple (subst_trm f F (subst_trm x X t1)) H' Q'
-> app F X H' Q') ->
triple (subst_trm f F t2) H Q) ->
triple (trm_letfix f x t1 t2) H Q.
Proof using.
introv M D H1.
forwards (h1'&h3&r&R1&R2&R3): M (val_fix f x t1) D H1.
{ clears h1 h2 H Q. intros X H Q M. unfolds.
introv D H1.
forwards (h1'&h3&r&R1&R2&R3): M D H1.
exists h1' h3 r. splits.
{ rew_disjoint; jauto. }
{ applys~ red_app. }
{ auto. } }
exists h1' h3 r. splits.
{ rew_disjoint; jauto. }
{ applys~ red_fix. }
{ auto. }
Qed.
Lemma rule_new : forall v,
triple (trm_new v) \[] (fun r => Hexists l, [r = val_loc l] \* l ~~> v).
Proof using.
skip.
Qed.
Lemma rule_get : forall l,
triple (trm_get (val_loc l)) (l ~~> v) (fun x => \[x = v] \* l ~~> v).
Proof using.
skip.
Qed.
Lemma rule_set : forall l v w,
triple (trm_set (val_loc l) w) (l ~~> v) (fun r => \[r = val_unit] \* l ~~> w).
Proof using.
skip.
Qed.
End Red.
(********************************************************************)
(* ** More *)
(** Substitution
Lemma subst_lemma : forall x v t H Q,
(forall (X:val), triple (subst_trm x X t) (H X) (Q X)) ->
triple (subst_trm x v t) (H v) (Q v).
Proof using.
auto.
Qed.
*)
\ No newline at end of file
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