Require Import String.
Require Import Ascii.
Require Import List.
Inductive optionE (X:Type) : Type :=
| SomeE : X -> optionE X
| NoneE : string -> optionE X.
Implicit Arguments SomeE [[X]].
Implicit Arguments NoneE [[X]].
Inductive sublist {A : Set} : list A -> list A -> Prop :=
| sl_tail : forall (c : A) l, sublist l (c::l)
| sl_cons : forall (c : A) l' l, sublist l' l -> sublist l' (c::l).
Definition parser (T : Type) :=
forall l : list ascii, optionE (T * {l' : list ascii | sublist l' l}).
(* This works. And I don't understand why. The type checker seems to be able to figure out that xs = c::t. *)
Definition foo {T : Type} (f : T) : parser T :=
fun xs => match xs with
| nil => NoneE "End of token stream"
| (c::t) => SomeE (f, exist _ t (sl_tail c t))
end.
(* And this one doesn't. And given that the above works, I don't understand why this doesn't. *)
Definition bar (f : ascii) : parser ascii :=
fun xs => match xs with
| nil => NoneE "End of token stream"
| (c::t) => SomeE (f, exist _ t (sl_tail c t))
end.
(* And this is how I would like to actually write this code: create a placeholder at the point of
proof, and use the tactic language to write down the proof. Explicitly constructing a proof
is tedious, but there seems to be no way around it when using dependent types. *)
Definition baz (f : T) : parser T :=
fun xs => match xs with
| nil => NoneE "End of token stream"
| (c::t) => SomeE (f, exist _ t _)
end.
Proof
apply sl_tail. (* or whatever *)
Qed.