-
Notifications
You must be signed in to change notification settings - Fork 0
/
Prefix.v
106 lines (95 loc) · 2.72 KB
/
Prefix.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
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Import ListNotations.
Require Export Parser.Structures.
Require Export Parser.Tactics.
Require Export Parser.Matches.
Definition prefix { A B } (s1: Syntax A) (s2: Syntax B): Prop :=
forall ts v, matches s1 ts v ->
exists ts' v', matches s2 (ts ++ ts') v'.
Ltac prefix :=
match goal with
| H1: matches_without _ ?s1 ?ts ?v, H2: prefix ?s1 ?s2 |- _ =>
poseNew (Mark (ts,s2) "prefix");
unshelve epose proof (H2 ts v _)
end.
Lemma prefix_disj_l:
forall A B (s1 s2: Syntax A) (s: Syntax B),
prefix (Disjunction s1 s2) s ->
prefix s1 s.
Proof.
unfold prefix; repeat light; eauto with matches.
Qed.
Lemma prefix_disj_r:
forall A B (s1 s2: Syntax A) (s: Syntax B),
prefix (Disjunction s1 s2) s ->
prefix s2 s.
Proof.
unfold prefix; repeat light; eauto with matches.
Qed.
Lemma prefix_seq_l:
forall A1 A2 B (s1: Syntax A1) (s2: Syntax A2) (s: Syntax B) ts v,
prefix (Sequence s1 s2) s ->
matches s2 ts v ->
prefix s1 s.
Proof.
unfold prefix; repeat light;
eauto with matches.
unshelve epose proof (H (ts0 ++ ts) (v0, v) _);
repeat light || rewrite <- app_assoc in *;
eauto with matches.
Qed.
Lemma prefix_seq_r:
forall A1 A2 B (s1: Syntax A1) (s2: Syntax A2) (s: Syntax B) v,
prefix (Sequence s1 s2) s ->
matches s1 [] v ->
prefix s2 s.
Proof.
unfold prefix; repeat light;
eauto with matches.
Qed.
Lemma prefix_map:
forall A B C (f: A -> B) g (s: Syntax A) (s': Syntax C),
prefix (Map f g s) s' ->
prefix s s'.
Proof.
unfold prefix; repeat light;
eauto with matches.
Qed.
Lemma prefix_var:
forall A x (s: Syntax A),
prefix (Var x) s ->
prefix (e x) s.
Proof.
unfold prefix; repeat light;
eauto with matches.
Qed.
Hint Resolve prefix_disj_l: prefix.
Hint Resolve prefix_disj_r: prefix.
Hint Resolve prefix_seq_l: prefix.
Hint Resolve prefix_seq_r: prefix.
Hint Resolve prefix_map: prefix.
Hint Resolve prefix_var: prefix.
Ltac prefix_sub :=
match goal with
| H: prefix (Disjunction ?s _) _ |- _ =>
poseNew (Mark H "prefix_sub");
pose proof (prefix_disj_l _ _ _ _ _ H);
pose proof (prefix_disj_r _ _ _ _ _ H)
| H1: prefix (Sequence ?s1 ?s2) _,
H2: matches ?s2 _ _
|- _ =>
poseNew (Mark (H1, H2) "prefix_sub");
pose proof (prefix_seq_l _ _ _ _ _ _ _ _ H1 H2)
| H1: prefix (Sequence ?s1 ?s2) _,
H2: matches ?s1 [] _
|- _ =>
poseNew (Mark (H1, H2) "prefix_sub");
pose proof (prefix_seq_r _ _ _ _ _ _ _ H1 H2)
| H: prefix (Map _ _ _) _ |- _ =>
poseNew (Mark H "prefix_sub");
pose proof (prefix_map _ _ _ _ _ _ _ H)
(* | H: prefix (Var _) _ |- _ =>
poseNew (Mark H "prefix_sub");
pose proof (prefix_var _ _ _ H) *) (* loop *)
end.