summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/coq/Hoare.v146
-rw-r--r--lib/coq/Sail2_prompt.v6
-rw-r--r--lib/coq/Sail2_state.v6
-rw-r--r--lib/coq/Sail2_state_lemmas.v10
-rw-r--r--src/pretty_print_coq.ml20
5 files changed, 130 insertions, 58 deletions
diff --git a/lib/coq/Hoare.v b/lib/coq/Hoare.v
index aff3a210..e3090373 100644
--- a/lib/coq/Hoare.v
+++ b/lib/coq/Hoare.v
@@ -1,5 +1,5 @@
-Require Import String.
-Require Import Sail2_state_monad Sail2_state Sail2_state_monad_lemmas.
+Require Import String ZArith.
+Require Import Sail2_state_monad Sail2_prompt Sail2_state Sail2_state_monad_lemmas.
Require Import Sail2_state_lemmas.
(*adhoc_overloading
@@ -324,6 +324,13 @@ intros PP BC.
eauto using PrePostE_consequence.
Qed.
+Lemma PrePostE_weaken_Epost Regs Aty Ety (A : predS Regs) f (B : Aty -> predS Regs) (E F : ex Ety -> predS Regs) :
+ PrePostE A f B E ->
+ (forall v s, E v s -> F v s) ->
+ PrePostE A f B F.
+intros PP EF.
+eauto using PrePostE_consequence.
+Qed.
(*named_theorems PrePostE_compositeI
named_theorems PrePostE_atomI*)
@@ -605,47 +612,106 @@ intros H.
apply PrePost_foreachS_invariant with (Q := fun v => match v with Value a => Q a | Ex e => E e end).
auto.
Qed.
-(*
-Lemma PrePostE_untilS:
- assumes dom: (forall s, Inv Q vars s -> untilS_dom (vars, cond, body, s)"
- and cond: (forall vars, PrePostE (Inv' Q vars) (cond vars) (fun c s' => Inv Q vars s' /\ (c \<longrightarrow> Q vars s')) E"
- and body: (forall vars, PrePostE (Inv Q vars) (body vars) (Inv' Q) E"
- shows "PrePostE (Inv Q vars) (untilS vars cond body) Q E"
-proof (unfold PrePostE_def, rule PrePostI)
- fix s r s'
- assume Inv_s: "Inv Q vars s" and r: "(r, s') \<in> untilS vars cond body s"
- with dom[OF Inv_s] cond body
- show "(case r of Value a => Q a | result.Ex e => E e) s'"
- proof (induction vars cond body s rule: untilS.pinduct[case_names Step])
- case (Step vars cond body s)
- consider
- (Value) vars' c sb sc where "(Value vars', sb) \<in> body vars s" and "(Value c, sc) \<in> cond vars' sb"
- and "if c then r = Value vars' /\ s' = sc else (r, s') \<in> untilS vars' cond body sc"
- | (Ex) e where "(Ex e, s') \<in> bindS (body vars) cond s" and "r = Ex e"
- using Step(1,6)
- by (auto simp: untilS.psimps returnS_def Ex_bindS_iff elim!: bindS_cases split: if_splits; fastforce)
- then show ?case
- proof cases
- case Value
- then show ?thesis using Step.IH[OF Value(1,2) _ Step(3,4)] Step(3,4,5)
- by (auto split: if_splits elim: PrePostE_elim)
- next
- case Ex
- then show ?thesis using Step(3,4,5) by (auto elim!: bindS_cases PrePostE_elim)
- qed
- qed
-qed
-lemma PrePostE_untilS_pure_cond:
- assumes dom: (forall s, Inv Q vars s -> untilS_dom (vars, returnS \<circ> cond, body, s)"
- and body: (forall vars, PrePostE (Inv Q vars) (body vars) (fun vars' s' => Inv Q vars' s' /\ (cond vars' \<longrightarrow> Q vars' s')) E"
- shows "PrePostE (Inv Q vars) (untilS vars (returnS \<circ> cond) body) Q E"
- using assms by (intro PrePostE_untilS) (auto simp: comp_def)
+Lemma PrePostE_use_pre Regs A Ety m (P : predS Regs) (Q : A -> predS Regs) (E : ex Ety -> predS Regs) :
+ (forall s, P s -> PrePostE P m Q E) ->
+ PrePostE P m Q E.
+unfold PrePostE, PrePost.
+intros H s p r s' IN.
+eapply H; eauto.
+Qed.
+
+Local Open Scope Z.
+Local Opaque _limit_reduces.
+Ltac gen_reduces :=
+ match goal with |- context[@_limit_reduces ?a ?b ?c] => generalize (@_limit_reduces a b c) end.
+
+
+Lemma PrePostE_untilST Regs Vars Ety vars measure cond (body : Vars -> monadS Regs Vars Ety) Inv Inv' (Q : Vars -> predS Regs) E :
+ (forall vars, PrePostE (Inv' Q vars) (cond vars) (fun c s' => Inv Q vars s' /\ (c = true -> Q vars s')) E) ->
+ (forall vars, PrePostE (Inv Q vars) (body vars) (fun vars' s' => Inv' Q vars' s' /\ measure vars' < measure vars) E) ->
+ (forall vars s, Inv Q vars s -> measure vars >= 0) ->
+ PrePostE (Inv Q vars) (untilST vars measure cond body) Q E.
+
+intros Hcond Hvars Hmeasure.
+unfold untilST.
+apply PrePostE_use_pre. intros s0 Pre0.
+assert (measure vars >= 0) as Hlimit_0 by eauto. clear s0 Pre0.
+remember (measure vars) as limit eqn: Heqlimit in Hlimit_0 |- *.
+assert (measure vars <= limit) as Hlimit by omega. clear Heqlimit.
+generalize (Sail2_prompt.Zwf_guarded limit).
+revert vars Hlimit.
+apply Wf_Z.natlike_ind with (x := limit).
+* intros vars Hmeasure_limit [acc]. simpl.
+ eapply PrePostE_bindS with (R := (fun vars' s' => Inv' Q vars' s' /\ measure vars' < measure vars)).
+ + intros s vars' s' IN.
+ eapply PrePostE_bindS with (R := (fun c s' => (Inv Q vars' s' /\ (c = true -> Q vars' s')) /\ measure vars' < measure vars)).
+ 2: {
+ apply PrePostE_weaken_Epost with (E := (fun e s' => E e s' /\ measure vars' < measure vars)). 2: tauto.
+ eapply PrePostE_conj_conds.
+ apply Hcond.
+ apply PrePostE_I; tauto.
+ }
+ intros.
+ destruct a.
+ - eapply PrePostE_strengthen_pre; try apply PrePostE_returnS.
+ intros ? [[? ?] ?]; auto.
+ - apply PrePostE_I.
+ intros ? ? ? [[? ?] ?] ?. exfalso.
+ specialize (Hmeasure _ _ H0). omega.
+ intros ? ? ? [[? ?] ?] ?. exfalso.
+ specialize (Hmeasure _ _ H0). omega.
+ + apply Hvars.
+* intros limit' Hlimit' IH vars Hmeasure_limit [acc].
+ simpl.
+ destruct (Z_ge_dec _ _); try omega.
+ eapply PrePostE_bindS; [ | apply Hvars].
+ intros s vars' s' IN.
+ eapply PrePostE_bindS with (R := (fun c s' => (Inv Q vars' s' /\ (c = true -> Q vars' s')) /\ measure vars' < measure vars)).
+ 2: {
+ apply PrePostE_weaken_Epost with (E := (fun e s' => E e s' /\ measure vars' < measure vars)). 2: tauto.
+ eapply PrePostE_conj_conds.
+ apply Hcond.
+ apply PrePostE_I; tauto.
+ }
+ intros.
+ destruct a.
+ - eapply PrePostE_strengthen_pre; try apply PrePostE_returnS.
+ intros ? [[? ?] ?]; auto.
+ - gen_reduces.
+ replace (Z.succ limit' - 1) with limit'; [ | omega].
+ intro acc'.
+ apply PrePostE_use_pre. intros sx [[Pre _] Hreduces].
+ apply Hmeasure in Pre.
+ eapply PrePostE_strengthen_pre; [apply IH | ].
+ + omega.
+ + tauto.
+* omega.
+Qed.
+
+
+Lemma PrePostE_untilST_pure_cond Regs Vars Ety vars measure cond (body : Vars -> monadS Regs Vars Ety) Inv (Q : Vars -> predS Regs) E :
+ (forall vars, PrePostE (Inv Q vars) (body vars) (fun vars' s' => Inv Q vars' s' /\ measure vars' < measure vars /\ (cond vars' = true -> Q vars' s')) E) ->
+ (forall vars s, Inv Q vars s -> measure vars >= 0) ->
+ (PrePostE (Inv Q vars) (untilST vars measure (fun vars => returnS (cond vars)) body) Q E).
+intros.
+apply PrePostE_untilST with (Inv' := fun Q vars s => Inv Q vars s /\ (cond vars = true -> Q vars s)).
+* intro.
+ apply PrePostE_returnS with (P := fun c s' => Inv Q vars0 s' /\ (c = true -> Q vars0 s')).
+* intro.
+ eapply PrePost_weaken_post; [ apply H | ].
+ simpl. intros [a |e]; eauto. tauto.
+* apply H0.
+Qed.
+
+Local Close Scope Z.
+
+(*
lemma PrePostE_liftState_untilM:
- assumes dom: (forall s, Inv Q vars s -> untilM_dom (vars, cond, body)"
- and cond: (forall vars, PrePostE (Inv' Q vars) (liftState r (cond vars)) (fun c s' => Inv Q vars s' /\ (c \<longrightarrow> Q vars s')) E"
- and body: (forall vars, PrePostE (Inv Q vars) (liftState r (body vars)) (Inv' Q) E"
+ assumes dom: (forall s, Inv Q vars s -> untilM_dom (vars, cond, body))
+ and cond: (forall vars, PrePostE (Inv' Q vars) (liftState r (cond vars)) (fun c s' => Inv Q vars s' /\ (c \<longrightarrow> Q vars s')) E)
+ and body: (forall vars, PrePostE (Inv Q vars) (liftState r (body vars)) (Inv' Q) E)
shows "PrePostE (Inv Q vars) (liftState r (untilM vars cond body)) Q E"
proof -
have domS: "untilS_dom (vars, liftState r \<circ> cond, liftState r \<circ> body, s)" if "Inv Q vars s" for s
diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index b5e94e46..79bf87eb 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -149,7 +149,8 @@ Fixpoint whileMT' {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool
else returnm vars
else Fail "Termination limit reached".
-Definition whileMT {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) : monad RV Vars E :=
+Definition whileMT {RV Vars E} (vars : Vars) (measure : Vars -> Z) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) : monad RV Vars E :=
+ let limit := measure vars in
whileMT' limit vars cond body (Zwf_guarded limit).
(*val untilM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
@@ -161,7 +162,8 @@ Fixpoint untilMT' {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool
if cond_val then returnm vars else untilMT' (limit - 1) vars cond body (_limit_reduces acc)
else Fail "Termination limit reached".
-Definition untilMT {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) : monad RV Vars E :=
+Definition untilMT {RV Vars E} (vars : Vars) (measure : Vars -> Z) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) : monad RV Vars E :=
+ let limit := measure vars in
untilMT' limit vars cond body (Zwf_guarded limit).
(*let write_two_regs r1 r2 vec =
diff --git a/lib/coq/Sail2_state.v b/lib/coq/Sail2_state.v
index bd18783f..dc635cb4 100644
--- a/lib/coq/Sail2_state.v
+++ b/lib/coq/Sail2_state.v
@@ -130,7 +130,8 @@ Fixpoint whileST' {RV Vars E} limit (vars : Vars) (cond : Vars -> monadS RV bool
else returnS vars
else failS "Termination limit reached".
-Definition whileST {RV Vars E} limit (vars : Vars) (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) : monadS RV Vars E :=
+Definition whileST {RV Vars E} (vars : Vars) measure (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) : monadS RV Vars E :=
+ let limit := measure vars in
whileST' limit vars cond body (Zwf_guarded limit).
(*val untilM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
@@ -142,7 +143,8 @@ Fixpoint untilST' {RV Vars E} limit (vars : Vars) (cond : Vars -> monadS RV bool
if cond_val then returnS vars else untilST' (limit - 1) vars cond body (_limit_reduces acc)
else failS "Termination limit reached".
-Definition untilST {RV Vars E} limit (vars : Vars) (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) : monadS RV Vars E :=
+Definition untilST {RV Vars E} (vars : Vars) measure (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) : monadS RV Vars E :=
+ let limit := measure vars in
untilST' limit vars cond body (Zwf_guarded limit).
diff --git a/lib/coq/Sail2_state_lemmas.v b/lib/coq/Sail2_state_lemmas.v
index 563a17a6..54cf45cc 100644
--- a/lib/coq/Sail2_state_lemmas.v
+++ b/lib/coq/Sail2_state_lemmas.v
@@ -480,9 +480,10 @@ Local Opaque _limit_reduces.
Ltac gen_reduces :=
match goal with |- context[@_limit_reduces ?a ?b ?c] => generalize (@_limit_reduces a b c) end.
-Lemma liftState_whileM RV Vars E r limit vars cond (body : Vars -> monad RV Vars E) s :
- liftState (Regs := RV) r (whileMT limit vars cond body) s = whileST limit vars (fun vars => liftState r (cond vars)) (fun vars => liftState r (body vars)) s.
+Lemma liftState_whileM RV Vars E r measure vars cond (body : Vars -> monad RV Vars E) s :
+ liftState (Regs := RV) r (whileMT vars measure cond body) s = whileST vars measure (fun vars => liftState r (cond vars)) (fun vars => liftState r (body vars)) s.
unfold whileMT, whileST.
+generalize (measure vars) as limit. intro.
revert vars s.
destruct (Z.le_decidable 0 limit).
* generalize (Zwf_guarded limit) as acc.
@@ -552,9 +553,10 @@ proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState
qed auto
qed*)
-Lemma liftState_untilM RV Vars E r limit vars cond (body : Vars -> monad RV Vars E) s :
- liftState (Regs := RV) r (untilMT limit vars cond body) s = untilST limit vars (fun vars => liftState r (cond vars)) (fun vars => liftState r (body vars)) s.
+Lemma liftState_untilM RV Vars E r measure vars cond (body : Vars -> monad RV Vars E) s :
+ liftState (Regs := RV) r (untilMT vars measure cond body) s = untilST vars measure (fun vars => liftState r (cond vars)) (fun vars => liftState r (body vars)) s.
unfold untilMT, untilST.
+generalize (measure vars) as limit. intro.
revert vars s.
destruct (Z.le_decidable 0 limit).
* generalize (Zwf_guarded limit) as acc.
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 1fea72ea..52117a74 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1610,22 +1610,22 @@ let doc_exp, doc_let =
,_),body'),_) -> body'
| _ -> body
in
- let msuffix, measure_pp =
- match measure with
- | None -> "", []
- | Some exp -> "T", [expY exp]
- in
let used_vars_body = find_e_ids body in
let varstuple_pp, lambda =
make_loop_vars [] varstuple
in
+ let msuffix, measure_pp =
+ match measure with
+ | None -> "", []
+ | Some exp -> "T", [parens (prefix 2 1 (group lambda) (expN exp))]
+ in
parens (
(prefix 2 1)
- ((separate space) (string (combinator ^ csuffix ^ msuffix)::
- measure_pp@[varstuple_pp]))
- ((prefix 0 1)
- (parens (prefix 2 1 (group lambda) (expN cond)))
- (parens (prefix 2 1 (group lambda) (expN body))))
+ (string (combinator ^ csuffix ^ msuffix))
+ (separate (break 1)
+ (varstuple_pp::measure_pp@
+ [parens (prefix 2 1 (group lambda) (expN cond));
+ parens (prefix 2 1 (group lambda) (expN body))]))
)
end
| Id_aux (Id "early_return", _) ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 16:28:03 +0000