From 2ed1d52171bdda1e610184f3a543f0c7333b6280 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Pit-Claudel?= Date: Mon, 12 Apr 2021 15:04:56 -0400 Subject: [PATCH 1/2] =?UTF-8?q?Get=20rid=20of=20the=20=E2=80=9Creset?= =?UTF-8?q?=E2=80=9D=20scope=20in=20HoareLogic.v?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit It's not needed, and it makes everything harder to read. --- HoareLogic.v | 11 +---------- HoareLogic_template.v | 10 +--------- 2 files changed, 2 insertions(+), 19 deletions(-) diff --git a/HoareLogic.v b/HoareLogic.v index 1ca0273..834cd1c 100644 --- a/HoareLogic.v +++ b/HoareLogic.v @@ -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). diff --git a/HoareLogic_template.v b/HoareLogic_template.v index a196e23..5ddce34 100644 --- a/HoareLogic_template.v +++ b/HoareLogic_template.v @@ -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). From 1e817212680553abda44a95ae16e2be28429b41d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Pit-Claudel?= Date: Mon, 12 Apr 2021 15:07:34 -0400 Subject: [PATCH 2/2] Make the ht1 tactic a bit more robust in HoareLogic.v (Without this change, the HtIf rule can fail to generalize and unify spuriously with goals of the right shape) --- HoareLogic.v | 12 +++++++++--- HoareLogic_template.v | 12 +++++++++--- 2 files changed, 18 insertions(+), 6 deletions(-) diff --git a/HoareLogic.v b/HoareLogic.v index 834cd1c..244955d 100644 --- a/HoareLogic.v +++ b/HoareLogic.v @@ -215,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 - || eapply HtIf || eapply HtWhile || eapply HtAssert - || eapply HtStrengthenPost. +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 + else + eapply HtStrengthenPost + end. Ltac t := cbv beta; propositional; subst; repeat match goal with diff --git a/HoareLogic_template.v b/HoareLogic_template.v index 5ddce34..baae6e2 100644 --- a/HoareLogic_template.v +++ b/HoareLogic_template.v @@ -186,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 - || eapply HtIf || eapply HtWhile || eapply HtAssert - || eapply HtStrengthenPost. +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 + else + eapply HtStrengthenPost + end. Ltac t := cbv beta; propositional; subst; repeat match goal with