Commit 25b8b2fc authored by charguer's avatar charguer

cp

parent 39594924
......@@ -2,119 +2,16 @@ Set Implicit Arguments.
(* LibInt LibWf *)
Require Import CFLib.
Require Import Demo_ml.
Require Import Stdlib.
(*
Require Import Pervasives_ml. (* optional, improves display of, e.g. [incr] *)
Print TLC.LibOrder.ge_from_le.
Definition f := (fun x_ y_ : int => TLC.LibReflect.isTrue (x_ >= y_)).
Print f.
Locate list.
Definition g := .
(fun x_ y_ : int => TLC.LibReflect.isTrue (TLC.LibOrder.lt (TLC.LibOrder.ge_from_le TLC.LibInt.le) x_ y_)).
"Pervasives.<=", (Primitive_binary_only_numbers, "(fun x_ y_ : int => TLC.LibReflect.isTrue (@TLC.LibOrder.le int TLC.LibInt.le_int_inst x_ y_))");
"Pervasives.>", (Primitive_binary_only_numbers, "(fun x_ y_ : int => TLC.LibReflect.isTrue (@TLC.LibOrder.gt int (TLC.LibOrder.gt_from_le TLC.LibInt.le_int_inst) x_ y_))");
"Pervasives.>=", (Primitive_binary_only_numbers, "(fun x_ y_ : int => TLC.LibReflect.isTrue (@TLC.LibOrder.ge int (TLC.LibOrder.ge_from_le TLC.LibInt.le_int_inst) x_ y_))");
Print f.
Locate ge_from_le.
Locate le_int_inst.
Definition g :=
(fun x_ y_ : int => TLC.LibReflect.isTrue (x_ <> y_))..
Print g.
Locate le_int_inst.
(*Open Scope tag_scope.*)
Lemma if_true_spec :
app if_true [tt] \[] \[= 1].
Proof using.
xcf. xif. xret. xsimpl. auto.
Qed.
Lemma if_term_spec :
app if_term [tt] \[] \[= 1].
Proof using.
xcf. xfun. xapp. xret. xextracts.
xif. xrets~.
Qed.
Lemma if_else_if_spec :
app if_else_if [tt] \[] \[= 0].
Proof using.
xcf. xfun (fun f => forall (x:int), app f [x] \[] \[= false]).
{ xrets~. }
xapps. xif. xapps. xif. xrets~.
Qed.
Definition Ref a (v:a) (l:loc) := (* TODO: change *)
heap_is_single l v.
Notation "l '~~>' v" := (hdata (Ref v) l)
(at level 32, no associativity) : heap_scope.
Notation "'app_keep' f xs H Q" :=
(app f xs H%h (Q \*+ H))
(at level 80, f at level 0, xs at level 0, H at level 0) : charac.
Parameter ref_spec : forall a (v:a),
app ref [v] \[] (fun l => l ~~> v).
Parameter get_spec : forall a (v:a) l,
app_keep get [l] (l ~~> v) \[= v].
(* Print get_spec. *)
(* keep (app get [l]) (l ~~> v) \[= v].*)
Parameter set_spec : forall a (v w:a) l,
app set [l w] (l ~~> v) (# l ~~> w).
Parameter incr_spec : forall (n:int) l,
app incr [l] (l ~~> n) (# l ~~> (n+1)).
Parameter decr_spec : forall (n:int) l,
app decr [l] (l ~~> n) (# l ~~> (n+1)).
Hint Extern 1 (RegisterSpec ref) => Provide ref_spec.
Hint Extern 1 (RegisterSpec get) => Provide get_spec.
Hint Extern 1 (RegisterSpec set) => Provide set_spec.
Hint Extern 1 (RegisterSpec incr) => Provide incr_spec.
Hint Extern 1 (RegisterSpec decr) => Provide decr_spec.
Notation "`! l" := (App infix_emark_ l;)
(at level 69, no associativity, format "`! l") : machine_op_scope.
Lemma if_then_no_else_spec : forall (b:bool),
app if_then_no_else [b] \[] \[= 1].
Proof using.
xcf. xapp. dup 3.
{ xseq. xif. { xapp. } { xrets. skip. (* stuck *) } skip. }
{ xseq....
(* TODO: raise error message on xif *)
Qed.
......@@ -236,7 +133,7 @@ Lemma let_val_poly_spec :
app let_val_poly [tt] \[] \[= 3].
Proof using.
xcf. dup 3.
xval. xret. xsimpl. auto.
xval. x ret. xsimpl. auto.
xval as r. xrets~.
xvals. xrets~.
Qed.
......@@ -665,6 +562,38 @@ Qed.
(* ** Conditionals *)
Lemma if_true_spec :
app if_true [tt] \[] \[= 1].
Proof using.
xcf. xif. xret. xsimpl. auto.
Qed.
Lemma if_term_spec :
app if_term [tt] \[] \[= 1].
Proof using.
xcf. xfun. xapp. xret. xextracts.
xif. xrets~.
Qed.
Lemma if_else_if_spec :
app if_else_if [tt] \[] \[= 0].
Proof using.
xcf. xfun (fun f => forall (x:int), app f [x] \[] \[= false]).
{ xrets~. }
xapps. xif. xapps. xif. xrets~.
Qed.
Lemma if_then_no_else_spec : forall (b:bool),
app if_then_no_else [b] \[] (fun x => \[ x >= 0]).
Proof using.
xcf. xapp.
xseq. xif (Hexists n, \[n >= 0] \* r ~~> n).
{ xapp. xsimpl. math. }
{ xrets. math. }
{ (*xclean.*) xextract ;=>> P. xapp. xextracts. xsimpl. math. }.
Qed.
(********************************************************************)
(* ** Records *)
......
......@@ -383,7 +383,7 @@ let infix_name_symbols =
'-', "minus";
'.', "dot";
'/', "slash";
':', "column";
':', "colon";
'<', "lt";
'=', "eq";
'>', "gt";
......
......@@ -160,6 +160,12 @@ Notation "'app' f xs" :=
(at level 80, f at level 0, xs at level 0) : charac.
Open Scope charac.
(** [app_keep f xs H Q] is the same as [app f xs H (Q \*+ H)] *)
Notation "'app_keep' f xs H Q" :=
(app f xs H%h (Q \*+ H))
(at level 80, f at level 0, xs at level 0, H at level 0) : charac.
Definition demo_arglist :=
forall f (xs:list int) (x y:int) B H (Q:B->hprop),
......
......@@ -57,7 +57,7 @@ Tactic Notation "=>" simple_intropattern(I1) simple_intropattern(I2)
Ltac intro_nondeps_aux is_already_hnf :=
match goal with
| |- (_ -> _) => idtac
| |- (?P -> ?Q) => idtac
| |- (Inhab _) -> _ => intro; intro_nondeps_aux true
| |- (forall _,_) => intros ?; intro_nondeps_aux true
| |- _ =>
......@@ -479,9 +479,14 @@ Tactic Notation "xpre" constr(H) :=
(** [xpost] applies to a goal of the form [F H Q] and
allows to weaken the pre-condition [Q].
It produces [F ?H' Q] and [H ==> ?H' \* \GC],
where [Hexists HG, HG] can be instantiated with garbage
to collect. *)
It produces [F H ?Q'] and [?Q' ==> ?Q \* \GC].
[xpost Q'] applies to a goal of the form [F H Q]
and leaves the goals [F H Q'] and [Q' ===> Q].
[xpost H'] is a shorthand for [xpost (#H')].
*)
(* Lemma used by [xpost] *)
......@@ -503,8 +508,18 @@ Lemma fix_post : forall (B:Type) (Q':B->hprop) (F:~~B) (H:hprop) Q,
F H Q.
Proof. intros. apply* local_weaken. Qed.
Ltac xpost_core Q :=
let Q' := match type of Q with
| hprop => constr:(fun (_:unit) => Q)
| _ => constr:(Q)
end in
match cfml_postcondition_is_evar tt with
| true => apply (@fix_post _ Q'); [ try xlocal | | apply rel_le_refl ]
| false => apply (@fix_post _ Q'); [ try xlocal | | ]
end.
Tactic Notation "xpost" constr(Q) :=
apply (@fix_post _ Q); [ try xlocal | | try apply rel_le_refl ].
xpost_core Q.
(*--------------------------------------------------------*)
......@@ -1507,19 +1522,20 @@ Tactic Notation "xrets" "*" :=
It leaves two subgoals [F1 H Q] under the assumption [v=true]
and [F2 H Q] under the assumption [v=false].
If [Q] is not instantiated, it will automatically be instantiated
with [if v then ?Q1 else ?Q2]. Without this behavior, when
the post-condition is not instantiated, then the post-condition will
be inferred when solving the first branch, and it will very likely
not fit the second branch.
Sometimes it is preferable to specify [Q] explicitly, calling [xif Q].
The tactic [xif] attemps to simplify or prove false from obvious
contradictions. To disable this behaviour, use [xif_no_simpl]
contradictions. To disable this behaviour, use [xif_no_simpl].
[xif Q'] allows to specify the post-condition. It is useful
when [Q] is an evar. If the post-condition is an evar and
[xif] is called without argument, the post-condition will
be inferred when solving the first branch, and it will thus
very likely not fit the second branch.
when [Q] is an evar.
Remark: [xif Q'] is equivalent to [xpost Q'; xif].
TODO: have a runtime check that the post is instantiated, else fail
(and same for xmatch).
[xif as X] allows to name [X] the hypothesis [v=true] or [v=false].
[xif Q' as X] is also valid syntax. *)
......@@ -1534,12 +1550,36 @@ Ltac xif_post H := (* todo: cleanup *)
try fix_bool_of_known tt;
try (check_noevar_hyp H; rew_reflect in H; rew_logic in H).
(* DEPRECATED
Lemma xif_instantiate_lemma :
forall B (Q1 Q2:B->hprop) H (v:bool) (F1 F2:hprop->(B->hprop)->Prop),
(If_ v Then F1 Else F2)%charac H (if v then Q1 else Q2) ->
(If_ v Then F1 Else F2)%charac H (fun x => if v then Q1 x else Q2 x).
Proof using. introv M. eapply local_weaken_post. xlocal. apply M. intros x. case_if~. Qed.
Ltac xif_instantiate_post_if_needed tt :=
match cfml_postcondition_is_evar tt with
| true => apply xif_instantiate_lemma
| false => idtac
end.
*)
Ltac xif_check_post_instantiated tt :=
match cfml_postcondition_is_evar tt with
| true => fail 100 "xif requires a post-condition; use [xif Q] or [xpost Q] to set it."
| false => idtac
end.
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_core H; cont tt.
xuntag tag_if;
xif_core H;
cont tt.
Ltac xif_then H :=
xif_base H ltac:(fun _ => xif_post H).
......@@ -1568,11 +1608,18 @@ Tactic Notation "xif_no_simpl" :=
It automatically calls [xclean] on the remaining goal, to help.
[xfail_no_clean] is also available, to prevent [xclean]
from being called. *)
Variants:
Tactic Notation "xfail_no_clean" :=
- [xfail_no_clean] prevents [xclean] from being called.
- [xfail C] is a shorthand for [xfail; false C].
*)
Ltac xfail_core tt :=
xextract_check_not_needed tt; xuntag tag_fail; apply local_erase.
Tactic Notation "xfail_no_clean" :=
xfail_core tt.
Tactic Notation "xfail" :=
xfail_no_clean; xclean.
Tactic Notation "xfail" "~" :=
......@@ -1580,10 +1627,12 @@ Tactic Notation "xfail" "~" :=
Tactic Notation "xfail" "*" :=
xfail; xauto*.
(** [xfail C] is a shorthand for [xfail; false C]. *)
Tactic Notation "xfail" constr(C) :=
xfail; false C.
Tactic Notation "xfail" "~" constr(C) :=
xfail C; xauto~.
Tactic Notation "xfail" "*" constr(C) :=
xfail C; xauto*.
(*--------------------------------------------------------*)
......
......@@ -61,8 +61,8 @@ all: cmj vo
quick: cmj vio
cmj: $(CMJ)
vo: $(MLVO)
vio: $(MLVIO)
vo: $(MLVO) Stdlib.vo
vio: $(MLVIO) Stdlib.vio
tools:
@$(MAKE) -C $(CFML) --no-print-directory tools
......@@ -114,8 +114,16 @@ Array_ml.vio List_ml.vio: Pervasives_ml.vio
$(COQC) -quick $(COQINCLUDE) $*_ml.v
# V := $(MLV)
# include $(CFML)/lib/make/Makefile.coq
# Stdlib.vo: Stdlib.v Pervasives_ml.vo Array_ml.vo List_ml.vo
# $(COQC) $(COQINCLUDE) Stdlib.v
# Stdlib.vio: Stdlib.v Pervasives_ml.vio Array_ml.vio List_ml.vio
# $(COQC) -quick $(COQINCLUDE) Stdlib.v
#
V := $(MLV) Stdlib.v $(patsubst %.ml,%_proof.v,$(ML))
include $(CFML)/lib/make/Makefile.coq
##############################################################
......
......@@ -95,15 +95,11 @@ type 'a ref = { mutable contents : 'a }
let ref x =
{ contents = x }
let get r =
r.contents
let (!) r =
r.contents
let (!) = get
let set r x =
r.contents <- x
let (:=) = set
let (:=) r x =
r.contents <- x
let incr r =
r := !r + 1
......@@ -111,12 +107,6 @@ let incr r =
let decr r =
r := !r - 1
(** [ref_free r] is a logical free operation, useful for translating
to languages without garbage collection *)
let ref_free r =
()
(** [ref_unsafe_set r x] allows to modifies the contents of a reference *)
(* unsupported currently, needs explicit types
let ref_unsafe_set r x =
......
Set Implicit Arguments.
Require Import CFLib.
Require Import Pervasives_ml.
(************************************************************)
(** Boolean *)
Lemma not_spec : forall (a:bool),
app not [a] \[] \[= !a ].
Proof using.
xcf. skip.
Qed.
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),
app infix_eq_eq_ [a b] \[] \[= isTrue (a = b) ].
Lemma infix_emark_eq__spec : curried 2%nat infix_emark_eq_ /\
infix_emark_eq__spec (a b:loc),
app infix_emark_eq_ [a b] \[] \[= isTrue (a <> b) ].
Proof using.
xcf. skip.
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.
(************************************************************)
(** Comparison *)
Definition eq_spec_for (A:Type) : curried 2%nat infix_eq_ /\
forall (a b:bool),
app infix_eq_ [a b] \[] \[= isTrue (a = b) ].
Parameter eq_bool_spec : eq_spec_for bool.
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_ /\
forall (a b:bool),
app infix_lt_gt_ [a b] \[] \[= isTrue (a <> b) ].
Parameter neq_bool_spec : neq_spec_for bool.
Parameter neq_int_spec : neq_spec_for int.
Hint Extern 1 (RegisterSpec infix_lt_gt_) => Provide neq_int_spec.
(* LATER: give specification for partially applied comparison operators *)
Lemma min_spec : forall (n m:int),
app min [n m] \[] \[= Coq.ZArith.BinInt.Zmin n m ].
Proof using.
xcf. skip.
Qed.
Lemma max_spec : forall (n m:int),
app max [n m] \[] \[= Coq.ZArith.BinInt.Zmax n m ].
Proof using.
xcf. skip.
Qed.
Hint Extern 1 (RegisterSpec min) => Provide min_spec.
Hint Extern 1 (RegisterSpec max) => Provide max_spec.
(************************************************************)
(** Boolean *)
Parameter infix_bar_bar__spec : forall (a b:bool),
app infix_bar_bar_ [a b] \[] \[= a && b ].
Parameter infix_amp_amp__spec : forall (a b:bool),
app infix_amp_amp_ [a b] \[] \[= a || b ].
Hint Extern 1 (RegisterSpec infix_bar_bar_) => Provide infix_bar_bar__spec.
Hint Extern 1 (RegisterSpec infix_amp_amp_) => Provide infix_amp_amp__spec.
(************************************************************)
(** Integer *)
Parameter infix_tilde_minus__spec : curried 1%nat infix_tilde_minus_ /\
forall (n:int),
app infix_tilde_minus_ [n] \[] \[= Coq.ZArith.BinInt.Zopp n ].
Parameter infix_plus__spec : curried 2%nat infix_plus_ /\
forall (n m:int),
app infix_plus_ [n m] \[] \[= Coq.ZArith.BinInt.Zplus n m ].
Parameter infix_minus__spec : curried 2%nat infix_minus_ /\
forall (n m:int),
app infix_minus_ [n m] \[] \[= Coq.ZArith.BinInt.Zminus n m ].
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_ /\
forall (n m:int),
m <> 0 ->
app infix_div_ [n m] \[] \[= CFML.CFHeader.int_div n m ].
Parameter infix_mod__spec : curried 2%nat infix_mod_ /\
forall (n m:int),
m <> 0 ->
app infix_mod_ [n m] \[] \[= CFML.CFHeader.int_mod n m ].
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_mod_) => Provide infix_mod__spec.
(* NOT NEEDED
Notation "`~- n" := (App infix_tilde_minus_ n;)
(at level 69, no associativity) : app_scope.
Notation "n `+ m" := (App infix_plus_ n m;)
(at level 69, no associativity) : app_scope.
Notation "n `+ m" := (App infix_minus_ n m;)
(at level 69, no associativity) : app_scope.
Notation "n `+ m" := (App infix_star_ n m;)
(at level 69, no associativity) : app_scope.
Notation "n `+ m" := (App infix_div_ n m;)
(at level 69, no associativity) : app_scope.
Notation "n `+ m" := (App infix_mod_ n m;)
(at level 69, no associativity) : app_scope.
*)
Lemma succ_spec : forall (n:int),
app succ [n] \[] \[= n+1 ].
Proof using.
xcf. skip.
Qed.
Lemma pred_spec : forall (n:int),
app pred [n] \[] \[= n-1 ].
Proof using.
xcf. skip.
Qed.
Lemma abs_spec : forall (n:int),
app abs [n] \[] \[= Coq.ZArith.BinInt.Zabs n ].
Proof using.
xcf. skip.
Qed.
Hint Extern 1 (RegisterSpec succ) => Provide succ_spec.
Hint Extern 1 (RegisterSpec pred) => Provide pred_spec.
Hint Extern 1 (RegisterSpec abs) => Provide abs_spec.
(************************************************************)
(** References *)
Definition Ref a (v:a) (l:loc) := (* TODO: change *)
heap_is_single l v.
Notation "l '~~>' v" := (hdata (Ref v) l)
(at level 32, no associativity) : heap_scope.
Lemma ref_spec : forall a (v:a),
app ref [v] \[] (fun l => l ~~> v).
Proof using.
xcf. skip.
Qed.
Lemma infix_emark__spec : forall a (v:a) l,
app_keep infix_emark_ [l] (l ~~> v) \[= v].
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).
Proof using.
xcf. skip.
Qed.
Lemma incr_spec : forall (n:int) l,
app incr [l] (l ~~> n) (# l ~~> (n+1)).
Proof using.
xcf. skip.
Qed.
Lemma decr_spec : forall (n:int) l,
app decr [l] (l ~~> n) (# l ~~> (n+1)).
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_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;)
(at level 69, no associativity) : app_scope.
Open Scope app_scope.
(************************************************************)
(** Pairs *)
Lemma fst_spec : forall A B (x:A) (y:B),
app fst [x y] \[] \[= x].
Proof using.
xcf.
Qed.
Lemma snd_spec : forall A B (x:A) (y:B),
app snd [x y] \[] \[= y].
Proof using.
xcf.
Qed.
Hint Extern 1 (RegisterSpec fst) => Provide fst_spec.
Hint Extern 1 (RegisterSpec snd) => Provide snd_spec.
(************************************************************)
(** Unit *)
Lemma ignore_spec :
app ignore [tt] \[] \[= tt].
Proof using.
xcf.
Qed.
Hint Extern 1 (RegisterSpec ignore) => Provide ignore_spec.
(************************************************************)
(** Float *)
(* TODO *)
(************************************************************)
(************************************************************)
(************************************************************)
(* FUTURE
(*------------------------------------------------------------------*)
(* ** References *)
......@@ -52,52 +320,6 @@ Implicit Arguments unfocus_ref [a A].
(* does not really work? *)
Notation "l '~~>' v" := (hdata (@Ref _ _ (@Id _) v) l)
(at level 32, no associativity).
(************************************************************)
(** References *)
Parameter caml_ref_spec : forall a,
Spec caml_ref (v:a) |R>>
R \[] (~~> v).
Parameter caml_get_spec : forall a,
Spec caml_get (l:loc) |R>>
forall (v:a), keep R (l ~~> v) (fun x => \[x = v]).
Parameter caml_set_spec : forall a,
Spec caml_set (l:loc) (v:a) |R>>
forall (v':a), R (l ~> Ref Id v') (# l ~> Ref Id v).
Parameter caml_sset_spec : forall a a