70 lines
1.8 KiB
Coq
70 lines
1.8 KiB
Coq
Require Import List.
|
||
Import ListNotations.
|
||
|
||
(* Syntax of re *)
|
||
Inductive re {A:Type}: Type :=
|
||
| ε | Null: re
|
||
| Char: A -> re
|
||
| Cat: re -> re -> re
|
||
| Alt: re -> re -> re
|
||
| Star: re -> re.
|
||
Arguments re: clear implicits.
|
||
|
||
Module ReNotations.
|
||
Notation "∅" := Null.
|
||
Notation "'↑' a" := (Char a) (at level 10).
|
||
Notation "r '∗'" := (Star r) (at level 20).
|
||
Infix ";" := Cat (at level 60, right associativity).
|
||
Infix "│" := Alt (at level 65, right associativity).
|
||
End ReNotations.
|
||
|
||
(* Small-step operational semantics for re *)
|
||
Inductive reDe {A:Type}: list A -> re A -> Prop :=
|
||
| εDe: reDe [] ε
|
||
| CharDe: forall (a:A), reDe [a] (Char a)
|
||
| CatDe: forall (r1 r2:re A) (l1 l2: list A),
|
||
reDe l1 r1 -> reDe l2 r2 -> reDe (l1++l2) (Cat r1 r2)
|
||
| AltDeL: forall (r1 r2:re A) (l: list A),
|
||
reDe l r1 -> reDe l (Alt r1 r2)
|
||
| AltDeR: forall (r1 r2:re A) (l: list A),
|
||
reDe l r2 -> reDe l (Alt r1 r2)
|
||
| StarDeMore: forall (r:re A) (l1 l2:list A),
|
||
reDe l1 r -> reDe l2 (Star r) -> reDe (l1++l2) (Star r)
|
||
| StarDeDone: forall r:re A, reDe [] r.
|
||
Notation "w '⊨' r" := (reDe w r) (at level 50, only parsing).
|
||
|
||
|
||
Section Deriv.
|
||
Context {A:Type}.
|
||
Variable A_eqb: A -> A -> bool.
|
||
|
||
(* Brzozowski derivative *)
|
||
Fixpoint δ (a:A) (r: re A): re A :=
|
||
match r with
|
||
| ε | Null => Null
|
||
| Char c =>
|
||
if A_eqb c a then ε
|
||
else Null
|
||
| Cat r1 r2 => Cat (δ a r1) r2
|
||
| Alt r1 r2 => Alt (δ a r1) (δ a r2)
|
||
| Star r' => δ a r' (* ε case won't be possible in derivative *)
|
||
end.
|
||
End Deriv.
|
||
|
||
Theorem foo (A:Type) (A_eqb: A -> A -> bool) (r:re A) (a:A) (w:list A):
|
||
(a::w) ⊨ r -> w ⊨ (δ A_eqb a r).
|
||
Proof.
|
||
induction r; simpl.
|
||
- intro H; inversion H.
|
||
- intro H; inversion H.
|
||
|
||
- intro H.
|
||
pv_opt.
|
||
repeat in_inv.
|
||
induction w.
|
||
+ constructor.
|
||
+ induction w.
|
||
Abort.
|
||
|
||
|