Module Dictionary Fixpoint beq_nat nat bool match with match with true

 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
Module Dictionary.
Fixpoint beq_nat (n m : nat) : bool :=
match n with
| O => match m with
| O => true
| S m' => false
end
| S n' => match m with
| O => false
| S m' => beq_nat n' m'
end
end.
Inductive natoption : Type :=
| Some : nat -> natoption
| None : natoption.
Inductive dictionary : Type :=
| empty : dictionary
| record : nat -> nat -> dictionary -> dictionary.
Definition insert (key value : nat) (d : dictionary) : dictionary :=
(record key value d).
Fixpoint find (key : nat) (d : dictionary) : natoption :=
match d with
| empty => None
| record k v d' => if (beq_nat key k)
then (Some v)
else (find key d')
end.
Lemma beqnat_eq: forall n, beq_nat n n = true.
Proof.
intros.
induction n.
trivial.
rewrite <- IHn.
trivial.
Qed.
Theorem dictionary_invariant1' : forall(d : dictionary) (k v: nat),
(find k (insert k v d)) = Some v.
Proof.
intros.
induction d.
simpl.
rewrite -> beqnat_eq.
reflexivity.
simpl.
rewrite -> beqnat_eq.
reflexivity.
Qed.
End Dictionary.