mirror of
https://github.com/achlipala/frap.git
synced 2024-09-19 19:57:13 +00:00
100 lines
3.2 KiB
Coq
100 lines
3.2 KiB
Coq
Require Import Relations.
|
|
|
|
Set Implicit Arguments.
|
|
|
|
|
|
Record trsys state := {
|
|
Initial : state -> Prop;
|
|
Step : state -> state -> Prop
|
|
}.
|
|
|
|
Definition invariantFor {state} (sys : trsys state) (invariant : state -> Prop) :=
|
|
forall s, sys.(Initial) s
|
|
-> forall s', sys.(Step)^* s s'
|
|
-> invariant s'.
|
|
|
|
Theorem use_invariant : forall {state} (sys : trsys state) (invariant : state -> Prop) s s',
|
|
invariantFor sys invariant
|
|
-> sys.(Step)^* s s'
|
|
-> sys.(Initial) s
|
|
-> invariant s'.
|
|
Proof.
|
|
firstorder.
|
|
Qed.
|
|
|
|
Theorem invariant_weaken : forall {state} (sys : trsys state)
|
|
(invariant1 invariant2 : state -> Prop),
|
|
invariantFor sys invariant1
|
|
-> (forall s, invariant1 s -> invariant2 s)
|
|
-> invariantFor sys invariant2.
|
|
Proof.
|
|
unfold invariantFor; intuition eauto.
|
|
Qed.
|
|
|
|
Theorem invariant_induction : forall {state} (sys : trsys state)
|
|
(invariant : state -> Prop),
|
|
(forall s, sys.(Initial) s -> invariant s)
|
|
-> (forall s, invariant s -> forall s', sys.(Step) s s' -> invariant s')
|
|
-> invariantFor sys invariant.
|
|
Proof.
|
|
unfold invariantFor; intros.
|
|
assert (invariant s) by eauto.
|
|
clear H1.
|
|
induction H2; eauto.
|
|
Qed.
|
|
|
|
|
|
(** * General parallel composition *)
|
|
|
|
Record threaded_state shared private := {
|
|
Shared : shared;
|
|
Private : private
|
|
}.
|
|
|
|
Inductive parallel1 shared private1 private2
|
|
(init1 : threaded_state shared private1 -> Prop)
|
|
(init2 : threaded_state shared private2 -> Prop)
|
|
: threaded_state shared (private1 * private2) -> Prop :=
|
|
| Pinit : forall sh pr1 pr2,
|
|
init1 {| Shared := sh; Private := pr1 |}
|
|
-> init2 {| Shared := sh; Private := pr2 |}
|
|
-> parallel1 init1 init2 {| Shared := sh; Private := (pr1, pr2) |}.
|
|
|
|
Inductive parallel2 shared private1 private2
|
|
(step1 : threaded_state shared private1 -> threaded_state shared private1 -> Prop)
|
|
(step2 : threaded_state shared private2 -> threaded_state shared private2 -> Prop)
|
|
: threaded_state shared (private1 * private2)
|
|
-> threaded_state shared (private1 * private2) -> Prop :=
|
|
| Pstep1 : forall sh pr1 pr2 sh' pr1',
|
|
step1 {| Shared := sh; Private := pr1 |} {| Shared := sh'; Private := pr1' |}
|
|
-> parallel2 step1 step2 {| Shared := sh; Private := (pr1, pr2) |}
|
|
{| Shared := sh'; Private := (pr1', pr2) |}
|
|
| Pstep2 : forall sh pr1 pr2 sh' pr2',
|
|
step2 {| Shared := sh; Private := pr2 |} {| Shared := sh'; Private := pr2' |}
|
|
-> parallel2 step1 step2 {| Shared := sh; Private := (pr1, pr2) |}
|
|
{| Shared := sh'; Private := (pr1, pr2') |}.
|
|
|
|
Definition parallel shared private1 private2
|
|
(sys1 : trsys (threaded_state shared private1))
|
|
(sys2 : trsys (threaded_state shared private2)) := {|
|
|
Initial := parallel1 sys1.(Initial) sys2.(Initial);
|
|
Step := parallel2 sys1.(Step) sys2.(Step)
|
|
|}.
|
|
|
|
|
|
(** * Switching to multistep versions of systems *)
|
|
|
|
Lemma trc_idem : forall A (R : A -> A -> Prop) x1 x2,
|
|
R^*^* x1 x2
|
|
-> R^* x1 x2.
|
|
Proof.
|
|
induction 1; eauto using trc_trans.
|
|
Qed.
|
|
|
|
Theorem invariant_multistepify : forall {state} (sys : trsys state)
|
|
(invariant : state -> Prop),
|
|
invariantFor sys invariant
|
|
-> invariantFor {| Initial := Initial sys; Step := (Step sys)^* |} invariant.
|
|
Proof.
|
|
unfold invariantFor; simpl; intuition eauto using trc_idem.
|
|
Qed.
|