Commit bd90597a authored by charguer's avatar charguer

pervasives_proofs

parent 25b8b2fc
......@@ -394,16 +394,18 @@ let infix_name_symbols =
'~', "tilde" ]
let infix_name_encode name =
let gen = Buffer.create 20 in
String.iter (fun c ->
let s =
try List.assoc c infix_name_symbols
with Not_found -> failwith ("infix_name_encode: cannot encode name: " ^ name)
in
Buffer.add_string gen s;
Buffer.add_string gen "_";
) name;
"infix_" ^ (Buffer.contents gen)
if name = "mod" then "infix_mod_" else begin
let gen = Buffer.create 20 in
String.iter (fun c ->
let s =
try List.assoc c infix_name_symbols
with Not_found -> failwith ("infix_name_encode: cannot encode name: " ^ name)
in
Buffer.add_string gen s;
Buffer.add_string gen "_";
) name;
"infix_" ^ (Buffer.contents gen)
end
(*DEPRECATED
let gen = String.map (fun c ->
......@@ -414,8 +416,9 @@ let infix_name_encode name =
(** Convention for renaming infix function names *)
let is_infix_name name =
String.length name > 0
&& List.mem_assoc name.[0] infix_name_symbols
name = "mod" ||
( String.length name > 0
&& List.mem_assoc name.[0] infix_name_symbols)
let protect_infix name =
let r =
......
......@@ -1401,10 +1401,7 @@ Qed.
Lemma hsimpl_gc : forall H,
H ==> \GC.
Proof using.
intros. unfold heap_is_gc, heap_is_pack.
introv M. exists~ H.
Qed.
Proof using. intros. unfold heap_is_gc. introv M. exists~ H. Qed.
Lemma hsimpl_cancel_1 : forall H HA HR HT,
HT ==> HA \* HR -> H \* HT ==> HA \* (H \* HR).
......@@ -2410,8 +2407,8 @@ Proof using.
exists H1' (H2' \* H2) Q1'. splits.
rewrite star_assoc. exists~ h1 h2.
auto.
intros x. hchange (Qle' x). hextract as H'1.
hchange~ (Qle x). hextract as H'2. hsimpl.
intros x. hchange (Qle' x). hchange~ (Qle x).
set (H' := \GC) at 1 2. hsimpl.
apply~ local_erase.
Qed.
......@@ -2532,7 +2529,7 @@ Lemma local_weaken_gc_pre : forall B H' Q' (F:~~B) (H:hprop) Q,
Q' ===> Q ->
F H Q.
Proof using.
intros. apply* (@local_gc_pre \GC H'). hchange H2. hsimpl.
intros. apply* (@local_gc_pre_on (\GC) H'). hchange H2. hsimpl.
applys* local_weaken.
Qed.
......
......@@ -663,7 +663,7 @@ Lemma local_gc_pre_all : forall B Q (F:~~B) H,
is_local F ->
F \[] Q ->
F H Q.
Proof using. intros. apply* (@local_gc_pre H). hsimpl. Qed.
Proof using. intros. apply* (@local_gc_pre_on H). hsimpl. Qed.
Tactic Notation "xgc_all" :=
eapply local_gc_pre_all; [ try xlocal | ].
......@@ -1434,7 +1434,7 @@ Lemma xret_lemma : forall HG B (v:B) H (Q:B->hprop),
H ==> Q v \* HG ->
local (fun H' Q' => H' ==> Q' v) H Q.
Proof using.
introv W. eapply (@local_gc_pre HG).
introv W. eapply (@local_gc_pre_on HG).
auto. rewrite star_comm. apply W.
apply~ local_erase.
Qed.
......@@ -1575,8 +1575,8 @@ Ltac xif_core H :=
apply local_erase; split; intro H.
Ltac xif_base H cont :=
xif_check_post_instantiated tt;
xextract_check_not_needed tt;
xif_check_post_instantiated tt;
xuntag tag_if;
xif_core H;
cont tt.
......@@ -1653,7 +1653,7 @@ Proof using.
xextract. => HG. clear Hi. apply local_erase. introv LR HR.
gen bi. induction_wf IH: (int_downto_wf 0) mi. intros.
applys (rm HR). xlet. applys Hc. simpl. xif.
xseq. applys Hs. xextract. => b m' E. xapplys IH. applys E. hsimpl. hsimpl.
xseq. applys Hs. xextract. => b m' E. sapply IH. applys E.
xret_no_gc. subst Q. hsimpl.
Qed.
......@@ -2045,13 +2045,19 @@ Ltac xmatch_cases case_tactic :=
xmatch_case_core ltac:(fun _ =>
case_tactic ltac:(fun _ => xmatch_cases case_tactic)).
Ltac xmatch_check_post_instantiated tt :=
match cfml_postcondition_is_evar tt with
| true => fail 100 "xmatch requires a post-condition; use [xmatch Q] or [xpost Q] to set it."
| false => idtac
end.
Ltac xmatch_pre cont :=
xextract_check_not_needed tt;
xmatch_check_post_instantiated tt;
xuntag tag_match;
apply local_erase;
cont tt.
(* DEPRECATED
Ltac xmatch_cases case_tactic n :=
......
......@@ -95,7 +95,7 @@ Pervasives.cmj: Pervasives.ml $(CFML_MLV)
##############################################################
# Coq compilation rules
# Coq compilation rules for %_ml.v files
# We use Coq to produce a .vio file out of a .v file.
# We declare a dependency on the .cmj file, since %_ml.v is not known to "make".
......@@ -110,16 +110,24 @@ Array_ml.vio List_ml.vio: Pervasives_ml.vio
%_ml.vio: %.cmj
# Needed only when developing CFML. Ideally, should be removed.
@$(MAKE) -C $(CFML) --no-print-directory coqlib_quick_cf
@$(MAKE) -C $(CFML) --no-print-directory coqlib_quick_cf
$(COQC) -quick $(COQINCLUDE) $*_ml.v
##############################################################
# Coq compilation rules for %_proof.v files
# Stdlib.vo: Stdlib.v Pervasives_ml.vo Array_ml.vo List_ml.vo
# $(COQC) $(COQINCLUDE) Stdlib.v
# @$(MAKE) -C $(CFML) --no-print-directory coqlib_quick
# Stdlib.vio: Stdlib.v Pervasives_ml.vio Array_ml.vio List_ml.vio
# $(COQC) -quick $(COQINCLUDE) Stdlib.v
#%_proof.vo: %_proof.v
# @$(MAKE) -C $(CFML) --no-print-directory coqlib_quick
# $(COQC) $(COQINCLUDE) $<
#
V := $(MLV) Stdlib.v $(patsubst %.ml,%_proof.v,$(ML))
......
......@@ -27,7 +27,7 @@ let not x =
external ( == ) : 'a -> 'a -> bool = "%physical_eq"
let ( !== ) x y =
let ( != ) x y =
not (x == y)
......
......@@ -4,13 +4,77 @@ Require Import Pervasives_ml.
Ltac xgo_step tt :=
match cfml_get_tag tt with
| tag_ret => xret
| tag_apply => xapp
| tag_val => xval
| tag_fun => xfun
| tag_let => xlet
| tag_match => xmatch
| tag_case => xcase
| tag_fail => xfail
| tag_done => xdone
| tag_alias => xalias
| tag_seq => xseq
| tag_if => xif
| tag_for => fail 1
| tag_while => fail 1
| tag_assert => fail 1 (* TODO assert *)
| _ =>
match goal with
| |- _ ==> _ => first [ xsimpl | fail 2 ]
| |- _ ===> _ => first [ xsimpl | fail 2 ]
end
end.
(*
| tag_casewhen => fail 1
| tag_app_curried
| tag_pay*)
Ltac xgo_core tt :=
repeat (try (xextract; intros); xgo_step tt; instantiate).
Tactic Notation "xgo" :=
xgo_core tt.
Tactic Notation "xgo" "~" :=
xgo; xauto~.
Tactic Notation "xgo" "*" :=
xgo; xauto*.
Ltac xcf_core tt ::=
intros;
match goal with
| |- spec ?f ?n ?P => first [ xcf_core_spec f | xcf_fallback f | fail 2 ]
| |- curried ?n ?f /\ ?P => first [ xcf_core_spec f | xcf_fallback f | fail 2 ]
| |- app ?f ?xs ?H ?Q => first [ xcf_core_app f | xcf_fallback f | fail 2 ]
| |- tag tag_apply (app ?f ?xs ?H ?Q) => first [ xuntag tag_apply; xcf_core_app f | xcf_fallback f | fail 2 ]
| |- ?f = _ => first [ xcf_top_value f | xcf_fallback f | fail 2 ]
| _ => fail 1 "need to call [xcf f; => H], where [f] is the name of the definition"
end.
Ltac xcf_core_spec f ::=
xcf_find f;
let C := fresh "Curried" in
let H := fresh "Spec" in
intros [C H];
split;
[ clear H; try apply C (* curried part *)
| clear C; intros; xcf_core_app_exploit H ].
(************************************************************)
(** Boolean *)
Lemma not_spec : forall (a:bool),
app not [a] \[] \[= !a ].
Proof using.
xcf. skip.
xcf. xgo*.
Qed.
Hint Extern 1 (RegisterSpec not) => Provide not_spec.
......@@ -20,17 +84,18 @@ Hint Extern 1 (RegisterSpec not) => Provide not_spec.
(** Physical equality *)
Parameter infix_eq_eq__spec : curried 2%nat infix_eq_eq_ /\
infix_eq_eq__spec (a b:loc),
forall (a b:loc),
app infix_eq_eq_ [a b] \[] \[= isTrue (a = b) ].
Hint Extern 1 (RegisterSpec infix_eq_eq_) => Provide infix_eq_eq__spec.
Lemma infix_emark_eq__spec : curried 2%nat infix_emark_eq_ /\
infix_emark_eq__spec (a b:loc),
forall (a b:loc),
app infix_emark_eq_ [a b] \[] \[= isTrue (a <> b) ].
Proof using.
xcf. skip.
xcf. xgo*. rew_refl; xauto*.
Qed.
Hint Extern 1 (RegisterSpec infix_eq_eq_) => Provide infix_eq_eq__spec.
Hint Extern 1 (RegisterSpec infix_emark_eq_) => Provide infix_emark_eq__spec.
......@@ -38,7 +103,7 @@ Hint Extern 1 (RegisterSpec infix_emark_eq_) => Provide infix_emark_eq__spec.
(** Comparison *)
Definition eq_spec_for (A:Type) : curried 2%nat infix_eq_ /\
Definition eq_spec_for (A:Type) := curried 2%nat infix_eq_ /\
forall (a b:bool),
app infix_eq_ [a b] \[] \[= isTrue (a = b) ].
......@@ -48,7 +113,7 @@ Parameter eq_int_spec : eq_spec_for int.
Hint Extern 1 (RegisterSpec infix_eq_) => Provide eq_int_spec.
(* TODO: register several specs *)
Definition neq_spec_for (A:Type) : curried 2%nat infix_lt_gt_ /\
Definition neq_spec_for (A:Type) := curried 2%nat infix_lt_gt_ /\
forall (a b:bool),
app infix_lt_gt_ [a b] \[] \[= isTrue (a <> b) ].
......@@ -64,20 +129,23 @@ Hint Extern 1 (RegisterSpec infix_lt_gt_) => Provide neq_int_spec.
Lemma min_spec : forall (n m:int),
app min [n m] \[] \[= Coq.ZArith.BinInt.Zmin n m ].
Proof using.
xcf. skip.
xcf. xgo*.
{ rewrite~ Z.min_l. }
{ rewrite~ Z.min_r. math. }
Qed.
Lemma max_spec : forall (n m:int),
app max [n m] \[] \[= Coq.ZArith.BinInt.Zmax n m ].
Proof using.
xcf. skip.
xcf. xgo*.
{ rewrite~ Z.max_l. }
{ rewrite~ Z.max_r. math. }
Qed.
Hint Extern 1 (RegisterSpec min) => Provide min_spec.
Hint Extern 1 (RegisterSpec max) => Provide max_spec.
(************************************************************)
(** Boolean *)
......@@ -110,10 +178,10 @@ Parameter infix_star__spec : curried 2%nat infix_star_ /\
forall (n m:int),
app infix_star_ [n m] \[] \[= Coq.ZArith.BinInt.Zmult n m ].
Parameter infix_div__spec : curried 2%nat infix_div_ /\
Parameter infix_slash__spec : curried 2%nat infix_slash_ /\
forall (n m:int),
m <> 0 ->
app infix_div_ [n m] \[] \[= CFML.CFHeader.int_div n m ].
app infix_slash_ [n m] \[] \[= CFML.CFHeader.int_div n m ].
Parameter infix_mod__spec : curried 2%nat infix_mod_ /\
forall (n m:int),
......@@ -123,8 +191,8 @@ Parameter infix_mod__spec : curried 2%nat infix_mod_ /\
Hint Extern 1 (RegisterSpec infix_tilde_minus_) => Provide infix_tilde_minus__spec.
Hint Extern 1 (RegisterSpec infix_plus_) => Provide infix_plus__spec.
Hint Extern 1 (RegisterSpec infix_minus_) => Provide infix_minus__spec.
Hint Extern 1 (RegisterSpec infix_star_) => Provide infix_star__.spec
Hint Extern 1 (RegisterSpec infix_div_) => Provide infix_div__spec.
Hint Extern 1 (RegisterSpec infix_star_) => Provide infix_star__spec.
Hint Extern 1 (RegisterSpec infix_slash_) => Provide infix_slash__spec.
Hint Extern 1 (RegisterSpec infix_mod_) => Provide infix_mod__spec.
(* NOT NEEDED
......@@ -145,19 +213,21 @@ Notation "n `+ m" := (App infix_mod_ n m;)
Lemma succ_spec : forall (n:int),
app succ [n] \[] \[= n+1 ].
Proof using.
xcf. skip.
xcf. xgo*.
Qed.
Lemma pred_spec : forall (n:int),
app pred [n] \[] \[= n-1 ].
Proof using.
xcf. skip.
xcf. xgo*.
Qed.
Lemma abs_spec : forall (n:int),
app abs [n] \[] \[= Coq.ZArith.BinInt.Zabs n ].
app Pervasives_ml.abs [n] \[] \[= Coq.ZArith.BinInt.Zabs n ].
Proof using.
xcf. skip.
xcf. xgo.
{ rewrite~ Z.abs_eq. }
{ rewrite~ Z.abs_neq. math. }
Qed.
Hint Extern 1 (RegisterSpec succ) => Provide succ_spec.
......@@ -187,34 +257,35 @@ Proof using.
xcf. skip.
Qed.
Lemma infix_colon_equal__spec : forall a (v w:a) l,
app infix_colon_equal_ [l w] (l ~~> v) (# l ~~> w).
Lemma infix_colon_eq__spec : forall a (v w:a) l,
app infix_colon_eq_ [l w] (l ~~> v) (# l ~~> w).
Proof using.
xcf. skip.
Qed.
Hint Extern 1 (RegisterSpec ref) => Provide ref_spec.
Hint Extern 1 (RegisterSpec infix_emark_) => Provide infix_emark__spec.
Hint Extern 1 (RegisterSpec infix_colon_eq_) => Provide infix_colon_eq__spec.
Lemma incr_spec : forall (n:int) l,
app incr [l] (l ~~> n) (# l ~~> (n+1)).
Proof using.
xcf. skip.
xcf. xgo~.
Qed.
Lemma decr_spec : forall (n:int) l,
app decr [l] (l ~~> n) (# l ~~> (n+1)).
app decr [l] (l ~~> n) (# l ~~> (n-1)).
Proof using.
xcf. skip.
xcf. xgo~.
Qed.
Hint Extern 1 (RegisterSpec ref) => Provide ref_spec.
Hint Extern 1 (RegisterSpec infix_emark_) => Provide infix_emark__spec.
Hint Extern 1 (RegisterSpec infix_colon_equal_) => Provide infix_colon_equal__spec.
Hint Extern 1 (RegisterSpec incr) => Provide incr_spec.
Hint Extern 1 (RegisterSpec decr) => Provide decr_spec.
Notation "`! r" := (App infix_emark_ r;)
(at level 69, no associativity, format "`! r") : app_scope.
Notation "r `:= x" := (App infix_colon_equal_ r x;)
Notation "r `:= x" := (App infix_colon_eq_ r x;)
(at level 69, no associativity) : app_scope.
Open Scope app_scope.
......@@ -224,15 +295,15 @@ Open Scope app_scope.
(** Pairs *)
Lemma fst_spec : forall A B (x:A) (y:B),
app fst [x y] \[] \[= x].
app fst [(x,y)] \[] \[= x].
Proof using.
xcf.
xcf. xgo~.
Qed.
Lemma snd_spec : forall A B (x:A) (y:B),
app snd [x y] \[] \[= y].
app snd [(x,y)] \[] \[= y].
Proof using.
xcf.
xcf. xgo~.
Qed.
Hint Extern 1 (RegisterSpec fst) => Provide fst_spec.
......@@ -245,7 +316,7 @@ Hint Extern 1 (RegisterSpec snd) => Provide snd_spec.
Lemma ignore_spec :
app ignore [tt] \[] \[= tt].
Proof using.
xcf.
xcf. xgo~.
Qed.
Hint Extern 1 (RegisterSpec ignore) => Provide ignore_spec.
......
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