Skip to content

Commit 01729d3

Browse files
YaZkoYaZko
committed
elementary laws
1 parent 8420422 commit 01729d3

2 files changed

Lines changed: 117 additions & 48 deletions

File tree

‎theories/Eq/SBisim_draft.v‎

Lines changed: 63 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1393,57 +1393,102 @@ Section WithParams.
13931393
Context {HasC2 : B2 -< C}.
13941394
Context {HasC3 : B3 -< C}.
13951395

1396-
Lemma spin_bisim : forall {Z1 Z2} (c : C Z1) (c' : C Z2),
1397-
@spin_gen E C Z1 Z1 c ≃ @spin_gen E C Z2 Z2 c'.
1398-
Admitted.
1399-
1396+
Lemma spin_bisim : forall {D R X Y} (c : C X) (c' : D Y),
1397+
@spin_gen E C R X c ≃ @spin_gen E D R Y c'.
1398+
Proof.
1399+
intros.
1400+
play; exfalso; eapply spin_gen_is_stuck; eauto.
1401+
Qed.
1402+
14001403
Lemma br2_assoc {X} : forall (t u v : ctree E C X),
14011404
br2 (br2 t u) v ≃ br2 t (br2 u v).
1402-
Admitted.
1405+
Proof.
1406+
intros; play; inv_trans; answer.
1407+
Qed.
14031408

14041409
Lemma br2_commut {X} : forall (t u : ctree E C X),
14051410
br2 t u ≃ br2 u t.
1406-
Admitted.
1411+
Proof.
1412+
intros; play; inv_trans; answer.
1413+
Qed.
14071414

14081415
Lemma br2_idem {X} : forall (t : ctree E C X),
14091416
br2 t t ≃ t.
1410-
Admitted.
1417+
Proof.
1418+
intros; play; inv_trans; answer.
1419+
Qed.
14111420

14121421
Lemma br2_merge {X} : forall (t u v : ctree E C X),
14131422
br2 (br2 t u) v ≃ br3 t u v.
1414-
Admitted.
1423+
Proof.
1424+
intros; play; inv_trans; answer.
1425+
Qed.
14151426

14161427
Lemma br2_is_stuck {X} : forall (u v : ctree E C X),
14171428
is_stuck u -> br2 u v ≃ v.
1418-
Admitted.
1419-
1429+
Proof.
1430+
intros; play; inv_trans; answer.
1431+
(* todo: have inv_trans support stuck stepping *)
1432+
exfalso; eapply H; eauto.
1433+
Qed.
1434+
14201435
Lemma br2_stuck_l {X} : forall (t : ctree E C X),
14211436
br2 Stuck t ≃ t.
1422-
Admitted.
1437+
Proof.
1438+
intros; play; inv_trans; answer.
1439+
(* todo: have inv_trans support stuck stepping *)
1440+
exfalso; eapply trans_stuck_inv; eauto.
1441+
Qed.
14231442

14241443
Lemma br2_stuck_r {X} : forall (t : ctree E C X),
14251444
br2 t Stuck ≃ t.
1426-
Admitted.
1445+
Proof.
1446+
intros; play; inv_trans; answer.
1447+
(* todo: have inv_trans support stuck stepping *)
1448+
exfalso; eapply trans_stuck_inv; eauto.
1449+
Qed.
14271450

14281451
Lemma br2_spin_l {X} : forall (t : ctree E C X),
14291452
br2 spin t ≃ t.
1430-
Admitted.
1453+
Proof.
1454+
intros; play; inv_trans; answer.
1455+
(* todo: have inv_trans support stuck stepping *)
1456+
exfalso; eapply spin_is_stuck; eauto.
1457+
Qed.
14311458

14321459
Lemma br2_spin_r {X} : forall (t : ctree E C X),
14331460
br2 t spin ≃ t.
1434-
Admitted.
1461+
Proof.
1462+
intros; play; inv_trans; answer.
1463+
(* todo: have inv_trans support stuck stepping *)
1464+
exfalso; eapply spin_is_stuck; eauto.
1465+
Qed.
14351466

14361467
Lemma brS2_commut {X} : forall (t u : ctree E C X),
14371468
brS2 t u ≃ brS2 u t.
1438-
Admitted.
1469+
Proof.
1470+
intros; play;
1471+
apply trans_brS2_inv' in TR as (-> & [EQ | EQ]); setoid_rewrite EQ;
1472+
(ex2; split3; [| eauto |]; etrans).
1473+
Qed.
14391474

14401475
Lemma brS2_idem {X} : forall (t : ctree E C X),
14411476
brS2 t t ≃ Step t.
1442-
Admitted.
1443-
1477+
Proof.
1478+
intros; play.
1479+
- apply trans_brS2_inv' in TR as (-> & [EQ | EQ]); setoid_rewrite EQ;
1480+
( ex2; split3; [| eauto |]; etrans).
1481+
- inv_trans; setoid_rewrite EQ; answer.
1482+
Qed.
1483+
14441484
Lemma sb_unfold_forever {X} : forall (k : X -> ctree E C X) (i : X),
14451485
forever k i ≃ r <- k i ;; forever k r.
1446-
Admitted.
1486+
Proof.
1487+
intros.
1488+
rewrite unfold_forever.
1489+
apply sbisim_bind_eq; auto.
1490+
intros; now rewrite sbisim_guard.
1491+
Qed.
14471492

14481493
End WithParams.
14491494

‎theories/Eq/Trans.v‎

Lines changed: 54 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -567,25 +567,25 @@ Section BackwardBounded.
567567
now apply trans_br with t33.
568568
Qed.
569569

570-
Lemma trans_br31 :
571-
trans l t t' ->
572-
trans l (br3 t u v) t'.
570+
Lemma trans_br31 x :
571+
trans l t x ->
572+
trans l (br3 t u v) x.
573573
Proof.
574574
intros * TR.
575575
now apply trans_br with t31.
576576
Qed.
577577

578-
Lemma trans_br32 :
579-
trans l u u' ->
580-
trans l (br3 t u v) u'.
578+
Lemma trans_br32 x :
579+
trans l u x ->
580+
trans l (br3 t u v) x.
581581
Proof.
582582
intros * TR.
583583
now apply trans_br with t32.
584584
Qed.
585585

586-
Lemma trans_br33 :
587-
trans l v v' ->
588-
trans l (br3 t u v) v'.
586+
Lemma trans_br33 x :
587+
trans l v x ->
588+
trans l (br3 t u v) x.
589589
Proof.
590590
intros * TR.
591591
now apply trans_br with t33.
@@ -615,33 +615,33 @@ Section BackwardBounded.
615615
eapply trans_br with t44; eauto.
616616
Qed.
617617

618-
Lemma trans_br41 :
619-
trans l t t' ->
620-
trans l (br4 t u v w) t'.
618+
Lemma trans_br41 x :
619+
trans l t x ->
620+
trans l (br4 t u v w) x.
621621
Proof.
622622
intros * TR.
623623
eapply trans_br with t41; eauto.
624624
Qed.
625625

626-
Lemma trans_br42 :
627-
trans l u u' ->
628-
trans l (br4 t u v w) u'.
626+
Lemma trans_br42 x :
627+
trans l u x ->
628+
trans l (br4 t u v w) x.
629629
Proof.
630630
intros * TR.
631631
eapply trans_br with t42; eauto.
632632
Qed.
633633

634-
Lemma trans_br43 :
635-
trans l v v' ->
636-
trans l (br4 t u v w) v'.
634+
Lemma trans_br43 x :
635+
trans l v x ->
636+
trans l (br4 t u v w) x.
637637
Proof.
638638
intros * TR.
639639
eapply trans_br with t43; eauto.
640640
Qed.
641641

642-
Lemma trans_br44 :
643-
trans l w w' ->
644-
trans l (br4 t u v w) w'.
642+
Lemma trans_br44 x :
643+
trans l w x ->
644+
trans l (br4 t u v w) x.
645645
Proof.
646646
intros * TR.
647647
eapply trans_br with t44; eauto.
@@ -826,53 +826,69 @@ Structural rules
826826
Ad-hoc rules for pre-defined finite branching
827827
|*)
828828

829-
Variable (l : @label E X) (t t' u v w : ctree E B X).
829+
Variable (l : @label E X) (t u v w : ctree E B X).
830830
Context `{B2 -< B} `{B3 -< B} `{B4 -< B}.
831831

832-
Lemma trans_br2_inv :
832+
Lemma trans_br2_inv t' :
833833
trans l (br2 t u) t' ->
834834
(trans l t t' \/ trans l u t').
835835
Proof.
836836
intros * TR; apply trans_br_inv in TR as [[] TR]; auto.
837837
Qed.
838838

839-
Lemma trans_br3_inv :
839+
Lemma trans_br3_inv t' :
840840
trans l (br3 t u v) t' ->
841841
(trans l t t' \/ trans l u t' \/ trans l v t').
842842
Proof.
843843
intros * TR; apply trans_br_inv in TR as [n TR].
844844
destruct n; auto.
845845
Qed.
846846

847-
Lemma trans_br4_inv :
847+
Lemma trans_br4_inv t' :
848848
trans l (br4 t u v w) t' ->
849849
(trans l t t' \/ trans l u t' \/ trans l v t' \/ trans l w t').
850850
Proof.
851851
intros * TR; apply trans_br_inv in TR as [n TR].
852852
destruct n; auto.
853853
Qed.
854854

855-
Lemma trans_brS2_inv :
855+
Lemma trans_brS2_inv (t': ctree _ _ _) :
856856
trans l (brS2 t u) t' ->
857857
(l = τ /\ (t' ≅ t \/ t' ≅ u)).
858858
Proof.
859859
intros * TR; apply trans_brS_inv in TR as (? & TR & ->); split; auto.
860860
destruct x; auto.
861861
Qed.
862862

863-
Lemma trans_brS3_inv :
863+
Lemma trans_brS2_inv' t' :
864+
trans l (brS2 t u) t' ->
865+
(l = τ /\ (Seq t' t \/ Seq t' u)).
866+
Proof.
867+
intros * TR; apply trans_brS_inv' in TR as (? & TR & ->); split; auto.
868+
destruct x; auto.
869+
Qed.
870+
871+
Lemma trans_brS3_inv (t': ctree _ _ _) :
864872
trans l (brS3 t u v) t' ->
865873
(l = τ /\ (t' ≅ t \/ t' ≅ u \/ t' ≅ v)).
866874
Proof.
867875
intros * TR; apply trans_brS_inv in TR as (? & TR & ->); split; auto.
868876
destruct x; auto.
869877
Qed.
870878

871-
Lemma trans_brS4_inv :
879+
Lemma trans_brS3_inv' t' :
880+
trans l (brS3 t u v) t' ->
881+
(l = τ /\ (Seq t' t \/ Seq t' u \/ Seq t' v)).
882+
Proof.
883+
intros * TR; apply trans_brS_inv' in TR as (? & TR & ->); split; auto.
884+
destruct x; auto.
885+
Qed.
886+
887+
Lemma trans_brS4_inv' t' :
872888
trans l (brS4 t u v w) t' ->
873-
(l = τ /\ (t' ≅ t \/ t' ≅ u \/ t' ≅ v \/ t' ≅ w)).
889+
(l = τ /\ (Seq t' t \/ Seq t' u \/ Seq t' v \/ Seq t' w)).
874890
Proof.
875-
intros * TR; apply trans_brS_inv in TR as (? & TR & ->); split; auto.
891+
intros * TR; apply trans_brS_inv' in TR as (? & TR & ->); split; auto.
876892
destruct x; auto.
877893
Qed.
878894

@@ -2236,6 +2252,14 @@ Ltac inv_trans_one :=
22362252
| h : htrans _ (α Br _ _) _ |- _ =>
22372253
let TR := fresh "TR" in
22382254
apply trans_br_inv in h as (?n & TR)
2255+
2256+
| h : htrans _ (α br2 _ _) _ |- _ =>
2257+
let TR := fresh "TR" in
2258+
apply trans_br2_inv in h as [TR | TR]
2259+
2260+
| h : htrans _ (α br3 _ _ _) _ |- _ =>
2261+
let TR := fresh "TR" in
2262+
apply trans_br3_inv in h as [TR | [TR | TR]]
22392263

22402264
(* Guard *)
22412265
| h : htrans _ (α Guard _) _ |- _ =>

0 commit comments

Comments
 (0)