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.