Require Import Ascii String.

Inductive re : Set :=
| Atom: Ascii.ascii -> re
| Epsilon: re
| Dot: re
| Concat: re -> re -> re
| Alt: re -> re -> re
| Star: re -> re.

Inductive reDenote : re -> string -> Prop :=
| AtomDe: forall ch:Ascii.ascii,
    reDenote (Atom ch) (String ch EmptyString)
| EpsilonDe: reDenote Epsilon EmptyString
| DotDe: forall ch:Ascii.ascii,
    reDenote Dot (String ch EmptyString)
| ConcatDe r1 r2: forall s1 s2 s:string,
       reDenote r1 s1 -> reDenote r2 s2 -> s = append s1 s2
    -> reDenote (Concat r1 r2) s
| AltDe r1 r2: forall s:string,
       reDenote r1 s \/ reDenote r2 s
    -> reDenote (Alt r1 r2) s
| StarDe r: forall s:string,
       reDenote (Alt (Concat r (Star r)) Epsilon) s
    -> reDenote (Star r) s.

(*
Definition transl {r:re} {s:string} (inp:re) : reDenote r e :=
  match inp with
 | Atom 
 | Epsilon: re
 | Dot: re
 | Concat: re -> re -> re
 | Alt: re -> re -> re
 | Star: re -> re.
 end.

re -> reDenote
forall s:string, (r:re) : reDenote r s
Atom ch => AtomDe ch
*)

Infix "│" := Alt (at level 51, only parsing).
Infix ";" := Concat (at level 5, only parsing).
Notation " 'ε' " := Epsilon (only parsing).

Goal
  reDenote (Star (Atom "a"%char)) ""%string.
Proof.
  refine (StarDe (Atom "a"%char) _ _). 
  refine (AltDe _ _ _ _).
  right.
  exact EpsilonDe.
Qed.

Ltac rhamm :=
  match goal with
  | _ => auto
  | [ |- reDenote (Star _) _ ] => auto
  end.


Goal
  reDenote (Star (Atom "a"%char)) "a"%string.
Proof.
  refine (StarDe _ _ _). 
  refine (AltDe _ _ _ _).
  left.
  refine (ConcatDe _ _ _ _ _ _ _ _).
  - exact (AtomDe "a").
  - refine (StarDe _ _ _). 
    refine (AltDe _ Epsilon ""%string _).
    right.
    exact EpsilonDe.
  - reflexivity.
  Show Proof.
Restart.
  eapply StarDe.
  eapply AltDe.
  left.
  eapply ConcatDe.
  - eapply AtomDe.
  - eapply StarDe.
    eapply AltDe.
    right.
    eapply EpsilonDe.
  - reflexivity.
  Show Proof.
Qed.

Goal
  reDenote (Atom "a"%char) "a"%string.
Proof.
  exact (AtomDe "a"%char). 
Qed.

(*
Inductive reDenote : re -> string -> Prop :=
| AtomDe: forall (ch:Ascii.ascii) (s:string),
    reDenote (Atom ch) (String ch s)
| EpsilonDe: forall ch:Ascii.ascii,
    reDenote Epsilon EmptyString.
| DotDe:: forall ch:Ascii.ascii,
    reDenote Epsilon (String ch EmptyString).

| ConcatDe: re -> re -> re
| AltDe: re -> re -> re
| StarDe: re -> re.
*)