-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathparen.v
148 lines (131 loc) · 4.17 KB
/
paren.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
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
Require Import OrderedType OrderedTypeEx.
Import ListNotations.
Inductive Paren :=
| paren_end
| paren_nop (p: Paren)
| paren (inner p: Paren).
Function paren_append (p1 p2: Paren) :=
match p1 with
| paren_end => p2
| paren_nop p' => paren_nop (paren_append p' p2)
| paren inner p' => paren inner (paren_append p' p2)
end.
Inductive ParenNode :=
| pnode_open
| pnode_nop
| pnode_close.
Function print_paren (p: Paren): list ParenNode :=
match p with
| paren_end => []
| paren_nop p' => pnode_nop :: (print_paren p')
| paren inner p' => [pnode_open] ++ (print_paren inner) ++ [pnode_close]
++ (print_paren p')
end.
Inductive ParenParseState :=
| ok (next: Paren) (stack: list Paren)
| error.
Definition parse_init := ok paren_end [].
Function parse_paren_state (init_state: ParenParseState)
(ps: list ParenNode): ParenParseState :=
match ps with
| [] => init_state
| hd :: tl =>
match parse_paren_state init_state tl with
| error => error
| ok cur stack =>
match hd with
| pnode_nop => ok (paren_nop cur) stack
| pnode_close => ok paren_end (cur :: stack)
| pnode_open =>
match stack with
| [] => error
| next :: stack' => ok (paren cur next) stack'
end
end
end
end.
Function parse_paren (ps: list ParenNode): option Paren :=
match parse_paren_state parse_init ps with
| error => None
| ok p (_ :: _) => None
| ok p [] => Some p
end.
Example paren_print_parse_end:
parse_paren (print_paren paren_end) = Some paren_end.
auto. Qed.
Example paren_print_parse_nop:
parse_paren (print_paren (paren_nop paren_end)) = Some (paren_nop paren_end).
auto. Qed.
Example paren_print_parse_nesting:
let prog := (paren
(paren (paren_nop paren_end) paren_end)
(paren paren_end paren_end)) in
parse_paren (print_paren prog) = Some prog.
auto. Qed.
Lemma paren_parse_app (state: ParenParseState) (str1 str2: list ParenNode):
parse_paren_state state (str1 ++ str2) =
parse_paren_state (parse_paren_state state str2) str1.
Proof.
revert state str2.
induction str1; intros; auto.
rewrite <- app_comm_cons.
rewrite parse_paren_state_equation.
symmetry.
rewrite parse_paren_state_equation.
now rewrite <- IHstr1.
Qed.
Lemma paren_print_parse_paren (p: Paren):
parse_paren_state parse_init (print_paren p) = ok p [] ->
parse_paren_state parse_init (pnode_open :: (print_paren p) ++ [pnode_close])
= ok (paren p paren_end) [].
Proof.
intros; simpl in *.
rewrite paren_parse_app.
simpl in *.
induction (print_paren p).
- simpl in *.
unfold parse_init in *.
now replace p with paren_end in * by congruence.
- destruct a; simpl in *.
+ destruct (parse_paren_state parse_init l).
* destruct stack; try discriminate.
Admitted.
Lemma paren_print_parse_app (s1 s2: list ParenNode) (p1 p2: Paren)
(stack: list Paren):
parse_paren_state parse_init (s1) = ok p1 [] ->
parse_paren_state parse_init (s2) = ok p2 [] ->
parse_paren_state parse_init (s1 ++ s2) =
ok (paren_append p1 p2) stack.
Proof.
intros.
rewrite paren_parse_app.
rewrite H0; clear H0.
revert p1 H p2 stack.
induction s1; intros.
Admitted.
Lemma paren_print_parse_parens (p1 p2: Paren):
parse_paren_state parse_init (print_paren p1) = ok p1 [] ->
parse_paren_state parse_init (print_paren p2) = ok p2 [] ->
parse_paren_state parse_init (pnode_open :: (print_paren p1) ++ [pnode_close]
++ (print_paren p2))
= ok (paren p1 p2) [].
Proof.
intros.
rewrite app_assoc.
rewrite app_comm_cons.
replace (paren p1 p2) with (paren_append (paren p1 paren_end) p2) by auto.
apply paren_print_parse_app; auto.
apply paren_print_parse_paren; auto.
Qed.
Lemma paren_print_parse_state_inverse (p: Paren):
parse_paren_state parse_init (print_paren p) = ok p [].
Proof.
induction p; unfold parse_init in *;
rewrite print_paren_equation, parse_paren_state_equation;
[| rewrite IHp | apply (paren_print_parse_parens)]; auto.
Qed.
Theorem paren_print_parse_inverse (p: Paren):
parse_paren (print_paren p) = Some p.
Proof.
unfold parse_paren; now rewrite paren_print_parse_state_inverse.
Qed.