-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathexact.v
66 lines (61 loc) · 1.48 KB
/
exact.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
Require Import String.
Require Import Ascii.
Require Import Orders.
Inductive lex_lt: string -> string -> Prop :=
| lex_lt_lt : forall (c1 c2 : ascii) (s1 s2 : string),
nat_of_ascii c1 < nat_of_ascii c2 ->
lex_lt (String c1 s1) (String c2 s2)
| lex_lt_eq : forall (c : ascii) (s1 s2 : string),
lex_lt s1 s2 ->
lex_lt (String c s1) (String c s2)
| lex_lt_empty : forall (c : ascii) (s : string),
lex_lt EmptyString (String c s).
Theorem lex_lt_not_eq : forall s0 s1,
lex_lt s0 s1 -> s0 <> s1.
Proof.
induction s0.
- intros.
inversion H; subst.
congruence.
- intros.
inversion H; subst.
* intro H_eq.
injection H_eq; intros; subst.
contradict H3.
auto with arith.
* intro H_eq.
injection H_eq; intros; subst.
specialize (IHs0 s3).
apply IHs0 in H3.
auto.
Qed.
Lemma lex_lt_irrefl : Irreflexive lex_lt.
Proof.
intros s0 H_lt.
apply lex_lt_not_eq in H_lt.
auto.
Qed.
Theorem lex_lt_trans : forall s0 s1 s2,
lex_lt s0 s1 -> lex_lt s1 s2 -> lex_lt s0 s2.
Proof.
induction s0.
- intros.
inversion H; subst.
inversion H0; subst.
* apply lex_lt_empty.
* apply lex_lt_empty.
- intros.
inversion H; subst; inversion H0; subst.
* apply lex_lt_lt.
eauto with arith.
* apply lex_lt_lt.
assumption.
* apply lex_lt_lt.
assumption.
* apply lex_lt_eq.
eapply IHs0; eauto.
Qed.
Theorem lex_lt_strorder : StrictOrder lex_lt.
Proof.
exact (Build_StrictOrder _ lex_lt_irrefl lex_lt_trans).
Qed.