ArithmeticExpressionParser

This implements a certified parser on a simple grammar of arithmetic expressions. It assumes the input has already been tokenized.

{{{#!coq Require Import Program. Require Import ZArith. Require Import List.

Inductive token : Set := | NUM (n:Z) | PLUS | MINUS | TIMES | OPEN_PAREN | CLOSE_PAREN.

(* The target grammar, formalized below, is informally: expr <- summand => $1 | expr PLUS summand => $1 + $3 | expr MINUS summand => $1 - $3

summand <- factor => $1 | summand TIMES factor => $1 * $3

factor <- NUM => $1 | PLUS factor => $2 | MINUS factor => - $2 | OPEN_PAREN expr CLOSE_PAREN => $2 *)

Inductive expr_value : list token -> Z -> Prop := | expr_rule_1 : forall (l1 : list token) (val1 : Z), summand_value l1 val1 -> expr_value l1 val1 | expr_rule_2 : forall (l1 : list token) (val1 : Z) (l3 : list token) (val3 : Z), expr_value l1 val1 -> summand_value l3 val3 -> expr_value (l1 ++ PLUS :: l3) (val1 + val3) | expr_rule_3 : forall (l1 : list token) (val1 : Z) (l3 : list token) (val3 : Z), expr_value l1 val1 -> summand_value l3 val3 -> expr_value (l1 ++ MINUS :: l3) (val1 - val3) with summand_value : list token -> Z -> Prop := | summand_rule_1 : forall (l1 : list token) (val1 : Z), factor_value l1 val1 -> summand_value l1 val1 | summand_rule_2 : forall (l1 : list token) (val1 : Z) (l3 : list token) (val3 : Z), summand_value l1 val1 -> factor_value l3 val3 -> summand_value (l1 ++ TIMES :: l3) (val1 * val3) with factor_value : list token -> Z -> Prop := | factor_rule_1 : forall (n : Z), factor_value [NUM n] n | factor_rule_2 : forall (l2 : list token) (val2 : Z), factor_value l2 val2 -> factor_value (PLUS :: l2) val2 | factor_rule_3 : forall (l2 : list token) (val2 : Z), factor_value l2 val2 -> factor_value (MINUS :: l2) (- val2) | factor_rule_4 : forall (l2 : list token) (val2 : Z), expr_value l2 val2 -> factor_value (OPEN_PAREN :: l2 ++ [CLOSE_PAREN]) val2.

Lemma expr_nonempty : forall (l : list token) (n : Z), expr_value l n -> length l > 0 with summand_nonempty : forall (l : list token) (n : Z), summand_value l n -> length l > 0 with factor_nonempty : forall (l : list token) (n : Z), factor_value l n -> length l > 0. Proof. destruct 1; (repeat rewrite app_length; simpl; omega) || eauto. destruct 1; (repeat rewrite app_length; simpl; omega) || eauto. destruct 1; (repeat rewrite app_length; simpl; omega) || eauto. Qed.

(* A few trivial results to recognize a string expression involving l as being equal to ? ++ l. *) Lemma app_nil_start : forall l : list token, l = nil ++ l. Proof. reflexivity. Qed.

Lemma app_cons_start : forall (t : token) (l' hd l : list token), l' = hd ++ l -> t :: l' = (t :: hd) ++ l. Proof. intros. rewrite H. reflexivity. Qed.

Lemma app_app_start : forall (hd1 hd2 l l' : list token), l' = hd2 ++ l -> hd1 ++ l' = (hd1 ++ hd2) ++ l. Proof. intros. rewrite H. apply app_assoc. Qed.

Local Ltac recog_tail := eauto using app_nil_start, app_cons_start, app_app_start.

Inductive parse_ret (l : list token) (cond : list token -> Z -> Prop) : Set := | parse_success : forall (tl : list token) (n : Z), (exists hd : list token, l = hd ++ tl /\ cond hd n) -> parse_ret l cond | parse_failure : parse_ret l cond.

Definition expr_sub_value (n : Z) : list token -> Z -> Prop := fun l m => forall (n_str : list token), expr_value n_str n -> expr_value (n_str ++ l) m.

(* Reduction rules for the fake "expr_sub n" symbol: expr_sub n <- empty => n | PLUS summand (expr_sub (n+$2)) => $3 | MINUS summand (expr_sub (n-$2)) => $3 *) Lemma expr_sub_rule1 : forall n : Z, expr_sub_value n nil n. Proof. intros n ? ?; rewrite <- app_nil_end; trivial. Qed.

Lemma expr_sub_rule2 : forall (n : Z) (l2 : list token) (val2 : Z) (l3 : list token) (val3 : Z), summand_value l2 val2 -> expr_sub_value (n + val2) l3 val3 -> expr_sub_value n (PLUS :: l2 ++ l3) val3. Proof. intros. intros ? ?. evar (hd : list token); match goal with |- expr_value ?l _ => replace l with (hd ++ l3) by (symmetry; recog_tail); subst hd end. eauto using expr_value. Qed.

Lemma expr_sub_rule3 : forall (n : Z) (l2 : list token) (val2 : Z) (l3 : list token) (val3 : Z), summand_value l2 val2 -> expr_sub_value (n - val2) l3 val3 -> expr_sub_value n (MINUS :: l2 ++ l3) val3. Proof. intros. intros ? ?. evar (hd : list token); match goal with |- expr_value ?l _ => replace l with (hd ++ l3) by (symmetry; recog_tail); subst hd end. eauto using expr_value. Qed.

Definition summand_sub_value (n : Z) : list token -> Z -> Prop := fun l m => forall (n_str : list token), summand_value n_str n -> summand_value (n_str ++ l) m.

(* Reduction rules for the fake "summand_sub n" symbol: summand_sub n <- empty => n | TIMES factor (summand_sub (n*$2)) => $3 *) Lemma summand_sub_rule1 : forall n : Z, summand_sub_value n nil n. Proof. intros; intros ? ?; rewrite <- app_nil_end; trivial. Qed.

Lemma summand_sub_rule2 : forall (n : Z) (l2 : list token) (val2 : Z) (l3 : list token) (val3 : Z), factor_value l2 val2 -> summand_sub_value (n * val2) l3 val3 -> summand_sub_value n (TIMES :: l2 ++ l3) val3. Proof. intros. intros ? ?. evar (hd : list token); match goal with |- summand_value ?l _ => replace l with (hd ++ l3) by (symmetry; recog_tail); subst hd end. eauto using summand_value. Qed.

(* Notations to allow us to act as if our parser functions were instances of StateT (list token) Maybe Z -- which they are if one ignores the proof content. *)

(* First, a couple utility functions which are literally instances of StateT (list token) Maybe (option token), and StateT (list token) Maybe token, respectively. *)

(* Peek at the next token, without removing it from the parser stream; if at end of stream, return None, but don't signal an error *) Definition peek_token (l : list token) : option (list token * option token) := match l with | nil => Some (l, None) | t :: _ => Some (l, Some t) end.

(* Get the next token and remove it from the parser stream; if at end of stream, signal an error *) Definition get_token (l : list token) : option (list token * token) := match l with | nil => None | t :: l' => Some (l', t) end.

(* Our actual intermediate terms that we build as part of the notation will be of this form: ) Definition parse_monad_type (P : list token -> list token -> Prop) (cond : list token -> Z -> Prop) : Set := forall l l0, P l l0 -> parse_ret l0 cond. ( Here, l0 represents the "initial state", needed to specify the return type, and l represents the "current state". P will represent enough "context" from the monad invocations so far to continue. For example, in the first return_ statement in parse_expr_sub below, P might look like: fun l l0 => exists hd, expr_sub_value (n + m) hd result /
exists hd0, summand_value hd0 m /
exists l', get_token l' = Some (hd0 ++ hd ++ l, Anonymous) /
exists l'', peek_token l'' = Some (l', t) /
l'' = l0.

For the outer structure, we will build an instance of parse_monad_type eq cond, and then pass arguments l l eq_refl *)

Program Definition parse_monad_bind {X P cond} (x : list token -> option (list token * X)) (g : forall x0:X, parse_monad_type (fun l l0 => exists l', x l' = Some (l, x0) /
P l' l0) cond) : parse_monad_type P cond := fun l l0 H => match x l as o return (x l = o -> _) with | Some (l', x0) => fun _ => g x0 l' l0 _ | None => fun _ => parse_failure _ _ end eq_refl. Next Obligation. eexists; split; [ reflexivity | eassumption ]. Defined.

Program Definition parse_monad_bind_rec {P sz sz' cond cond'} (subparse : forall (l : list token), sz' l < sz -> parse_ret l cond') (g : forall n:Z, parse_monad_type (fun l l0 => exists hd, cond' hd n /\ P (hd ++ l) l0) cond) : (forall l l0:list token, P l l0 -> sz' l < sz) -> parse_monad_type P cond := fun Hlt l l0 H => match subparse l _ return _ with | parse_success tl n _ => g n tl l0 _ | parse_failure => parse_failure _ _ end. Next Obligation. eexists; split; eassumption. Defined.

Notation "'do' x0 <- x ; y" := (parse_monad_bind x (fun x0 => y)) (at level 70, right associativity, x0 ident). Notation "'do_rec' n <- x ; y" := (parse_monad_bind_rec x (fun n => y) ) (at level 70, right associativity, x0 ident). Notation "'return' n" := (fun l l0 _ => parse_success _ _ l n _) (at level 71). Notation "'error'" := (fun l l0 _ => parse_failure _ _) (at level 71).

(* Notation "'subparser' p Hacc" := (fun l Hlt => p l (Acc_inv Hacc Hlt)) (at level 90). *) Definition subparser {P sz} (p : forall l, Acc lt (sz l) -> P l) {n} (Hacc : Acc lt n) := fun (l:list token) (Hlt : sz l < n) => p l (Acc_inv Hacc Hlt).

Definition parse_expr_sz (l : list token) := 5 * length l + 4. Definition parse_expr_sub_sz (l : list token) := 5 * length l + 3. Definition parse_summand_sz (l : list token) := 5 * length l + 2. Definition parse_summand_sub_sz (l : list token) := 5 * length l + 1. Definition parse_factor_sz (l : list token) := 5 * length l.

Obligation Tactic := program_simpl; simpl; simpl in *; eauto using expr_value, summand_value, factor_value; try (repeat split; discriminate); repeat match goal with | H : ?f ?l = _ |- _ => match f with | peek_token => idtac | get_token => idtac | _ => fail end; (is_var l; destruct l; (discriminate H || (injection H; intros; subst)); clear H) || (simpl f in H; injection H; intros; subst; clear H) end; try (unfold parse_expr_sz, parse_expr_sub_sz, parse_summand_sz, parse_summand_sub_sz, parse_factor_sz; simpl length; repeat rewrite app_length; repeat match goal with H : _ |- _ => apply expr_nonempty in H || apply summand_nonempty in H || apply factor_nonempty in H end; omega); try (eexists; split; [ recog_tail | eauto using expr_value, summand_value, factor_value, expr_sub_rule1, expr_sub_rule2, expr_sub_rule3, summand_sub_rule1, summand_sub_rule2 ]).

Program Definition parse_expr_builder (l : list token) (parse_summand : forall l', parse_summand_sz l' < parse_expr_sz l -> parse_ret l' summand_value) (parse_expr_sub : forall n l', parse_expr_sub_sz l' < parse_expr_sz l -> parse_ret l' (expr_sub_value n)) : parse_ret l expr_value := (( do_rec n <- parse_summand; do_rec m <- parse_expr_sub n; return_ m ) : parse_monad_type (fun l0 l1 => l0 = l /\ l1 = l) _) l l _.

Program Definition parse_expr_sub_builder (n : Z) (l : list token) (parse_summand : forall l', parse_summand_sz l' < parse_expr_sub_sz l -> parse_ret l' summand_value) (parse_expr_sub : forall n l', parse_expr_sub_sz l' < parse_expr_sub_sz l -> parse_ret l' (expr_sub_value n)) : parse_ret l (expr_sub_value n) := (( do t <- peek_token; match t with | Some PLUS => do _ <- get_token; do_rec m <- parse_summand; do_rec result <- parse_expr_sub (n + m)%Z; return_ result | Some MINUS => do _ <- get_token; do_rec m <- parse_summand; do_rec result <- parse_expr_sub (n - m)%Z; return_ result | _ => return_ n end ) : parse_monad_type (fun l0 l1 => l0 = l /\ l1 = l) _) l l _.

Program Definition parse_summand_builder (l : list token) (parse_summand_sub : forall n l', parse_summand_sub_sz l' < parse_summand_sz l -> parse_ret l' (summand_sub_value n)) (parse_factor : forall l', parse_factor_sz l' < parse_summand_sz l -> parse_ret l' factor_value) : parse_ret l summand_value := (( do_rec n <- parse_factor; do_rec m <- parse_summand_sub n; return_ m ) : parse_monad_type (fun l0 l1 => l0 = l /\ l1 = l) _) l l _.

Program Definition parse_summand_sub_builder (n : Z) (l : list token) (parse_summand_sub : forall n l', parse_summand_sub_sz l' < parse_summand_sub_sz l -> parse_ret l' (summand_sub_value n)) (parse_factor : forall l', parse_factor_sz l' < parse_summand_sub_sz l -> parse_ret l' factor_value) : parse_ret l (summand_sub_value n) := (( do t <- peek_token; match t with | Some TIMES => do _ <- get_token; do_rec m <- parse_factor; do_rec result <- parse_summand_sub (n * m)%Z; return_ result | _ => return_ n end) : parse_monad_type (fun l0 l1 => l0 = l /\ l1 = l) _) l l _.

Program Definition parse_factor_builder (l : list token) (parse_expr : forall l', parse_expr_sz l' < parse_factor_sz l -> parse_ret l' expr_value) (parse_factor : forall l', parse_factor_sz l' < parse_factor_sz l -> parse_ret l' factor_value) : parse_ret l factor_value := (( do t <- get_token; match t with | NUM n => return_ n | PLUS => do_rec n <- parse_factor; return_ n | MINUS => do_rec n <- parse_factor; return_ (-n) | OPEN_PAREN => do_rec n <- parse_expr; do t <- get_token; match t with | CLOSE_PAREN => return_ n | _ => error end | _ => error end) : parse_monad_type (fun l0 l1 => l0 = l /\ l1 = l) _) l l _.

Fixpoint parse_expr (l : list token) (H : Acc lt (parse_expr_sz l)) {struct H} : parse_ret l expr_value := parse_expr_builder l (fun l' Hlt => parse_summand l' (Acc_inv H Hlt)) (fun n l' Hlt => parse_expr_sub n l' (Acc_inv H Hlt)) with parse_expr_sub (n : Z) (l : list token) (H : Acc lt (parse_expr_sub_sz l)) {struct H} : parse_ret l (expr_sub_value n) := parse_expr_sub_builder n l (fun l' Hlt => parse_summand l' (Acc_inv H Hlt)) (fun n l' Hlt => parse_expr_sub n l' (Acc_inv H Hlt)) with parse_summand (l : list token) (H : Acc lt (parse_summand_sz l)) {struct H} : parse_ret l summand_value := parse_summand_builder l (fun n l' Hlt => parse_summand_sub n l' (Acc_inv H Hlt)) (fun l' Hlt => parse_factor l' (Acc_inv H Hlt)) with parse_summand_sub (n : Z) (l : list token) (H : Acc lt (parse_summand_sub_sz l)) {struct H} : parse_ret l (summand_sub_value n) := parse_summand_sub_builder n l (fun n l' Hlt => parse_summand_sub n l' (Acc_inv H Hlt)) (fun l' Hlt => parse_factor l' (Acc_inv H Hlt)) with parse_factor (l : list token) (H : Acc lt (parse_factor_sz l)) {struct H} : parse_ret l factor_value := parse_factor_builder l (fun l' Hlt => parse_expr l' (Acc_inv H Hlt)) (fun l' Hlt => parse_factor l' (Acc_inv H Hlt)).

Obligation Tactic := program_simpl.

Definition parse_ret_data {l cond} (ret : parse_ret l cond) : option (list token * Z) := match ret with | parse_success l' n _ => Some (l', n) | parse_failure => None end.

Inductive starts_with {A:Type} : list A -> A -> Prop := | starts_with_intro : forall (tl : list A) (hd : A), starts_with (hd :: tl) hd.

Definition parse_expr_completeness_stmt hd n := forall tl, ~ starts_with tl TIMES -> forall H, exists H', parse_ret_data (parse_expr (hd ++ tl) H) = parse_ret_data (parse_expr_sub n tl H'). Definition parse_summand_completeness_stmt hd n := forall tl, forall H, exists H', parse_ret_data (parse_summand (hd ++ tl) H) = parse_ret_data (parse_summand_sub n tl H'). Definition parse_factor_completeness_stmt hd n := forall tl, forall H, parse_ret_data (parse_factor (hd ++ tl) H) = Some (tl, n).

Lemma parse_expr_completeness' {hd n} : parse_expr_completeness_stmt hd n -> forall tl, ~ starts_with tl PLUS -> ~ starts_with tl MINUS -> ~ starts_with tl TIMES -> forall H, parse_ret_data (parse_expr (hd ++ tl) H) = Some (tl, n). Proof. intros. destruct (H tl H2 H3) as [H' e]; rewrite e. destruct H'; simpl parse_expr_sub. destruct tl; simpl. reflexivity. destruct t; (match goal with | Hs : ~ starts_with (?t :: _) ?t |- _ => contradict Hs; constructor end || reflexivity). Qed.

Lemma parse_summand_completeness' {hd n} : parse_summand_completeness_stmt hd n -> forall tl, ~ starts_with tl TIMES -> forall H, parse_ret_data (parse_summand (hd ++ tl) H) = Some (tl, n). Proof. intros. destruct (H tl H1) as [H' e]; rewrite e. destruct H'; simpl parse_summand_sub. destruct tl; simpl. reflexivity. destruct t; (match goal with | Hs : ~ starts_with (?t :: _) ?t |- _ => contradict Hs; constructor end || reflexivity). Qed.

Lemma parse_expr_completeness : forall hd n, expr_value hd n -> parse_expr_completeness_stmt hd n with parse_summand_completeness : forall hd n, summand_value hd n -> parse_summand_completeness_stmt hd n with parse_factor_completeness : forall hd n, factor_value hd n -> parse_factor_completeness_stmt hd n. Proof. Local Ltac inst_sub_cases parse_expr_completeness parse_summand_completeness parse_factor_completeness := destruct 1; repeat match goal with | e : expr_value ?hd ?n |- _ => progress match goal with | _ : parse_expr_completeness_stmt hd n |- _ => idtac | |- _ => let H := fresh in pose proof (parse_expr_completeness _ _ e) as H; pose proof (parse_expr_completeness' H) end | s : summand_value ?hd ?n |- _ => progress match goal with | _ : parse_summand_completeness_stmt hd n |- _ => idtac | |- _ => let H := fresh in pose proof (parse_summand_completeness _ _ s) as H; pose proof (parse_summand_completeness' H) end | f : factor_value ?hd ?n |- _ => progress match goal with | _ : parse_factor_completeness_stmt hd n |- _ => idtac | |- _ => pose proof (parse_factor_completeness _ _ f) end end; clear parse_expr_completeness parse_summand_completeness parse_factor_completeness. 3: inst_sub_cases parse_expr_completeness parse_summand_completeness parse_factor_completeness. 2: inst_sub_cases parse_expr_completeness parse_summand_completeness parse_factor_completeness. inst_sub_cases parse_expr_completeness parse_summand_completeness parse_factor_completeness. Guarded.

Local Ltac subcase_intros := intro tl; repeat (simpl app; rewrite <- app_assoc; simpl app); intros.

Local Ltac expand_parser := match goal with | H : Acc _ _ |- _ => destruct H; simpl end; unfold parse_expr_builder, parse_expr_sub_builder, parse_summand_builder, parse_summand_sub_builder, parse_factor_builder, parse_monad_bind_rec, parse_monad_bind; simpl.

Local Ltac red_expr_completeness := match goal with | H : parse_expr_completeness_stmt ?l ?val |- appcontext [parse_expr (?l ++ ?tl) ?Hacc] => let H0 := fresh in assert (~ starts_with tl TIMES) as H0 by (red; inversion 1); destruct (H _ H0 Hacc) as [? e]; rewrite e end.

Local Ltac red_parse_expr := match goal with | |- appcontext [parse_expr (?l ++ ?tl) ?H] => let a := fresh "a" in generalize H as a; intro a; remember (parse_expr (l ++ tl) a) as pe_val; try (match goal with | H0 : forall tl, ~ starts_with tl PLUS -> ~ starts_with tl MINUS -> ~ starts_with tl TIMES -> forall H, parse_ret_data (parse_expr (l ++ tl) H) = Some (tl, ?val), Heq : pe_val = _ |- _ => let Hplus := fresh in assert (~ starts_with tl PLUS) as Hplus by (red; inversion 1); let Hminus := fresh in assert (~ starts_with tl MINUS) as Hminus by (red; inversion 1); let Htimes := fresh in assert (~ starts_with tl TIMES) as Htimes by (red; inversion 1); let Heqdata := fresh in assert (parse_ret_data pe_val = Some (tl, val)) as Heqdata by (rewrite Heq; apply (H0 _ Hplus Hminus Htimes)); destruct pe_val; discriminate Heqdata || (injection Heqdata; intros; subst) end) end.

Local Ltac red_summand_completeness := match goal with | H : parse_summand_completeness_stmt ?l ?val |- appcontext [parse_summand (?l ++ ?tl) ?Hacc] => destruct (H _ Hacc) as [? e]; rewrite e end.

Local Ltac red_parse_summand := match goal with | |- appcontext [parse_summand (?l ++ ?tl) ?H] => let a := fresh "a" in generalize H as a; intro a; remember (parse_summand (l ++ tl) a) as ps_val; try (match goal with | H0 : forall tl, ~ starts_with tl TIMES -> forall H, parse_ret_data (parse_summand (l ++ tl) H) = Some (tl, ?val), H1 : ~ starts_with tl TIMES, Heq : ps_val = _ |- _ => let Heqdata := fresh in assert (parse_ret_data ps_val = Some (tl, val)) as Heqdata by (rewrite Heq; apply (H0 _ H1)); destruct ps_val; discriminate Heqdata || (injection Heqdata; intros; subst) end) end.

Local Ltac red_parse_factor := match goal with | |- appcontext [parse_factor (?l ++ ?tl) ?H] => let a := fresh "a" in generalize H as a; intro a; remember (parse_factor (l ++ tl) a) as pf_val; try (match goal with | H0 : parse_factor_completeness_stmt l ?val, Heq : pf_val = _ |- _ => let Heqdata := fresh in assert (parse_ret_data pf_val = Some (tl, val)) as Heqdata by (rewrite Heq; apply H0); destruct pf_val; discriminate Heqdata || (injection Heqdata; intros; subst) end) end.

Local Ltac end_state p := match goal with | |- appcontext [p ?tl ?H] => exists H; destruct (p tl H); reflexivity end.

abstract (subcase_intros; expand_parser; red_parse_summand; end_state (parse_expr_sub val1)).

abstract (subcase_intros; red_expr_completeness; expand_parser; red_parse_summand; end_state (parse_expr_sub (val1 + val3))).

abstract (subcase_intros; red_expr_completeness; expand_parser; red_parse_summand; end_state (parse_expr_sub (val1 - val3))).

abstract (subcase_intros; expand_parser; red_parse_factor; end_state (parse_summand_sub val1)).

abstract (subcase_intros; red_summand_completeness; expand_parser; red_parse_factor; end_state (parse_summand_sub (val1 * val3))).

abstract (subcase_intros; expand_parser; reflexivity).

abstract (subcase_intros; expand_parser; red_parse_factor; reflexivity).

abstract (subcase_intros; expand_parser; red_parse_factor; reflexivity).

abstract (subcase_intros; expand_parser; red_parse_expr; simpl; reflexivity). Qed.

Corollary parse_expr_completeness'' : forall {hd n}, expr_value hd n -> forall tl, ~ starts_with tl PLUS -> ~ starts_with tl MINUS -> ~ starts_with tl TIMES -> forall H, parse_ret_data (parse_expr (hd ++ tl) H) = Some (tl, n). Proof. intros hd n Hexpr. apply parse_expr_completeness'. apply parse_expr_completeness; trivial. Qed.

Corollary parse_expr_completeness_no_tail : forall (l : list token) (n : Z), expr_value l n -> forall H, parse_ret_data (parse_expr l H) = Some (nil, n). Proof. intros l n ?; rewrite (app_nil_end l); intros. apply parse_expr_completeness''; trivial; red; inversion 1. Qed.

Program Definition parse_expr_wrapper (l : list token) : { n:Z | unique (expr_value l) n } + { forall n:Z, ~ expr_value l n } := match parse_expr l (lt_wf _) with | parse_success nil n _ => inleft _ n | _ => inright _ _ end. Next Obligation. clear Heq_anonymous. red; split. rewrite <- app_nil_end; trivial. intros m ?. rewrite <- app_nil_end in H. pose proof (parse_expr_completeness_no_tail _ _ H (lt_wf _)). rewrite (parse_expr_completeness_no_tail _ _ e0) in H0. injection H0; auto. Defined. Next Obligation. change (forall n wildcard', parse_success l expr_value [] n wildcard' <> parse_expr l (lt_wf _)) in H. intro. remember (parse_expr l (lt_wf _)) as pe_val. assert (parse_ret_data pe_val = Some (nil, n)) by (rewrite Heqpe_val; apply parse_expr_completeness_no_tail; trivial). destruct pe_val; simpl in H1; try discriminate H1. injection H1; intros; subst. contradiction (H n e); reflexivity. Defined.

(* For extraction, use:

Require Import ExtrOcamlBasic. Extraction Inline parse_expr_builder parse_expr_sub_builder parse_summand_builder parse_summand_sub_builder parse_factor_builder parse_monad_bind parse_monad_bind_rec. Recursive Extraction parse_expr_wrapper. *) }}}