-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathStringOps.v
105 lines (94 loc) · 3.36 KB
/
StringOps.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
Require Import Coq.Lists.List.
Require Import Coq.Strings.Ascii.
Require Import Coq.Strings.String.
Open Local Scope bool.
Fixpoint string2list (str: string) :=
match str with
| EmptyString => nil
| String head tail => head :: (string2list tail)
end.
Coercion string2list : string >-> list.
Fixpoint list2string (lst: list ascii) :=
match lst with
| nil => EmptyString
| head :: tail => String head (list2string tail)
end.
Definition ascii_eqb (lhs rhs: ascii) : bool :=
match (lhs, rhs) with
| (Ascii l1 l2 l3 l4 l5 l6 l7 l8, Ascii r1 r2 r3 r4 r5 r6 r7 r8) =>
(Bool.eqb l1 r1) && (Bool.eqb l2 r2)
&& (Bool.eqb l3 r3) && (Bool.eqb l4 r4)
&& (Bool.eqb l5 r5) && (Bool.eqb l6 r6)
&& (Bool.eqb l7 r7) && (Bool.eqb l8 r8)
end.
Lemma ascii_eqb_reflection (lhs rhs: ascii) :
ascii_eqb lhs rhs = true <-> lhs = rhs.
Proof.
split. (* -> *)
intros. unfold ascii_eqb in H.
destruct lhs. destruct rhs.
apply Bool.andb_true_iff in H. destruct H.
apply Bool.andb_true_iff in H. destruct H.
apply Bool.andb_true_iff in H. destruct H.
apply Bool.andb_true_iff in H. destruct H.
apply Bool.andb_true_iff in H. destruct H.
apply Bool.andb_true_iff in H. destruct H.
apply Bool.andb_true_iff in H. destruct H.
apply Bool.eqb_prop in H; rewrite H; clear H.
apply Bool.eqb_prop in H0; rewrite H0; clear H0.
apply Bool.eqb_prop in H1; rewrite H1; clear H1.
apply Bool.eqb_prop in H2; rewrite H2; clear H2.
apply Bool.eqb_prop in H3; rewrite H3; clear H3.
apply Bool.eqb_prop in H4; rewrite H4; clear H4.
apply Bool.eqb_prop in H5; rewrite H5; clear H5.
apply Bool.eqb_prop in H6; rewrite H6; clear H6.
reflexivity.
(* <- *)
intros. unfold ascii_eqb.
destruct lhs. destruct rhs. inversion H.
apply Bool.andb_true_iff. split; [| apply Bool.eqb_reflx].
apply Bool.andb_true_iff. split; [| apply Bool.eqb_reflx].
apply Bool.andb_true_iff. split; [| apply Bool.eqb_reflx].
apply Bool.andb_true_iff. split; [| apply Bool.eqb_reflx].
apply Bool.andb_true_iff. split; [| apply Bool.eqb_reflx].
apply Bool.andb_true_iff. split; [| apply Bool.eqb_reflx].
apply Bool.andb_true_iff. split; [| apply Bool.eqb_reflx].
apply Bool.eqb_reflx.
Qed.
Fixpoint string_eqb (lhs rhs: string) :=
match (lhs, rhs) with
| (EmptyString, EmptyString) => true
| (String l ltail, String r rtail) =>
(ascii_eqb l r) && (string_eqb ltail rtail)
| _ => false
end.
Lemma string_eqb_reflection (lhs rhs: string) :
string_eqb lhs rhs = true <-> lhs = rhs.
Proof.
split. (* -> *)
generalize rhs.
induction lhs.
destruct rhs0.
reflexivity.
intros. compute in H. discriminate H.
destruct rhs0.
intros. compute in H. discriminate H.
intros. unfold string_eqb in H.
apply Bool.andb_true_iff in H. destruct H.
apply ascii_eqb_reflection in H. rewrite H; clear H.
apply IHlhs in H0. rewrite H0; clear H0.
reflexivity.
(* <- *)
generalize rhs.
induction lhs.
destruct rhs0.
reflexivity.
intros. discriminate H.
destruct rhs0.
intros. discriminate H.
intros. unfold string_eqb.
inversion H.
apply Bool.andb_true_iff. split.
apply ascii_eqb_reflection. reflexivity.
rewrite <- H2 at 1. apply IHlhs in H2. auto.
Qed.