Commit 66f61d49 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Improve heap_lang notations a bit.

parent 38d2f0d2
...@@ -32,7 +32,7 @@ Module notations. ...@@ -32,7 +32,7 @@ Module notations.
(* What about Arguments for hoare triples?. *) (* What about Arguments for hoare triples?. *)
(* The colons indicate binders. "let" is not consistent here though, (* The colons indicate binders. "let" is not consistent here though,
thing are only bound in the "in". *) thing are only bound in the "in". *)
Notation "# n" := (Var n) (at level 1, format "# n") : lang_scope. Notation "# n" := (ids (term:=expr) n) (at level 1, format "# n") : lang_scope.
Notation "! e" := (Load e%L) (at level 10, format "! e") : lang_scope. Notation "! e" := (Load e%L) (at level 10, format "! e") : lang_scope.
Notation "'ref' e" := (Alloc e%L) (at level 30) : lang_scope. Notation "'ref' e" := (Alloc e%L) (at level 30) : lang_scope.
Notation "e1 + e2" := (Plus e1%L e2%L) Notation "e1 + e2" := (Plus e1%L e2%L)
...@@ -41,12 +41,14 @@ Module notations. ...@@ -41,12 +41,14 @@ Module notations.
Notation "e1 < e2" := (Lt e1%L e2%L) (at level 70) : lang_scope. Notation "e1 < e2" := (Lt e1%L e2%L) (at level 70) : lang_scope.
(* The unicode ← is already part of the notation "_ ← _; _" for bind. *) (* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
Notation "e1 <- e2" := (Store e1%L e2%L) (at level 80) : lang_scope. Notation "e1 <- e2" := (Store e1%L e2%L) (at level 80) : lang_scope.
Notation "e1 ; e2" := (Seq e1%L e2%L) (at level 100) : lang_scope. Notation "e1 ; e2" := (Seq e1%L e2%L)
Notation "'let:' e1 'in' e2" := (Let e1%L e2%L) (at level 102) : lang_scope. (at level 100, e2 at level 200) : lang_scope.
Notation "'λ:' e" := (Lam e%L) (at level 102) : lang_scope. Notation "'let:' e1 'in' e2" := (Let e1%L e2%L)
Notation "'rec::' e" := (Rec e%L) (at level 102) : lang_scope. (at level 102, e2 at level 200) : lang_scope.
Notation "'λ:' e" := (Lam e%L) (at level 102, e at level 200) : lang_scope.
Notation "'rec::' e" := (Rec e%L) (at level 102, e at level 200) : lang_scope.
Notation "'if' e1 'then' e2 'else' e3" := (If e1%L e2%L e3%L) Notation "'if' e1 'then' e2 'else' e3" := (If e1%L e2%L e3%L)
(at level 200, e1, e2, e3 at level 200, only parsing) : lang_scope. (at level 200, e1, e2, e3 at level 200) : lang_scope.
End notations. End notations.
Section suger. Section suger.
......
...@@ -54,16 +54,15 @@ Module LiftingTests. ...@@ -54,16 +54,15 @@ Module LiftingTests.
(* TODO: once asimpl preserves notation, we don't need (* TODO: once asimpl preserves notation, we don't need
FindPred' anymore. *) FindPred' anymore. *)
(* FIXME: fix notation so that we do not need parenthesis or %L *) (* FIXME: fix notation so that we do not need parenthesis or %L *)
Definition FindPred' n1 Sn1 n2 f : expr := Definition FindPred' (n1 Sn1 n2 f : expr) : expr :=
if Sn1 < n2 then f Sn1 else n1. if Sn1 < n2 then f Sn1 else n1.
Definition FindPred n2 : expr := Definition FindPred (n2 : expr) : expr :=
rec:: (let: #1 + 1 in FindPred' #2 #0 n2.[ren(+3)] #1)%L. rec:: let: #1 + 1 in FindPred' #2 #0 n2.[ren(+3)] #1.
Definition Pred : expr := Definition Pred : expr :=
λ: (if #0 0 then 0 else FindPred #0 0)%L. λ: if #0 0 then 0 else FindPred #0 0.
Lemma FindPred_spec n1 n2 E Q : Lemma FindPred_spec n1 n2 E Q :
((n1 < n2) Q (pred n2)) ( (n1 < n2) Q (pred n2)) wp E (FindPred n2 n1) Q.
wp E (FindPred n2 n1) Q.
Proof. Proof.
revert n1. apply löb_all_1=>n1. revert n1. apply löb_all_1=>n1.
rewrite -wp_rec //. asimpl. rewrite -wp_rec //. asimpl.
...@@ -71,8 +70,10 @@ Module LiftingTests. ...@@ -71,8 +70,10 @@ Module LiftingTests.
etransitivity; first (etransitivity; last eapply equiv_spec, later_and). etransitivity; first (etransitivity; last eapply equiv_spec, later_and).
{ apply and_mono; first done. by rewrite -later_intro. } { apply and_mono; first done. by rewrite -later_intro. }
apply later_mono. apply later_mono.
(* Go on. *) (* "rewrite -(wp_let _ _ (FindPred' n1 #0 n2 (FindPred n2)))" started to
rewrite -(wp_let _ _ (FindPred' n1 #0 n2 (FindPred n2))). fail after we changed # n to use ids instead of Var *)
pose proof (wp_let (Σ:=Σ) E (n1 + 1)%L (FindPred' n1 #0 n2 (FindPred n2)) Q).
unfold Let, Lam in H; rewrite -H.
rewrite -wp_plus. asimpl. rewrite -wp_plus. asimpl.
rewrite -(wp_bindi (CaseCtx _ _)). rewrite -(wp_bindi (CaseCtx _ _)).
rewrite -!later_intro /=. rewrite -!later_intro /=.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment