Commit 87e1c36f authored by charguer's avatar charguer
Browse files

xwhile

parent 5546d871
xwhile: error reporting when arguments don't have the right types.
notation "# H" uniquement lorsque H est au type hprop.
rename xextract to xpull; and xgen to xpush.
todo: model K/E -> list V
comparable_type A || comparable_value x || comparable_value y
x = y : A
comparable_value x || comparable_value y
x = y : A
forall x : int, comparable_value x
mettre trop de let pour les fonctions builtin;
xuntag_goal. => dans xcf.
CFPrint.tag
app_def
infix_eq_
assume
......@@ -7,6 +38,8 @@ MAJOR TODAY
- loops
- for downto
MAJOR NEXT
- record with
......
......@@ -2546,13 +2546,13 @@ Tactic Notation "xfor_inv" constr(I) :=
(************************************************************)
(* ** [xfocus] *)
(* ** [xopen] *)
(* e.g.
Hint Extern 1 (Register focus (Tree _)) =>
Provide tree_focus_contents.
then [xfocus t] or [xfocus t as I1 I2]
then [xopen t] or [xopen t as I1 I2]
*)
......@@ -2567,79 +2567,79 @@ Ltac get_refocus_args tt :=
Ltac get_refocus_constr_in H t :=
match H with context [ t ~> ?T ] => constr:(T) end.
Ltac xfocus_constr t :=
Ltac xopen_constr t :=
match get_refocus_args tt with (?H1,?H2) =>
get_refocus_constr_in H1 t end.
Ltac xfocus_core t :=
let C1 := xfocus_constr t in
Ltac xopen_core t :=
let C1 := xopen_constr t in
ltac_database_get database_spec_focus C1;
let K := fresh "TEMP" in
intros K; xchange (K t); clear K.
Ltac xfocus_show t :=
let C1 := xfocus_constr t in
Ltac xopen_show t :=
let C1 := xopen_constr t in
pose C1; try ltac_database_get database_spec_focus C1; intros.
Tactic Notation "xfocus" constr(t) :=
xfocus_core t.
Tactic Notation "xfocus" "~" constr(t) :=
xfocus t; auto_tilde.
Tactic Notation "xfocus" "*" constr(t) :=
xfocus t; auto_star.
Tactic Notation "xfocus" constr(t) "as" simple_intropattern(I1) :=
xfocus t; xextract as I1.
Tactic Notation "xfocus" constr(t) "as" simple_intropattern(I1) simple_intropattern(I2) :=
xfocus t; xextract as I1 I2.
Tactic Notation "xfocus" constr(t) "as" simple_intropattern(I1) simple_intropattern(I2)
Tactic Notation "xopen" constr(t) :=
xopen_core t.
Tactic Notation "xopen" "~" constr(t) :=
xopen t; auto_tilde.
Tactic Notation "xopen" "*" constr(t) :=
xopen t; auto_star.
Tactic Notation "xopen" constr(t) "as" simple_intropattern(I1) :=
xopen t; xextract as I1.
Tactic Notation "xopen" constr(t) "as" simple_intropattern(I1) simple_intropattern(I2) :=
xopen t; xextract as I1 I2.
Tactic Notation "xopen" constr(t) "as" simple_intropattern(I1) simple_intropattern(I2)
simple_intropattern(I3) :=
xfocus t; xextract as I1 I2 I3.
Tactic Notation "xfocus" constr(t) "as" simple_intropattern(I1) simple_intropattern(I2)
xopen t; xextract as I1 I2 I3.
Tactic Notation "xopen" constr(t) "as" simple_intropattern(I1) simple_intropattern(I2)
simple_intropattern(I3) simple_intropattern(I4) :=
xfocus t; xextract as I1 I2 I3 I4.
Tactic Notation "xfocus" constr(t) "as" simple_intropattern(I1) simple_intropattern(I2)
xopen t; xextract as I1 I2 I3 I4.
Tactic Notation "xopen" constr(t) "as" simple_intropattern(I1) simple_intropattern(I2)
simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) :=
xfocus t; xextract as I1 I2 I3 I4 I5.
xopen t; xextract as I1 I2 I3 I4 I5.
(************************************************************)
(* ** [xunfocus] *)
(* ** [xclose] *)
(** e.g.
Hint Extern 1 (Register unfocus (Ref Id (MNode _ _ _))) =>
Provide tree_node_unfocus.
then [xunfocus t] or [xunfocus t1 t2 t3]
then [xclose t] or [xclose t1 t2 t3]
*)
Ltac xunfocus_constr t :=
Ltac xclose_constr t :=
match get_refocus_args tt with (?H1,?H2) =>
get_refocus_constr_in H1 t end.
Ltac xunfocus_core t :=
let C1 := xunfocus_constr t in
Ltac xclose_core t :=
let C1 := xclose_constr t in
ltac_database_get database_spec_unfocus C1;
let K := fresh "TEMP" in
intros K; xchange (K t); clear K.
Ltac xunfocus_show t :=
let C1 := xunfocus_constr t in
Ltac xclose_show t :=
let C1 := xclose_constr t in
pose C1; try ltac_database_get database_spec_unfocus C1; intros.
Tactic Notation "xunfocus" constr(t) :=
xunfocus_core t.
Tactic Notation "xunfocus" "~" constr(t) :=
xunfocus t; auto_tilde.
Tactic Notation "xunfocus" "*" constr(t) :=
xunfocus t; auto_star.
Tactic Notation "xunfocus" constr(t1) constr(t2) :=
xunfocus t1; xunfocus t2.
Tactic Notation "xunfocus" constr(t1) constr(t2) constr(t3) :=
xunfocus t1; xunfocus t2 t3.
Tactic Notation "xunfocus" constr(t1) constr(t2) constr(t3) constr(t4) :=
xunfocus t1; xunfocus t2 t3 t4.
Tactic Notation "xclose" constr(t) :=
xclose_core t.
Tactic Notation "xclose" "~" constr(t) :=
xclose t; auto_tilde.
Tactic Notation "xclose" "*" constr(t) :=
xclose t; auto_star.
Tactic Notation "xclose" constr(t1) constr(t2) :=
xclose t1; xclose t2.
Tactic Notation "xclose" constr(t1) constr(t2) constr(t3) :=
xclose t1; xclose t2 t3.
Tactic Notation "xclose" constr(t1) constr(t2) constr(t3) constr(t4) :=
xclose t1; xclose t2 t3 t4.
......
......@@ -131,12 +131,12 @@ Hint Resolve tree_sub_wf : wf.
(***--------------------------------------------------------***)
Hint Extern 1 (Register focus (Tree _)) => Provide tree_focus.
Hint Extern 1 (Register unfocus (Ref Id (MNode _ _ _))) => Provide tree_node_unfocus.
Hint Extern 1 (Register unfocus (Ref Id MLeaf)) => Provide tree_leaf_unfocus.
Hint Extern 1 (Register xopen (Tree _)) => Provide tree_focus.
Hint Extern 1 (Register xclose (Ref Id (MNode _ _ _))) => Provide tree_node_unfocus.
Hint Extern 1 (Register xclose (Ref Id MLeaf)) => Provide tree_leaf_unfocus.
Hint Extern 1 (Register focus (Stree _)) => Provide Stree_focus.
Hint Extern 1 (Register unfocus (Tree _)) => Provide Stree_unfocus.
Hint Extern 1 (Register xopen (Stree _)) => Provide Stree_focus.
Hint Extern 1 (Register xclose (Tree _)) => Provide Stree_unfocus.
Hint Constructors stree.
......@@ -154,12 +154,12 @@ Lemma fill_root_spec :
(fun (_:unit) => Hexists T', \[stree T' (E \- \{x})] \* t ~> Tree T').
Proof using.
xinduction_heap tree_sub. xcf. intros t T IH T1 x T2 E IE ET.
xfocus t as v. xapps. xmatch.
xopen t as v. xapps. xmatch.
xextract as ET'. xfail. false.
xextract as T1' T2' EQ. inverts EQ. xfocus t2 as v2.
xextract as T1' T2' EQ. inverts EQ. xopen t2 as v2.
xapps. xmatch.
xextract as ET2'. subst. xfocus t1 as v1. xapps. xapps.
intros _. xextract. xunfocus t1. xsimpl.
xextract as ET2'. subst. xopen t1 as v1. xapps. xapps.
intros _. xextract. xclose t1. xsimpl.
Qed.
......@@ -171,15 +171,15 @@ Lemma delete_spec_ind :
(fun (_:unit) => Hexists T', \[stree T' (E \- \{x})] \* t ~> Tree T').
Proof using.
xinduction_heap tree_sub. xcf. intros x t T IH E IE.
xfocus t. xextract as v. xapps. xmatch.
xextract as HT. subst. inverts IE. xret. xunfocus t. xsimpl*. skip. (* todo *)
xopen t. xextract as v. xapps. xmatch.
xextract as HT. subst. inverts IE. xret. xclose t. xsimpl*. skip. (* todo *)
xextract as T1 T2 HT. subst T. inverts IE as IE1 IE2 F1 F2 EQ.
xif. xapps*. xextract as T' HT'. xunfocus t. xsimpl*.
xif. xapps*. xextract as T' HT'. xclose t. xsimpl*.
constructors~. skip. subst E. skip. (* mk no x in E2,y *)
xif. xapps*. xextract as T' HT'. xunfocus t. xsimpl*.
xif. xapps*. xextract as T' HT'. xclose t. xsimpl*.
constructors~. skip. subst E. skip. (* mk no x in E1,y *)
asserts Exy: (x = y). math.
xapps. xunfocus t.
xapps. xclose t.
xsimpl*.
Qed.
......@@ -190,12 +190,12 @@ Lemma delete_spec :
(fun (_:unit) => t ~> Stree (E \- \{x})).
Proof using.
xcf. intros.
xfocus t. xextract as T HT1. xfocus t as v. xapps. xmatch.
{ xret. xextracts. xunfocus t. xunfocus* t. xsimpl. inverts~ HT1. skip. (* todo *) }
xopen t. xextract as T HT1. xopen t as v. xapps. xmatch.
{ xret. xextracts. xclose t. xclose* t. xsimpl. inverts~ HT1. skip. (* todo *) }
{ xextract as T1 T2 ET. xif.
{ xapps.
xret. xextract as T1 T2 ET. subst T. xunfocus t. xunfocus* t. xsimpl.
xret. xextract as T1 T2 ET. subst T. xclose t. xclose* t. xsimpl.
inverts HT1. subst. skip. (* todo *) }
Qed.
......@@ -232,9 +232,9 @@ Lemma is_empty_spec :
(fun (b:bool) => t ~> Stree E \* \[b = isTrue(E = \{})]).
Proof using.
xcf. intros.
xfocus t. xextract as T HT1. xfocus t as v. xapps. xmatch.
{ xret. xextracts. xunfocus t. xunfocus* t. xsimpl. inverts~ HT1. }
{ xret. xextract as T1 T2 ET. subst T. xunfocus t. xunfocus* t. xsimpl.
xopen t. xextract as T HT1. xopen t as v. xapps. xmatch.
{ xret. xextracts. xclose t. xclose* t. xsimpl. inverts~ HT1. }
{ xret. xextract as T1 T2 ET. subst T. xclose t. xclose* t. xsimpl.
inverts HT1. subst. skip. (* todo *) }
Qed.
......@@ -251,13 +251,13 @@ Lemma add_spec_ind :
(fun (_:unit) => Hexists T', \[stree T' (E \u \{x})] \* t ~> Tree T').
Proof using.
xinduction_heap (tree_sub). xcf. intros x t T IH E IE.
xfocus t. xextract as v. xapps. xmatch.
xopen t. xextract as v. xapps. xmatch.
xextract as HT. subst. inverts IE. xapp as t1. xapp as t2. xapps.
intros _. xunfocus t1 t2 t. xsimpl*.
intros _. xclose t1 t2 t. xsimpl*.
xextract as T1 T2 HT. subst T. inverts IE as IE1 IE2 F1 F2 EQ.
xif. xapps*. xextract as T' HT'. xunfocus t. xsimpl*.
xif. xapps*. xextract as T' HT'. xunfocus t. xsimpl*.
xret. xunfocus t. asserts_rewrite (x = y). math. xsimpl*.
xif. xapps*. xextract as T' HT'. xclose t. xsimpl*.
xif. xapps*. xextract as T' HT'. xclose t. xsimpl*.
xret. xclose t. asserts_rewrite (x = y). math. xsimpl*.
Qed.
Lemma add_spec :
......@@ -267,8 +267,8 @@ Lemma add_spec :
(fun (_:unit) => t ~> Stree (E \u \{x})).
Proof using.
xweaken add_spec_ind. simpl. intros x t R HR S1 E.
xfocus t as T1 HT1. xapply* S1. xsimpl. xextract as T' HT'.
xunfocus* t. xsimpl*.
xopen t as T1 HT1. xapply* S1. xsimpl. xextract as T' HT'.
xclose* t. xsimpl*.
Qed.
......@@ -282,22 +282,22 @@ Lemma search_spec_ind :
(fun b => \[b = isTrue (x \in E)] \* t ~> Tree T).
Proof using.
xinduction_heap (tree_sub). xcf. intros x t T IH E IE.
xfocus t. xextract as v. xapps. xmatch.
xextract as HT. subst. inverts IE. xret. xunfocus t.
xopen t. xextract as v. xapps. xmatch.
xextract as HT. subst. inverts IE. xret. xclose t.
xsimpl. applys* @notin_empty. typeclass.
xextract as T1 T2 HT. subst. inverts IE as IE1 IE2 F1 F2 EQ.
xif. xapps*. intros b.
xextracts. xunfocus t. xsimpl. subst E. iff M.
xextracts. xclose t. xsimpl. subst E. iff M.
eauto.
set_in M. math. auto. false* foreach_gt_notin F2.
xif. xapps*. intros b.
xextracts. xunfocus t. xsimpl. subst E. iff M.
xextracts. xclose t. xsimpl. subst E. iff M.
(* too slow: auto / in_union_get. *)
rewrite <- for_set_union_empty_r.
repeat rewrite <- for_set_union_assoc.
apply in_union_get_3. assumption.
set_in M. math. false* foreach_lt_notin F1. math. auto.
xret. xunfocus t. xsimpl. asserts_rewrite (x = y). math. subst E. auto.
xret. xclose t. xsimpl. asserts_rewrite (x = y). math. subst E. auto.
Qed.
......@@ -308,9 +308,9 @@ Lemma search_spec :
(fun b => \[b = isTrue (x \in E)] \* t ~> Stree E).
Proof using.
xweaken search_spec_ind. simpl. intros x t R HR S1 E.
xfocus t. xextract as T1 HT1.
xopen t. xextract as T1 HT1.
xapply* S1. hsimpl. intros b. xextract as Hb.
xunfocus* t. xsimpl*.
xclose* t. xsimpl*.
Qed.
......
......@@ -8,6 +8,23 @@ open Pervasives
*)
(*--TODO
let f () =
let r : '_a ref = ref [] in
!r
let f () =
let r : int ref = ref [] in
!r
let f () : 'a list =
let r : 'a ref = ref [] in
!r
*)
(********************************************************************)
(* ** Return *)
......@@ -255,6 +272,7 @@ let let_poly_nil_pair_heterogeneous () =
let x : ('a list * int list) = ([], []) in x
(********************************************************************)
(* ** Type annotations *)
......@@ -484,15 +502,22 @@ let while_false () =
(********************************************************************)
(* ** For loops *)
let for_incr () =
let for_to_incr r =
let n = ref 0 in
for i = 1 to 10 do
for i = 0 to pred r do
incr n;
done;
!n
(* "for .. down to" not yet supported *)
(*
let for_downto r =
let n = ref 0 in
for i = pred r downto 0 do
incr n;
done;
!n
*)
(********************************************************************)
(* ** Recursive function *)
......@@ -592,7 +617,7 @@ type typerecb1 = | Typerecb_1 of typerecb2
--> the work around is to break circularity using polymorphism, e.g.:
*)
type 'a typerecb2 = { typerecb_2 : 'a }
type 'a typerecb2 = { mutable typerecb_2 : 'a }
type typerecb1 = | Typerecb_1 of typerecb1 typerecb2
(*----*)
......@@ -600,12 +625,12 @@ type typerecb1 = | Typerecb_1 of typerecb1 typerecb2
(* Circularity between mutable records and inductive is broken
through the indirection at type loc *)
type 'a typerecd1 = { typerecd1_f : 'a typerecd2 }
type 'a typerecd1 = { mutable typerecd1_f : 'a typerecd2 }
and 'a typerecd2 =
| Typerecd_2a
| Typerecd_2b of 'a typerecd1
| Typerecd_2c of 'a typerecd3
and 'a typerecd3 = { typerecd3_f : 'a typerecd2 }
and 'a typerecd3 = { mutable typerecd3_f : 'a typerecd2 }
......
Set Implicit Arguments.
(*
*)
(* LibInt LibWf *)
Require Import CFLib.
Require Import Demo_ml.
Require Import Stdlib.
Require Import Stdlib.
(** [xwhile] applies to a goal of the form [(While F1 Do F2) H Q].
It introduces an abstract local predicate [S] that denotes the behavior
of the loop. The goal is [S H Q]. An assumption is provided to unfold
the loop:
[forall H' Q', (If_ F1 Then (Seq_ F2 ;; S) Else (Ret tt)) H' Q' -> S H' Q'].
After [xwhile], the typical proof pattern is to generalize the goal
by calling [assert (forall X, S (I X) Q)] for some predicate [I],
and then performing a well-founded induction on [X] w.r.t. wf relation.
(Or, using [xind_skip] to skip the termination proof.)
Alternatively, one can call one of the [xwhile_inv] tactics described
below to automatically set up the induction. The use of an invariant
makes the proof simpler but
Forms:
- [xwhile] is the basic form, described above.
- [xwhile as S] is equivalent to [xwhile; intros S LR HS].
- [xwhile_inv I R] where [R] is a well-founded relation on
type [A] and then invariant [I] has the form
[fun (b:bool) (X:A) => H]. Compared with [xwhile], this tactic
saves the need to set up the induction. However, this tactic
does not allow calling the [frame] rule during the loop iterations.
- [xwhile_inv_basic I R] where [R] is a well-founded relation on
type [A] and then invariant [I] has the form
[fun (b:bool) (X:A) => H]. This tactic processes the loop so
as to provide separate goals for the loop condition and for
the loop body. However, this tactic should not be use when both
the loop condition and the loop body require unfolding a
representation predicate.
- [xwhile_inv_basic_measure I] where then invariant [I] has the
form [fun (b:bool) (m:int) => H], where [b] indicates whether
the loop has terminated, and [m] gives the measure of [H].
It is just a special case of [xwhile_inv_basic].
- [xwhile_inv_skip I] is similar to [xwhile_inv], but the termination
proof is not required. Here, [I] takes the form [fun (b:bool) => H].
- [xwhile_inv_basic_skip I] is similar to [xwhile_inv_basic], but the termination
proof is not required. Here, [I] takes the form [fun (b:bool) => H].
*)
Lemma xwhile_inv_lemma :
forall (A:Type) (I:bool->A->hprop) (R:A->A->Prop),
forall (F1:~~bool) (F2:~~unit) H,
wf R ->
(H ==> (Hexists b X0, I b X0) \* \GC) ->
(forall (S:~~unit), is_local S -> forall b X,
(forall b'' X'', R X'' X -> S (I b'' X'') (# Hexists X', I false X')) ->
(Let _c := F1 in If_ _c Then (F2 ;; S) Else Ret tt) (I b X) (# Hexists X', I false X')) ->
(While F1 Do F2 Done_) H (# Hexists X, I false X).
Proof using.
introv WR HH HS.
applys local_gc_pre (Hexists b X0, I b X0); [ xlocal | apply HH | ].
apply local_erase. intros S LS FS.
xextract ;=> b X0. gen b. induction_wf IH: WR X0. intros.
applys (rm FS). applys HS. auto.
intros b'' X'' LX. applys IH. applys LX.
Qed.
Lemma xwhile_inv_basic_lemma :
forall (A:Type) (I:bool->A->hprop) (R:A->A->Prop),
forall (F1:~~bool) (F2:~~unit) H,
wf R ->
(H ==> (Hexists b X0, I b X0) \* \GC) ->
(forall b X, F1 (I b X) (fun b' => I b' X)) ->
(forall X, F2 (I true X) (# Hexists b X', \[R X' X] \* I b X')) ->
(While F1 Do F2 Done_) H (# Hexists X, I false X).
Proof using.
introv WR HH HF1 HF2.
applys local_gc_pre (Hexists b X, I b X); [ xlocal | apply HH | ].
applys xwhile_inv_lemma (fun X m => I X m) R; [ auto | hsimpl | ].
introv LS FS. xlet as b'.
{ applys HF1. }
{ simpl. xif.
{ xseq. applys HF2. simpl. xextract ;=>. applys~ FS. }
{ xret. hsimpl. } }
Qed.
Lemma xwhile_inv_basic_measure_lemma :
forall (I:bool->int->hprop),
forall (F1:~~bool) (F2:~~unit) H,
(H ==> (Hexists b m, I b m) \* \GC) ->
(forall b m, F1 (I b m) (fun b' => I b' m)) ->
(forall m, F2 (I true m) (# Hexists b m', \[0 <= m' < m] \* I b m')) ->
(While F1 Do F2 Done_) H (# Hexists m, I false m).
Proof using.
introv HH HF1 HF2. applys~ xwhile_inv_basic_lemma I (int_downto_wf 0).
Qed.
(* for cheaters *)
Axiom xwhile_inv_basic_skip_lemma :
forall (I:bool->hprop),
forall (F1:~~bool) (F2:~~unit) H,
(H ==> (Hexists b, I b) \* \GC) ->
(forall b, F1 (I b) (fun b' => I b')) ->
(F2 (I true) (# Hexists b, I b)) ->
(While F1 Do F2 Done_) H (# I false).
(* for cheaters *)
Axiom xwhile_inv_skip_lemma :
forall (I:bool->hprop),
forall (F1:~~bool) (F2:~~unit) H,
(H ==> (Hexists b, I b) \* \GC) ->
(forall (S:~~unit), is_local S -> forall b,
(forall b'', S (I b'') (# I false)) ->
(Let _c := F1 in If_ _c Then (F2 ;; S) Else Ret tt) (I b) (# I false)) ->
(While F1 Do F2 Done_) H (# I false).
Ltac cfml_relation_of_relation_or_measure E :=
match type of E with
| _ -> nat => constr:(LibWf.measure E)
| _ => E
end.
Ltac xwhile_pre cont :=
let aux tt := xuntag tag_while; cont tt in
match cfml_get_tag tt with
| tag_while =>
match cfml_postcondition_is_evar tt with
| true => aux tt
| false => xgc_post; [ aux tt | ]
end
| tag_seq => xseq; [ aux tt | instantiate; try xextract ]
end.
Tactic Notation "xwhile" :=
xwhile_pre ltac:(fun _ => apply local_erase).
Tactic Notation "xwhile" "as" ident(S) :=
xwhile_pre ltac:(fun _ =>
let LS := fresh "L" S in
let HS := fresh "H" S in
apply local_erase;
intros S LS HS).
Ltac xwhile_inv_core I R :=
let R := cfml_relation_of_relation_or_measure R in
xwhile_pre ltac:(fun _ => apply (@xwhile_inv_lemma _ I R);
[ auto with wf | | ]).
Tactic Notation "xwhile_inv" constr(I) constr(R) :=
xwhile_inv_core I R.
Ltac xwhile_inv_basic_core I R :=
let R := cfml_relation_of_relation_or_measure R in
xwhile_pre ltac:(fun _ => apply (@xwhile_inv_basic_lemma _ I R);