pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-27 23:06:20 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Merge pull request #55 from cpitclaudel/hoare_tweaks

Browse source 
Two tweaks in HoareLogic.v
This commit is contained in:
Adam Chlipala 2021-04-12 16:01:44 -04:00 committed by GitHub
commit 1d93f6f994
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 20 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
HoareLogic.v
View file

@ -191,20 +191,11 @@ Notation "'when' b 'then' then_ 'else' else_ 'done'" := (If_ b then_ else_) (at
Notation "{{ I }} 'while' b 'loop' body 'done'" := (While_ I b body) (at level 75).
Notation "'assert' {{ I }}" := (Assert I) (at level 75).
Delimit Scope cmd_scope with cmd.
(*Declare Scope reset_scope.*)
Infix "+" := plus : reset_scope.
Infix "-" := Init.Nat.sub : reset_scope.
Infix "*" := mult : reset_scope.
Infix "=" := eq : reset_scope.
Infix "<" := lt : reset_scope.
Delimit Scope reset_scope with reset.
Open Scope reset_scope.
(* END macros *)
(* We should draw some attention to the next notation, which defines special
* lambdas for writing assertions. *)
Notation "h & v ~> e" := (fun h v => e%reset) (at level 85, v at level 0).
Notation "h & v ~> e" := (fun h v => e%nat%type) (at level 85, v at level 0).
(* And here's the classic notation for Hoare triples. *)
Notation "{{ P }} c {{ Q }}" := (hoare_triple P c%cmd Q) (at level 90, c at next level).
@ -224,9 +215,15 @@ Qed.
* rules. Some other obligations are generated, generally of implications
* between assertions, and [ht] also makes a best effort to solve those. *)
Ltac ht1 := apply HtSkip || apply HtAssign || apply HtWrite || eapply HtSeq
Ltac ht1 :=
match goal with
| [ |- {{ _ }} _ {{ ?P }} ] =>
tryif is_evar P then
apply HtSkip || apply HtAssign || apply HtWrite || eapply HtSeq
|| eapply HtIf || eapply HtWhile || eapply HtAssert
|| eapply HtStrengthenPost.
else
eapply HtStrengthenPost
end.
Ltac t := cbv beta; propositional; subst;
repeat match goal with

20
HoareLogic_template.v
View file

@ -162,19 +162,11 @@ Notation "'when' b 'then' then_ 'else' else_ 'done'" := (If_ b then_ else_) (at
Notation "{{ I }} 'while' b 'loop' body 'done'" := (While_ I b body) (at level 75).
Notation "'assert' {{ I }}" := (Assert I) (at level 75).
Delimit Scope cmd_scope with cmd.
Infix "+" := plus : reset_scope.
Infix "-" := Init.Nat.sub : reset_scope.
Infix "*" := mult : reset_scope.
Infix "=" := eq : reset_scope.
Infix "<" := lt : reset_scope.
Delimit Scope reset_scope with reset.
Open Scope reset_scope.
(* END macros *)
(* We should draw some attention to the next notation, which defines special
* lambdas for writing assertions. *)
Notation "h & v ~> e" := (fun h v => e%reset) (at level 85, v at level 0).
Notation "h & v ~> e" := (fun h v => e%nat%type) (at level 85, v at level 0).
(* And here's the classic notation for Hoare triples. *)
Notation "{{ P }} c {{ Q }}" := (hoare_triple P c%cmd Q) (at level 90, c at next level).
@ -194,9 +186,15 @@ Qed.
* rules. Some other obligations are generated, generally of implications
* between assertions, and [ht] also makes a best effort to solve those. *)
Ltac ht1 := apply HtSkip || apply HtAssign || apply HtWrite || eapply HtSeq
Ltac ht1 :=
match goal with
| [ |- {{ _ }} _ {{ ?P }} ] =>
tryif is_evar P then
apply HtSkip || apply HtAssign || apply HtWrite || eapply HtSeq
|| eapply HtIf || eapply HtWhile || eapply HtAssert
|| eapply HtStrengthenPost.
else
eapply HtStrengthenPost
end.
Ltac t := cbv beta; propositional; subst;
repeat match goal with