From 939de4c3b0eefc18ba502fa939368bcc75e8731b Mon Sep 17 00:00:00 2001 From: charguer Date: Fri, 18 Mar 2016 17:03:35 +0100 Subject: [PATCH] simplification --- {lib/coq => bin}/CFLemmasForTactics.v | 169 +--- bin/CF_xgo.v | 171 ++++ examples/DemoMake/Aux.ml | 1 - examples/DemoMake/Auxi.ml | 1 + examples/DemoMake/{Aux.mli => Auxi.mli} | 0 .../DemoMake/{Aux_proof.v => Auxi_proof.v} | 0 examples/DemoMake/Main.ml | 2 +- examples/DemoMake/Main_proof.v | 2 +- lib/coq/CFApp.v | 154 ++-- lib/coq/CFHeaps.v | 7 +- lib/coq/CFPrint.v | 853 +++++++++--------- lib/coq/CFTactics.v | 330 +++---- lib/coq/Makefile | 1 - lib/coq/Shared.v | 10 + 14 files changed, 857 insertions(+), 844 deletions(-) rename {lib/coq => bin}/CFLemmasForTactics.v (56%) create mode 100644 bin/CF_xgo.v delete mode 100644 examples/DemoMake/Aux.ml create mode 100644 examples/DemoMake/Auxi.ml rename examples/DemoMake/{Aux.mli => Auxi.mli} (100%) rename examples/DemoMake/{Aux_proof.v => Auxi_proof.v} (100%) diff --git a/lib/coq/CFLemmasForTactics.v b/bin/CFLemmasForTactics.v similarity index 56% rename from lib/coq/CFLemmasForTactics.v rename to bin/CFLemmasForTactics.v index 3e79e3a..4ef4ae3 100644 --- a/lib/coq/CFLemmasForTactics.v +++ b/bin/CFLemmasForTactics.v @@ -1,172 +1,5 @@ Set Implicit Arguments. -Require Export LibInt CFSpec CFPrint. - - -(********************************************************************) -(* ** Lemmas for tactics *) - -(** Lemma used by [xframe] *) - -Lemma xframe_lemma : forall H1 H2 B Q1 (F:~~B) H Q, - is_local F -> - H ==> H1 \* H2 -> - F H1 Q1 -> - Q1 \*+ H2 ===> Q -> - F H Q. -Proof using. intros. apply* local_wframe. Qed. - -(** Lemma used by [xchange] *) - -Lemma xchange_lemma : forall H1 H1' H2 B H Q (F:~~B), - is_local F -> - (H1 ==> H1') -> - (H ==> H1 \* H2) -> - F (H1' \* H2) Q -> - F H Q. -Proof using. - introv W1 L W2 M. applys local_wframe __ \[]; eauto. - hsimpl. hchange~ W2. hsimpl~. rew_heap~. -Qed. - -(** Lemma used by [xgc_all], - to remove everything from the pre-condition *) - -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. - -(** Lemma used by [xret] and [xret_no_gc] - for when post-condition unifies trivially *) - -Lemma xret_lemma_unify : forall B (v:B) H, - local (fun H' Q' => H' ==> Q' v) H (fun x => \[x = v] \* H). -Proof using. - intros. apply~ local_erase. hsimpl. auto. -Qed. - -(** Lemma used by [xret] *) - -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). - auto. rewrite star_comm. apply W. - apply~ local_erase. -Qed. - -(** Lemma used by [xret_no_gc] *) - -Lemma xret_no_gc_lemma : forall B (v:B) H (Q:B->hprop), - H ==> Q v -> - local (fun H' Q' => H' ==> Q' v) H Q. -Proof using. - introv W. apply~ local_erase. -Qed. - -(** Lemma used by [xpost], - for introducing an evar for the post-condition *) - -Lemma xpost_lemma : forall B Q' Q (F:~~B) H, - is_local F -> - F H Q' -> - Q' ===> Q -> - F H Q. -Proof using. intros. applys* local_weaken. Qed. - - - -(********************************************************************) -(* ** Local parameterized formulae *) - -(** [is_local_pred S] asserts that [is_local (S x)] holds for any [x]. - It is useful for describing loop invariants. *) - -Definition is_local_pred A1 B (S:A1->~~B) := - forall x, is_local (S x). - - -(********************************************************************) -(* ** While-loops *) - -Lemma while_loop_cf_inv_measure : - forall (I:bool->int->hprop), - forall (F1:~~bool) (F2:~~unit) H (Q:unit->hprop), - (exists b m, H ==> I b m \* (Hexists G, G)) -> - (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')) -> - (Q = fun _ => Hexists m, I false m) -> - (_While F1 _Do F2 _Done) H Q. -Proof using. - introv (bi&mi&Hi) Hc Hs He. applys~ local_weaken_gc_pre (I bi mi). xlocal. - xextract as 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 as b m' E. xapplys IH. applys E. hsimpl. hsimpl. - xret_no_gc. subst Q. hsimpl. -Qed. - - -(********************************************************************) -(* ** For-loops *) - -Lemma for_loop_cf_to_inv : - forall I H', - forall (a:int) (b:int) (F:int->~~unit) H (Q:unit->hprop), - (a > (b)%Z -> H ==> (Q tt)) -> - (a <= (b)%Z -> - (H ==> I a \* H') - /\ (forall i, a <= i /\ i <= (b)%Z -> F i (I i) (# I(i+1))) - /\ (I ((b)%Z+1) \* H' ==> Q tt)) -> - (For i = a To b Do F i _Done) H Q. -Proof. - introv M1 M2. apply local_erase. intros S LS HS. - tests C: (a > b). - apply (rm HS). split; intros C'. math. xret_no_gc~. - forwards (Ma&Mb&Mc): (rm M2). math. - cuts P: (forall i, a <= i <= b+1 -> S i (I i) (# I (b+1))). - xapply P. math. hchanges Ma. hchanges Mc. - intros i. induction_wf IH: (int_upto_wf (b+1)) i. intros Bnd. - applys (rm HS). split; intros C'. - xseq. eapply Mb. math. xapply IH; auto with maths; hsimpl. - xret_no_gc. math_rewrite~ (i = b +1). -Qed. - -Lemma for_loop_cf_to_inv_gen' : - forall I H', - forall (a:int) (b:int) (F:int->~~unit) H, - (a <= (b)%Z -> - (H ==> I a \* H') - /\ (forall i, a <= i /\ i <= (b)%Z -> F i (I i) (# I(i+1)))) -> - (a > (b)%Z -> H ==> I ((b)%Z+1) \* H') -> - (For i = a To b Do F i _Done) H (# I ((b)%Z+1) \* H'). -Proof. intros. applys* for_loop_cf_to_inv. Qed. - -Lemma for_loop_cf_to_inv_gen : - forall I H', - forall (a:int) (b:int) (F:int->~~unit) H Q, - (a <= (b)%Z -> H ==> I a \* H') -> - (forall i, a <= i <= (b)%Z -> F i (I i) (# I(i+1))) -> - (a > (b)%Z -> H ==> I ((b)%Z+1) \* H') -> - (# (I ((b)%Z+1) \* H')) ===> Q -> - (For i = a To b Do F i _Done) H Q. -Proof. intros. applys* for_loop_cf_to_inv. intros C. hchange (H2 C). hchange (H3 tt). hsimpl. Qed. - - -Lemma for_loop_cf_to_inv_up : - forall I H', - forall (a:int) (b:int) (F:int->~~unit) H (Q:unit->hprop), - (a <= (b)%Z) -> - (H ==> I a \* H') -> - (forall i, a <= i /\ i <= (b)%Z -> F i (I i) (# I(i+1))) -> - ((# I ((b)%Z+1) \* H') ===> Q) -> - (For i = a To b Do F i _Done) H Q. -Proof. intros. applys* for_loop_cf_to_inv. intros. math. Qed. - - - +Require Export LibInt CFApp CFPrint. (********************************************************************) diff --git a/bin/CF_xgo.v b/bin/CF_xgo.v new file mode 100644 index 0000000..3dfd040 --- /dev/null +++ b/bin/CF_xgo.v @@ -0,0 +1,171 @@ + + +(************************************************************) +(* ** [xgo] *) + +Inductive Xhint_cmd := + | Xstop : Xhint_cmd + | XstopNoclear : Xhint_cmd + | XstopAfter : Xhint_cmd + | XstopInside : Xhint_cmd + | Xtactic : Xhint_cmd + | XtacticNostop : Xhint_cmd + | XtacticNoclear : Xhint_cmd + | XsubstAlias : Xhint_cmd + | XspecArgs : list Boxer -> list Boxer -> Xhint_cmd + | Xargs : forall A, A -> Xhint_cmd + | Xlet : forall A, A -> Xhint_cmd + | Xlets : forall A, A -> Xhint_cmd + | Xsimple : Xhint_cmd. + +Inductive Xhint (a : tag_name) (h : Xhint_cmd) := + | Xhint_intro : Xhint a h. + +Ltac add_hint a h := + let H := fresh "Hint" in + lets H: (Xhint_intro a h). + +Ltac clear_hint a := + match goal with H: Xhint a _ |- _ => clear H end. + +Ltac clears_hint tt := + repeat match goal with H: Xhint _ _ |- _ => clear H end. + +Ltac find_hint a := + match goal with H: Xhint a ?h |- _ => constr:(h) end. + +Ltac xgo_default solver cont := + match ltac_get_tag tt with + | tag_ret => xret; cont tt + | tag_fail => xfail; cont tt + | tag_done => xdone; cont tt + | tag_apply => xapp + | tag_seq => xseq; cont tt + | tag_let_val => xval; cont tt + | tag_let_trm => xlet; cont tt + | tag_let_fun => fail + | tag_body => fail + | tag_letrec => fail + | tag_case => xcases_real; cont tt + | tag_casewhen => fail + | tag_if => xif; cont tt + | tag_alias => xalias; cont tt + | tag_match ?n => xmatch; cont tt + | tag_top_val => fail + | tag_top_trm => fail + | tag_top_fun => fail + | tag_for => fail + | tag_while => fail + end. + +Ltac xtactic tag := idtac. + +Ltac run_hint h cont := + let tag := ltac_get_tag tt in + match h with + | Xstop => clears_hint tt; idtac + | XstopNoclear => idtac + | XstopAfter => + match tag with + | tag_let_trm => fail (* todo: xlet_with cont ltac:(fun _ => idtac)*) + | _ => xgo_default ltac:(fun _ => idtac) ltac:(fun _ => idtac) + end + | XstopInside => + match tag with + | tag_let_trm => fail (*todo: xlet_with ltac:(fun _ => idtac) cont *) + end + | Xtactic => clears_hint tt; xtactic tag + | XtacticNostop => xtactic tag; cont tt + | XtacticNoclear => xtactic tag + | XsubstAlias => xmatch_subst_alias; cont tt + | Xargs ?E => + match tag with + | tag_let_trm => fail (* todo!!*) + | tag_apply => xapp E (*todo: not needed?*) + end + | XspecArgs (>> ?S) ?E => + match tag with + | tag_let_trm => fail (* todo!!*) + | tag_apply => xapp_spec S E (*todo: not needed?*) + end + | Xlet ?S => + match tag with + | tag_let_trm => xlet S; cont tt + | tag_let_fun => xfun_noxbody S + end + | Xsimple => xmatch_simple; cont tt + (* todo : generalize + | tag_case => xcases_real + | tag_if => xif + | tag_match ?n => xmatch + *) + end. + +Ltac find_and_run_hint cont := + let a := ltac_get_label tt in + let h := find_hint a in + clear_hint a; + first [ run_hint h cont | fail 1 ]. + +Tactic Notation "xhint" := + find_and_run_hint ltac:(fun _ => idtac). + +Ltac xgo_core solver cont := + first [ find_and_run_hint cont + | xgo_default solver cont ]. + +Ltac xgo_core_once solver := + xgo_core solver ltac:(fun _ => idtac). + +Ltac xgo_core_repeat solver := + xgo_core solver ltac:(fun _ => instantiate; try solve [ solver tt ]; + instantiate; try xgo_core_repeat solver). + +Ltac xgo_pre tt := + first [ xcf; repeat progress(intros) + | repeat progress(intros) + | idtac ]. + +Ltac xgo_base solver := + xgo_pre tt; xgo_core_repeat solver. + +Tactic Notation "xgo1" := + xgo_core_once ltac:(fun _ => idtac). + +Tactic Notation "xgo" := + xgo_base ltac:(fun tt => idtac). +Tactic Notation "xgo" "~" := + xgo_base ltac:(fun tt => xauto~ ); instantiate; xauto~. +Tactic Notation "xgo" "*" := + xgo_base ltac:(fun tt => xauto* ); instantiate; xauto*. + +Tactic Notation "xgo" constr(a1) constr(h1) := + add_hint a1 h1; xgo. +Tactic Notation "xgo" constr(a1) constr(h1) "," constr(a2) constr(h2) := + add_hint a1 h1; add_hint a2 h2; xgo. +Tactic Notation "xgo" constr(a1) constr(h1) "," constr(a2) constr(h2) "," + constr(a3) constr(h3) := + add_hint a1 h1; add_hint a2 h2; add_hint a3 h3; xgo. +Tactic Notation "xgo" constr(a1) constr(h1) "," constr(a2) constr(h2) "," + constr(a3) constr(h3) "," constr(a4) constr(h4) := + add_hint a1 h1; add_hint a2 h2; add_hint a3 h3; add_hint a4 h4; xgo. + +Tactic Notation "xgo" "~" constr(a1) constr(h1) := + add_hint a1 h1; xgo~. +Tactic Notation "xgo" "~" constr(a1) constr(h1) "," constr(a2) constr(h2) := + add_hint a1 h1; add_hint a2 h2; xgo~. +Tactic Notation "xgo" "~" constr(a1) constr(h1) "," constr(a2) constr(h2) "," + constr(a3) constr(h3) := + add_hint a1 h1; add_hint a2 h2; add_hint a3 h3; xgo~. +Tactic Notation "xgo" "~" constr(a1) constr(h1) "," constr(a2) constr(h2) "," + constr(a3) constr(h3) "," constr(a4) constr(h4) := + add_hint a1 h1; add_hint a2 h2; add_hint a3 h3; add_hint a4 h4; xgo~. + +Tactic Notation "xgos" := + xgo; hsimpl. +Tactic Notation "xgos" "~" := + xgos; auto_tilde. +Tactic Notation "xgos" "*" := + xgos; auto_star. + + diff --git a/examples/DemoMake/Aux.ml b/examples/DemoMake/Aux.ml deleted file mode 100644 index 79b11f3..0000000 --- a/examples/DemoMake/Aux.ml +++ /dev/null @@ -1 +0,0 @@ -let f x = x diff --git a/examples/DemoMake/Auxi.ml b/examples/DemoMake/Auxi.ml new file mode 100644 index 0000000..ce77364 --- /dev/null +++ b/examples/DemoMake/Auxi.ml @@ -0,0 +1 @@ +let f x = x \ No newline at end of file diff --git a/examples/DemoMake/Aux.mli b/examples/DemoMake/Auxi.mli similarity index 100% rename from examples/DemoMake/Aux.mli rename to examples/DemoMake/Auxi.mli diff --git a/examples/DemoMake/Aux_proof.v b/examples/DemoMake/Auxi_proof.v similarity index 100% rename from examples/DemoMake/Aux_proof.v rename to examples/DemoMake/Auxi_proof.v diff --git a/examples/DemoMake/Main.ml b/examples/DemoMake/Main.ml index 5cf2cec..6f22987 100644 --- a/examples/DemoMake/Main.ml +++ b/examples/DemoMake/Main.ml @@ -1,6 +1,6 @@ open NullPointers -let g x = Aux.f x +let g x = Auxi.f x diff --git a/examples/DemoMake/Main_proof.v b/examples/DemoMake/Main_proof.v index 30e007d..cbfb245 100644 --- a/examples/DemoMake/Main_proof.v +++ b/examples/DemoMake/Main_proof.v @@ -1,5 +1,5 @@ Require Export CFLib Main_ml. -Require Import Aux_ml Aux_proof Extra. +Require Import Auxi_ml Auxi_proof Extra. Lemma g_spec : Spec g (x:int) |R>> R \[] (fun y => \[same x y]). diff --git a/lib/coq/CFApp.v b/lib/coq/CFApp.v index 3d19eff..a1bef3d 100644 --- a/lib/coq/CFApp.v +++ b/lib/coq/CFApp.v @@ -1,6 +1,6 @@ Set Implicit Arguments. Require Export LibCore LibEpsilon Shared. -Require Export CFHeaps CFApp. +Require Export CFHeaps. Open Local Scope heap_scope_advanced. Hint Extern 1 (_ ===> _) => apply rel_le_refl. @@ -17,7 +17,7 @@ Hint Extern 1 (_ ===> _) => apply rel_le_refl. Based on [eval], we define [app_basic f x H Q], which is a like [eval] modulo frame and weakening and garbage collection. - On top of [app_basic], we define [App f xs H Q], which describes the + On top of [app_basic], we define [app f xs H Q], which describes the evaluation of a call to [f] on the arguments described by the list [xs]. We also define a predicate [curried n f] which asserts that the function @@ -25,11 +25,11 @@ Hint Extern 1 (_ ===> _) => apply rel_le_refl. applications are partial. The characteristic formula generated for a function application - [f x y z] is "App f [x y z]". + [f x y z] is "app f [x y z]". The characteristic formula generated for a function definition [let f x y z = t] is: - [curried 3 f /\ (forall x y z H Q, CF(t) H Q -> App f [x y z] H Q)]. + [curried 3 f /\ (forall x y z H Q, CF(t) H Q -> app f [x y z] H Q)]. These definitions are correct and sufficient to reasoning about all function calls, including partial and over applications. @@ -63,7 +63,7 @@ Axiom eval : forall A B, func -> A -> heap -> B -> heap -> Prop. (********************************************************************) -(* ** Definition and properties of the primitive App predicate *) +(* ** Definition and properties of the primitive app predicate *) (** The primitive predicate [app_basic], which makes a [local] version of [eval]. *) @@ -132,133 +132,139 @@ Notation "[ x1 x2 x3 x4 ]" := ((dyn x1)::(dyn x2)::(dyn x3)::(dyn x4)::nil) Notation "[ x1 x2 x3 x4 x5 ]" := ((dyn x1)::(dyn x2)::(dyn x3)::(dyn x4)::(dyn x5)::nil) (at level 0, x1 at level 0, x2 at level 0, x3 at level 0, x4 at level 0, x5 at level 0) : dynlist. -Bind Scope dynlist with dyn list. -Delimit Scope dynlist with dyns. +(*Bind Scope dynlist with list.*) +Delimit Scope dynlist with dynlist. (********************************************************************) -(* ** Definition of [App] and properties *) +(* ** Definition of [app] and properties *) -(** Definition of [App f xs], recursive. *) +(** Definition of [app f xs], recursive. + Can be written, e.g. Notation [app f [x y z] H Q] *) -Fixpoint AppDef (f:func) (xs:list dynamic) B (H:hprop) (Q:B->hprop) : Prop := +Fixpoint app_def (f:func) (xs:list dynamic) {B} (H:hprop) (Q:B->hprop) : Prop := match xs with | nil => False | (dyn x)::nil => app_basic f x H Q | (dyn x)::xs => app_basic f x H - (fun g => Hexists H', H' \* \[ AppDef g xs H' Q]) + (fun g => Hexists H', H' \* \[ app_def g xs H' Q]) end. -(** Notation [App f [x y z]] *) +(* +TODO: does not seem to work, hence the work-around using the notation below +Arguments app f%dummy_scope xs%dynlist B%type_scope H%heap_scope Q%heap_scope. +*) -Notation "'App' f xs" := - (@AppDef f xs _) (* (@AppDef f (xs)%dynlist _) *) +Notation "'app' f xs" := + (@app_def f (xs)%dynlist _) (* (@app_def f (xs)%dynlist _) *) (at level 80, f at level 0, xs at level 0) : charac. -Open Scope charac. +Open Scope charac. + Definition demo_arglist := forall f (xs:list int) (x y:int) B H (Q:B->hprop), - App f [ x y ] H Q. -(* TODO: find a way that the parentheses are not printed around "App" *) + app f [ x y ] H Q. (* Print demo_arglist. *) +(* TODO: find a way that the parentheses are not printed around "app" *) + (** Reformulation of the definition *) -Lemma App_ge_2_unfold : +Lemma app_ge_2_unfold : forall (f:func) A (x:A) (xs:list dynamic) B (H:hprop) (Q:B->hprop), (xs <> nil) -> - App f ((dyn x)::xs) H Q + app f ((dyn x)::xs) H Q = app_basic f x H - (fun g => Hexists H', H' \* \[ AppDef g xs H' Q]). + (fun g => Hexists H', H' \* \[ app_def g xs H' Q]). Proof using. intros. destruct xs. false. auto. Qed. -Lemma App_ge_2_unfold' : +Lemma app_ge_2_unfold' : forall (f:func) A (x:A) (xs:list dynamic) B (H:hprop) (Q:B->hprop), (length xs >= 1)%nat -> - App f ((dyn x)::xs) H Q + app f ((dyn x)::xs) H Q = app_basic f x H - (fun g => Hexists H', H' \* \[ AppDef g xs H' Q]). + (fun g => Hexists H', H' \* \[ app_def g xs H' Q]). Proof using. - intros. rewrite~ App_ge_2_unfold. destruct xs; rew_list in *. + intros. rewrite~ app_ge_2_unfold. destruct xs; rew_list in *. math. introv N. false. Qed. -Lemma App_ge_2_unfold_extens : +Lemma app_ge_2_unfold_extens : forall (f:func) A (x:A) (xs:list dynamic) B, (xs <> nil) -> - AppDef f ((dyn x)::xs) (B:=B) + app_def f ((dyn x)::xs) (B:=B) = (fun H Q => app_basic f x H - (fun g => Hexists H', H' \* \[ AppDef g xs H' Q])). + (fun g => Hexists H', H' \* \[ app_def g xs H' Q])). Proof using. - introv N. applys func_ext_2. intros H Q. rewrite~ App_ge_2_unfold. + introv N. applys func_ext_2. intros H Q. rewrite~ app_ge_2_unfold. Qed. -(** Weaken-frame-gc for [App] -- auxiliary lemma for [App_local]. *) +(** Weaken-frame-gc for [app] -- auxiliary lemma for [app_local]. *) -Lemma App_wgframe : forall B f xs H H1 H2 (Q1 Q:B->hprop), - App f xs H1 Q1 -> +Lemma app_wgframe : forall B f xs H H1 H2 (Q1 Q:B->hprop), + app f xs H1 Q1 -> H ==> (H1 \* H2) -> (Q1 \*+ H2) ===> (Q \*+ (Hexists H', H')) -> - App f xs H Q. + app f xs H Q. Proof using. intros B f xs. gen f. induction xs as [|[A x] xs]; introv M WH WQ. false. tests E: (xs = nil). simpls. applys~ local_wgframe M. - rewrite~ App_ge_2_unfold. rewrite~ App_ge_2_unfold in M. + rewrite~ app_ge_2_unfold. rewrite~ app_ge_2_unfold in M. applys~ local_wframe M. intros g. hextract as HR LR. hsimpl (HR \* H2). applys* IHxs LR. Qed. -Lemma App_weaken : forall B f xs H (Q Q':B->hprop), - App f xs H Q -> +Lemma app_weaken : forall B f xs H (Q Q':B->hprop), + app f xs H Q -> Q ===> Q' -> - App f xs H Q'. + app f xs H Q'. Proof using. - introv M W. applys* App_wgframe. hsimpl. intros r. hsimpl~ \[]. + introv M W. applys* app_wgframe. hsimpl. intros r. hsimpl~ \[]. Qed. (* DEPRECATED -Lemma App_frame : forall B f xs H H' (Q:B->hprop), - App f xs H Q -> - App f xs (H \* H') (Q \*+ H'). +Lemma app_frame : forall B f xs H H' (Q:B->hprop), + app f xs H Q -> + app f xs (H \* H') (Q \*+ H'). Proof using. intros B f xs. gen f. induction xs as [|[A x] xs]; introv M. false. tests E: (xs = nil). simpls. applys~ local_wframe M. - rewrite~ App_ge_2_unfold. rewrite~ App_ge_2_unfold in M. + rewrite~ app_ge_2_unfold. rewrite~ app_ge_2_unfold in M. applys~ local_wframe M. intros g. hextract as HR LR. hsimpl (HR \* H'). applys* IHxs. Qed. -Lemma App_weaken : forall B f xs H (Q Q':B->hprop), - App f xs H Q -> +Lemma app_weaken : forall B f xs H (Q Q':B->hprop), + app f xs H Q -> Q ===> Q' -> - App f xs H Q'. + app f xs H Q'. Proof using. intros B f xs. gen f. induction xs as [|[A x] xs]; introv M W. false. tests E: (xs = nil). simpls. applys~ local_weaken_post M. - rewrite~ App_ge_2_unfold'. rewrite~ App_ge_2_unfold' in M. + rewrite~ app_ge_2_unfold'. rewrite~ app_ge_2_unfold' in M. applys~ local_weaken_post M. intros g. hsimpl. rew_heap. applys* IHxs. Qed. *) -(** Local property for [App] *) +(** Local property for [app] *) -Lemma App_local : forall f xs B, - xs <> nil -> is_local (AppDef f xs (B:=B)). +Lemma app_local : forall f xs B, + xs <> nil -> is_local (app_def f xs (B:=B)). Proof using. introv N. apply is_local_prove. intros H Q. destruct xs as [|[A1 x1] xs]; tryfalse. destruct xs as [|[A2 x2] xs]. { simpl. rewrite~ <- app_basic_local. iff*. } - { rewrite App_ge_2_unfold_extens; auto_false. + { rewrite app_ge_2_unfold_extens; auto_false. iff M. apply local_erase. auto. rewrite app_basic_local. @@ -266,10 +272,10 @@ Proof using. destruct M as (H1&H2&Q1&R1&R2&R3). exists___. splits. eauto. eauto. intros g. hextract as H' L. hsimpl (H' \* H2). - applys App_wgframe L. hsimpl. hchange R3. hsimpl. } + applys app_wgframe L. hsimpl. hchange R3. hsimpl. } Qed. -Hint Resolve App_local. +Hint Resolve app_local. (********************************************************************) @@ -285,7 +291,7 @@ Fixpoint curried (n:nat) (f:func) : Prop := app_basic f x \[] (fun g => \[ curried n g /\ forall xs B H (Q:B->hprop), length xs = n -> - App f ((dyn x)::xs) H Q -> App g xs H Q]) + app f ((dyn x)::xs) H Q -> app g xs H Q]) end. (** Unfolding lemma for [curried] *) @@ -296,7 +302,7 @@ Lemma curried_ge_2_unfold : forall n f, = forall A (x:A), app_basic f x \[] (fun g => \[ curried (pred n) g /\ forall xs B H (Q:B->hprop), length xs = (pred n) -> - App f ((dyn x)::xs) H Q -> App g xs H Q]). + app f ((dyn x)::xs) H Q -> app g xs H Q]). Proof using. introv N. destruct n. math. destruct n. math. auto. Qed. @@ -305,20 +311,20 @@ Qed. (********************************************************************) (* ** Lemma for over-applications *) -(** [App f (xs++ys)] can be expressed as [App f xs] that returns - a function [g] such that the behavior is that of [App g ys]. *) +(** [app f (xs++ys)] can be expressed as [app f xs] that returns + a function [g] such that the behavior is that of [app g ys]. *) -Lemma App_over_app : forall xs ys f B H (Q:B->hprop), +Lemma app_over_app : forall xs ys f B H (Q:B->hprop), (length xs > 0)%nat -> (length ys > 0)%nat -> - App f (xs++ys) H Q - = App f xs H (fun g => Hexists H', H' \* - \[ App g ys H' Q ]). + app f (xs++ys) H Q + = app f xs H (fun g => Hexists H', H' \* + \[ app g ys H' Q ]). Proof using. induction xs. rew_list. math. introv N1 N2. rew_list. destruct a as [A x]. destruct xs. rew_list. simpl. destruct ys. rew_list in *. math. auto. - sets_eq xs': (d :: xs). do 2 (rewrite App_ge_2_unfold; + sets_eq xs': (d :: xs). do 2 (rewrite app_ge_2_unfold; [ | subst; rew_list; auto_false ]). fequal. apply func_ext_1. intros g. apply func_equal_1. auto. apply func_ext_1. intros H'. @@ -327,16 +333,16 @@ Qed. (** Alternative formulation *) -Lemma App_over_take : forall n xs f B H (Q:B->hprop), +Lemma app_over_take : forall n xs f B H (Q:B->hprop), (0 < n < length xs)%nat -> - App f xs H Q - = App f (take n xs) H (fun g => Hexists H', H' \* - \[ App g (drop n xs) H' Q ]). + app f xs H Q + = app f (take n xs) H (fun g => Hexists H', H' \* + \[ app g (drop n xs) H' Q ]). Proof using. introv N. forwards* (M&E1&E2): take_and_drop n xs. math. set (xs' := xs) at 1. change xs with xs' in M. rewrite M. - subst xs'. rewrite App_over_app; try math. auto. + subst xs'. rewrite app_over_app; try math. auto. Qed. @@ -344,35 +350,35 @@ Qed. (* ** Lemma for partial-applications *) (** When [curried n f] holds and the number of the arguments [xs] - is less than [n], then [App f xs] is a function [g] such that - [App g ys] has the same behavior as [App f (xs++ys)]. *) + is less than [n], then [app f xs] is a function [g] such that + [app g ys] has the same behavior as [app f (xs++ys)]. *) -Lemma App_partial : forall n xs f, +Lemma app_partial : forall n xs f, curried n f -> (0 < length xs < n)%nat -> - App f xs \[] (fun g => \[ + app f xs \[] (fun g => \[ curried (n - length xs)%nat g /\ forall ys B H (Q:B->hprop), (length xs + length ys = n)%nat -> - App f (xs++ys) H Q -> App g ys H Q]). + app f (xs++ys) H Q -> app g ys H Q]). Proof using. intros n. induction_wf IH: lt_wf n. introv C N. destruct xs as [|[A x] zs]. rew_list in N. math. rewrite curried_ge_2_unfold in C; [|math]. tests E: (zs = nil). - { unfold AppDef at 1. eapply local_weaken_post. auto. applys (rm C). + { unfold app_def at 1. eapply local_weaken_post. auto. applys (rm C). intros g. hextract as [M1 M2]. hsimpl. split. rew_list. applys_eq M1 2. math. introv E AK. rew_list in *. applys M2. math. auto. } { asserts Pzs: (0 < length zs). { destruct zs. tryfalse. rew_list. math. } - rew_list in N. rewrite~ App_ge_2_unfold. + rew_list in N. rewrite~ app_ge_2_unfold. eapply local_weaken_post. auto. applys (rm C). clear C. (* todo: make work rm *) intros h. hextract as [M1 M2]. hsimpl. - applys App_weaken. applys (rm IH) M1. math. math. clear IH. + applys app_weaken. applys (rm IH) M1. math. math. clear IH. intros g. hextract as [N1 N2]. hsimpl. split. { rew_list. applys_eq N1 2. math. } { introv P1 P2. rew_list in P1. applys N2. math. applys M2. rew_list; math. - rew_list in P2. applys P2. } + rew_list in P2. applys P2. } } Qed. diff --git a/lib/coq/CFHeaps.v b/lib/coq/CFHeaps.v index 8acd354..155e2ef 100644 --- a/lib/coq/CFHeaps.v +++ b/lib/coq/CFHeaps.v @@ -2357,6 +2357,12 @@ Definition local B (F:~~B) : ~~B := Definition is_local B (F:~~B) := F = local F. +(** [is_local_pred S] asserts that [is_local (S x)] holds for any [x]. + It is useful for describing loop invariants. *) + +Definition is_local_pred A B (S:A->~~B) := + forall x, is_local (S x). + (** The weakening property is implied by locality *) Definition weakenable B (F:~~B) := @@ -2712,4 +2718,3 @@ Ltac hclean_main tt := Tactic Notation "hclean" := hclean_main tt. Tactic Notation "hclean" "~" := hclean; auto_tilde. Tactic Notation "hclean" "*" := hclean; auto_star. - diff --git a/lib/coq/CFPrint.v b/lib/coq/CFPrint.v index 5c27eaf..59c5e77 100644 --- a/lib/coq/CFPrint.v +++ b/lib/coq/CFPrint.v @@ -1,140 +1,16 @@ Set Implicit Arguments. -Require Import CFApp. +Require Import CFHeaps CFApp. - -(********************************************************************) -(* ** Notation for specifications *) - -Open Local Scope func. - -(*------------------------------------------------------------------*) -(* ** Printing abstract specifications *) - -Notation "'Spec_1' f K" := (spec_1 K f) - (at level 69, f at level 0) : func. - -Notation "'Spec_2' f K" := (spec_2 K f) - (at level 69, f at level 0) : func. - -Notation "'Spec_3' f K" := (spec_3 K f) - (at level 69, f at level 0) : func. - -Notation "'Spec_4' f K" := (spec_4 K f) - (at level 69, f at level 0) : func. - -(*------------------------------------------------------------------*) -(* ** Printing general specifications *) - -Notation "'Spec' f '()' | R >> H" - := (Spec_1 f (fun (_:unit) R => H)) - (at level 69, f at level 0, - R ident, H at level 99, - format "Spec f '()' | R >> '/' '[v' H ']'") : func. - - Notation "'Spec' f '()' ':' T | R >> H" - := (Spec_1 f (fun (_:unit) (R:~~T) => H)) - (at level 69, f at level 0, T at level 30, - R ident, H at level 99, only parsing) : func. - -Notation "'Spec' f x1 | R >> H" - := (Spec_1 f (fun x1 R => H)) - (at level 69, f at level 0, x1 ident, - R ident, H at level 99, - format "Spec f x1 | R >> '/' '[v' H ']'") : func. - -Notation "'Spec' f x1 x2 | R >> H" - := (Spec_2 f (fun x1 x2 R => H)) - (at level 69, f at level 0, x1 ident, x2 ident, - R ident, H at level 99, - format "Spec f x1 x2 | R >> '/' '[v' H ']'") : func. - -Notation "'Spec' f x1 x2 x3 | R >> H" - := (Spec_3 f (fun x1 x2 x3 R => H)) - (at level 69, f at level 0, x1 ident, x2 ident, x3 ident, - R ident, H at level 99, - format "Spec f x1 x2 x3 | R >> '/' '[v' H ']'") : func. - -Notation "'Spec' f x1 x2 x3 x4 | R >> H" - := (Spec_4 f (fun x1 x2 x3 x4 R => H)) - (at level 69, f at level 0, x1 ident, x2 ident, x3 ident, x4 ident, - R ident, H at level 99, - format "Spec f x1 x2 x3 x4 | R >> '/' '[v' H ']'") : func. - -Notation "'Spec' f ( x1 : A1 ) | R >> H" - := (Spec_1 f (fun (x1:A1) R => H)) - (at level 69, f at level 0, x1 ident, - R ident, H at level 99, - A1 at level 0, only parsing) : func. - -Notation "'Spec' f ( x1 : A1 ) ( x2 : A2 ) | R >> H" - := (Spec_2 f (fun (x1:A1) (x2:A2) R => H)) - (at level 69, f at level 0, x1 ident, x2 ident, - R ident, H at level 99, - A1 at level 0, A2 at level 0, only parsing) : func. - -Notation "'Spec' f ( x1 : A1 ) ( x2 : A2 ) ( x3 : A3 ) | R >> H" - := (Spec_3 f (fun (x1:A1) (x2:A2) (x3:A3) R => H)) - (at level 69, f at level 0, x1 ident, x2 ident, x3 ident, - R ident, H at level 99, - A1 at level 0, A2 at level 0, A3 at level 0, only parsing) : func. - -Notation "'Spec' f ( x1 : A1 ) ( x2 : A2 ) ( x3 : A3 ) ( x4 : A4 ) | R >> H" - := (Spec_4 f (fun (x1:A1) (x2:A2) (x3:A3) (x4:A4) R => H)) - (at level 69, f at level 0, x1 ident, x2 ident, x3 ident, x4 ident, - R ident, H at level 99, - A1 at level 0, A2 at level 0, A3 at level 0, A4 at level 0, only parsing) : func. +(** The idea is to tag nodes of the formulae with identity predicates + carrying a tag information, that indicates the language construct + from which the piece of characteristic formula has been generated. *) (********************************************************************) -(* Implementation of labels *) - -Module Export AtomsEff. +(* ** Implementation of tags *) -(** Variables are described as list of bits, e.g. [1::2::1::1::2::0]. - For efficiency, we do not use the type [list bool], but an ad-hoc - predicate with three constructors. *) - -Inductive atom : Set := - | atom_0 : atom - | atom_1 : atom -> atom - | atom_2 : atom -> atom. - -Instance atom_inhab : Inhab atom. -Proof. apply (prove_Inhab atom_0). Qed. - -(** Notation system *) - -Notation "'`0'" := (atom_0) - (at level 50, format "`0") : atom_scope. -Notation "'`1' v" := (atom_1 v) - (at level 50, v at level 50, format "`1 v") : atom_scope. -Notation "'`2' v" := (atom_2 v) - (at level 50, v at level 50, format "`2 v") : atom_scope. -Open Scope atom_scope. -Bind Scope atom_scope with atom. -Delimit Scope atom_scope with atom. - -End AtomsEff. - - -(********************************************************************) -(* ** Implementation of tags and labels *) - -Definition tag_name := atom. -Definition no_name := `0. - -Class Label := Label_create { Label_get : tag_name }. - -Instance Label_default : Label. -Proof. constructor. exact no_name. Defined. - -(* The core idea of labelling can be summarized as follows: - Definition tag `{x:Label} (P:Prop) := P. - Notation "# P" := (@tag _ P) (at level 30). - Definition test P := (@tag (Label_create 3) P). - --> test displays as "fun P => # P" and does not show "3" -*) +(** Grammar of tags *) Inductive tag_type : Type := | tag_ret @@ -143,446 +19,519 @@ Inductive tag_type : Type := | tag_let_fun | tag_let_trm | tag_body - | tag_letrec + | tag_match (n : nat) | tag_case | tag_casewhen + | tag_alias | tag_fail | tag_done | tag_if - | tag_alias - | tag_top_val - | tag_top_fun - | tag_top_trm - | tag_match (n : nat) | tag_seq | tag_for | tag_while - | tag_pay. + | tag_pay + | tag_top_val + | tag_top_fun + . + (* | tag_top_trm -- FUTURE *) + +(** Tag carrier, as an identity function *) -Definition tag (t:tag_type) `{x:Label} (A:Type) (P:A) := P. +Definition tag (t:tag_type) (A:Type) (P:A) := P. Implicit Arguments tag [A]. -Notation "'!B' P" := (tag tag_body _ P) - (at level 95). -Notation "'!M' n P" := (tag (tag_match n) _ P) - (at level 95, n at level 0). -Notation "'!A' P" := (tag tag_apply _ P) - (at level 95). -Notation "'!R' P" := (tag tag_ret _ (local P)) - (at level 69). -Notation "'!V' P" := (tag tag_let_val _ (local P)) - (at level 95). -Notation "'!F' P" := (tag tag_let_fun _ (local P)) - (at level 95). -Notation "'!T' P" := (tag tag_let_trm _ (local P)) - (at level 95). -Notation "'!C' P" := (tag tag_case _ (local P)) - (at level 95). -Notation "'!W' P" := (tag tag_casewhen _ (local P)) - (at level 95). -Notation "'!I' P" := (tag tag_if _ (local P)) - (at level 95). -Notation "'!E' P" := (tag tag_fail _ (local P)) - (at level 95). -Notation "'!S' P" := (tag tag_alias _ (local P)) - (at level 95). -Notation "'!D' P" := (tag tag_done _ (local P)) - (at level 95). -Notation "'!Seq' P" := (tag tag_seq _ (local P)) - (at level 95). -Notation "'!For' P" := (tag tag_for _ (local P)) - (at level 95). -Notation "'!Pay' P" := (tag tag_pay _ (local P)) - (at level 95). -Notation "'!While' P" := (tag tag_while _ (local P)) - (at level 95). -Notation "'!TV' P" := (tag tag_top_val _ (local P)) - (at level 95). -Notation "'!TF' P" := (tag tag_top_fun _ (local P)) - (at level 95). -Notation "'!TT' P" := (tag tag_top_trm _ (local P)) - (at level 95). +(** Lemmas and tactics to manipulate tags *) Lemma add_tag : forall (T:Prop->Prop), (T = fun P:Prop => P) -> forall (G:Prop), (T G) -> G. Proof. intros. subst. auto. Qed. +(** [ltac_add_tag T] adds a tag [T] to the head of the goal *) + Ltac ltac_add_tag T := apply (@add_tag T (refl_equal _)). +(** [ltac_get_tag tt] returns the tag at the head of the goal *) + Ltac ltac_get_tag tt := - match goal with |- tag ?t _ _ _ _ => constr:(t) end. + match goal with |- tag ?t _ _ _ => constr:(t) end. + +(** [xuntag T] removes the tag [T] at the head of the goal, + and fails if it is not there. *) -Ltac ltac_get_label tt := - match goal with |- tag _ (Label_create ?l) _ _ _ => constr:(l) end. +Tactic Notation "xuntag" constr(T) := + match goal with |- tag T _ _ _ => unfold tag at 1 end. -Tactic Notation "xuntag" constr(t) := - match goal with |- tag t _ _ _ _ => unfold tag at 1 end. +(** [xuntag] removes the tag at the head of the goal, + and fails if there is not tag there. *) Tactic Notation "xuntag" := - match goal with |- tag _ _ _ _ _ => unfold tag at 1 end. + match goal with |- tag _ _ _ _ => unfold tag at 1 end. + +(** [xuntags] removes all tags from everywhere in the goal; + useful for debugging. *) Tactic Notation "xuntags" := unfold tag in *. (********************************************************************) -(* ** Notation for characteristic formulae *) +(* ** Notation for tags *) + +(* TODO: these notation might be presented as definition, since the + notation are not really visible by the user in practice *) + +Notation "'!Ret' P" := (tag tag_ret (local P)) + (at level 69) : tag_scope. +Notation "'!App' P" := (tag tag_apply P) + (at level 95) : tag_scope. +Notation "'!LetVal' P" := (tag tag_let_val (local P)) + (at level 95) : tag_scope. +Notation "'!LetFun' P" := (tag tag_let_fun (local P)) + (at level 95) : tag_scope. +Notation "'!LetTrm' P" := (tag tag_let_trm (local P)) + (at level 95) : tag_scope. +Notation "'!Body' P" := (tag tag_body P) + (at level 95) : tag_scope. + +Notation "'!Match' n P" := (tag (tag_match n) P) + (at level 95, n at level 0). +Notation "'!Case' P" := (tag tag_case (local P)) + (at level 95) : tag_scope. +Notation "'!CaseWhen' P" := (tag tag_casewhen (local P)) + (at level 95) : tag_scope. +Notation "'!Alias' P" := (tag tag_alias (local P)) + (at level 95) : tag_scope. +Notation "'!Fail' P" := (tag tag_fail (local P)) + (at level 95) : tag_scope. +Notation "'!Done' P" := (tag tag_done (local P)) + (at level 95) : tag_scope. + +Notation "'!If' P" := (tag tag_if (local P)) + (at level 95) : tag_scope. +Notation "'!Seq' P" := (tag tag_seq (local P)) + (at level 95) : tag_scope. +Notation "'!For' P" := (tag tag_for (local P)) + (at level 95) : tag_scope. +Notation "'!While' P" := (tag tag_while (local P)) + (at level 95) : tag_scope. +Notation "'!Pay' P" := (tag tag_pay (local P)) + (at level 95) : tag_scope. + +Notation "'!TopVal' P" := (tag tag_top_val P) + (at level 95) : tag_scope. +Notation "'!TopFun' P" := (tag tag_top_fun P) + (at level 95) : tag_scope. + +(* FUTURE +Notation "'!TopTerm' P" := (tag tag_top_trm (local P)) + (at level 95) : tag_scope. +*) + +Local Open Scope tag_scope. -(** Basic *) + +(********************************************************************) +(** Ret *) Notation "'Ret' v" := - (!R (fun H Q => H ==> Q v)) + (!Ret (fun H Q => H ==> Q v)) (at level 69) : charac. -Notation "'Fail'" := - (!E (fun _ _ => False)) - (at level 0) : charac. +Open Scope charac. -Notation "'Done'" := - (!D (fun _ _ => True)) - (at level 0) : charac. -Open Scope charac. +(********************************************************************) +(** App and LetApp and SeqApp*) -(** Application *) +(* Note: see CFapp.v for the [app] notation. *) + +Notation "'App_' f xs" := + (!App (app f xs)) + (at level 68, f at level 0, xs at level 0) : charac. + +(* To improve readbility, the open-ended [App] notation. *) Notation "'App' f x1 ;" := - (!A (app_1 f x1)) + (App_ f [x1]) (at level 68, f at level 0, x1 at level 0) : charac. Notation "'App' f x1 x2 ;" := - (!A (app_2 f x1 x2)) + (App_ f [x1 x2]) (at level 68, f at level 0, x1 at level 0, x2 at level 0) : charac. - + Notation "'App' f x1 x2 x3 ;" := - (!A (app_3 f x1 x2 x3)) + (App_ f [x1 x2 x3]) (at level 68, f at level 0, x1 at level 0, x2 at level 0, x3 at level 0) : charac. - + Notation "'App' f x1 x2 x3 x4 ;" := - (!A (app_4 f x1 x2 x3 x4)) + (App_ f [x1 x2 x3 x4]) (at level 68, f at level 0, x1 at level 0, x2 at level 0, x3 at level 0, x4 at level 0) : charac. -Notation "'AppReturns'" := (@app_1 _ _). +Notation "'App' f x1 x2 x3 x4 x5 ;" := + (App_ f [x1 x2 x3 x4 x5]) + (at level 68, f at level 0, x1 at level 0, x2 at level 0, + x3 at level 0, x4 at level 0, x5 at level 0) : charac. + + +Notation "'LetApp' x ':=' f xs 'in' F2" := + (!LetTrm (fun H Q => exists Q1, App_ f xs H Q1 /\ forall x, F2 (Q1 x) Q)) + (at level 69, x ident, f at level 0, xs at level 0, + right associativity, + format "'[v' '[' 'LetApp' x ':=' f xs 'in' ']' '/' '[' F2 ']' ']'") : charac. +(* TODO: above, reuse notation of Let *) + + +(* FUTURE: notation for LetApp of various arities +-Notation "'LetApp' x ':=' f x1 'in' F2" := +- (!T (fun H Q => exists Q1, (App f x1;) H Q1 /\ forall x, F2 (Q1 x) Q)) +- (at level 69, x ident, f at level 0, x1 at level 0, +- right associativity, +- format "'[v' '[' 'LetApp' x ':=' f x1 'in' ']' '/' '[' F2 ']' ']'") : +- +-Notation "'LetApp' x ':=' f x1 x2 'in' F2" := +- (!T (fun H Q => exists Q1, (App f x1 x2;) H Q1 /\ forall x, F2 (Q1 x) Q)) +- (at level 69, x ident, f at level 0, x1 at level 0, x2 at level 0, +- right associativity, +- format "'[v' '[' 'LetApp' x ':=' f x1 x2 'in' ']' '/' '[' F2 ']' ']'" +- +-Notation "'LetApp' x ':=' f x1 x2 x3 'in' F2" := +- (!T (fun H Q => exists Q1, (App f x1 x2 x3;) H Q1 /\ forall x, F2 (Q1 x) Q)) +- (at level 69, x ident, f at level 0, x1 at level 0, x2 at level 0, +- x3 at level 0, right associativity, +- format "'[v' '[' 'LetApp' x ':=' f x1 x2 x3 'in' ']' '/' '[' F2 ']'" +- +-Notation "'LetApp' x ':=' f x1 x2 x3 x4 'in' F2" := +- (!T (fun H Q => exists Q1, (App f x1 x2 x3 x4;) H Q1 /\ forall x, F2 (Q1 x) Q +- (at level 69, x ident, f at level 0, x1 at level 0, x2 at level 0, +*) +Notation "'SeqApp' f xs ;; Q2" := + (!Seq (fun H Q => exists Q', (App f xs;) H Q' /\ Q2 (Q' tt) Q)) + (at level 68, f at level 0, xs at level 0, right associativity, + format "'[v' 'SeqApp' '[' f xs ']' ;; '/' '[' Q2 ']' ']'") : charac. +(* TODO: notation for SeqApp at all arities *) + + +(********************************************************************) (** LetVal *) Notation "'LetVal' x ':=' V 'in' F" := - (!V (fun H Q => forall x, x = V -> F H Q)) + (!LetVal (fun H Q => forall x, x = V -> F H Q)) (at level 69, x ident) : charac. Notation "'LetVal' [ A1 ] x ':=' V 'in' F" := - (!V (fun H Q => forall x, x = (fun (A1:Type) => V) -> F H Q)) + (!LetVal (fun H Q => forall x, x = (fun (A1:Type) => V) -> F H Q)) (at level 69, x ident, A1 ident) : charac. Notation "'LetVal' [ A1 A2 ] x ':=' V 'in' F" := - (!V (fun H Q => forall x, x = (fun (A1 A2:Type) => V) -> F H Q)) + (!LetVal (fun H Q => forall x, x = (fun (A1 A2:Type) => V) -> F H Q)) (at level 69, x ident, A1 ident, A2 ident) : charac. Notation "'LetVal' [ A1 A2 A3 ] x ':=' V 'in' F" := - (!V (fun H Q => forall x, x = (fun (A1 A2 A3:Type) => V) -> F H Q)) + (!LetVal (fun H Q => forall x, x = (fun (A1 A2 A3:Type) => V) -> F H Q)) (at level 69, x ident, A1 ident, A2 ident, A3 ident) : charac. Notation "'LetVal' [ A1 A2 A3 A4 ] x ':=' V 'in' F" := - (!V (fun H Q => forall x, x = (fun (A1 A2 A3 A4:Type) => V) -> F H Q)) + (!LetVal (fun H Q => forall x, x = (fun (A1 A2 A3 A4:Type) => V) -> F H Q)) (at level 69, x ident, A1 ident, A2 ident, A3 ident, A4 ident) : charac. -(** Let / Seq / Pay *) - -Notation "'Let' x ':=' F1 'in' F2" := - (!T (fun H Q => exists Q1, F1 H Q1 /\ forall x, F2 (Q1 x) Q)) - (at level 69, x ident, right associativity, - format "'[v' '[' 'Let' x ':=' F1 'in' ']' '/' '[' F2 ']' ']'") : charac. - -Notation "'Let' x ':' T ':=' F1 'in' F2" := - (!T (fun H Q => exists Q1, F1 H Q1 /\ forall x:T, F2 (Q1 x) Q)) - (at level 69, x ident, right associativity, only parsing) : charac. - - (* todo: rename: Qi into Fi *) - -Notation "'Seq_' Q1 ;; Q2" := - (!Seq (fun H Q => exists Q', Q1 H Q' /\ Q2 (Q' tt) Q)) - (at level 68, right associativity, - format "'[v' 'Seq_' '[' Q1 ']' ;; '/' '[' Q2 ']' ']'") : charac. - -Notation "Q1 ;; Q2" := - (!Seq (fun H Q => exists Q', Q1 H Q' /\ Q2 (Q' tt) Q)) - (at level 68, right associativity, only parsing, - format "'[v' '[' Q1 ']' ;; '/' '[' Q2 ']' ']'") : charac. - -Notation "'Pay_' ;; Q1" := - (!Pay (fun H Q => exists H', pay_one H H' /\ Q1 H' Q)) - (at level 68, right associativity, - format "'[v' 'Pay_' ;; '[' Q1 ']' ']'") : charac. - -(** LetApp *) - -Notation "'LetApp' x ':=' f x1 'in' F2" := - (!T (fun H Q => exists Q1, (App f x1;) H Q1 /\ forall x, F2 (Q1 x) Q)) - (at level 69, x ident, f at level 0, x1 at level 0, - right associativity, - format "'[v' '[' 'LetApp' x ':=' f x1 'in' ']' '/' '[' F2 ']' ']'") : charac. - -Notation "'LetApp' x ':=' f x1 x2 'in' F2" := - (!T (fun H Q => exists Q1, (App f x1 x2;) H Q1 /\ forall x, F2 (Q1 x) Q)) - (at level 69, x ident, f at level 0, x1 at level 0, x2 at level 0, - right associativity, - format "'[v' '[' 'LetApp' x ':=' f x1 x2 'in' ']' '/' '[' F2 ']' ']'") : charac. - -Notation "'LetApp' x ':=' f x1 x2 x3 'in' F2" := - (!T (fun H Q => exists Q1, (App f x1 x2 x3;) H Q1 /\ forall x, F2 (Q1 x) Q)) - (at level 69, x ident, f at level 0, x1 at level 0, x2 at level 0, - x3 at level 0, right associativity, - format "'[v' '[' 'LetApp' x ':=' f x1 x2 x3 'in' ']' '/' '[' F2 ']' ']'") : charac. - -Notation "'LetApp' x ':=' f x1 x2 x3 x4 'in' F2" := - (!T (fun H Q => exists Q1, (App f x1 x2 x3 x4;) H Q1 /\ forall x, F2 (Q1 x) Q)) - (at level 69, x ident, f at level 0, x1 at level 0, x2 at level 0, - x3 at level 0, x4 at level 0, right associativity, - format "'[v' '[' 'LetApp' x ':=' f x1 x2 x3 x4 'in' ']' '/' '[' F2 ']' ']'") : charac. - -(** SeqApp *) - -Notation "'SeqApp' f x1 ;; Q2" := - (!Seq (fun H Q => exists Q', (App f x1;) H Q' /\ Q2 (Q' tt) Q)) - (at level 68, f at level 0, x1 at level 0, right associativity, - format "'[v' 'SeqApp' '[' f x1 ']' ;; '/' '[' Q2 ']' ']'") : charac. - -Notation "'SeqApp' f x1 x2 ;; Q2" := - (!Seq (fun H Q => exists Q', (App f x1 x2;) H Q' /\ Q2 (Q' tt) Q)) - (at level 68, f at level 0, x1 at level 0, x2 at level 0, right associativity, - format "'[v' 'SeqApp' '[' f x1 x2 ']' ;; '/' '[' Q2 ']' ']'") : charac. - -Notation "'SeqApp' f x1 x2 x3 ;; Q2" := - (!Seq (fun H Q => exists Q', (App f x1 x2 x3;) H Q' /\ Q2 (Q' tt) Q)) - (at level 68, f at level 0, x1 at level 0, x2 at level 0, - x3 at level 0, right associativity, - format "'[v' 'SeqApp' '[' f x1 x2 x3 ']' ;; '/' '[' Q2 ']' ']'") : charac. - -Notation "'SeqApp' f x1 x2 x3 x4 ;; Q2" := - (!Seq (fun H Q => exists Q', (App f x1 x2 x3 x4;) H Q' /\ Q2 (Q' tt) Q)) - (at level 68, f at level 0, x1 at level 0, x2 at level 0, - x3 at level 0, x4 at level 0, right associativity, - format "'[v' 'SeqApp' '[' f x1 x2 x3 x4 ']' ;; '/' '[' Q2 ']' ']'") : charac. +(********************************************************************) (** Body *) -Notation "'Body' f x1 '=>' Q" := - (!B (forall K, is_spec_1 K -> - (forall x1, K x1 Q) -> spec_1 K f)) +Notation "'Body' f x1 '=>' K" := + (!Body ( curried 1 f + /\ (forall x1 B H Q, K H Q -> app f [x1] H Q))) (at level 0, f at level 0, x1 ident) : charac. -Notation "'Body' f x1 x2 '=>' Q" := - (!B (forall K, is_spec_2 K -> - (forall x1 x2, K x1 x2 Q) -> spec_2 K f)) +Notation "'Body' f x1 x2 '=>' K" := + (!Body ( curried 2 f + /\ (forall x1 x2 B H Q, K H Q -> app f [x1 x2] H Q))) (at level 0, f at level 0, x1 ident, x2 ident) : charac. -Notation "'Body' f x1 x2 x3 '=>' Q" := - (!B (forall K, is_spec_3 K -> - (forall x1 x2 x3, K x1 x2 x3 Q) -> spec_3 K f)) +Notation "'Body' f x1 x2 x3 '=>' K" := + (!Body ( curried 3 f + /\ (forall x1 x2 x3 B H Q, K H Q -> app f [x1 x2 x3] H Q))) (at level 0, f at level 0, x1 ident, x2 ident, x3 ident) : charac. -Notation "'Body' f [ A1 ] x1 '=>' Q" := - (!B (forall A1 K, is_spec_1 K -> - (forall x1, K x1 Q) -> spec_1 K f)) +Notation "'Body' f x1 x2 x3 x4 '=>' K" := + (!Body ( curried 4 f + /\ (forall x1 x2 x3 x4 B H Q, K H Q -> app f [x1 x2 x3 x4] H Q))) + (at level 0, f at level 0, x1 ident, x2 ident, x3 ident, x4 ident) : charac. + + +Notation "'Body' f [ A1 ] x1 '=>' K" := + (!Body ( curried 1 f + /\ (forall A1 x1 B H Q, K H Q -> app f [x1] H Q))) (at level 0, f at level 0, x1 ident, A1 ident) : charac. -Notation "'Body' f [ A1 ] x1 x2 '=>' Q" := - (!B (forall A1 K, is_spec_2 K -> - (forall x1 x2, K x1 x2 Q) -> spec_2 K f)) +Notation "'Body' f [ A1 ] x1 x2 '=>' K" := + (!Body ( curried 2 f + /\ (forall A1 x1 x2 B H Q, K H Q -> app f [x1 x2] H Q))) (at level 0, f at level 0, x1 ident, x2 ident, A1 ident) : charac. -Notation "'Body' f [ A1 A2 ] x1 '=>' Q" := - (!B (forall A1 A2 K, is_spec_1 K -> - (forall x1, K x1 Q) -> spec_1 K f)) +Notation "'Body' f [ A1 A2 ] x1 '=>' K" := + (!Body ( curried 1 f + /\ (forall A1 A2 x1 B H Q, K H Q -> app f [x1] H Q))) (at level 0, f at level 0, x1 ident, A1 ident, A2 ident) : charac. -Notation "'Body' f [ A1 A2 ] x1 x2 '=>' Q" := - (!B (forall A1 A2 K, is_spec_2 K -> - (forall x1 x2, K x1 x2 Q) -> spec_2 K f)) +Notation "'Body' f [ A1 A2 ] x1 x2 '=>' K" := + (!Body ( curried 2 f + /\ (forall A1 A2 x1 x2 B H Q, K H Q -> app f [x1 x2] H Q))) (at level 0, f at level 0, x1 ident, x2 ident, A1 ident, A2 ident) : charac. -(** Functions *) -Notation "'LetFuncs' f1 ':=' Q1 'in' Q2" := (* todo *) - (!F (fun H Q => forall f1, exists P1, - (Q1 -> P1 f1) /\ (P1 f1 -> Q2 H Q))) - (at level 69, f1 ident) : charac. -Notation "'LetFunc' f1 ':=' Q1 'in' Q2" := - (!F (fun H Q => forall f1, exists P1, - (Q1 -> P1 f1) /\ (P1 f1 -> Q2 H Q))) - (at level 69, f1 ident, only parsing) : charac. +(********************************************************************) +(** LetFun *) + + (* [LetFunc] is an auxiliary notation used by [LetFun] *) +Notation "'LetFunc' f ':=' F1 'in' F2" := + (!LetFun (fun H Q => forall f, exists P1, + (F1 -> P1 f) /\ (P1 f -> F2 H Q))) + (at level 69, f ident, only parsing) : charac. -Notation "'LetFun' f x1 ':=' Q 'in' F" := - (LetFunc f := (Body f x1 => Q) in F) +Notation "'LetFun' f x1 ':=' K 'in' F" := + (LetFunc f := (Body f x1 => K) in F) (at level 69, f ident, x1 ident) : charac. -Notation "'LetFun' f x1 x2 ':=' Q 'in' F" := - (LetFunc f := (Body f x1 x2 => Q) in F) +Notation "'LetFun' f x1 x2 ':=' K 'in' F" := + (LetFunc f := (Body f x1 x2 => K) in F) (at level 69, f ident, x1 ident, x2 ident) : charac. -Notation "'LetFun' f x1 x2 x3 ':=' Q 'in' F" := - (LetFunc f := (Body f x1 x2 x3 => Q) in F) +Notation "'LetFun' f x1 x2 x3 ':=' K 'in' F" := + (LetFunc f := (Body f x1 x2 x3 => K) in F) (at level 69, f ident, x1 ident, x2 ident, x3 ident) : charac. -Notation "'LetFun' f [ A1 ] x1 ':=' Q 'in' F" := - (LetFunc f := (Body f [ A1 ] x1 => Q) in F) +Notation "'LetFun' f x1 x2 x3 x4 ':=' K 'in' F" := + (LetFunc f := (Body f x1 x2 x3 x4 => K) in F) + (at level 69, f ident, x1 ident, x2 ident, x3 ident, x4 ident) : charac. + +(* FUTURE: LetFun for local polymorphic functions, following the above, + yet too many possibilities to do this now ... +Notation "'LetFun' f [ A1 ] x1 ':=' K 'in' F" := + (LetFunc f := (Body f [ A1 ] x1 => K) in F) (at level 69, f ident, x1 ident) : charac. +*) - (* todo: LetFun for local polymorphic functions *) -(** Mutually-recursive functions *) +(********************************************************************) +(** LetFuns *) -Notation "'LetFuns' f1 ':=' Q1 'and' f2 ':=' Q2 'in' F" := - (!F fun H Q => forall f1 f2, exists P1 P2, - (Q1 -> Q2 -> P1 f1 /\ P2 f2) /\ (P1 f1 -> P2 f2 -> F H Q)) +Notation "'LetFuns' f1 ':=' K1 'and' f2 ':=' K2 'in' F" := + (!LetFun fun H Q => forall f1 f2, exists P1 P2, + (K1 -> K2 -> P1 f1 /\ P2 f2) + /\ (P1 f1 -> P2 f2 -> F H Q)) (at level 69, f1 ident, f2 ident) : charac. -Notation "'LetFuns' f1 ':=' Q1 'and' f2 ':=' Q2 'and' f3 ':=' Q3 'in' F" := - (!F fun H Q => forall f1 f2 f3, exists P1 P2 P3, - (Q1 -> Q2 -> Q3 -> P1 f1 /\ P2 f2 /\ P3 f3) /\ (P1 f1 -> P2 f2 -> P3 f3 -> F H Q)) +Notation "'LetFuns' f1 ':=' K1 'and' f2 ':=' K2 'and' f3 ':=' K3 'in' F" := + (!LetFun fun H Q => forall f1 f2 f3, exists P1 P2 P3, + (K1 -> K2 -> K3 -> P1 f1 /\ P2 f2 /\ P3 f3) + /\ (P1 f1 -> P2 f2 -> P3 f3 -> F H Q)) (at level 69, f1 ident, f2 ident, f3 ident) : charac. -(** Tests *) +(* TODO: other arities for futual recursion *) -(* --old -Notation "'If_' F0 'Then' F1 'Else' F2" := - (!I (fun H Q => exists Q', - F0 H Q' /\ F1 (Q' true) Q /\ F2 (Q' false) Q)) - (at level 69, x at level 0) : charac. -*) -Notation "'_If' x 'Then' F1 'Else' F2" := - (!I (fun H Q => (x = true -> F1 H Q) /\ (x = false -> F2 H Q))) +(********************************************************************) +(** Let *) + +Notation "'Let' x ':=' F1 'in' F2" := + (!LetTrm (fun H Q => exists Q1, F1 H Q1 /\ forall x, F2 (Q1 x) Q)) + (at level 69, x ident, right associativity, + format "'[v' '[' 'Let' x ':=' F1 'in' ']' '/' '[' F2 ']' ']'") : charac. + +Notation "'Let' x ':' T ':=' F1 'in' F2" := + (!LetTrm (fun H Q => exists Q1, F1 H Q1 /\ forall x:T, F2 (Q1 x) Q)) + (at level 69, x ident, right associativity, only parsing) : charac. + + +(********************************************************************) +(** Seq *) + +Notation "'Seq_' Q1 ;; Q2" := + (!Seq (fun H Q => exists Q', Q1 H Q' /\ Q2 (Q' tt) Q)) + (at level 68, right associativity, + format "'[v' 'Seq_' '[' Q1 ']' ;; '/' '[' Q2 ']' ']'") : charac. + +Notation "Q1 ;; Q2" := + (!Seq (fun H Q => exists Q', Q1 H Q' /\ Q2 (Q' tt) Q)) + (at level 68, right associativity, only parsing, + format "'[v' '[' Q1 ']' ;; '/' '[' Q2 ']' ']'") : charac. + + +(********************************************************************) +(** Pay *) + +Notation "'Pay_' ;; Q1" := + (!Pay (fun H Q => exists H', pay_one H H' /\ Q1 H' Q)) + (at level 68, right associativity, + format "'[v' 'Pay_' ;; '[' Q1 ']' ']'") : charac. + + +(********************************************************************) +(** If and IfTrm and IfProp LetIf *) + +Notation "'If_' x 'Then' F1 'Else' F2" := + (!If (fun H Q => (x = true -> F1 H Q) /\ (x = false -> F2 H Q))) (at level 69, x at level 0) : charac. -Notation "'If_' F0 'Then' F1 'Else' F2" := - (Let x := F0 in _If x Then F1 Else F2) +Notation "'LetIf' F0 'Then' F1 'Else' F2" := + (Let x := F0 in If_ x Then F1 Else F2) (at level 69, only parsing) : charac. -Notation "'_If_' P 'Then' F1 'Else' F2" := - (!I (fun H Q => (P -> F1 H Q) /\ (~ P -> F2 H Q))) +Notation "'IfProp' P 'Then' F1 'Else' F2" := + (!If (fun H Q => (P -> F1 H Q) /\ (~ P -> F2 H Q))) (at level 69, P at level 0) : charac. -Notation "'LetIf' F0 'Then' F1 'Else' F2" := - (Let x := F0 in _If x Then F1 Else F2) - (at level 69, only parsing) : charac. + +(********************************************************************) +(** Case *) Notation "'Case' x '=' p 'Then' Q1 'Else' Q2" := - (!C (fun H Q => (x = p -> Q1 H Q) /\ (x <> p -> Q2 H Q))) + (!Case (fun H Q => (x = p -> Q1 H Q) /\ (x <> p -> Q2 H Q))) (at level 69, x at level 0) : charac. Notation "'Case' x '=' p [ x1 ] 'Then' Q1 'Else' Q2" := - (!C (fun H Q => (forall x1, x = p -> Q1 H Q) + (!Case (fun H Q => (forall x1, x = p -> Q1 H Q) /\ ((forall x1, x <> p) -> Q2 H Q))) (at level 69, x at level 0, x1 ident) : charac. Notation "'Case' x '=' p [ x1 x2 ] 'Then' Q1 'Else' Q2" := - (!C (fun H Q => (forall x1 x2, x = p -> Q1 H Q) + (!Case (fun H Q => (forall x1 x2, x = p -> Q1 H Q) /\ ((forall x1 x2, x <> p) -> Q2 H Q))) (at level 69, x at level 0, x1 ident, x2 ident) : charac. Notation "'Case' x '=' p [ x1 x2 x3 ] 'Then' Q1 'Else' Q2" := - (!C (fun H Q => (forall x1 x2 x3, x = p -> Q1 H Q) + (!Case (fun H Q => (forall x1 x2 x3, x = p -> Q1 H Q) /\ ((forall x1 x2 x3, x <> p) -> Q2 H Q))) (at level 69, x at level 0, x1 ident, x2 ident, x3 ident) : charac. Notation "'Case' x '=' p [ x1 x2 x3 x4 ] 'Then' Q1 'Else' Q2" := - (!C (fun H Q => (forall x1 x2 x3 x4, x = p -> Q1 H Q) + (!Case (fun H Q => (forall x1 x2 x3 x4, x = p -> Q1 H Q) /\ ((forall x1 x2 x3 x4, x <> p) -> Q2 H Q))) (at level 69, x at level 0, x1 ident, x2 ident, x3 ident, x4 ident) : charac. Notation "'Case' x '=' p [ x1 x2 x3 x4 x5 ] 'Then' Q1 'Else' Q2" := - (!C (fun H Q => (forall x1 x2 x3 x4 x5, x = p -> Q1 H Q) + (!Case (fun H Q => (forall x1 x2 x3 x4 x5, x = p -> Q1 H Q) /\ ((forall x1 x2 x3 x4 x5, x <> p) -> Q2 H Q))) (at level 69, x at level 0, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident) : charac. Notation "'Case' x '=' p [ x1 x2 x3 x4 x5 x6 ] 'Then' Q1 'Else' Q2" := - (!C (fun H Q => (forall x1 x2 x3 x4 x5 x6, x = p -> Q1 H Q) + (!Case (fun H Q => (forall x1 x2 x3 x4 x5 x6, x = p -> Q1 H Q) /\ ((forall x1 x2 x3 x4 x5 x6, x <> p) -> Q2 H Q))) (at level 69, x at level 0, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, x6 ident) : charac. Notation "'Case' x '=' p [ x1 x2 x3 x4 x5 x6 x7 ] 'Then' Q1 'Else' Q2" := - (!C (fun H Q => (forall x1 x2 x3 x4 x5 x6 x7, x = p -> Q1 H Q) + (!Case (fun H Q => (forall x1 x2 x3 x4 x5 x6 x7, x = p -> Q1 H Q) /\ ((forall x1 x2 x3 x4 x5 x6 x7, x <> p) -> Q2 H Q))) (at level 69, x at level 0, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, x6 ident, x7 ident) : charac. + +(********************************************************************) +(** CaseWhen *) + Notation "'Case' x '=' p 'When' w 'Then' Q1 'Else' Q2" := - (!W (fun H Q => (x = p -> istrue (w)%bool -> Q1 H Q) + (!CaseWhen (fun H Q => (x = p -> istrue (w)%bool -> Q1 H Q) /\ (x <> p \/ istrue (!w) -> Q2 H Q))) (at level 69, x at level 0) : charac. Notation "'Case' x '=' p [ x1 ] 'When' w 'Then' Q1 'Else' Q2" := - (!W (fun H Q => (forall x1, x = p -> istrue w%bool -> Q1 H Q) + (!CaseWhen (fun H Q => (forall x1, x = p -> istrue w%bool -> Q1 H Q) /\ ((forall x1, x <> p \/ istrue (!w)) -> Q2 H Q))) (at level 69, x at level 0, x1 ident) : charac. Notation "'Case' x '=' p [ x1 x2 ] 'When' w 'Then' Q1 'Else' Q2" := - (!W (fun H Q => (forall x1 x2, x = p -> istrue w%bool -> Q1 H Q) + (!CaseWhen (fun H Q => (forall x1 x2, x = p -> istrue w%bool -> Q1 H Q) /\ ((forall x1 x2, x <> p \/ istrue (!w)) -> Q2 H Q))) (at level 69, x at level 0, x1 ident, x2 ident) : charac. Notation "'Case' x '=' p [ x1 x2 x3 ] 'When' w 'Then' Q1 'Else' Q2" := - (!W (fun H Q => (forall x1 x2 x3, x = p -> istrue w%bool -> Q1 H Q) + (!CaseWhen (fun H Q => (forall x1 x2 x3, x = p -> istrue w%bool -> Q1 H Q) /\ ((forall x1 x2 x3, x <> p \/ istrue (!w)) -> Q2 H Q))) (at level 69, x at level 0, x1 ident, x2 ident, x3 ident) : charac. Notation "'Case' x '=' p [ x1 x2 x3 x4 ] 'When' w 'Then' Q1 'Else' Q2" := - (!W (fun H Q => (forall x1 x2 x3 x4, x = p -> istrue w%bool -> Q1 H Q) + (!CaseWhen (fun H Q => (forall x1 x2 x3 x4, x = p -> istrue w%bool -> Q1 H Q) /\ ((forall x1 x2 x3 x4, x <> p \/ istrue (!w)) -> Q2 H Q))) (at level 69, x at level 0, x1 ident, x2 ident, x3 ident, x4 ident) : charac. Notation "'Case' x '=' p [ x1 x2 x3 x4 x5 ] 'When' w 'Then' Q1 'Else' Q2" := - (!W (fun H Q => (forall x1 x2 x3 x4 x5, x = p -> istrue w%bool -> Q1 H Q) + (!CaseWhen (fun H Q => (forall x1 x2 x3 x4 x5, x = p -> istrue w%bool -> Q1 H Q) /\ ((forall x1 x2 x3 x4 x5, x <> p \/ istrue (!w)) -> Q2 H Q))) (at level 69, x at level 0, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident) : charac. Notation "'Case' x '=' p [ x1 x2 x3 x4 x5 x6 ] 'When' w 'Then' Q1 'Else' Q2" := - (!W (fun H Q => (forall x1 x2 x3 x4 x5 x6, x = p -> istrue w%bool -> Q1 H Q) + (!CaseWhen (fun H Q => (forall x1 x2 x3 x4 x5 x6, x = p -> istrue w%bool -> Q1 H Q) /\ ((forall x1 x2 x3 x4 x5 x6, x <> p \/ istrue (!w)) -> Q2 H Q))) (at level 69, x at level 0, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, x6 ident) : charac. Notation "'Case' x '=' p [ x1 x2 x3 x4 x5 x6 x7 ] 'When' w 'Then' Q1 'Else' Q2" := - (!W (fun H Q => (forall x1 x2 x3 x4 x5 x6 x7, x = p -> istrue w%bool -> Q1 H Q) + (!CaseWhen (fun H Q => (forall x1 x2 x3 x4 x5 x6 x7, x = p -> istrue w%bool -> Q1 H Q) /\ ((forall x1 x2 x3 x4 x5 x6 x7, x <> p \/ istrue (!w)) -> Q2 H Q))) (at level 69, x at level 0, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, x6 ident, x7 ident) : charac. + +(********************************************************************) +(** Match *) + Notation "'Match' n Q" := - (!M n Q) + (!Match n Q) (at level 69, n at level 0) : charac. -Notation "'Match' x : n Q" := - (!!M x n Q) - (at level 69, x ident, n at level 0) : charac. + +(********************************************************************) +(** Alias *) Notation "'Alias' x ':=' v 'in' Q" := - (!S (fun H Q => forall x, x = v -> Q H Q)) + (!Alias (fun H Q => forall x, x = v -> Q H Q)) (at level 69, x ident) : charac. -(** Loops *) -Notation "'_While' Q1 '_Do' Q2 '_Done'" := +(********************************************************************) +(** Fail *) + +Notation "'Fail'" := + (!Fail (fun _ _ => False)) + (at level 0) : charac. + + +(********************************************************************) +(** Done *) + +Notation "'Done'" := + (!Done (fun _ _ => True)) + (at level 0) : charac. + + +(********************************************************************) +(** While *) + +Notation "'While' Q1 'Do' Q2 'Done_'" := (!While (fun H Q => forall R:~~unit, is_local R -> - (forall H Q, (If_ Q1 Then (Q2 ;; R) Else (Ret tt)) H Q -> R H Q) + (forall H Q, (LetIf Q1 Then (Q2 ;; R) Else (Ret tt)) H Q -> R H Q) -> R H Q)) (at level 69, Q2 at level 68) : charac. -Notation "'For' i '=' a 'To' b 'Do' Q1 '_Done'" := - (!For (fun H Q => forall S:int->~~unit, is_local_pred S -> +(********************************************************************) +(** For *) + +Notation "'For' i '=' a 'To' b 'Do' Q1 'Done_'" := + (!For (fun H Q => forall S:int->~~unit, CFHeaps.is_local_pred S -> (forall i H Q, (i <= (b)%Z -> (Q1 ;; S (i+1)) H Q) /\ (i > b%Z -> (Ret tt) H Q) @@ -590,59 +539,56 @@ Notation "'For' i '=' a 'To' b 'Do' Q1 '_Done'" := -> S a H Q)) (at level 69, i ident, a at level 0, b at level 0) : charac. -(* DEPRECATED - - Notation "'While' Q1 'Do' Q2 'Done'" := - (!While (fun H Q => forall R:~~unit, is_local R -> - (forall H Q, (If_ Q1 Then (Q2 ;; R) Else (Ret tt)) H Q -> R H Q) - -> R H Q)) - (at level 69) : charac. - - Notation "'For' i '=' a 'To' b 'Do' Q1 'Done'" := - (!For (fun H Q => forall S:int->~~unit, is_local_pred S -> - (forall i H Q, - (i <= (b)%Z -> (Q1 ;; S (i+1)) H Q) - /\ (i > b%Z -> (Ret tt) H Q) - -> S i H Q) - -> S a H Q)) - (at level 69) : charac. -*) - -(** Top-level *) -Notation "'TopLet' x ':=' Q" := - (!TV (forall P, Q P -> P x)) - (at level 69, x at level 0, Q at level 200). +(********************************************************************) +(** TopVal *) + +Notation "'TopVal' x ':=' Q" := + (!TopVal (forall P, Q P -> P x)) + (at level 69, x at level 0, Q at level 200) + : charac. + +Notation "'TopVal' [ A1 ] x ':=' Q" := + (!TopVal (forall A1 P, Q (P A1) -> (P A1) x)) + (at level 69, x at level 0, A1 ident, Q at level 200) + : charac. + +Notation "'TopVal' [ A1 A2 ] x ':=' Q" := + (!TopVal (forall A1 A2 P, Q (P A1 A2) -> (P A1 A2) x)) + (at level 69, x at level 0, A1 ident, A2 ident, Q at level 200) + : charac. + +Notation "'TopVal' [ A1 A2 A3 ] x ':=' Q" := + (!TopVal (forall A1 A2 A3 P, Q (P A1 A2 A3) -> (P A1 A2 A3) x)) + (at level 69, x at level 0, A1 ident, A2 ident, A3 ident, Q at level 200) + : charac. + +(* DEPRECATED + Notation "'TopVal' x ':=' Q" := + (!TopVal (forall P:_->Prop, Q P -> P x)) (* with type annot *) + (at level 69, x at level 0, Q at level 200, only parsing) + : charac. +*) -Notation "'TopLet' x ':=' Q" := (* todo: needed? *) - (!TV (forall P:_->Prop, Q P -> P x)) - (at level 69, x at level 0, Q at level 200). -Notation "'TopLet' [ A1 ] x ':=' Q" := - (!TV (forall A1 P, Q (P A1) -> (P A1) x)) - (at level 69, x at level 0, A1 ident, Q at level 200). +(********************************************************************) +(** TopFun *) -Notation "'TopLet' [ A1 A2 ] x ':=' Q" := - (!TV (forall A1 A2 P, Q (P A1 A2) -> (P A1 A2) x)) - (at level 69, x at level 0, A1 ident, A2 ident, Q at level 200). +(* TODO: only one should be needed *) -Notation "'TopLet' [ A1 A2 A3 ] x ':=' Q" := - (!TV (forall A1 A2 A3 P, Q (P A1 A2 A3) -> (P A1 A2 A3) x)) - (at level 69, x at level 0, A1 ident, A2 ident, A3 ident, Q at level 200). +Notation "'TopFun' ':=' H" := + (!TopFun H) + (at level 69, H at level 200) : charac. -Notation "'TopLetFunc' ':=' H" := - (!TF H) - (at level 69, H at level 200). +Notation "'TopFun' f ':=' K" := + (!TopFun (fun P => forall f, K -> P f)) + (at level 69, f ident) : charac. -Notation "'TopLevelFun' P" := (* todo: why needed? *) - (tag tag_top_fun _ P) - (at level 95). -Notation "'Func' f ':=' Q" := (* todo:needed?*) - (!F (fun P => forall f, Q -> P f)) - (at level 69) : charac. +(********************************************************************) +(********************************************************************) (********************************************************************) (* ** Database of characteristic formulae *) @@ -678,3 +624,80 @@ Definition database_spec_unfocus := True. Notation "'unfocus'" := database_spec_unfocus. + + + + + + + + + + + + + + +(********************************************************************) +(********************************************************************) +(********************************************************************) +(* Implementation of labels *) + +(* FOR FUTURE USE + + Module Export AtomsEff. + + (** Variables are described as list of bits, e.g. [1::2::1::1::2::0]. + For efficiency, we do not use the type [list bool], but an ad-hoc + predicate with three constructors. *) + + Inductive atom : Set := + | atom_0 : atom + | atom_1 : atom -> atom + | atom_2 : atom -> atom. + + Instance atom_inhab : Inhab atom. + Proof. apply (prove_Inhab atom_0). Qed. + + (** Notation system *) + + Notation "'`0'" := (atom_0) + (at level 50, format "`0") : atom_scope. + Notation "'`1' v" := (atom_1 v) + (at level 50, v at level 50, format "`1 v") : atom_scope. + Notation "'`2' v" := (atom_2 v) + (at level 50, v at level 50, format "`2 v") : atom_scope. + Open Scope atom_scope. + Bind Scope atom_scope with atom. + Delimit Scope atom_scope with atom. + + End AtomsEff. + + Definition tag_name := atom. + Definition no_name := `0. + + Class Label := Label_create { Label_get : tag_name }. + + Instance Label_default : Label. + Proof. constructor. exact no_name. Defined. + + (* deprecated: The core idea of labelling can be summarized as follows: + Definition tag `{x:Label} (P:Prop) := P. + Notation "# P" := (@tag _ P) (at level 30). + Definition test P := (@tag (Label_create 3) P). + --> test displays as "fun P => # P" and does not show "3" + *) + + (* Update tags to: + Definition tag (t:tag_type) `{x:Label} (A:Type) (P:A) := P. + e.g. + Notation "'!B' P" := (tag tag_body _ P) + *) + + (* + + Ltac ltac_get_label tt := + match goal with |- tag _ (Label_create ?l) _ _ => constr:(l) end. + +*) +*) \ No newline at end of file diff --git a/lib/coq/CFTactics.v b/lib/coq/CFTactics.v index 7f19850..cbcfe4a 100644 --- a/lib/coq/CFTactics.v +++ b/lib/coq/CFTactics.v @@ -1,11 +1,6 @@ Set Implicit Arguments. -Require Export LibInt CFSpec CFPrint CFLemmasForTactics. +Require Export LibInt CFSpec CFPrint. -(* todo: move to libtactics *) - -Ltac is_not_evar E := - first [ is_evar E; fail 1 - | idtac ]. (********************************************************************) @@ -744,6 +739,36 @@ Tactic Notation "xskip_credits" := (*--------------------------------------------------------*) (* ** [xret] *) +(** Lemma used by [xret] *) + +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). + auto. rewrite star_comm. apply W. + apply~ local_erase. +Qed. + +(** Lemma used by [xret_no_gc] *) + +Lemma xret_no_gc_lemma : forall B (v:B) H (Q:B->hprop), + H ==> Q v -> + local (fun H' Q' => H' ==> Q' v) H Q. +Proof using. + introv W. apply~ local_erase. +Qed. + +(** Lemma used by [xret] and [xret_no_gc] + for when post-condition unifies trivially *) + +Lemma xret_lemma_unify : forall B (v:B) H, + local (fun H' Q' => H' ==> Q' v) H (fun x => \[x = v] \* H). +Proof using. + intros. apply~ local_erase. hsimpl. auto. +Qed. + + (** [xret]. *) Ltac xret_core := @@ -813,6 +838,16 @@ Tactic Notation "xpre" constr(H) := (*--------------------------------------------------------*) (* ** [xpost] *) +(** Lemma used by [xpost], + for introducing an evar for the post-condition *) + +Lemma xpost_lemma : forall B Q' Q (F:~~B) H, + is_local F -> + F H Q' -> + Q' ===> Q -> + F H Q. +Proof using. intros. applys* local_weaken. Qed. + Tactic Notation "xpost" := eapply xpost_lemma; [ try xlocal | | ]. @@ -863,6 +898,17 @@ Qed. (*--------------------------------------------------------*) (* ** [xgc] *) +(** Lemma used by [xgc_all], + to remove everything from the pre-condition *) + +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. + + + Ltac xgc_core := xextractible tt; eapply local_gc_post; @@ -898,6 +944,17 @@ Tactic Notation "xgc_all" := (*--------------------------------------------------------*) (* ** [xframe] *) +(** Lemma used by [xframe] *) + +Lemma xframe_lemma : forall H1 H2 B Q1 (F:~~B) H Q, + is_local F -> + H ==> H1 \* H2 -> + F H1 Q1 -> + Q1 \*+ H2 ===> Q -> + F H Q. +Proof using. intros. apply* local_wframe. Qed. + + Ltac xframe_remove_core H := xextractible tt; eapply xframe_lemma with (H2 := H); @@ -957,6 +1014,20 @@ Tactic Notation "xframes" constr(s1) constr(s2) constr(s3) := (*--------------------------------------------------------*) (* ** [xchange] *) +(** Lemma used by [xchange] *) + +Lemma xchange_lemma : forall H1 H1' H2 B H Q (F:~~B), + is_local F -> + (H1 ==> H1') -> + (H ==> H1 \* H2) -> + F (H1' \* H2) Q -> + F H Q. +Proof using. + introv W1 L W2 M. applys local_wframe __ \[]; eauto. + hsimpl. hchange~ W2. hsimpl~. rew_heap~. +Qed. + + Ltac xchange_apply L cont := eapply xchange_lemma; [ try xlocal | applys L | cont tt | ]. @@ -1794,6 +1865,25 @@ Tactic Notation "xfun_induction_nointro_skip" constr(S) ident(IH) := (*--------------------------------------------------------*) (* ** [xwhile] *) + +Lemma while_loop_cf_inv_measure : + forall (I:bool->int->hprop), + forall (F1:~~bool) (F2:~~unit) H (Q:unit->hprop), + (exists b m, H ==> I b m \* (Hexists G, G)) -> + (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')) -> + (Q = fun _ => Hexists m, I false m) -> + (While F1 Do F2 Done_) H Q. +Proof using. + introv (bi&mi&Hi) Hc Hs He. applys~ local_weaken_gc_pre (I bi mi). xlocal. + xextract as 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 as b m' E. xapplys IH. applys E. hsimpl. hsimpl. + xret_no_gc. subst Q. hsimpl. +Qed. + + Tactic Notation "xgeneralize" constr(E) "as" ident(H) := cuts H: E; [ eapply local_weaken_pre; [xlocal | | ] | ]. @@ -1821,6 +1911,58 @@ Tactic Notation "xwhile" constr(E) := (*--------------------------------------------------------*) (* ** [xfor] *) +Lemma for_loop_cf_to_inv : + forall I H', + forall (a:int) (b:int) (F:int->~~unit) H (Q:unit->hprop), + (a > (b)%Z -> H ==> (Q tt)) -> + (a <= (b)%Z -> + (H ==> I a \* H') + /\ (forall i, a <= i /\ i <= (b)%Z -> F i (I i) (# I(i+1))) + /\ (I ((b)%Z+1) \* H' ==> Q tt)) -> + (For i = a To b Do F i _Done) H Q. +Proof. + introv M1 M2. apply local_erase. intros S LS HS. + tests C: (a > b). + apply (rm HS). split; intros C'. math. xret_no_gc~. + forwards (Ma&Mb&Mc): (rm M2). math. + cuts P: (forall i, a <= i <= b+1 -> S i (I i) (# I (b+1))). + xapply P. math. hchanges Ma. hchanges Mc. + intros i. induction_wf IH: (int_upto_wf (b+1)) i. intros Bnd. + applys (rm HS). split; intros C'. + xseq. eapply Mb. math. xapply IH; auto with maths; hsimpl. + xret_no_gc. math_rewrite~ (i = b +1). +Qed. + +Lemma for_loop_cf_to_inv_gen' : + forall I H', + forall (a:int) (b:int) (F:int->~~unit) H, + (a <= (b)%Z -> + (H ==> I a \* H') + /\ (forall i, a <= i /\ i <= (b)%Z -> F i (I i) (# I(i+1)))) -> + (a > (b)%Z -> H ==> I ((b)%Z+1) \* H') -> + (For i = a To b Do F i _Done) H (# I ((b)%Z+1) \* H'). +Proof. intros. applys* for_loop_cf_to_inv. Qed. + +Lemma for_loop_cf_to_inv_gen : + forall I H', + forall (a:int) (b:int) (F:int->~~unit) H Q, + (a <= (b)%Z -> H ==> I a \* H') -> + (forall i, a <= i <= (b)%Z -> F i (I i) (# I(i+1))) -> + (a > (b)%Z -> H ==> I ((b)%Z+1) \* H') -> + (# (I ((b)%Z+1) \* H')) ===> Q -> + (For i = a To b Do F i _Done) H Q. +Proof. intros. applys* for_loop_cf_to_inv. intros C. hchange (H2 C). hchange (H3 tt). hsimpl. Qed. + + +Lemma for_loop_cf_to_inv_up : + forall I H', + forall (a:int) (b:int) (F:int->~~unit) H (Q:unit->hprop), + (a <= (b)%Z) -> + (H ==> I a \* H') -> + (forall i, a <= i /\ i <= (b)%Z -> F i (I i) (# I(i+1))) -> + ((# I ((b)%Z+1) \* H') ===> Q) -> + (For i = a To b Do F i _Done) H Q. +Proof. intros. applys* for_loop_cf_to_inv. intros. math. Qed. Ltac xfor_intros tt := let S := fresh "S" in let LS := fresh "L" S in @@ -2370,179 +2512,3 @@ Tactic Notation "xunfocus" constr(t1) constr(t2) constr(t3) := Tactic Notation "xunfocus" constr(t1) constr(t2) constr(t3) constr(t4) := xunfocus t1; xunfocus t2 t3 t4. - - -(************************************************************) -(* ** [xgo] *) - -Inductive Xhint_cmd := - | Xstop : Xhint_cmd - | XstopNoclear : Xhint_cmd - | XstopAfter : Xhint_cmd - | XstopInside : Xhint_cmd - | Xtactic : Xhint_cmd - | XtacticNostop : Xhint_cmd - | XtacticNoclear : Xhint_cmd - | XsubstAlias : Xhint_cmd - | XspecArgs : list Boxer -> list Boxer -> Xhint_cmd - | Xargs : forall A, A -> Xhint_cmd - | Xlet : forall A, A -> Xhint_cmd - | Xlets : forall A, A -> Xhint_cmd - | Xsimple : Xhint_cmd. - -Inductive Xhint (a : tag_name) (h : Xhint_cmd) := - | Xhint_intro : Xhint a h. - -Ltac add_hint a h := - let H := fresh "Hint" in - lets H: (Xhint_intro a h). - -Ltac clear_hint a := - match goal with H: Xhint a _ |- _ => clear H end. - -Ltac clears_hint tt := - repeat match goal with H: Xhint _ _ |- _ => clear H end. - -Ltac find_hint a := - match goal with H: Xhint a ?h |- _ => constr:(h) end. - -Ltac xgo_default solver cont := - match ltac_get_tag tt with - | tag_ret => xret; cont tt - | tag_fail => xfail; cont tt - | tag_done => xdone; cont tt - | tag_apply => xapp - | tag_seq => xseq; cont tt - | tag_let_val => xval; cont tt - | tag_let_trm => xlet; cont tt - | tag_let_fun => fail - | tag_body => fail - | tag_letrec => fail - | tag_case => xcases_real; cont tt - | tag_casewhen => fail - | tag_if => xif; cont tt - | tag_alias => xalias; cont tt - | tag_match ?n => xmatch; cont tt - | tag_top_val => fail - | tag_top_trm => fail - | tag_top_fun => fail - | tag_for => fail - | tag_while => fail - end. - -Ltac xtactic tag := idtac. - -Ltac run_hint h cont := - let tag := ltac_get_tag tt in - match h with - | Xstop => clears_hint tt; idtac - | XstopNoclear => idtac - | XstopAfter => - match tag with - | tag_let_trm => fail (* todo: xlet_with cont ltac:(fun _ => idtac)*) - | _ => xgo_default ltac:(fun _ => idtac) ltac:(fun _ => idtac) - end - | XstopInside => - match tag with - | tag_let_trm => fail (*todo: xlet_with ltac:(fun _ => idtac) cont *) - end - | Xtactic => clears_hint tt; xtactic tag - | XtacticNostop => xtactic tag; cont tt - | XtacticNoclear => xtactic tag - | XsubstAlias => xmatch_subst_alias; cont tt - | Xargs ?E => - match tag with - | tag_let_trm => fail (* todo!!*) - | tag_apply => xapp E (*todo: not needed?*) - end - | XspecArgs (>> ?S) ?E => - match tag with - | tag_let_trm => fail (* todo!!*) - | tag_apply => xapp_spec S E (*todo: not needed?*) - end - | Xlet ?S => - match tag with - | tag_let_trm => xlet S; cont tt - | tag_let_fun => xfun_noxbody S - end - | Xsimple => xmatch_simple; cont tt - (* todo : generalize - | tag_case => xcases_real - | tag_if => xif - | tag_match ?n => xmatch - *) - end. - -Ltac find_and_run_hint cont := - let a := ltac_get_label tt in - let h := find_hint a in - clear_hint a; - first [ run_hint h cont | fail 1 ]. - -Tactic Notation "xhint" := - find_and_run_hint ltac:(fun _ => idtac). - -Ltac xgo_core solver cont := - first [ find_and_run_hint cont - | xgo_default solver cont ]. - -Ltac xgo_core_once solver := - xgo_core solver ltac:(fun _ => idtac). - -Ltac xgo_core_repeat solver := - xgo_core solver ltac:(fun _ => instantiate; try solve [ solver tt ]; - instantiate; try xgo_core_repeat solver). - -Ltac xgo_pre tt := - first [ xcf; repeat progress(intros) - | repeat progress(intros) - | idtac ]. - -Ltac xgo_base solver := - xgo_pre tt; xgo_core_repeat solver. - -Tactic Notation "xgo1" := - xgo_core_once ltac:(fun _ => idtac). - -Tactic Notation "xgo" := - xgo_base ltac:(fun tt => idtac). -Tactic Notation "xgo" "~" := - xgo_base ltac:(fun tt => xauto~ ); instantiate; xauto~. -Tactic Notation "xgo" "*" := - xgo_base ltac:(fun tt => xauto* ); instantiate; xauto*. - -Tactic Notation "xgo" constr(a1) constr(h1) := - add_hint a1 h1; xgo. -Tactic Notation "xgo" constr(a1) constr(h1) "," constr(a2) constr(h2) := - add_hint a1 h1; add_hint a2 h2; xgo. -Tactic Notation "xgo" constr(a1) constr(h1) "," constr(a2) constr(h2) "," - constr(a3) constr(h3) := - add_hint a1 h1; add_hint a2 h2; add_hint a3 h3; xgo. -Tactic Notation "xgo" constr(a1) constr(h1) "," constr(a2) constr(h2) "," - constr(a3) constr(h3) "," constr(a4) constr(h4) := - add_hint a1 h1; add_hint a2 h2; add_hint a3 h3; add_hint a4 h4; xgo. - -Tactic Notation "xgo" "~" constr(a1) constr(h1) := - add_hint a1 h1; xgo~. -Tactic Notation "xgo" "~" constr(a1) constr(h1) "," constr(a2) constr(h2) := - add_hint a1 h1; add_hint a2 h2; xgo~. -Tactic Notation "xgo" "~" constr(a1) constr(h1) "," constr(a2) constr(h2) "," - constr(a3) constr(h3) := - add_hint a1 h1; add_hint a2 h2; add_hint a3 h3; xgo~. -Tactic Notation "xgo" "~" constr(a1) constr(h1) "," constr(a2) constr(h2) "," - constr(a3) constr(h3) "," constr(a4) constr(h4) := - add_hint a1 h1; add_hint a2 h2; add_hint a3 h3; add_hint a4 h4; xgo~. - -Tactic Notation "xgos" := - xgo; hsimpl. -Tactic Notation "xgos" "~" := - xgos; auto_tilde. -Tactic Notation "xgos" "*" := - xgos; auto_star. - - - -(**************************************************) -(**************************************************) -(**************************************************) - diff --git a/lib/coq/Makefile b/lib/coq/Makefile index b89fdd5..912a03a 100644 --- a/lib/coq/Makefile +++ b/lib/coq/Makefile @@ -17,7 +17,6 @@ SRC :=\ CFHeaps \ CFApp \ CFPrint \ - CFLemmasForTactics \ CFTactics \ CFHeader \ CFRep \ diff --git a/lib/coq/Shared.v b/lib/coq/Shared.v index a268c6c..0264bc4 100644 --- a/lib/coq/Shared.v +++ b/lib/coq/Shared.v @@ -1,6 +1,16 @@ Set Implicit Arguments. + +(********************************************************************) +(* TODO: move to libtactics *) + +Ltac is_not_evar E := + first [ is_evar E; fail 1 + | idtac ]. + + + (********************************************************************) (** Notation for functions expecting tuples as arguments *) -- GitLab