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
|
use int.Int
use seq.Seq
use seq.FreeMonoid
(** {Logical definition of Regular Expressions} *)
type char
type regexp =
| Empty
| Epsilon
| Char char
| Alt regexp regexp
| Concat regexp regexp
| Star regexp
predicate re_g (r r1: regexp)
axiom re_g_alt :
forall r r1 r2: regexp.
r = Alt r1 r2 -> re_g r r1 /\ re_g r r2
axiom re_g_concat :
forall r r1 r2: regexp.
r = Concat r1 r2 -> re_g r r1 /\ re_g r r2
axiom re_g_star :
forall r r1: regexp.
r = Star r1 -> re_g r r1
-- lemma re_g_trans :
-- forall r1 r2 r3: regexp. re_g r1 r2 -> re_g r2 r3 -> re_g r1 r3
type word = seq char
inductive mem (w: word) (r: regexp) =
| mem_eps:
mem empty Epsilon
| mem_char:
forall c: char. mem (singleton c) (Char c)
| mem_altl:
forall w: word, r1 r2: regexp. mem w r1 -> mem w (Alt r1 r2)
| mem_altr:
forall w: word, r1 r2: regexp. mem w r2 -> mem w (Alt r1 r2)
| mem_concat:
forall w1 w2: word, r1 r2: regexp.
mem w1 r1 -> mem w2 r2 -> mem (w1 ++ w2) (Concat r1 r2)
| mems1:
forall r: regexp. mem empty (Star r)
| mems2:
forall w1 w2: word, r: regexp.
mem w1 r -> mem w2 (Star r) -> mem (w1 ++ w2) (Star r)
lemma mem_star_nonempty: forall w: word. forall r: regexp.
mem w (Star r) ->
w <> empty ->
exists k: int.
0 < k <= length w /\
mem w[..k] r /\
mem w[k..] (Star r)
lemma split_concat: forall w: word. forall r1 r2: regexp.
mem w (Concat r1 r2) ->
exists k: int.
0 <= k <= length w /\
mem w[..k] r1 /\ mem w[k..] r2
lemma concat_split: forall w: word. forall r1 r2: regexp. forall i j k: int.
0 <= i <= k <= j <= length w ->
mem w[i..k] r1 ->
mem w[k..j] r2 ->
mem w[i..j] (Concat r1 r2)
lemma extseq: forall w: word. w[0..length w] = w
(** {Coma Part} *)
use coma.Std
let unRe (r: regexp)
(empty {r = Empty})
(eps {r = Epsilon})
(char (c: char) {r = Char c})
(alt (r1 r2: regexp) {r = Alt r1 r2})
(cat (r1 r2: regexp) {r = Concat r1 r2})
(star (r1: regexp) {r = Star r1})
= any
predicate cons (w: word) (r: regexp) (ck: int -> bool) (i: int) =
[@inline:trivial]
exists j. i <= j <= length w /\ mem w[i..j] r /\ ck j
let accept_nonterm (r: regexp) (w: word) {} (ret (b: bool) {b <-> mem w r})
= a {r} {0} {fun j -> j = n}
(fun (i: int) (h) -> if {i = n} (ret {true}) h)
(ret {false})
[ a (r: regexp) (i: int) (ck: int -> bool) {0 <= i <= n}
(k (j: int) {mem w[i..j] r} {i <= j <= n} (h {not ck j}))
(o {not cons w r ck i})
= unRe {r} empty eps char alt cat star
[ empty -> o
| eps -> k {i} o
| char (c: char) ->
if {i < n && w[i] = c} (k {i+1} o) o
| alt (r1 r2: regexp) ->
a {r1} {i} {ck} k (-> a {r2} {i} {ck} k o)
| cat (r1 r2: regexp) ->
a {r1} {i} {cons w r2 ck}
(fun (j: int) (h) -> a {r2} {j} {ck} k h) o
| star (r1: regexp) ->
k {i} (-> a {r1} {i} {fun j -> i < j && cons w r ck j}
(fun (j: int) (h) -> if {i < j} (-> a {r} {j} {ck} k h) h)
o)
]
]
[ n: int = length w ]
predicate v (n old_i i: int) (old_r r: regexp) =
(n-i) < (n-old_i) || (old_i=i /\ re_g old_r r)
-- variant lexico : n-i, r
let accept_terminates (r: regexp) (w: word) {} (ret (b: bool) {b <-> mem w r})
= a {r} {0} {fun j -> j = n}
(fun (i: int) (h) -> if {i = n} (ret {true}) h)
({not mem w[0..n] r} ret {false})
[ a (r: regexp) (i: int) (ck: int -> bool) {0 <= i <= n}
(k (j: int) {mem w[i..j] r} {i <= j <= n} (h {not ck j}))
(o {not cons w r ck i})
= (fun (r__: regexp) (i__: int) ->
unRe {r} empty eps char alt cat star
[ empty -> o
| eps -> k {i} o
| char (c: char) ->
if {i < n && w[i] = c} (k {i+1} o) o
| alt (r1 r2: regexp) ->
arec {r1} {i} {ck} k (-> arec {r2} {i} {ck} k o)
| cat (r1 r2: regexp) ->
arec {r1} {i} {cons w r2 ck}
(fun (j: int) (h) -> arec {r2} {j} {ck} k h) o
| star (r1: regexp) ->
k {i} (-> arec {r1} {i} {fun j -> i < j && cons w r ck j}
(fun (j: int) (h) -> if {i < j} (-> arec {r} {j} {ck} k h) h)
o)
]
[ arec (r_: regexp) (i_: int) (ck_: int -> bool) (k_ (j: int) (h)) (o_)
-> { v n i__ i_ r__ r_ } a {r_} {i_} {ck_} k_ o_ ]) {r} {i}
]
[ n: int = length w ]
|
