Newer
Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
Set Warnings "-notation-overridden,-parsing".
From sdram Require Export Requests.
Section Commands.
Context {BANK_CFG : Bank_configuration}.
Inductive Command_kind_t : Set :=
ACT |
PRE |
CRD |
CWR.
Local Definition Command_kind_eqdef (a b : Command_kind_t) :=
match a, b with
| ACT, ACT
| PRE, PRE
| CRD, CRD
| CWR, CWR => true
| _, _ => false
end.
Lemma Command_kind_eqn : Equality.axiom Command_kind_eqdef.
Proof.
unfold Equality.axiom. intros.
destruct (Command_kind_eqdef x y) eqn:H; unfold Command_kind_eqdef in *.
apply ReflectT. destruct x, y; inversion H; auto.
apply ReflectF; destruct x, y; inversion H; unfold not; intros; inversion H0.
Qed.
Canonical Command_kind_eqMixin := EqMixin Command_kind_eqn.
Canonical Command_kind_eqType := Eval hnf in EqType Command_kind_t Command_kind_eqMixin.
Record Command_t : Set := mkCmd
{
CDate : nat;
CKind : Command_kind_t;
Request : Request_t
}.
Local Definition Command_eqdef (a b : Command_t) :=
(a.(CDate) == b.(CDate)) &&
(a.(Request) == b.(Request)) &&
(a.(CKind) == b.(CKind)).
Lemma Command_eqn : Equality.axiom Command_eqdef.
Proof.
unfold Equality.axiom. intros. destruct Command_eqdef eqn:H; unfold Command_eqdef in *.
{
apply ReflectT.
move: H => /andP [/andP [/eqP CD /eqP R /eqP C]].
destruct x,y. simpl in *. subst. auto.
}
apply ReflectF. unfold not in *. intro BUG.
apply negbT in H; rewrite negb_and in H.
destruct x, y.
rewrite negb_and in H.
move: H => /orP [H | /eqP CK].
move: H => /orP [H | /eqP R].
move: H => /eqP CD.
by apply CD; inversion BUG.
by apply R; inversion BUG.
by apply CK; inversion BUG.
Qed.
Canonical Command_eqMixin := EqMixin Command_eqn.
Canonical Command_eqType := Eval hnf in EqType Command_t Command_eqMixin.
Definition Kind_of_req req :=
match req.(Kind) with
| RD => CRD
| WR => CWR
end.
Definition PRE_of_req req t :=
mkCmd t PRE req.
Definition ACT_of_req req t :=
mkCmd t ACT req.
Definition Cmd_of_req req t :=
mkCmd t (Kind_of_req req) req.
Lemma Command_ne_ACT_PRE
reqa ta reqb tb: (ACT_of_req reqa ta) != (PRE_of_req reqb tb).
Proof.
unfold ACT_of_req, PRE_of_req. unfold "==". simpl. unfold Commands.Command_eqdef. simpl.
rewrite negb_and. apply /orP. by right.
Qed.
Lemma Command_ne_CMD_ACT
reqa ta reqb tb: (Cmd_of_req reqa ta) != (ACT_of_req reqb tb).
Proof.
unfold ACT_of_req, Cmd_of_req, Kind_of_req. unfold "==". simpl. unfold Commands.Command_eqdef. simpl.
rewrite negb_and. apply /orP.
destruct (Kind reqa);by right.
Qed.
Lemma Command_ne_CMD_PRE
reqa ta reqb tb: (Cmd_of_req reqa ta) != (PRE_of_req reqb tb).
Proof.
unfold PRE_of_req, Cmd_of_req, Kind_of_req. unfold "==". simpl. unfold Commands.Command_eqdef. simpl.
rewrite negb_and. apply /orP.
destruct (Kind reqa);by right.
Qed.
Definition Commands_t := seq Command_t.
End Commands.