mirror of
https://github.com/achlipala/frap.git
synced 2024-11-28 07:16:20 +00:00
Turn off some warnings
This commit is contained in:
parent
19d915fb37
commit
64fe989cdb
4 changed files with 75 additions and 64 deletions
|
@ -3,6 +3,8 @@
|
||||||
* Author: Adam Chlipala
|
* Author: Adam Chlipala
|
||||||
* License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *)
|
* License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *)
|
||||||
|
|
||||||
|
Set Warnings "-notation-overridden". (* <-- needed while we play with defining one
|
||||||
|
* of the book's notations ourselves locally *)
|
||||||
Require Import Frap TransitionSystems.
|
Require Import Frap TransitionSystems.
|
||||||
|
|
||||||
Set Implicit Arguments.
|
Set Implicit Arguments.
|
||||||
|
|
|
@ -3,6 +3,8 @@
|
||||||
* Author: Adam Chlipala
|
* Author: Adam Chlipala
|
||||||
* License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *)
|
* License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *)
|
||||||
|
|
||||||
|
Set Warnings "-notation-overridden". (* <-- needed while we play with defining one
|
||||||
|
* of the book's notations ourselves locally *)
|
||||||
Require Import Frap TransitionSystems.
|
Require Import Frap TransitionSystems.
|
||||||
|
|
||||||
Set Implicit Arguments.
|
Set Implicit Arguments.
|
||||||
|
@ -175,28 +177,64 @@ Qed.
|
||||||
Theorem factorial_ok_2 :
|
Theorem factorial_ok_2 :
|
||||||
invariantFor (factorial_sys 2) (fact_correct 2).
|
invariantFor (factorial_sys 2) (fact_correct 2).
|
||||||
Proof.
|
Proof.
|
||||||
Admitted.
|
simplify.
|
||||||
|
eapply invariant_weaken.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
apply multiStepClosure_ok.
|
||||||
|
simplify.
|
||||||
|
rewrite fact_init_is.
|
||||||
|
|
||||||
|
eapply MscStep.
|
||||||
|
apply oneStepClosure_split.
|
||||||
|
simplify.
|
||||||
|
invert H.
|
||||||
|
simplify.
|
||||||
|
apply singleton_in.
|
||||||
|
apply oneStepClosure_empty.
|
||||||
|
simplify.
|
||||||
|
|
||||||
|
eapply MscStep.
|
||||||
|
apply oneStepClosure_split.
|
||||||
|
simplify.
|
||||||
|
invert H.
|
||||||
|
simplify.
|
||||||
|
apply singleton_in.
|
||||||
|
apply oneStepClosure_split.
|
||||||
|
simplify.
|
||||||
|
invert H.
|
||||||
|
simplify.
|
||||||
|
apply singleton_in.
|
||||||
|
apply oneStepClosure_empty.
|
||||||
|
simplify.
|
||||||
|
|
||||||
|
eapply MscStep.
|
||||||
|
apply oneStepClosure_split.
|
||||||
|
simplify.
|
||||||
|
invert H.
|
||||||
|
simplify.
|
||||||
|
apply singleton_in.
|
||||||
|
apply oneStepClosure_split.
|
||||||
|
simplify.
|
||||||
|
invert H.
|
||||||
|
simplify.
|
||||||
|
apply singleton_in.
|
||||||
|
apply oneStepClosure_split.
|
||||||
|
simplify.
|
||||||
|
invert H.
|
||||||
|
simplify.
|
||||||
|
apply singleton_in.
|
||||||
|
apply oneStepClosure_empty.
|
||||||
|
simplify.
|
||||||
|
|
||||||
|
apply MscDone.
|
||||||
|
apply prove_oneStepClosure; simplify.
|
||||||
|
assumption.
|
||||||
|
propositional; subst; invert H0; simplify; propositional.
|
||||||
|
|
||||||
|
simplify.
|
||||||
|
unfold fact_correct.
|
||||||
|
propositional; subst; trivial.
|
||||||
|
Qed.
|
||||||
|
|
||||||
(* BEGIN CODE THAT WILL NOT BE EXPLAINED IN DETAIL! *)
|
(* BEGIN CODE THAT WILL NOT BE EXPLAINED IN DETAIL! *)
|
||||||
|
|
||||||
|
@ -404,25 +442,10 @@ Proof.
|
||||||
assumption.
|
assumption.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Theorem add2_ok :
|
(*Theorem add2_ok :
|
||||||
invariantFor add2_sys add2_correct.
|
invariantFor add2_sys add2_correct.
|
||||||
Proof.
|
Proof.
|
||||||
Admitted.
|
Admitted.*)
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
Inductive add2_bthread :=
|
Inductive add2_bthread :=
|
||||||
| BRead
|
| BRead
|
||||||
|
@ -488,7 +511,7 @@ Qed.
|
||||||
Hint Rewrite add2_init_is.
|
Hint Rewrite add2_init_is.
|
||||||
|
|
||||||
(* Now, let's verify the original system. *)
|
(* Now, let's verify the original system. *)
|
||||||
(*Theorem add2_ok :
|
Theorem add2_ok :
|
||||||
invariantFor add2_sys add2_correct.
|
invariantFor add2_sys add2_correct.
|
||||||
Proof.
|
Proof.
|
||||||
(* First step: strengthen the invariant. We leave an underscore for the
|
(* First step: strengthen the invariant. We leave an underscore for the
|
||||||
|
@ -597,7 +620,7 @@ Proof.
|
||||||
|
|
||||||
invert H1.
|
invert H1.
|
||||||
propositional.
|
propositional.
|
||||||
Qed.*)
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
(** * Another abstraction example *)
|
(** * Another abstraction example *)
|
||||||
|
@ -1373,35 +1396,17 @@ Qed.
|
||||||
Theorem twoadd2_ok :
|
Theorem twoadd2_ok :
|
||||||
invariantFor (parallel twoadd_sys twoadd_sys) (twoadd_correct (private := _)).
|
invariantFor (parallel twoadd_sys twoadd_sys) (twoadd_correct (private := _)).
|
||||||
Proof.
|
Proof.
|
||||||
Admitted.
|
eapply invariant_weaken.
|
||||||
|
eapply invariant_simulates.
|
||||||
|
apply withInterference_abstracts.
|
||||||
|
apply withInterference_parallel.
|
||||||
|
apply twoadd_ok.
|
||||||
|
apply twoadd_ok.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
unfold twoadd_correct.
|
||||||
|
invert 1.
|
||||||
|
assumption.
|
||||||
|
Qed.
|
||||||
|
|
||||||
(* In fact, this modularity technique is so powerful that we now get correctness
|
(* In fact, this modularity technique is so powerful that we now get correctness
|
||||||
* for any number of threads, "for free"! Here's a tactic definition, which we
|
* for any number of threads, "for free"! Here's a tactic definition, which we
|
||||||
|
|
|
@ -85,6 +85,8 @@ Proof.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
(* Transitive-reflexive closure is so common that it deserves a shorthand notation! *)
|
(* Transitive-reflexive closure is so common that it deserves a shorthand notation! *)
|
||||||
|
Set Warnings "-notation-overridden". (* <-- needed while we play with defining one
|
||||||
|
* of the book's notations ourselves locally *)
|
||||||
Notation "R ^*" := (trc R) (at level 0).
|
Notation "R ^*" := (trc R) (at level 0).
|
||||||
|
|
||||||
(* Now let's use it to execute the factorial program. *)
|
(* Now let's use it to execute the factorial program. *)
|
||||||
|
|
|
@ -50,6 +50,8 @@ Inductive trc {A} (R : A -> A -> Prop) : A -> A -> Prop :=
|
||||||
-> trc R x z.
|
-> trc R x z.
|
||||||
|
|
||||||
(* Transitive-reflexive closure is so common that it deserves a shorthand notation! *)
|
(* Transitive-reflexive closure is so common that it deserves a shorthand notation! *)
|
||||||
|
Set Warnings "-notation-overridden". (* <-- needed while we play with defining one
|
||||||
|
* of the book's notations ourselves locally *)
|
||||||
Notation "R ^*" := (trc R) (at level 0).
|
Notation "R ^*" := (trc R) (at level 0).
|
||||||
|
|
||||||
(* Now let's use it to execute the factorial program. *)
|
(* Now let's use it to execute the factorial program. *)
|
||||||
|
|
Loading…
Reference in a new issue