-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathMaps.v
executable file
·154 lines (139 loc) · 3.81 KB
/
Maps.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
From Coq Require Import Arith.Arith.
From Coq Require Import Bool.Bool.
Require Export Coq.Strings.String.
From Coq Require Import Logic.FunctionalExtensionality.
From Coq Require Import Lists.List.
Import ListNotations.
Definition eqb_string (x y: string): bool :=
if string_dec x y then true else false.
Theorem eqb_string_refl : forall s : string, true = eqb_string s s.
Proof.
intros s.
unfold eqb_string.
destruct (string_dec s s) as [H|H].
- reflexivity.
- destruct H. reflexivity.
Qed.
Theorem eqb_string_true_iff: forall x y: string,
eqb_string x y = true <-> x = y.
Proof.
intros x y.
unfold eqb_string.
destruct (string_dec x y) as [H|H].
- rewrite H. split. reflexivity. reflexivity.
- split.
+ intros contra. discriminate contra.
+ intros H'. rewrite H' in H. destruct H. reflexivity.
Qed.
Theorem eqb_string_false_iff : forall x y : string,
eqb_string x y = false <-> x <> y.
Proof.
intros x y. rewrite <- eqb_string_true_iff.
rewrite not_true_iff_false. reflexivity.
Qed.
Theorem false_eqb_string: forall x y: string,
x <> y -> eqb_string x y = false.
Proof.
intros x y.
rewrite eqb_string_false_iff.
intros H. apply H.
Qed.
Definition total_map (A: Type) := string->A.
Definition t_empty {A: Type} (v: A) :total_map A :=
(fun _ => v).
Definition t_update {A: Type} (m: total_map A) (x: string) (v: A) :=
fun x' => if eqb_string x x' then v else m x'.
Definition examplemap :=
t_update (t_update (t_empty false) "foo" true) "bar" true.
Notation "'_' '!->' v" := (t_empty v)
(at level 100, right associativity).
Example example_empty := (_ !-> false).
Notation "x '!->' v ';' m" := (t_update m x v) (at level 100, v at next level, right associativity).
Definition examplemap' :=
( "bar" !-> true;
"foo" !-> true;
_ !-> false
).
Lemma t_apply_empty: forall (A: Type) (x: string) (v: A),
(_!->v) x = v.
Proof.
intros A x v.
unfold t_empty.
reflexivity.
Qed.
Lemma t_update_eq:
forall (A: Type) (m: total_map A) x v,
(x !->v; m) x = v.
Proof.
intros A m x v.
unfold t_update.
destruct (eqb_string x x) eqn: E.
- reflexivity.
- rewrite <- eqb_string_refl in E.
discriminate E.
Qed.
Lemma t_update_neq:
forall (A: Type) (m: total_map A) x y v,
x <> y -> (x !-> v; m) y = m y.
Proof.
intros.
unfold t_update.
apply eqb_string_false_iff in H.
rewrite H.
reflexivity.
Qed.
Lemma eqb_stringP: forall x y: string,
reflect (x = y) (eqb_string x y).
Proof.
intros x y.
unfold eqb_string.
destruct (string_dec x y).
- rewrite e.
apply ReflectT. reflexivity.
- apply ReflectF. apply n.
Qed.
Theorem t_update_same:
forall (A: Type) (m: total_map A) x,
(x !-> m x ; m) = m.
Proof.
intros. unfold t_update.
apply functional_extensionality.
intros x0.
destruct (eqb_stringP x x0).
- rewrite e. reflexivity.
- reflexivity.
Qed.
Theorem t_update_permute:
forall (A: Type) (m: total_map A) v1 v2 x1 x2,
x2 <> x1 ->
(x1 !-> v1 ; x2 !-> v2 ; m) =
(x2 !-> v2 ; x1 !-> v1 ; m).
Proof.
intros.
unfold t_update.
apply functional_extensionality.
intros.
destruct (eqb_stringP x1 x).
- destruct (eqb_stringP x2 x).
+ exfalso. apply H. rewrite e0. symmetry. apply e.
+ reflexivity.
- reflexivity.
Qed.
Lemma t_update_shadow : forall A (m: total_map A) v1 v2 x,
t_update (t_update m x v1) x v2
= t_update m x v2.
Proof.
(* FILL IN HERE *) Admitted.
Definition partial_map (A: Type) :=
total_map (option A).
Definition empty {A : Type} : partial_map A :=
t_empty None.
Definition update {A : Type} (m : partial_map A)
(x : string) (v : A) :=
(x !-> Some v ; m).
Notation "x '|->' v ';' m" := (update m x v)
(at level 100, v at next level, right associativity).
Notation "x '|->' v" := (update empty x v)
(at level 100).
Example examplepmap :=
("Church" |-> true ; "Turing" |-> false).