-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathSfLib.v
161 lines (128 loc) · 5.05 KB
/
SfLib.v
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
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
(** * SfLib: Modified From the Software Foundations Library
These are the basic notions that will go into our development.
We introduce identifiers and states, and discuss their properties.
This file in particular, as well as core part PrImp.v were based upon
Pierce et al's Software Foundations, available at:
http://www.cis.upenn.edu/~bcpierce/sf/current/index.html
*)
(** Imports and basic notions *)
Require Omega.
Require Export Bool.
Require Export Arith.
Require Export Arith.EqNat. (* Contains [beq_nat], among other things *)
Require Export Coq.Logic.FunctionalExtensionality.
Require String. Open Scope string_scope.
Fixpoint ble_nat (n m : nat) : bool :=
match n with
| O => true
| S n' =>
match m with
| O => false
| S m' => ble_nat n' m'
end
end.
(** Arithmetic Identifiers *)
Inductive aid : Type := Aid : nat -> aid.
Definition beq_aid (i1 i2 : aid) :=
match (i1, i2) with (Aid n1, Aid n2) => beq_nat n1 n2 end.
Theorem beq_aid_refl : forall i, beq_aid i i = true.
Proof. intros. destruct i. symmetry. apply beq_nat_refl. Qed.
Theorem beq_aid_eq : forall i1 i2, beq_aid i1 i2 = true -> i1 = i2.
Proof.
intros i1 i2 H. destruct i1; destruct i2.
symmetry in H. apply beq_nat_eq in H; subst; reflexivity.
Qed.
Theorem beq_aid_false_iff : forall i1 i2, beq_aid i1 i2 = false <-> i1 <> i2.
Proof.
split.
intros H eq. rewrite eq in H. rewrite beq_aid_refl in H. inversion H.
intros H. destruct i1; destruct i2. apply beq_nat_false_iff. auto.
Qed.
(** Boolean Identifiers *)
Inductive bid : Type := Bid : nat -> bid.
Definition beq_bid (i1 i2 : bid) :=
match (i1, i2) with (Bid n1, Bid n2) => beq_nat n1 n2 end.
Theorem beq_bid_refl : forall i, beq_bid i i = true.
Proof. intros. destruct i. symmetry. apply beq_nat_refl. Qed.
Theorem beq_bid_eq : forall i1 i2, beq_bid i1 i2 = true -> i1 = i2.
Proof.
intros i1 i2 H. destruct i1; destruct i2.
symmetry in H; apply beq_nat_eq in H; subst; reflexivity.
Qed.
Theorem beq_bid_false_iff : forall i1 i2, beq_bid i1 i2 = false <-> i1 <> i2.
Proof.
split.
intros H eq. rewrite eq in H. rewrite beq_bid_refl in H. inversion H.
intros H. destruct i1; destruct i2. apply beq_nat_false_iff. auto.
Qed.
(* ####################################################### *)
(** ** States *)
(** A _state_ represents the current values of all the variables at
some point in the execution of a program. *)
(** For simplicity (to avoid dealing with partial functions), we
let the state be defined for _all_ variables, even though any
given program is only going to mention a finite number of them. *)
Definition state := ((aid -> nat) * (bid -> bool))%type.
Definition empty_state : state :=
(fun _ => 0, fun _ => false).
Definition update (st : state) (x : aid) (n : nat) : state :=
(fun x' => if beq_aid x x' then n else (fst st) x', snd st).
Definition update_b (st : state) (y : bid) (b : bool) : state :=
(fst st, fun y' => if beq_bid y y' then b else (snd st) y').
(** Properties of [update]. *)
Theorem update_eq : forall n x st, fst (update st x n) x = n.
Proof. intros; unfold update; simpl; rewrite beq_aid_refl; reflexivity. Qed.
Theorem update_neq : forall x2 x1 n st,
beq_aid x2 x1 = false -> fst (update st x2 n) x1 = (fst st x1).
Proof.
intros x2 x1 n st Hneq; simpl.
unfold update.
rewrite -> Hneq.
reflexivity.
Qed.
Theorem update_same : forall n1 x1 st,
fst st x1 = n1 -> update st x1 n1 = st.
Proof.
intros n1 x1 st Heq; simpl.
apply injective_projections; trivial.
apply functional_extensionality; intros.
unfold update. subst. simpl.
destruct (beq_aid x1 x) eqn:Eq; trivial.
apply beq_aid_eq in Eq. subst. reflexivity.
Qed.
Theorem update_permute : forall n1 n2 x1 x2 st,
beq_aid x2 x1 = false ->
update (update st x2 n1) x1 n2 = update (update st x1 n2) x2 n1.
Proof.
intros n1 n2 x1 x2 st H; simpl.
apply injective_projections; trivial.
apply functional_extensionality; intros.
simpl.
destruct (beq_aid x1 x) eqn:Eq1, (beq_aid x2 x) eqn:Eq2; trivial.
apply beq_aid_eq in Eq1; apply beq_aid_eq in Eq2.
apply beq_aid_false_iff in H.
subst.
contradict H. reflexivity.
Qed.
Theorem update_permute_b : forall b1 b2 y1 y2 st,
beq_bid y2 y1 = false ->
update_b (update_b st y2 b1) y1 b2 = update_b (update_b st y1 b2) y2 b1.
Proof.
intros b1 b2 y1 y2 st H; simpl.
apply injective_projections; trivial.
apply functional_extensionality; intros.
simpl.
destruct (beq_bid y1 x) eqn:Eq1, (beq_bid y2 x) eqn:Eq2; trivial.
apply beq_bid_eq in Eq1; apply beq_bid_eq in Eq2.
apply beq_bid_false_iff in H.
subst.
contradict H. reflexivity.
Qed.
(** The following is trivial due to the non-conflicting nature of our updates,
but worth expressing explicitly. (In fact, reflexivity alone can prove this.) *)
Theorem update_interpermute : forall x y n b st,
update_b (update st x n) y b = update (update_b st y b) x n.
Proof.
intros.
apply injective_projections; reflexivity.
Qed.