/
Strlib.v
33 lines (26 loc) · 864 Bytes
/
Strlib.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
Require Import Coq.Bool.Bool.
Require Import Coq.Arith.Arith.
Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.
Definition beq_char (a:ascii) (b:ascii) : bool :=
beq_nat (nat_of_ascii a) (nat_of_ascii b).
Fixpoint beq_string (str1:string) (str2:string) : bool :=
match str1,str2 with
| String h1 t1, String h2 t2 => if beq_char h1 h2 then beq_string t1 t2 else false
| EmptyString, EmptyString => true
| _, _ => false
end.
Example beg_string_test1 : (beq_string "123123" "123123") = true.
Proof.
simpl. reflexivity.
Qed.
Example beg_string_test2 : (beq_string "123123" "abcabc") = false.
Proof.
simpl. reflexivity.
Qed.
Lemma string_eq_ref : forall s1 s2, beq_string s1 s2 = true -> s1 = s2.
Proof.
intros. Admitted.
Lemma string_neq_ref : forall s1 s2, beq_string s1 s2 = false -> s1 <> s2.
Proof.
intros. Admitted.