New parser based on new version of the Coq backend of Menhir (#276)

What's new:

1. A rewrite of the Coq interpreter of Menhir automaton, with
   dependent types removing the need for runtime checks for the
   well-formedness of the LR stack. This seem to cause some speedup on
   the parsing time (~10% for lexing + parsing).

2. Thanks to 1., it is now possible to avoid the use of int31 for
   comparing symbols: Since this is only used for validation,
   positives are enough.

3. Speedup of Validation: on my machine, the time needed for compiling
   Parser.v goes from about 2 minutes to about 1 minute. This seem to
   be related to a performance bug in the completeness validator and
   to the use of positive instead of int31.

3. Menhir now generates a dedicated inductive type for
   (semantic-value-carrying) tokens (in addition to the already
   existing inductive type for (non-semantic-value-carrying)
   terminals. The end result is that the OCaml support code for the
   parser no longer contain calls to Obj.magic. The bad side of this
   change is that the formal specification of the parser is perhaps
   harder to read.

4. The parser and its library are now free of axioms (I used to use
   axiom K and proof irrelevance for easing proofs involving dependent
   types).

5. Use of a dedicated custom negative coinductive type for the input
   stream of tokens, instead of Coq stdlib's `Stream`. `Stream` is a
   positive coinductive type, which are now deprecated by Coq.

6. The fuel of the parser is now specified using its logarithm instead
   of its actual value. This makes it possible to give large fuel
   values instead of using the `let rec fuel = S fuel` hack.

7. Some refactoring in the lexer, the parser and the Cabs syntax tree.

The corresponding changes in Menhir have been released as part of
version 20190626. The `MenhirLib` directory is identical to the
content of the `src` directory of the corresponding `coq-menhirlib`
opam package except that:
   - In order to try to make CompCert compatible with several Menhir
     versions without updates, we do not check the version of menhir
     is compatible with the version of coq-menhirlib. Hence the
     `Version.v` file is not present in CompCert's copy.
   - Build-system related files have been removed.

10 files changed, 2807 insertions, 0 deletions

diff --git a/MenhirLib/Alphabet.v b/MenhirLib/Alphabet.v
new file mode 100644
index 00000000..29070e3d
--- /dev/null
+++ b/MenhirLib/Alphabet.v
@@ -0,0 +1,247 @@
+(****************************************************************************)
+(*                                                                          *)
+(*                                   Menhir                                 *)
+(*                                                                          *)
+(*           Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud         *)
+(*                                                                          *)
+(*  Copyright Inria. All rights reserved. This file is distributed under    *)
+(*  the terms of the GNU Lesser General Public License as published by the  *)
+(*  Free Software Foundation, either version 3 of the License, or (at your  *)
+(*  option) any later version, as described in the file LICENSE.            *)
+(*                                                                          *)
+(****************************************************************************)
+
+From Coq Require Import Omega List Syntax Relations RelationClasses.
+
+Local Obligation Tactic := intros.
+
+(** A comparable type is equiped with a [compare] function, that define an order
+   relation. **)
+Class Comparable (A:Type) := {
+  compare : A -> A -> comparison;
+  compare_antisym : forall x y, CompOpp (compare x y) = compare y x;
+  compare_trans :  forall x y z c,
+    (compare x y) = c -> (compare y z) = c -> (compare x z) = c
+}.
+
+Theorem compare_refl {A:Type} (C: Comparable A) :
+  forall x, compare x x = Eq.
+Proof.
+intros.
+pose proof (compare_antisym x x).
+destruct (compare x x); intuition; try discriminate.
+Qed.
+
+(** The corresponding order is a strict order. **)
+Definition comparableLt {A:Type} (C: Comparable A) : relation A :=
+  fun x y => compare x y = Lt.
+
+Instance ComparableLtStrictOrder {A:Type} (C: Comparable A) :
+  StrictOrder (comparableLt C).
+Proof.
+apply Build_StrictOrder.
+unfold Irreflexive, Reflexive, complement, comparableLt.
+intros.
+pose proof H.
+rewrite <- compare_antisym in H.
+rewrite H0 in H.
+discriminate H.
+unfold Transitive, comparableLt.
+intros x y z.
+apply compare_trans.
+Qed.
+
+(** nat is comparable. **)
+Program Instance natComparable : Comparable nat :=
+  { compare := Nat.compare }.
+Next Obligation.
+symmetry.
+destruct (Nat.compare x y)  as [] eqn:?.
+rewrite Nat.compare_eq_iff in Heqc.
+destruct Heqc.
+rewrite Nat.compare_eq_iff.
+trivial.
+rewrite <- nat_compare_lt in *.
+rewrite <- nat_compare_gt in *.
+trivial.
+rewrite <- nat_compare_lt in *.
+rewrite <- nat_compare_gt in *.
+trivial.
+Qed.
+Next Obligation.
+destruct c.
+rewrite Nat.compare_eq_iff in *; destruct H; assumption.
+rewrite <- nat_compare_lt in *.
+apply (Nat.lt_trans _ _ _ H H0).
+rewrite <- nat_compare_gt in *.
+apply (gt_trans _ _ _ H H0).
+Qed.
+
+(** A pair of comparable is comparable. **)
+Program Instance PairComparable {A:Type} (CA:Comparable A) {B:Type} (CB:Comparable B) :
+  Comparable (A*B) :=
+  { compare := fun x y =>
+      let (xa, xb) := x in let (ya, yb) := y in
+      match compare xa ya return comparison with
+        | Eq => compare xb yb
+        | x => x
+      end }.
+Next Obligation.
+destruct x, y.
+rewrite <- (compare_antisym a a0).
+rewrite <- (compare_antisym b b0).
+destruct (compare a a0); intuition.
+Qed.
+Next Obligation.
+destruct x, y, z.
+destruct (compare a a0) as [] eqn:?, (compare a0 a1) as [] eqn:?;
+try (rewrite <- H0 in H; discriminate);
+try (destruct (compare a a1) as [] eqn:?;
+  try (rewrite <- compare_antisym in Heqc0;
+         rewrite CompOpp_iff in Heqc0;
+         rewrite (compare_trans _ _ _  _ Heqc0 Heqc2) in Heqc1;
+         discriminate);
+  try (rewrite <- compare_antisym in Heqc1;
+         rewrite CompOpp_iff in Heqc1;
+         rewrite (compare_trans _ _ _ _ Heqc2 Heqc1) in Heqc0;
+         discriminate);
+  assumption);
+rewrite (compare_trans _ _ _ _ Heqc0 Heqc1);
+try assumption.
+apply (compare_trans _ _ _ _ H H0).
+Qed.
+
+(** Special case of comparable, where equality is Leibniz equality. **)
+Class ComparableLeibnizEq {A:Type} (C: Comparable A) :=
+  compare_eq : forall x y, compare x y = Eq -> x = y.
+
+(** Boolean equality for a [Comparable]. **)
+Definition compare_eqb {A:Type} {C:Comparable A} (x y:A) :=
+  match compare x y with
+    | Eq => true
+    | _ => false
+  end.
+
+Theorem compare_eqb_iff {A:Type} {C:Comparable A} {U:ComparableLeibnizEq C} :
+  forall x y, compare_eqb x y = true <-> x = y.
+Proof.
+unfold compare_eqb.
+intuition.
+apply compare_eq.
+destruct (compare x y); intuition; discriminate.
+destruct H.
+rewrite compare_refl; intuition.
+Qed.
+
+Instance NComparableLeibnizEq : ComparableLeibnizEq natComparable := Nat.compare_eq.
+
+(** A pair of ComparableLeibnizEq is ComparableLeibnizEq **)
+Instance PairComparableLeibnizEq
+  {A:Type} {CA:Comparable A} (UA:ComparableLeibnizEq CA)
+  {B:Type} {CB:Comparable B} (UB:ComparableLeibnizEq CB) :
+    ComparableLeibnizEq (PairComparable CA CB).
+Proof.
+intros x y; destruct x, y; simpl.
+pose proof (compare_eq a a0); pose proof (compare_eq b b0).
+destruct (compare a a0); try discriminate.
+intuition.
+destruct H2, H0.
+reflexivity.
+Qed.
+
+(** An [Finite] type is a type with the list of all elements. **)
+Class Finite (A:Type) := {
+  all_list : list A;
+  all_list_forall : forall x:A, In x all_list
+}.
+
+(** An alphabet is both [ComparableLeibnizEq] and [Finite]. **)
+Class Alphabet (A:Type) := {
+  AlphabetComparable :> Comparable A;
+  AlphabetComparableLeibnizEq :> ComparableLeibnizEq AlphabetComparable;
+  AlphabetFinite :> Finite A
+}.
+
+(** The [Numbered] class provides a conveniant way to build [Alphabet] instances,
+   with a good computationnal complexity. It is mainly a injection from it to
+   [positive] **)
+Class Numbered (A:Type) := {
+  inj : A -> positive;
+  surj : positive -> A;
+  surj_inj_compat : forall x, surj (inj x) = x;
+  inj_bound : positive;
+  inj_bound_spec : forall x, (inj x < Pos.succ inj_bound)%positive
+}.
+
+Program Instance NumberedAlphabet {A:Type} (N:Numbered A) : Alphabet A :=
+  { AlphabetComparable := {| compare := fun x y => Pos.compare (inj x) (inj y) |};
+    AlphabetFinite :=
+      {| all_list := fst (Pos.iter
+                           (fun '(l, p) => (surj p::l, Pos.succ p))
+                           ([], 1%positive) inj_bound) |} }.
+Next Obligation. simpl. now rewrite <- Pos.compare_antisym. Qed.
+Next Obligation.
+  match goal with c : comparison |- _ => destruct c end.
+  - rewrite Pos.compare_eq_iff in *. congruence.
+  - rewrite Pos.compare_lt_iff in *. eauto using Pos.lt_trans.
+  - rewrite Pos.compare_gt_iff in *. eauto using Pos.lt_trans.
+Qed.
+Next Obligation.
+  intros x y. unfold compare. intros Hxy.
+  assert (Hxy' : inj x = inj y).
+  (* We do not use [Pos.compare_eq_iff] directly to make sure the
+     proof is executable. *)
+  { destruct (Pos.eq_dec (inj x) (inj y)) as [|[]]; [now auto|].
+    now apply Pos.compare_eq_iff. }
+  (* Using rewrite here leads to non-executable proofs. *)
+  transitivity (surj (inj x)).
+  { apply eq_sym, surj_inj_compat. }
+  transitivity (surj (inj y)); cycle 1.
+  { apply surj_inj_compat. }
+  apply f_equal, Hxy'.
+Defined.
+Next Obligation.
+  rewrite <-(surj_inj_compat x).
+  generalize (inj_bound_spec x). generalize (inj x). clear x. intros x.
+  match goal with |- ?Hx -> In ?s (fst ?p) =>
+    assert ((Hx -> In s (fst p)) /\ snd p = Pos.succ inj_bound); [|now intuition] end.
+  rewrite Pos.lt_succ_r.
+  induction inj_bound as [|y [IH1 IH2]] using Pos.peano_ind;
+    (split; [intros Hx|]); simpl.
+  - rewrite (Pos.le_antisym _ _ Hx); auto using Pos.le_1_l.
+  - auto.
+  - rewrite Pos.iter_succ. destruct Pos.iter; simpl in *. subst.
+    rewrite Pos.le_lteq in Hx. destruct Hx as [?%Pos.lt_succ_r| ->]; now auto.
+  - rewrite Pos.iter_succ. destruct Pos.iter. simpl in IH2. subst. reflexivity.
+Qed.
+
+(** Definitions of [FSet]/[FMap] from [Comparable] **)
+Require Import OrderedTypeAlt.
+Require FSetAVL.
+Require FMapAVL.
+Import OrderedType.
+
+Module Type ComparableM.
+  Parameter t : Type.
+  Declare Instance tComparable : Comparable t.
+End ComparableM.
+
+Module OrderedTypeAlt_from_ComparableM (C:ComparableM) <: OrderedTypeAlt.
+  Definition t := C.t.
+  Definition compare : t -> t -> comparison := compare.
+
+  Infix "?=" := compare (at level 70, no associativity).
+
+  Lemma compare_sym x y : (y?=x) = CompOpp (x?=y).
+  Proof. exact (Logic.eq_sym (compare_antisym x y)). Qed.
+  Lemma compare_trans c x y z :
+    (x?=y) = c -> (y?=z) = c -> (x?=z) = c.
+  Proof.
+  apply compare_trans.
+  Qed.
+End OrderedTypeAlt_from_ComparableM.
+
+Module OrderedType_from_ComparableM (C:ComparableM) <: OrderedType.
+  Module Alt := OrderedTypeAlt_from_ComparableM C.
+  Include (OrderedType_from_Alt Alt).
+End OrderedType_from_ComparableM.
diff --git a/MenhirLib/Automaton.v b/MenhirLib/Automaton.v
new file mode 100644
index 00000000..c310fc61
--- /dev/null
+++ b/MenhirLib/Automaton.v
@@ -0,0 +1,164 @@
+(****************************************************************************)
+(*                                                                          *)
+(*                                   Menhir                                 *)
+(*                                                                          *)
+(*           Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud         *)
+(*                                                                          *)
+(*  Copyright Inria. All rights reserved. This file is distributed under    *)
+(*  the terms of the GNU Lesser General Public License as published by the  *)
+(*  Free Software Foundation, either version 3 of the License, or (at your  *)
+(*  option) any later version, as described in the file LICENSE.            *)
+(*                                                                          *)
+(****************************************************************************)
+
+Require Grammar.
+Require Export Alphabet.
+From Coq Require Import Orders.
+From Coq Require Export List Syntax.
+
+Module Type AutInit.
+  (** The grammar of the automaton. **)
+  Declare Module Gram:Grammar.T.
+  Export Gram.
+
+  (** The set of non initial state is considered as an alphabet. **)
+  Parameter noninitstate : Type.
+  Declare Instance NonInitStateAlph : Alphabet noninitstate.
+
+  Parameter initstate : Type.
+  Declare Instance InitStateAlph : Alphabet initstate.
+
+  (** When we are at this state, we know that this symbol is the top of the
+     stack. **)
+  Parameter last_symb_of_non_init_state: noninitstate -> symbol.
+End AutInit.
+
+Module Types(Import Init:AutInit).
+  (** In many ways, the behaviour of the initial state is different from the
+     behaviour of the other states. So we have chosen to explicitaly separate
+     them: the user has to provide the type of non initial states. **)
+  Inductive state :=
+    | Init: initstate -> state
+    | Ninit: noninitstate -> state.
+
+  Program Instance StateAlph : Alphabet state :=
+    { AlphabetComparable := {| compare := fun x y =>
+        match x, y return comparison with
+          | Init _, Ninit _ => Lt
+          | Init x, Init y => compare x y
+          | Ninit _, Init _ => Gt
+          | Ninit x, Ninit y => compare x y
+        end |};
+      AlphabetFinite := {| all_list := map Init all_list ++ map Ninit all_list |} }.
+  Local Obligation Tactic := intros.
+  Next Obligation.
+  destruct x, y; intuition; apply compare_antisym.
+  Qed.
+  Next Obligation.
+  destruct x, y, z; intuition.
+  apply (compare_trans _ i0); intuition.
+  congruence.
+  congruence.
+  apply (compare_trans _ n0); intuition.
+  Qed.
+  Next Obligation.
+  intros x y.
+  destruct x, y; intuition; try discriminate.
+  rewrite (compare_eq i i0); intuition.
+  rewrite (compare_eq n n0); intuition.
+  Qed.
+  Next Obligation.
+  apply in_or_app; destruct x; intuition;
+    [left|right]; apply in_map; apply  all_list_forall.
+  Qed.
+
+  Coercion Ninit : noninitstate >-> state.
+  Coercion Init : initstate >-> state.
+
+  (** For an LR automaton, there are four kind of actions that can be done at a
+     given state:
+       - Shifting, that is reading a token and putting it into the stack,
+       - Reducing a production, that is popping the right hand side of the
+          production from the stack, and pushing the left hand side,
+       - Failing
+       - Accepting the word (special case of reduction)
+
+     As in the menhir parser generator, we do not want our parser to read after
+     the end of stream. That means that once the parser has read a word in the
+     grammar language, it should stop without peeking the input stream. So, for
+     the automaton to be complete, the grammar must be particular: if a word is
+     in its language, then it is not a prefix of an other word of the language
+     (otherwise, menhir reports an end of stream conflict).
+
+     As a consequence of that, there is two notions of action: the first one is
+     an action performed before having read the stream, the second one is after
+  **)
+
+  Inductive lookahead_action (term:terminal) :=
+  | Shift_act: forall s:noninitstate,
+                 T term = last_symb_of_non_init_state s -> lookahead_action term
+  | Reduce_act: production -> lookahead_action term
+  | Fail_act: lookahead_action term.
+  Arguments Shift_act [term].
+  Arguments Reduce_act [term].
+  Arguments Fail_act [term].
+
+  Inductive action :=
+  | Default_reduce_act: production -> action
+  | Lookahead_act : (forall term:terminal, lookahead_action term) -> action.
+
+  (** Types used for the annotations of the automaton. **)
+
+  (** An item is a part of the annotations given to the validator.
+     It is acually a set of LR(1) items sharing the same core. It is needed
+     to validate completeness. **)
+  Record item := {
+  (** The pseudo-production of the item. **)
+    prod_item: production;
+
+  (** The position of the dot. **)
+    dot_pos_item: nat;
+
+  (** The lookahead symbol of the item. We are using a list, so we can store
+     together multiple LR(1) items sharing the same core. **)
+    lookaheads_item: list terminal
+  }.
+End Types.
+
+Module Type T.
+  Include AutInit <+ Types.
+  Module Export GramDefs := Grammar.Defs Gram.
+
+  (** For each initial state, the non terminal it recognizes. **)
+  Parameter start_nt: initstate -> nonterminal.
+
+  (** The action table maps a state to either a map terminal -> action. **)
+  Parameter action_table:
+    state -> action.
+  (** The goto table of an LR(1) automaton. **)
+  Parameter goto_table: state -> forall nt:nonterminal,
+    option { s:noninitstate | NT nt = last_symb_of_non_init_state s }.
+
+  (** Some annotations on the automaton to help the validation. **)
+
+  (** When we are at this state, we know that these symbols are just below
+     the top of the stack. The list is ordered such that the head correspond
+     to the (almost) top of the stack. **)
+  Parameter past_symb_of_non_init_state: noninitstate -> list symbol.
+
+  (** When we are at this state, the (strictly) previous states verify these
+     predicates. **)
+  Parameter past_state_of_non_init_state: noninitstate -> list (state -> bool).
+
+  (** The items of the state. **)
+  Parameter items_of_state: state -> list item.
+
+  (** The nullable predicate for non terminals :
+     true if and only if the symbol produces the empty string **)
+  Parameter nullable_nterm: nonterminal -> bool.
+
+  (** The first predicates for non terminals, symbols or words of symbols. A
+     terminal is in the returned list if, and only if the parameter produces a
+     word that begins with the given terminal **)
+  Parameter first_nterm: nonterminal -> list terminal.
+End T.
diff --git a/MenhirLib/Grammar.v b/MenhirLib/Grammar.v
new file mode 100644
index 00000000..a371318b
--- /dev/null
+++ b/MenhirLib/Grammar.v
@@ -0,0 +1,162 @@
+(****************************************************************************)
+(*                                                                          *)
+(*                                   Menhir                                 *)
+(*                                                                          *)
+(*           Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud         *)
+(*                                                                          *)
+(*  Copyright Inria. All rights reserved. This file is distributed under    *)
+(*  the terms of the GNU Lesser General Public License as published by the  *)
+(*  Free Software Foundation, either version 3 of the License, or (at your  *)
+(*  option) any later version, as described in the file LICENSE.            *)
+(*                                                                          *)
+(****************************************************************************)
+
+From Coq Require Import List Syntax Orders.
+Require Import Alphabet.
+
+(** The terminal non-terminal alphabets of the grammar. **)
+Module Type Alphs.
+  Parameters terminal nonterminal : Type.
+  Declare Instance TerminalAlph: Alphabet terminal.
+  Declare Instance NonTerminalAlph: Alphabet nonterminal.
+End Alphs.
+
+(** Definition of the alphabet of symbols, given the alphabet of terminals
+    and the alphabet of non terminals **)
+Module Symbol(Import A:Alphs).
+
+  Inductive symbol :=
+    | T: terminal -> symbol
+    | NT: nonterminal -> symbol.
+
+  Program Instance SymbolAlph : Alphabet symbol :=
+    { AlphabetComparable := {| compare := fun x y =>
+        match x, y return comparison with
+          | T _, NT _ => Gt
+          | NT _, T _ => Lt
+          | T x, T y => compare x y
+          | NT x, NT y => compare x y
+        end |};
+      AlphabetFinite := {| all_list :=
+        map T all_list++map NT all_list |} }.
+  Next Obligation.
+    destruct x; destruct y; intuition; apply compare_antisym.
+  Qed.
+  Next Obligation.
+    destruct x; destruct y; destruct z; intuition; try discriminate.
+    apply (compare_trans _ t0); intuition.
+    apply (compare_trans _ n0); intuition.
+  Qed.
+  Next Obligation.
+    intros x y.
+    destruct x; destruct y; try discriminate; intros.
+    rewrite (compare_eq t t0); now intuition.
+    rewrite (compare_eq n n0); now intuition.
+  Defined.
+  Next Obligation.
+    rewrite in_app_iff.
+    destruct x; [left | right]; apply in_map; apply all_list_forall.
+  Qed.
+
+End Symbol.
+
+(** A curryfied function with multiple parameters **)
+Definition arrows_right: Type -> list Type -> Type :=
+  fold_right (fun A B => A -> B).
+
+Module Type T.
+  Include Alphs <+ Symbol.
+
+  (** [symbol_semantic_type] maps a symbols to the type of its semantic
+     values. **)
+  Parameter symbol_semantic_type: symbol -> Type.
+
+  (** The type of productions identifiers **)
+  Parameter production : Type.
+  Declare Instance ProductionAlph : Alphabet production.
+
+  (** Accessors for productions: left hand side, right hand side,
+     and semantic action. The semantic actions are given in the form
+     of curryfied functions, that take arguments in the reverse order. **)
+  Parameter prod_lhs: production -> nonterminal.
+  (* The RHS of a production is given in reversed order, so that symbols  *)
+  Parameter prod_rhs_rev: production -> list symbol.
+  Parameter prod_action:
+    forall p:production,
+      arrows_right
+        (symbol_semantic_type (NT (prod_lhs p)))
+        (map symbol_semantic_type (prod_rhs_rev p)).
+
+  (** Tokens are the atomic elements of the input stream: they contain
+     a terminal and a semantic value of the type corresponding to this
+     terminal. *)
+  Parameter token : Type.
+  Parameter token_term : token -> terminal.
+  Parameter token_sem :
+    forall tok : token, symbol_semantic_type (T (token_term tok)).
+End T.
+
+Module Defs(Import G:T).
+
+  (** The semantics of a grammar is defined in two stages. First, we
+    define the notion of parse tree, which represents one way of
+    recognizing a word with a head symbol. Semantic values are stored
+    at the leaves.
+
+      This notion is defined in two mutually recursive flavours:
+    either for a single head symbol, or for a list of head symbols. *)
+  Inductive parse_tree:
+    forall (head_symbol:symbol) (word:list token), Type :=
+
+  (** Parse tree for a terminal symbol. *)
+  | Terminal_pt:
+    forall (tok:token), parse_tree (T (token_term tok)) [tok]
+
+  (** Parse tree for a non-terminal symbol.  *)
+  | Non_terminal_pt:
+    forall (prod:production) {word:list token},
+      parse_tree_list (prod_rhs_rev prod) word ->
+      parse_tree (NT (prod_lhs prod)) word
+
+  (* Note : the list head_symbols_rev is reversed. *)
+  with parse_tree_list:
+    forall (head_symbols_rev:list symbol) (word:list token), Type :=
+
+  | Nil_ptl: parse_tree_list [] []
+
+  | Cons_ptl:
+    forall {head_symbolsq:list symbol} {wordq:list token},
+      parse_tree_list head_symbolsq wordq ->
+
+    forall {head_symbolt:symbol} {wordt:list token},
+      parse_tree head_symbolt wordt ->
+
+      parse_tree_list (head_symbolt::head_symbolsq) (wordq++wordt).
+
+  (** We can now finish the definition of the semantics of a grammar,
+    by giving the semantic value assotiated with a parse tree. *)
+  Fixpoint pt_sem {head_symbol word} (tree:parse_tree head_symbol word) :
+    symbol_semantic_type head_symbol :=
+    match tree with
+    | Terminal_pt tok => token_sem tok
+    | Non_terminal_pt prod ptl => ptl_sem ptl (prod_action prod)
+    end
+  with ptl_sem {A head_symbols word} (tree:parse_tree_list head_symbols word) :
+    arrows_right A (map symbol_semantic_type head_symbols) -> A :=
+    match tree with
+    | Nil_ptl => fun act => act
+    | Cons_ptl q t => fun act => ptl_sem q (act (pt_sem t))
+    end.
+
+  Fixpoint pt_size {head_symbol word} (tree:parse_tree head_symbol word) :=
+    match tree with
+      | Terminal_pt _ => 1
+      | Non_terminal_pt _ l => S (ptl_size l)
+    end
+  with ptl_size {head_symbols word} (tree:parse_tree_list head_symbols word) :=
+    match tree with
+      | Nil_ptl => 0
+      | Cons_ptl q t =>
+         pt_size t + ptl_size q
+    end.
+End Defs.
diff --git a/MenhirLib/Interpreter.v b/MenhirLib/Interpreter.v
new file mode 100644
index 00000000..568597ba
--- /dev/null
+++ b/MenhirLib/Interpreter.v
@@ -0,0 +1,453 @@
+(****************************************************************************)
+(*                                                                          *)
+(*                                   Menhir                                 *)
+(*                                                                          *)
+(*           Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud         *)
+(*                                                                          *)
+(*  Copyright Inria. All rights reserved. This file is distributed under    *)
+(*  the terms of the GNU Lesser General Public License as published by the  *)
+(*  Free Software Foundation, either version 3 of the License, or (at your  *)
+(*  option) any later version, as described in the file LICENSE.            *)
+(*                                                                          *)
+(****************************************************************************)
+
+From Coq Require Import List Syntax.
+From Coq.ssr Require Import ssreflect.
+Require Automaton.
+Require Import Alphabet Grammar Validator_safe.
+
+Module Make(Import A:Automaton.T).
+Module Import ValidSafe := Validator_safe.Make A.
+
+(** A few helpers for dependent types. *)
+
+(** Decidable propositions. *)
+Class Decidable (P : Prop) := decide : {P} + {~P}.
+Arguments decide _ {_}.
+
+(** A [Comparable] type has decidable equality. *)
+Instance comparable_decidable_eq T `{ComparableLeibnizEq T} (x y : T) :
+  Decidable (x = y).
+Proof.
+  unfold Decidable.
+  destruct (compare x y) eqn:EQ; [left; apply compare_eq; intuition | ..];
+    right; intros ->; by rewrite compare_refl in EQ.
+Defined.
+
+Instance list_decidable_eq T :
+  (forall x y : T, Decidable (x = y)) ->
+  (forall l1 l2 : list T, Decidable (l1 = l2)).
+Proof. unfold Decidable. decide equality. Defined.
+
+Ltac subst_existT :=
+  repeat
+    match goal with
+    | _ => progress subst
+    | H : @existT ?A ?P ?x ?y1 = @existT ?A ?P ?x ?y2 |- _ =>
+      let DEC := fresh in
+      assert (DEC : forall u1 u2 : A, Decidable (u1 = u2)) by apply _;
+      apply Eqdep_dec.inj_pair2_eq_dec in H; [|by apply DEC];
+      clear DEC
+    end.
+
+(** The interpreter is written using dependent types. In order to
+  avoid reducing proof terms while executing the parser, we thunk all
+  the propositions behind an arrow.
+  Note that thunkP is still in Prop so that it is erased by
+  extraction.
+ *)
+Definition thunkP (P : Prop) : Prop := True -> P.
+
+(** Sometimes, we actually need a reduced proof in a program (for
+  example when using an equality to cast a value). In that case,
+  instead of reducing the proof we already have, we reprove the
+  assertion by using decidability. *)
+Definition reprove {P} `{Decidable P} (p : thunkP P) : P :=
+  match decide P with
+  | left p => p
+  | right np => False_ind _ (np (p I))
+  end.
+
+(** Combination of reprove with eq_rect. *)
+Definition cast {T : Type} (F : T -> Type) {x y : T} (eq : thunkP (x = y))
+                {DEC : unit -> Decidable (x = y)}:
+                F x -> F y :=
+  fun a => eq_rect x F a y (@reprove _ (DEC ()) eq).
+
+Lemma cast_eq T F (x : T) (eq : thunkP (x = x)) `{forall x y, Decidable (x = y)} a :
+  cast F eq a = a.
+Proof. by rewrite /cast -Eqdep_dec.eq_rect_eq_dec. Qed.
+
+(** Input buffers and operations on them. **)
+CoInductive buffer : Type :=
+  Buf_cons { buf_head : token; buf_tail : buffer }.
+
+Delimit Scope buffer_scope with buf.
+Bind Scope buffer_scope with buffer.
+
+Infix "::" := Buf_cons (at level 60, right associativity) : buffer_scope.
+
+(** Concatenation of a list and an input buffer **)
+Fixpoint app_buf (l:list token) (buf:buffer) :=
+  match l with
+    | nil => buf
+    | cons t q => (t :: app_buf q buf)%buf
+  end.
+Infix "++" := app_buf (at level 60, right associativity) : buffer_scope.
+
+Lemma app_buf_assoc (l1 l2:list token) (buf:buffer) :
+  (l1 ++ (l2 ++ buf) = (l1 ++ l2) ++ buf)%buf.
+Proof. induction l1 as [|?? IH]=>//=. rewrite IH //. Qed.
+
+(** The type of a non initial state: the type of semantic values associated
+   with the last symbol of this state. *)
+Definition noninitstate_type state :=
+  symbol_semantic_type (last_symb_of_non_init_state state).
+
+(** The stack of the automaton : it can be either nil or contains a non
+    initial state, a semantic value for the symbol associted with this state,
+    and a nested stack. **)
+Definition stack := list (sigT noninitstate_type). (* eg. list {state & state_type state} *)
+
+Section Interpreter.
+
+Hypothesis safe: safe.
+
+(* Properties of the automaton deduced from safety validation. *)
+Proposition shift_head_symbs: shift_head_symbs.
+Proof. pose proof safe; unfold ValidSafe.safe in H; intuition. Qed.
+Proposition goto_head_symbs: goto_head_symbs.
+Proof. pose proof safe; unfold ValidSafe.safe in H; intuition. Qed.
+Proposition shift_past_state: shift_past_state.
+Proof. pose proof safe; unfold ValidSafe.safe in H; intuition. Qed.
+Proposition goto_past_state: goto_past_state.
+Proof. pose proof safe; unfold ValidSafe.safe in H; intuition. Qed.
+Proposition reduce_ok: reduce_ok.
+Proof. pose proof safe; unfold ValidSafe.safe in H; intuition. Qed.
+
+Variable init : initstate.
+
+(** The top state of a stack **)
+Definition state_of_stack (stack:stack): state :=
+  match stack with
+    | [] => init
+    | existT _ s _::_ => s
+  end.
+
+(** The stack of states of an automaton stack **)
+Definition state_stack_of_stack (stack:stack) :=
+  (List.map
+    (fun cell:sigT noninitstate_type => singleton_state_pred (projT1 cell))
+    stack ++ [singleton_state_pred init])%list.
+
+(** The stack of symbols of an automaton stack **)
+Definition symb_stack_of_stack (stack:stack) :=
+  List.map
+    (fun cell:sigT noninitstate_type => last_symb_of_non_init_state (projT1 cell))
+    stack.
+
+(** The stack invariant : it basically states that the assumptions on the
+    states are true. **)
+Inductive stack_invariant: stack -> Prop :=
+  | stack_invariant_constr:
+    forall stack,
+      prefix      (head_symbs_of_state (state_of_stack stack))
+                  (symb_stack_of_stack stack) ->
+      prefix_pred (head_states_of_state (state_of_stack stack))
+                  (state_stack_of_stack stack) ->
+      stack_invariant_next stack ->
+      stack_invariant stack
+with stack_invariant_next: stack -> Prop :=
+  | stack_invariant_next_nil:
+      stack_invariant_next []
+  | stack_invariant_next_cons:
+    forall state_cur st stack_rec,
+      stack_invariant stack_rec ->
+      stack_invariant_next (existT _ state_cur st::stack_rec).
+
+(** [pop] pops some symbols from the stack. It returns the popped semantic
+    values using [sem_popped] as an accumulator and discards the popped
+    states.**)
+Fixpoint pop (symbols_to_pop:list symbol) {A:Type} (stk:stack) :
+  thunkP (prefix symbols_to_pop (symb_stack_of_stack stk)) ->
+  forall (action:arrows_right A (map symbol_semantic_type symbols_to_pop)),
+    stack * A.
+unshelve refine
+  (match symbols_to_pop
+      return
+         (thunkP (prefix symbols_to_pop (symb_stack_of_stack stk))) ->
+         forall (action:arrows_right A (map _ symbols_to_pop)), stack * A
+   with
+     | [] => fun _ action => (stk, action)
+     | t::q => fun Hp action =>
+       match stk
+          return thunkP (prefix (t::q) (symb_stack_of_stack stk)) -> stack * A
+       with
+         | existT _ state_cur sem::stack_rec => fun Hp =>
+           let sem_conv := cast symbol_semantic_type _ sem in
+           pop q _ stack_rec _ (action sem_conv)
+         | [] => fun Hp => False_rect _ _
+       end Hp
+   end).
+Proof.
+  - simpl in Hp. clear -Hp. abstract (intros _ ; specialize (Hp I); now inversion Hp).
+  - clear -Hp. abstract (specialize (Hp I); now inversion Hp).
+  - simpl in Hp. clear -Hp. abstract (intros _ ; specialize (Hp I); now inversion Hp).
+Defined.
+
+(* Equivalent declarative specification for pop, so that we avoid
+   (part of) the dependent types nightmare. *)
+Inductive pop_spec {A:Type} :
+    forall (symbols_to_pop:list symbol) (stk : stack)
+           (action : arrows_right A (map symbol_semantic_type symbols_to_pop))
+           (stk' : stack) (sem : A),
+      Prop :=
+  | Nil_pop_spec stk sem : pop_spec [] stk sem stk sem
+  | Cons_pop_spec symbols_to_pop st stk action sem stk' res :
+      pop_spec symbols_to_pop stk (action sem) stk' res ->
+      pop_spec (last_symb_of_non_init_state st::symbols_to_pop)
+               (existT _ st sem :: stk) action stk' res.
+
+Lemma pop_spec_ok {A:Type} symbols_to_pop stk Hp action stk' res:
+  pop symbols_to_pop stk Hp action = (stk', res) <->
+  pop_spec (A:=A) symbols_to_pop stk action stk' res.
+Proof.
+  revert stk Hp action.
+  induction symbols_to_pop as [|t symbols_to_pop IH]=>stk Hp action /=.
+  - split.
+    + intros [= <- <-]. constructor.
+    + intros H. inversion H. by subst_existT.
+  - destruct stk as [|[st sem]]=>/=; [by destruct pop_subproof0|].
+    remember (pop_subproof t symbols_to_pop stk st Hp) as EQ eqn:eq. clear eq.
+    generalize EQ. revert Hp action. rewrite <-(EQ I)=>Hp action ?.
+    rewrite cast_eq. rewrite IH. split.
+    + intros. by constructor.
+    + intros H. inversion H. by subst_existT.
+Qed.
+
+
+Lemma pop_preserves_invariant symbols_to_pop stk Hp A action :
+  stack_invariant stk ->
+  stack_invariant (fst (pop symbols_to_pop stk Hp (A:=A) action)).
+Proof.
+  revert stk Hp A action. induction symbols_to_pop as [|t q IH]=>//=.
+  intros stk Hp A action Hi.
+  destruct Hi as [stack Hp' Hpp [|state st stk']].
+  - destruct pop_subproof0.
+  - now apply IH.
+Qed.
+
+Lemma pop_state_valid symbols_to_pop stk Hp A action lpred :
+  prefix_pred lpred (state_stack_of_stack stk) ->
+  let stk' := fst (pop symbols_to_pop stk Hp (A:=A) action) in
+  state_valid_after_pop (state_of_stack stk') symbols_to_pop lpred.
+Proof.
+  revert stk Hp A action lpred. induction symbols_to_pop as [|t q IH]=>/=.
+  - intros stk Hp A a lpred Hpp. destruct lpred as [|pred lpred]; constructor.
+    inversion Hpp as [|? lpred' ? pred' Himpl Hpp' eq1 eq2]; subst.
+    specialize (Himpl (state_of_stack stk)).
+    destruct (pred' (state_of_stack stk)) as [] eqn:Heqpred'=>//.
+    destruct stk as [|[]]; simpl in *.
+    + inversion eq2; subst; clear eq2.
+      unfold singleton_state_pred in Heqpred'.
+      now rewrite compare_refl in Heqpred'; discriminate.
+    + inversion eq2; subst; clear eq2.
+      unfold singleton_state_pred in Heqpred'.
+      now rewrite compare_refl in Heqpred'; discriminate.
+  - intros stk Hp A a lpred Hpp. destruct stk as [|[] stk]=>//=.
+    + destruct pop_subproof0.
+    + destruct lpred as [|pred lpred]; [by constructor|].
+      constructor. apply IH. by inversion Hpp.
+Qed.
+
+(** [step_result] represents the result of one step of the automaton : it can
+    fail, accept or progress. [Fail_sr] means that the input is incorrect.
+    [Accept_sr] means that this is the last step of the automaton, and it
+    returns the semantic value of the input word. [Progress_sr] means that
+    some progress has been made, but new steps are needed in order to accept
+    a word.
+
+    For [Accept_sr] and [Progress_sr], the result contains the new input buffer.
+
+    [Fail_sr] means that the input word is rejected by the automaton. It is
+    different to [Err] (from the error monad), which mean that the automaton is
+    bogus and has perfomed a forbidden action. **)
+Inductive step_result :=
+  | Fail_sr: step_result
+  | Accept_sr: symbol_semantic_type (NT (start_nt init)) -> buffer -> step_result
+  | Progress_sr: stack -> buffer -> step_result.
+
+(** [reduce_step] does a reduce action :
+   - pops some elements from the stack
+   - execute the action of the production
+   - follows the goto for the produced non terminal symbol **)
+Definition reduce_step stk prod (buffer : buffer)
+        (Hval : thunkP (valid_for_reduce (state_of_stack stk) prod))
+        (Hi : thunkP (stack_invariant stk))
+  : step_result.
+refine
+  ((let '(stk', sem) as ss := pop (prod_rhs_rev prod) stk _ (prod_action prod)
+      return thunkP (state_valid_after_pop (state_of_stack (fst ss)) _
+                               (head_states_of_state (state_of_stack stk))) -> _
+    in fun Hval' =>
+    match goto_table (state_of_stack stk') (prod_lhs prod) as goto
+      return (thunkP (goto = None ->
+                      match state_of_stack stk' with
+                      | Init i => prod_lhs prod = start_nt i
+                      | Ninit _ => False
+                      end)) -> _
+    with
+    | Some (exist _ state_new e) => fun _ =>
+      let sem := eq_rect _ _ sem _ e in
+      Progress_sr (existT noninitstate_type state_new sem::stk') buffer
+    | None => fun Hval =>
+      let sem := cast symbol_semantic_type _ sem in
+      Accept_sr sem buffer
+    end (fun _ => _))
+   (fun _ => pop_state_valid _ _ _ _ _ _ _)).
+Proof.
+  - clear -Hi Hval.
+    abstract (intros _; destruct Hi=>//; eapply prefix_trans; [by apply Hval|eassumption]).
+  - clear -Hval.
+    abstract (intros _; f_equal; specialize (Hval I eq_refl); destruct stk' as [|[]]=>//).
+  - simpl in Hval'. clear -Hval Hval'.
+    abstract (move : Hval => /(_ I) [_ /(_ _ (Hval' I))] Hval2 Hgoto; by rewrite Hgoto in Hval2).
+  - clear -Hi. abstract by destruct Hi.
+Defined.
+
+Lemma reduce_step_stack_invariant_preserved stk prod buffer Hv Hi stk' buffer':
+  reduce_step stk prod buffer Hv Hi = Progress_sr stk' buffer' ->
+  stack_invariant stk'.
+Proof.
+  unfold reduce_step.
+  match goal with
+  | |- context [pop ?symbols_to_pop stk ?Hp ?action] =>
+    assert (Hi':=pop_preserves_invariant symbols_to_pop stk Hp _ action (Hi I));
+    generalize (pop_state_valid symbols_to_pop stk Hp _ action)
+  end.
+  destruct pop as [stk0 sem]=>/=. simpl in Hi'. intros Hv'.
+  assert (Hgoto1:=goto_head_symbs (state_of_stack stk0) (prod_lhs prod)).
+  assert (Hgoto2:=goto_past_state (state_of_stack stk0) (prod_lhs prod)).
+  match goal with | |- context [fun _ : True => ?X] => generalize X end.
+  destruct goto_table as [[state_new e]|] eqn:EQgoto=>//.
+  intros _ [= <- <-]. constructor=>/=.
+  - constructor. eapply prefix_trans. apply Hgoto1. by destruct Hi'.
+  - unfold state_stack_of_stack; simpl; constructor.
+    + intros ?. by destruct singleton_state_pred.
+    + eapply prefix_pred_trans. apply Hgoto2. by destruct Hi'.
+  - by constructor.
+Qed.
+
+(** One step of parsing. **)
+Definition step stk buffer (Hi : thunkP (stack_invariant stk)): step_result :=
+  match action_table (state_of_stack stk) as a return
+    thunkP
+      match a return Prop with
+      | Default_reduce_act prod => _
+      | Lookahead_act awt => forall t : terminal,
+        match awt t with
+        | Reduce_act p => _
+        | _ => True
+        end
+      end -> _
+  with
+  | Default_reduce_act prod => fun Hv =>
+    reduce_step stk prod buffer Hv Hi
+  | Lookahead_act awt => fun Hv =>
+    match buf_head buffer with
+    | tok =>
+      match awt (token_term tok) as a return
+        thunkP match a return Prop with Reduce_act p => _ | _ => _ end -> _
+      with
+      | Shift_act state_new e => fun _ =>
+        let sem_conv := eq_rect _ symbol_semantic_type (token_sem tok) _ e in
+        Progress_sr (existT noninitstate_type state_new sem_conv::stk)
+                    (buf_tail buffer)
+      | Reduce_act prod => fun Hv =>
+        reduce_step stk prod buffer Hv Hi
+      | Fail_act => fun _ =>
+        Fail_sr
+      end (fun _ => Hv I (token_term tok))
+    end
+  end (fun _ => reduce_ok _).
+
+Lemma step_stack_invariant_preserved stk buffer Hi stk' buffer':
+  step stk buffer Hi = Progress_sr stk' buffer' ->
+  stack_invariant stk'.
+Proof.
+  unfold step.
+  generalize (reduce_ok (state_of_stack stk))=>Hred.
+  assert (Hshift1 := shift_head_symbs (state_of_stack stk)).
+  assert (Hshift2 := shift_past_state (state_of_stack stk)).
+  destruct action_table as [prod|awt]=>/=.
+  - eauto using reduce_step_stack_invariant_preserved.
+  - set (term := token_term (buf_head buffer)).
+    generalize (Hred term). clear Hred. intros Hred.
+    specialize (Hshift1 term). specialize (Hshift2 term).
+    destruct (awt term) as [state_new e|prod|]=>//.
+    + intros [= <- <-]. constructor=>/=.
+      * constructor. eapply prefix_trans. apply Hshift1. by destruct Hi.
+      * unfold state_stack_of_stack; simpl; constructor.
+        -- intros ?. by destruct singleton_state_pred.
+        -- eapply prefix_pred_trans. apply Hshift2. by destruct Hi.
+      * constructor; by apply Hi.
+    + eauto using reduce_step_stack_invariant_preserved.
+Qed.
+
+(** The parsing use a [nat] fuel parameter [log_n_steps], so that we
+    do not have to prove terminaison, which is difficult.
+
+    Note that [log_n_steps] is *not* the fuel in the conventionnal
+    sense: this parameter contains the logarithm (in base 2) of the
+    number of steps to perform. Hence, a value of, e.g., 50 will
+    usually be enough to ensure termination. *)
+Fixpoint parse_fix stk buffer (log_n_steps : nat) (Hi : thunkP (stack_invariant stk)):
+  { sr : step_result |
+    forall stk' buffer', sr = Progress_sr stk' buffer' -> stack_invariant stk' } :=
+  match log_n_steps with
+  | O => exist _ (step stk buffer Hi)
+                 (step_stack_invariant_preserved _ _ Hi)
+  | S log_n_steps =>
+    match parse_fix stk buffer log_n_steps Hi with
+    | exist _ (Progress_sr stk buffer) Hi' =>
+      parse_fix stk buffer log_n_steps (fun _ => Hi' _ buffer eq_refl)
+    | sr => sr
+    end
+  end.
+
+(** The final result of a parsing is either a failure (the automaton
+    has rejected the input word), either a timeout (the automaton has
+    spent all the given [2^log_n_steps]), either a parsed semantic value
+    with a rest of the input buffer.
+
+    Note that we do not make parse_result depend on start_nt for the
+    result type, so that this inductive is extracted without the use
+    of Obj.t in OCaml.  **)
+Inductive parse_result {A : Type} :=
+  | Fail_pr: parse_result
+  | Timeout_pr: parse_result
+  | Parsed_pr: A -> buffer -> parse_result.
+Global Arguments parse_result _ : clear implicits.
+
+Definition parse (buffer : buffer) (log_n_steps : nat):
+  parse_result (symbol_semantic_type (NT (start_nt init))).
+refine (match proj1_sig (parse_fix [] buffer log_n_steps _) with
+        | Fail_sr => Fail_pr
+        | Accept_sr sem buffer' => Parsed_pr sem buffer'
+        | Progress_sr _ _ => Timeout_pr
+        end).
+Proof.
+  abstract (repeat constructor; intros; by destruct singleton_state_pred).
+Defined.
+
+End Interpreter.
+
+Arguments Fail_sr {init}.
+Arguments Accept_sr {init} _ _.
+Arguments Progress_sr {init} _ _.
+
+End Make.
+
+Module Type T(A:Automaton.T).
+  Include (Make A).
+End T.
diff --git a/MenhirLib/Interpreter_complete.v b/MenhirLib/Interpreter_complete.v
new file mode 100644
index 00000000..ec69592b
--- /dev/null
+++ b/MenhirLib/Interpreter_complete.v
@@ -0,0 +1,825 @@
+(****************************************************************************)
+(*                                                                          *)
+(*                                   Menhir                                 *)
+(*                                                                          *)
+(*           Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud         *)
+(*                                                                          *)
+(*  Copyright Inria. All rights reserved. This file is distributed under    *)
+(*  the terms of the GNU Lesser General Public License as published by the  *)
+(*  Free Software Foundation, either version 3 of the License, or (at your  *)
+(*  option) any later version, as described in the file LICENSE.            *)
+(*                                                                          *)
+(****************************************************************************)
+
+From Coq Require Import List Syntax Arith.
+From Coq.ssr Require Import ssreflect.
+Require Import Alphabet Grammar.
+Require Automaton Interpreter Validator_complete.
+
+Module Make(Import A:Automaton.T) (Import Inter:Interpreter.T A).
+Module Import Valid := Validator_complete.Make A.
+
+(** * Completeness Proof **)
+
+Section Completeness_Proof.
+
+Hypothesis safe: Inter.ValidSafe.safe.
+Hypothesis complete: complete.
+
+(* Properties of the automaton deduced from completeness validation. *)
+Proposition nullable_stable: nullable_stable.
+Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed.
+Proposition first_stable: first_stable.
+Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed.
+Proposition start_future: start_future.
+Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed.
+Proposition terminal_shift: terminal_shift.
+Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed.
+Proposition end_reduce: end_reduce.
+Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed.
+Proposition start_goto: start_goto.
+Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed.
+Proposition non_terminal_goto: non_terminal_goto.
+Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed.
+Proposition non_terminal_closed: non_terminal_closed.
+Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed.
+
+(** If the nullable predicate has been validated, then it is correct. **)
+Lemma nullable_correct head word :
+  word = [] -> parse_tree head word -> nullable_symb head = true
+with nullable_correct_list heads word :
+  word = [] ->
+  parse_tree_list heads word -> nullable_word heads = true.
+Proof.
+  - destruct 2=>//. assert (Hnull := nullable_stable prod).
+    erewrite nullable_correct_list in Hnull; eauto.
+  - intros Hword. destruct 1=>//=. destruct (app_eq_nil _ _ Hword).
+    eauto using andb_true_intro.
+Qed.
+
+(** Auxiliary lemma for first_correct.  *)
+Lemma first_word_set_app t word1 word2 :
+  TerminalSet.In t (first_word_set (word1 ++ word2)) <->
+  TerminalSet.In t (first_word_set word1) \/
+  TerminalSet.In t (first_word_set word2) /\ nullable_word (rev word1) = true.
+Proof.
+  induction word1 as [|s word1 IH]=>/=.
+  - split; [tauto|]. move=>[/TerminalSet.empty_1 ?|[? _]]//.
+  - rewrite /nullable_word forallb_app /=. destruct nullable_symb=>/=.
+    + rewrite Bool.andb_true_r. split.
+      * move=>/TerminalSet.union_1. rewrite IH.
+        move=>[?|[?|[??]]]; auto using TerminalSet.union_2, TerminalSet.union_3.
+      * destruct IH.
+        move=>[/TerminalSet.union_1 [?|?]|[??]];
+        auto using TerminalSet.union_2, TerminalSet.union_3.
+    + rewrite Bool.andb_false_r. by intuition.
+Qed.
+
+(** If the first predicate has been validated, then it is correct. **)
+Lemma first_correct head word t q :
+  word = t::q ->
+  parse_tree head word ->
+  TerminalSet.In (token_term t) (first_symb_set head)
+with first_correct_list heads word t q :
+  word = t::q ->
+  parse_tree_list heads word ->
+  TerminalSet.In (token_term t) (first_word_set (rev' heads)).
+Proof.
+  - intros Hword. destruct 1=>//.
+    + inversion Hword. subst. apply TerminalSet.singleton_2, compare_refl.
+    + eapply first_stable. eauto.
+  - intros Hword. destruct 1 as [|symq wordq ptl symt wordt pt]=>//=.
+    rewrite /rev' -rev_alt /= first_word_set_app /= rev_involutive rev_alt.
+    destruct wordq; [right|left].
+    + destruct nullable_symb; eauto using TerminalSet.union_2, nullable_correct_list.
+    + inversion Hword. subst. fold (rev' symq). eauto.
+Qed.
+
+(** A PTL is compatible with a stack if the top of the stack contains
+  data representing to this PTL. *)
+Fixpoint ptl_stack_compat {symbs word}
+         (stk0 : stack) (ptl : parse_tree_list symbs word) (stk : stack) : Prop :=
+  match ptl with
+  | Nil_ptl => stk0 = stk
+  | @Cons_ptl _ _ ptl sym _ pt =>
+    match stk with
+    | [] => False
+    | existT _ _ sem::stk =>
+      ptl_stack_compat stk0 ptl stk /\
+      exists e,
+        sem = eq_rect _ symbol_semantic_type (pt_sem pt) _ e
+    end
+  end.
+
+(** .. and when a PTL is compatible with a stack, then calling the pop
+  function return the semantic value of this PTL. *)
+Lemma pop_stack_compat_pop_spec {A symbs word}
+    (ptl:parse_tree_list symbs word) (stk:stack) (stk0:stack) action :
+  ptl_stack_compat stk0 ptl stk ->
+  pop_spec symbs stk action stk0 (ptl_sem (A:=A) ptl action).
+Proof.
+  revert stk. induction ptl=>stk /= Hstk.
+  - subst. constructor.
+  - destruct stk as [|[st sem] stk]=>//. destruct Hstk as [Hstk [??]]. subst.
+    simpl. constructor. eauto.
+Qed.
+
+Variable init: initstate.
+
+(** In order to prove compleness, we first fix a word to be parsed
+  together with the content of the parser at the end of the parsing. *)
+Variable full_word: list token.
+Variable buffer_end: buffer.
+
+(** Completeness is proved by following the traversal of the parse
+  tree which is performed by the parser. Each step of parsing
+  correspond to one step of traversal. In order to represent the state
+  of the traversal, we define the notion of "dotted" parse tree, which
+  is a parse tree with one dot on one of its node. The place of the
+  dot represents the place of the next action to be executed.
+
+  Such a dotted parse tree is decomposed into two part: a "regular"
+  parse tree, which is the parse tree placed under the dot, and a
+  "parse tree zipper", which is the part of the parse tree placed
+  above the dot. Therefore, a parse tree zipper is a parse tree with a
+  hole. Moreover, for easier manipulation, a parse tree zipper is
+  represented "upside down". That is, the root of the parse tree is
+  actually a leaf of the zipper, while the root of the zipper is the
+  hole.
+ *)
+Inductive pt_zipper:
+  forall (hole_symb:symbol) (hole_word:list token), Type :=
+| Top_ptz:
+  pt_zipper (NT (start_nt init)) full_word
+| Cons_ptl_ptz:
+  forall {head_symbolsq:list symbol} {wordq:list token},
+    parse_tree_list head_symbolsq wordq ->
+
+  forall {head_symbolt:symbol} {wordt:list token},
+
+    ptl_zipper (head_symbolt::head_symbolsq) (wordq++wordt) ->
+    pt_zipper head_symbolt wordt
+with ptl_zipper:
+  forall (hole_symbs:list symbol) (hole_word:list token), Type :=
+| Non_terminal_pt_ptlz:
+  forall {p:production} {word:list token},
+    pt_zipper (NT (prod_lhs p)) word ->
+    ptl_zipper (prod_rhs_rev p) word
+
+| Cons_ptl_ptlz:
+  forall {head_symbolsq:list symbol} {wordq:list token},
+
+  forall {head_symbolt:symbol} {wordt:list token},
+    parse_tree head_symbolt wordt ->
+
+  ptl_zipper (head_symbolt::head_symbolsq) (wordq++wordt) ->
+
+  ptl_zipper head_symbolsq wordq.
+
+(** A dotted parse tree is the combination of a parse tree zipper with
+  a parse tree. It can be intwo flavors, depending on which is the next
+  action to be executed (shift or reduce). *)
+Inductive pt_dot: Type :=
+| Reduce_ptd: forall {prod word},
+    parse_tree_list (prod_rhs_rev prod) word ->
+    pt_zipper (NT (prod_lhs prod)) word ->
+    pt_dot
+| Shift_ptd: forall (tok : token) {symbolsq wordq},
+    parse_tree_list symbolsq wordq ->
+    ptl_zipper (T (token_term tok)::symbolsq) (wordq++[tok]) ->
+    pt_dot.
+
+(** We can compute the full semantic value of a parse tree when
+  represented as a dotted ptd. *)
+
+Fixpoint ptlz_sem {hole_symbs hole_word}
+         (ptlz:ptl_zipper hole_symbs hole_word) :
+         (forall A, arrows_right A (map symbol_semantic_type hole_symbs) -> A) ->
+         (symbol_semantic_type (NT (start_nt init))) :=
+  match ptlz with
+  | @Non_terminal_pt_ptlz prod _ ptz =>
+    fun k => ptz_sem ptz (k _ (prod_action prod))
+  | Cons_ptl_ptlz pt ptlz =>
+    fun k => ptlz_sem ptlz (fun _ f => k _ (f (pt_sem pt)))
+  end
+with ptz_sem {hole_symb hole_word}
+             (ptz:pt_zipper hole_symb hole_word):
+  symbol_semantic_type hole_symb -> symbol_semantic_type (NT (start_nt init)) :=
+  match ptz with
+  | Top_ptz => fun sem => sem
+  | Cons_ptl_ptz ptl ptlz =>
+    fun sem => ptlz_sem ptlz (fun _ f => ptl_sem ptl (f sem))
+  end.
+
+Definition ptd_sem (ptd : pt_dot) :=
+  match ptd with
+  | @Reduce_ptd prod _ ptl ptz =>
+    ptz_sem ptz (ptl_sem ptl (prod_action prod))
+  | Shift_ptd tok ptl ptlz =>
+    ptlz_sem ptlz (fun _ f => ptl_sem ptl (f (token_sem tok)))
+  end.
+
+(** The buffer associated with a dotted parse tree corresponds to the
+  buffer left to be read by the parser when at the state represented
+  by the dotted parse tree. *)
+Fixpoint ptlz_buffer {hole_symbs hole_word}
+         (ptlz:ptl_zipper hole_symbs hole_word): buffer :=
+  match ptlz with
+  | Non_terminal_pt_ptlz ptz =>
+    ptz_buffer ptz
+  | @Cons_ptl_ptlz _ _ _ wordt _ ptlz' =>
+    wordt ++ ptlz_buffer ptlz'
+  end
+with ptz_buffer {hole_symb hole_word}
+                (ptz:pt_zipper hole_symb hole_word): buffer :=
+  match ptz with
+  | Top_ptz => buffer_end
+  | Cons_ptl_ptz _ ptlz =>
+    ptlz_buffer ptlz
+  end.
+
+Definition ptd_buffer (ptd:pt_dot) :=
+  match ptd with
+  | Reduce_ptd _ ptz => ptz_buffer ptz
+  | @Shift_ptd tok _ wordq _ ptlz => (tok::ptlz_buffer ptlz)%buf
+  end.
+
+(** We are now ready to define the main invariant of the proof of
+  completeness: we need to specify when a stack is compatible with a
+  dotted parse tree. Informally, a stack is compatible with a dotted
+  parse tree when it is the concatenation stack fragments which are
+  compatible with each of the partially recognized productions
+  appearing in the parse tree zipper. Moreover, the head of each of
+  these stack fragment contains a state which has an item predicted by
+  the corresponding zipper.
+
+  More formally, the compatibility relation first needs the following
+  auxiliary definitions: *)
+Fixpoint ptlz_prod {hole_symbs hole_word}
+         (ptlz:ptl_zipper hole_symbs hole_word): production :=
+  match ptlz with
+  | @Non_terminal_pt_ptlz prod _ _ => prod
+  | Cons_ptl_ptlz _ ptlz' => ptlz_prod ptlz'
+  end.
+
+Fixpoint ptlz_future {hole_symbs hole_word}
+  (ptlz:ptl_zipper hole_symbs hole_word): list symbol :=
+  match ptlz with
+  | Non_terminal_pt_ptlz _ => []
+  | @Cons_ptl_ptlz _ _ s _ _ ptlz' => s::ptlz_future ptlz'
+  end.
+
+Fixpoint ptlz_lookahead {hole_symbs hole_word}
+  (ptlz:ptl_zipper hole_symbs hole_word) : terminal :=
+  match ptlz with
+  | Non_terminal_pt_ptlz ptz => token_term (buf_head (ptz_buffer ptz))
+  | Cons_ptl_ptlz _ ptlz' => ptlz_lookahead ptlz'
+  end.
+
+Fixpoint ptz_stack_compat {hole_symb hole_word}
+         (stk : stack) (ptz : pt_zipper hole_symb hole_word) : Prop :=
+  match ptz with
+  | Top_ptz => stk = []
+  | Cons_ptl_ptz ptl ptlz =>
+    exists stk0,
+      state_has_future (state_of_stack init stk) (ptlz_prod ptlz)
+                       (hole_symb::ptlz_future ptlz) (ptlz_lookahead ptlz) /\
+      ptl_stack_compat stk0 ptl stk /\
+      ptlz_stack_compat stk0 ptlz
+  end
+with ptlz_stack_compat {hole_symbs hole_word}
+     (stk : stack) (ptlz : ptl_zipper hole_symbs hole_word) : Prop :=
+  match ptlz with
+  | Non_terminal_pt_ptlz ptz => ptz_stack_compat stk ptz
+  | Cons_ptl_ptlz _ ptlz => ptlz_stack_compat stk ptlz
+  end.
+
+Definition ptd_stack_compat (ptd:pt_dot) (stk:stack): Prop :=
+  match ptd with
+  | @Reduce_ptd prod _ ptl ptz =>
+    exists stk0,
+      state_has_future (state_of_stack init stk) prod []
+                       (token_term (buf_head (ptz_buffer ptz))) /\
+      ptl_stack_compat stk0 ptl stk /\
+      ptz_stack_compat stk0 ptz
+  | Shift_ptd tok ptl ptlz =>
+    exists stk0,
+      state_has_future (state_of_stack init stk) (ptlz_prod ptlz)
+                       (T (token_term tok) :: ptlz_future ptlz) (ptlz_lookahead ptlz) /\
+      ptl_stack_compat stk0 ptl stk /\
+      ptlz_stack_compat stk0 ptlz
+  end.
+
+Lemma ptz_stack_compat_cons_state_has_future {symbsq wordq symbt wordt} stk
+      (ptl : parse_tree_list symbsq wordq)
+      (ptlz : ptl_zipper (symbt :: symbsq) (wordq ++ wordt)) :
+  ptz_stack_compat stk (Cons_ptl_ptz ptl ptlz) ->
+  state_has_future (state_of_stack init stk) (ptlz_prod ptlz)
+                   (symbt::ptlz_future ptlz) (ptlz_lookahead ptlz).
+Proof. move=>[stk0 [? [? ?]]] //. Qed.
+
+Lemma ptlz_future_ptlz_prod hole_symbs hole_word
+      (ptlz:ptl_zipper hole_symbs hole_word) :
+  rev_append (ptlz_future ptlz) hole_symbs = prod_rhs_rev (ptlz_prod ptlz).
+Proof. induction ptlz=>//=. Qed.
+
+Lemma ptlz_future_first {symbs word} (ptlz : ptl_zipper symbs word) :
+  TerminalSet.In (token_term (buf_head (ptlz_buffer ptlz)))
+    (first_word_set (ptlz_future ptlz)) \/
+  token_term (buf_head (ptlz_buffer ptlz)) = ptlz_lookahead ptlz /\
+  nullable_word (ptlz_future ptlz) = true.
+Proof.
+  induction ptlz as [|??? [|tok] pt ptlz IH]; [by auto| |]=>/=.
+  - rewrite (nullable_correct _ _ eq_refl pt).
+    destruct IH as [|[??]]; [left|right]=>/=; auto using TerminalSet.union_3.
+  - left. destruct nullable_symb; eauto using TerminalSet.union_2, first_correct.
+Qed.
+
+(** We now want to define what is the next dotted parse tree which is
+  to be handled after one action. Such dotted parse is built in two
+  steps: Not only we have to perform the action by completing the
+  parse tree, but we also have to prepare for the following step by
+  moving the dot down to place it in front of the next action to be
+  performed.
+*)
+Fixpoint build_pt_dot_from_pt {symb word}
+         (pt : parse_tree symb word) (ptz : pt_zipper symb word)
+  : pt_dot :=
+  match pt in parse_tree symb word
+    return pt_zipper symb word -> pt_dot
+  with
+  | Terminal_pt tok =>
+    fun ptz =>
+      let X :=
+          match ptz in pt_zipper symb word
+            return match symb with T term => True | NT _ => False end ->
+                   { symbsq : list symbol &
+                     { wordq : list token &
+                       (parse_tree_list symbsq wordq *
+                        ptl_zipper (symb :: symbsq) (wordq ++ word))%type } }
+          with
+          | Top_ptz => fun F => False_rect _ F
+          | Cons_ptl_ptz ptl ptlz => fun _ =>
+            existT _ _ (existT _ _ (ptl, ptlz))
+          end I
+      in
+      Shift_ptd tok (fst (projT2 (projT2 X))) (snd (projT2 (projT2 X)))
+  | Non_terminal_pt prod ptl => fun ptz =>
+    let is_notnil :=
+      match ptl in parse_tree_list w _
+        return option (match w return Prop with [] => False | _ => True end)
+      with
+      | Nil_ptl => None
+      | _ => Some I
+      end
+    in
+    match is_notnil with
+    | None => Reduce_ptd ptl ptz
+    | Some H => build_pt_dot_from_pt_rec ptl H (Non_terminal_pt_ptlz ptz)
+    end
+  end ptz
+with build_pt_dot_from_pt_rec {symbs word}
+       (ptl : parse_tree_list symbs word)
+       (Hsymbs : match symbs with [] => False | _ => True end)
+       (ptlz : ptl_zipper symbs word)
+  : pt_dot :=
+  match ptl in parse_tree_list symbs word
+    return match symbs with [] => False | _ => True end ->
+           ptl_zipper symbs word ->
+           pt_dot
+  with
+  | Nil_ptl => fun Hsymbs _ => False_rect _ Hsymbs
+  | Cons_ptl ptl' pt => fun _ =>
+    match ptl' in parse_tree_list symbsq wordq
+      return parse_tree_list symbsq wordq ->
+             ptl_zipper (_ :: symbsq) (wordq ++ _) ->
+             pt_dot
+    with
+    | Nil_ptl => fun _ ptlz =>
+      build_pt_dot_from_pt pt (Cons_ptl_ptz Nil_ptl ptlz)
+    | _ => fun ptl' ptlz =>
+      build_pt_dot_from_pt_rec ptl' I (Cons_ptl_ptlz pt ptlz)
+    end ptl'
+  end Hsymbs ptlz.
+
+Definition build_pt_dot_from_ptl {symbs word}
+         (ptl : parse_tree_list symbs word)
+         (ptlz : ptl_zipper symbs word)
+  : pt_dot :=
+  match ptlz in ptl_zipper symbs word
+    return parse_tree_list symbs word -> pt_dot
+  with
+  | Non_terminal_pt_ptlz ptz => fun ptl =>
+    Reduce_ptd ptl ptz
+  | Cons_ptl_ptlz pt ptlz => fun ptl =>
+    build_pt_dot_from_pt pt (Cons_ptl_ptz ptl ptlz)
+  end ptl.
+
+Definition next_ptd (ptd:pt_dot) : option pt_dot :=
+  match ptd with
+  | Shift_ptd tok ptl ptlz =>
+    Some (build_pt_dot_from_ptl (Cons_ptl ptl (Terminal_pt tok)) ptlz)
+  | Reduce_ptd ptl ptz =>
+    match ptz in pt_zipper symb word
+      return parse_tree symb word -> _
+    with
+    | Top_ptz => fun _ => None
+    | Cons_ptl_ptz ptl' ptlz => fun pt =>
+      Some (build_pt_dot_from_ptl (Cons_ptl ptl' pt) ptlz)
+    end (Non_terminal_pt _ ptl)
+  end.
+
+Fixpoint next_ptd_iter (ptd:pt_dot) (log_n_steps:nat) : option pt_dot :=
+  match log_n_steps with
+  | O => next_ptd ptd
+  | S log_n_steps =>
+    match next_ptd_iter ptd log_n_steps with
+    | None => None
+    | Some ptd => next_ptd_iter ptd log_n_steps
+    end
+  end.
+
+(** We prove that these functions behave well w.r.t. semantic values. *)
+Lemma sem_build_from_pt {symb word}
+      (pt : parse_tree symb word) (ptz : pt_zipper symb word)  :
+  ptz_sem ptz (pt_sem pt)
+  = ptd_sem (build_pt_dot_from_pt pt ptz)
+with sem_build_from_pt_rec {symbs word}
+     (ptl : parse_tree_list symbs word) (ptlz : ptl_zipper symbs word)
+     Hsymbs :
+  ptlz_sem ptlz (fun _ f => ptl_sem ptl f)
+  = ptd_sem (build_pt_dot_from_pt_rec ptl Hsymbs ptlz).
+Proof.
+  - destruct pt as [tok|prod word ptl]=>/=.
+    + revert ptz. generalize [tok].
+      generalize (token_sem tok). generalize I.
+      change True with (match T (token_term tok) with T _ => True | NT _ => False end) at 1.
+      generalize (T (token_term tok)) => symb HT sem word ptz. by destruct ptz.
+    + match goal with
+      | |- context [match ?X with Some H => _ | None => _ end] => destruct X=>//
+      end.
+      by rewrite -sem_build_from_pt_rec.
+  - destruct ptl; [contradiction|].
+    specialize (sem_build_from_pt_rec _ _ ptl)=>/=. destruct ptl.
+    + by rewrite -sem_build_from_pt.
+    + by rewrite -sem_build_from_pt_rec.
+Qed.
+
+Lemma sem_build_from_ptl {symbs word}
+      (ptl : parse_tree_list symbs word) (ptlz : ptl_zipper symbs word) :
+  ptlz_sem ptlz (fun _ f => ptl_sem ptl f)
+  = ptd_sem (build_pt_dot_from_ptl ptl ptlz).
+Proof. destruct ptlz=>//=. by rewrite -sem_build_from_pt. Qed.
+
+Lemma sem_next_ptd (ptd : pt_dot) :
+  match next_ptd ptd with
+  | None => True
+  | Some ptd' => ptd_sem ptd = ptd_sem ptd'
+  end.
+Proof.
+  destruct ptd as [prod word ptl ptz|tok symbs word ptl ptlz] =>/=.
+  - change (ptl_sem ptl (prod_action prod))
+      with (pt_sem (Non_terminal_pt prod ptl)).
+    generalize (Non_terminal_pt prod ptl). clear ptl.
+    destruct ptz as [|?? ptl ?? ptlz]=>// pt. by rewrite -sem_build_from_ptl.
+  - by rewrite -sem_build_from_ptl.
+Qed.
+
+Lemma sem_next_ptd_iter (ptd : pt_dot) (log_n_steps : nat) :
+  match next_ptd_iter ptd log_n_steps with
+  | None => True
+  | Some ptd' => ptd_sem ptd = ptd_sem ptd'
+  end.
+Proof.
+  revert ptd.
+  induction log_n_steps as [|log_n_steps IH]; [by apply sem_next_ptd|]=>/= ptd.
+  assert (IH1 := IH ptd). destruct next_ptd_iter as [ptd'|]=>//.
+  specialize (IH ptd'). destruct next_ptd_iter=>//. congruence.
+Qed.
+
+(** We prove that these functions behave well w.r.t. xxx_buffer. *)
+Lemma ptd_buffer_build_from_pt {symb word}
+      (pt : parse_tree symb word) (ptz : pt_zipper symb word) :
+  (word ++ ptz_buffer ptz)%buf = ptd_buffer (build_pt_dot_from_pt pt ptz)
+with ptd_buffer_build_from_pt_rec {symbs word}
+     (ptl : parse_tree_list symbs word) (ptlz : ptl_zipper symbs word)
+     Hsymbs :
+  (word ++ ptlz_buffer ptlz)%buf = ptd_buffer (build_pt_dot_from_pt_rec ptl Hsymbs ptlz).
+Proof.
+  - destruct pt as [tok|prod word ptl]=>/=.
+    + f_equal. revert ptz. generalize [tok].
+      generalize (token_sem tok). generalize I.
+      change True with (match T (token_term tok) with T _ => True | NT _ => False end) at 1.
+      generalize (T (token_term tok)) => symb HT sem word ptz. by destruct ptz.
+    + match goal with
+      | |- context [match ?X with Some H => _ | None => _ end] => destruct X eqn:EQ
+      end.
+      * by rewrite -ptd_buffer_build_from_pt_rec.
+      * rewrite [X in (X ++ _)%buf](_ : word = []) //. clear -EQ. by destruct ptl.
+  - destruct ptl as [|?? ptl ?? pt]; [contradiction|].
+    specialize (ptd_buffer_build_from_pt_rec _ _ ptl).
+    destruct ptl.
+    + by rewrite /= -ptd_buffer_build_from_pt.
+    + by rewrite -ptd_buffer_build_from_pt_rec //= app_buf_assoc.
+Qed.
+
+Lemma ptd_buffer_build_from_ptl {symbs word}
+      (ptl : parse_tree_list symbs word) (ptlz : ptl_zipper symbs word) :
+  ptlz_buffer ptlz = ptd_buffer (build_pt_dot_from_ptl ptl ptlz).
+Proof.
+  destruct ptlz as [|???? pt]=>//=. by rewrite -ptd_buffer_build_from_pt.
+Qed.
+
+(** We prove that these functions behave well w.r.t. xxx_stack_compat. *)
+Lemma ptd_stack_compat_build_from_pt {symb word}
+      (pt : parse_tree symb word) (ptz : pt_zipper symb word)
+      (stk: stack) :
+  ptz_stack_compat stk ptz ->
+  ptd_stack_compat (build_pt_dot_from_pt pt ptz) stk
+with ptd_stack_compat_build_from_pt_rec {symbs word}
+     (ptl : parse_tree_list symbs word) (ptlz : ptl_zipper symbs word)
+     (stk : stack) Hsymbs :
+  ptlz_stack_compat stk ptlz ->
+  state_has_future (state_of_stack init stk) (ptlz_prod ptlz)
+                   (rev' (prod_rhs_rev (ptlz_prod ptlz))) (ptlz_lookahead ptlz) ->
+  ptd_stack_compat (build_pt_dot_from_pt_rec ptl Hsymbs ptlz) stk.
+Proof.
+  - intros Hstk. destruct pt as [tok|prod word ptl]=>/=.
+    + revert ptz Hstk. generalize [tok]. generalize (token_sem tok). generalize I.
+      change True with (match T (token_term tok) with T _ => True | NT _ => False end) at 1.
+      generalize (T (token_term tok)) => symb HT sem word ptz. by destruct ptz.
+    + assert (state_has_future (state_of_stack init stk) prod
+               (rev' (prod_rhs_rev prod)) (token_term (buf_head (ptz_buffer ptz)))).
+      { revert ptz Hstk. remember (NT (prod_lhs prod)) eqn:EQ=>ptz.
+        destruct ptz as [|?? ptl0 ?? ptlz0].
+        - intros ->. apply start_future. congruence.
+        - subst. intros (stk0 & Hfut & _). apply non_terminal_closed in Hfut.
+          specialize (Hfut prod eq_refl).
+          destruct (ptlz_future_first ptlz0) as [Hfirst|[Hfirst Hnull]].
+          + destruct Hfut as [_ Hfut]. auto.
+          + destruct Hfut as [Hfut _]. by rewrite Hnull -Hfirst in Hfut. }
+      match goal with
+      | |- context [match ?X with Some H => _ | None => _ end] => destruct X eqn:EQ
+      end.
+      * by apply ptd_stack_compat_build_from_pt_rec.
+      * exists stk. destruct ptl=>//.
+  - intros Hstk Hfut. destruct ptl as [|?? ptl ?? pt]; [contradiction|].
+    specialize (ptd_stack_compat_build_from_pt_rec _ _ ptl). destruct ptl.
+    + eapply ptd_stack_compat_build_from_pt=>//. exists stk.
+      split; [|split]=>//; [].
+      by rewrite -ptlz_future_ptlz_prod rev_append_rev /rev' -rev_alt
+                 rev_app_distr rev_involutive in Hfut.
+    + by apply ptd_stack_compat_build_from_pt_rec.
+Qed.
+
+Lemma ptd_stack_compat_build_from_ptl {symbs word}
+      (ptl : parse_tree_list symbs word) (ptlz : ptl_zipper symbs word)
+      (stk stk0: stack) :
+  ptlz_stack_compat stk0 ptlz ->
+  ptl_stack_compat stk0 ptl stk ->
+  state_has_future (state_of_stack init stk) (ptlz_prod ptlz)
+                   (ptlz_future ptlz) (ptlz_lookahead ptlz) ->
+  ptd_stack_compat (build_pt_dot_from_ptl ptl ptlz) stk.
+Proof.
+  intros Hstk0 Hstk Hfut. destruct ptlz=>/=.
+  - eauto.
+  - apply ptd_stack_compat_build_from_pt=>/=. eauto.
+Qed.
+
+(** We can now proceed by proving that the invariant is preserved by
+  each step of parsing. We also prove that each step of parsing
+  follows next_ptd.
+
+  We start with reduce steps: *)
+Lemma reduce_step_next_ptd (prod : production) (word : list token)
+      (ptl : parse_tree_list (prod_rhs_rev prod) word)
+      (ptz : pt_zipper (NT (prod_lhs prod)) word)
+      (stk : stack)
+      Hval Hi :
+  ptd_stack_compat (Reduce_ptd ptl ptz) stk ->
+  match next_ptd (Reduce_ptd ptl ptz) with
+  | None =>
+    reduce_step init stk prod (ptz_buffer ptz) Hval Hi =
+      Accept_sr (ptd_sem (Reduce_ptd ptl ptz)) buffer_end
+  | Some ptd =>
+    exists stk',
+      reduce_step init stk prod (ptz_buffer ptz) Hval Hi =
+        Progress_sr stk' (ptd_buffer ptd) /\
+      ptd_stack_compat ptd stk'
+  end.
+Proof.
+  intros (stk0 & _ & Hstk & Hstk0).
+  apply pop_stack_compat_pop_spec with (action := prod_action prod) in Hstk.
+  rewrite <-pop_spec_ok with (Hp := reduce_step_subproof init stk prod Hval Hi) in Hstk.
+  unfold reduce_step.
+  match goal with
+  | |- context [pop_state_valid init ?A stk ?B ?C ?D ?E ?F] =>
+    generalize (pop_state_valid init A stk B C D E F)
+  end.
+  rewrite Hstk /=. intros Hv.
+  generalize (reduce_step_subproof1 init stk prod Hval stk0 (fun _ : True => Hv)).
+  clear Hval Hstk Hi Hv stk.
+  assert (Hgoto := fun fut prod' =>
+    non_terminal_goto (state_of_stack init stk0) prod' (NT (prod_lhs prod)::fut)).
+  simpl in Hgoto.
+  destruct goto_table as [[st Hst]|] eqn:Hgoto'.
+  - intros _.
+    assert (match ptz with Top_ptz => False | _ => True end).
+    { revert ptz Hst Hstk0 Hgoto'.
+      generalize (eq_refl (NT (prod_lhs prod))).
+      generalize (NT (prod_lhs prod)) at 1 3 5.
+      intros nt Hnt ptz. destruct ptz=>//. injection Hnt=> <- /= Hst -> /= Hg.
+      assert (Hsg := start_goto init). by rewrite Hg in Hsg. }
+    clear Hgoto'.
+
+    change (ptl_sem ptl (prod_action prod))
+      with (pt_sem (Non_terminal_pt prod ptl)).
+    generalize (Non_terminal_pt prod ptl). clear ptl.
+    destruct ptz as [|?? ptl ? ? ptlz]=>// pt.
+
+    subst=>/=. eexists _. split.
+    + f_equal. apply ptd_buffer_build_from_ptl.
+    + destruct Hstk0 as (stk0' & Hfut & Hstk0' & Hstk0).
+      apply (ptd_stack_compat_build_from_ptl _ _ _ stk0'); auto; [].
+      split=>//. by exists eq_refl.
+  - intros Hv. generalize (reduce_step_subproof0 _ prod _ (fun _ => Hv)).
+    intros EQnt. clear Hv Hgoto'.
+
+    change (ptl_sem ptl (prod_action prod))
+      with (pt_sem (Non_terminal_pt prod ptl)).
+    generalize (Non_terminal_pt prod ptl). clear ptl. destruct ptz.
+    + intros pt. f_equal. by rewrite cast_eq.
+    + edestruct Hgoto. eapply ptz_stack_compat_cons_state_has_future, Hstk0.
+Qed.
+
+Lemma step_next_ptd (ptd : pt_dot) (stk : stack) Hi :
+  ptd_stack_compat ptd stk ->
+  match next_ptd ptd with
+  | None =>
+    step safe init stk (ptd_buffer ptd) Hi =
+      Accept_sr (ptd_sem ptd) buffer_end
+  | Some ptd' =>
+    exists stk',
+      step safe init stk (ptd_buffer ptd) Hi =
+        Progress_sr stk' (ptd_buffer ptd') /\
+      ptd_stack_compat ptd' stk'
+  end.
+Proof.
+  intros Hstk. unfold step.
+  generalize (reduce_ok safe (state_of_stack init stk)).
+  destruct ptd as [prod word ptl ptz|tok symbs word ptl ptlz].
+  - assert (Hfut : state_has_future (state_of_stack init stk) prod []
+                                    (token_term (buf_head (ptz_buffer ptz)))).
+    { destruct Hstk as (? & ? & ?)=>//. }
+    assert (Hact := end_reduce _ _ _ _ Hfut).
+    destruct action_table as [?|awt]=>Hval /=.
+    + subst. by apply reduce_step_next_ptd.
+    + set (term := token_term (buf_head (ptz_buffer ptz))) in *.
+      generalize (Hval term). clear Hval. destruct (awt term)=>//. subst.
+      intros Hval. by apply reduce_step_next_ptd.
+  - destruct Hstk as (stk0 & Hfut & Hstk & Hstk0).
+    assert (Hact := terminal_shift _ _ _ _ Hfut). simpl in Hact. clear Hfut.
+    destruct action_table as [?|awt]=>//= /(_ (token_term tok)).
+    destruct awt as [st' EQ| |]=>// _. eexists. split.
+    + f_equal. rewrite -ptd_buffer_build_from_ptl //.
+    + apply (ptd_stack_compat_build_from_ptl _ _ _ stk0); simpl; eauto.
+Qed.
+
+(** We prove the completeness of the parser main loop. *)
+Lemma parse_fix_next_ptd_iter (ptd : pt_dot) (stk : stack) (log_n_steps : nat) Hi :
+  ptd_stack_compat ptd stk ->
+  match next_ptd_iter ptd log_n_steps with
+  | None =>
+    proj1_sig (parse_fix safe init stk (ptd_buffer ptd) log_n_steps Hi) =
+      Accept_sr (ptd_sem ptd) buffer_end
+  | Some ptd' =>
+    exists stk',
+      proj1_sig (parse_fix safe init stk (ptd_buffer ptd) log_n_steps Hi) =
+        Progress_sr stk' (ptd_buffer ptd') /\
+      ptd_stack_compat ptd' stk'
+  end.
+Proof.
+  revert ptd stk Hi.
+  induction log_n_steps as [|log_n_steps IH]; [by apply step_next_ptd|].
+  move => /= ptd stk Hi Hstk. assert (IH1 := IH ptd stk Hi Hstk).
+  assert (EQsem := sem_next_ptd_iter ptd log_n_steps).
+  destruct parse_fix as [sr Hi']. simpl in IH1.
+  destruct next_ptd_iter as [ptd'|].
+  - rewrite EQsem. destruct IH1 as (stk' & -> & Hstk'). by apply IH.
+  - by subst.
+Qed.
+
+(** The parser is defined by recursion over a fuel parameter. In the
+  completeness proof, we need to predict how much fuel is going to be
+  needed in order to prove that enough fuel gives rise to a successful
+  parsing.
+
+  To do so, of a dotted parse tree, which is the number of actions
+  left to be executed before complete parsing when the current state
+  is represented by the dotted parse tree. *)
+Fixpoint ptlz_cost {hole_symbs hole_word}
+         (ptlz:ptl_zipper hole_symbs hole_word) :=
+  match ptlz with
+  | Non_terminal_pt_ptlz ptz => ptz_cost ptz
+  | Cons_ptl_ptlz pt ptlz' => pt_size pt + ptlz_cost ptlz'
+  end
+with ptz_cost {hole_symb hole_word} (ptz:pt_zipper hole_symb hole_word) :=
+  match ptz with
+  | Top_ptz => 0
+  | Cons_ptl_ptz ptl ptlz' => 1 + ptlz_cost ptlz'
+  end.
+
+Definition ptd_cost (ptd:pt_dot) :=
+  match ptd with
+  | Reduce_ptd ptl ptz => ptz_cost ptz
+  | Shift_ptd _ ptl ptlz => 1 + ptlz_cost ptlz
+  end.
+
+Lemma ptd_cost_build_from_pt {symb word}
+      (pt : parse_tree symb word) (ptz : pt_zipper symb word) :
+  pt_size pt + ptz_cost ptz = S (ptd_cost (build_pt_dot_from_pt pt ptz))
+with ptd_cost_build_from_pt_rec {symbs word}
+     (ptl : parse_tree_list symbs word) (ptlz : ptl_zipper symbs word)
+     Hsymbs :
+  ptl_size ptl + ptlz_cost ptlz = ptd_cost (build_pt_dot_from_pt_rec ptl Hsymbs ptlz).
+Proof.
+  - destruct pt as [tok|prod word ptl']=>/=.
+    + revert ptz. generalize [tok]. generalize (token_sem tok). generalize I.
+      change True with (match T (token_term tok) with T _ => True | NT _ => False end) at 1.
+      generalize (T (token_term tok)) => symb HT sem word ptz. by destruct ptz.
+    + match goal with
+      | |- context [match ?X with Some H => _ | None => _ end] => destruct X eqn:EQ
+      end.
+      * rewrite -ptd_cost_build_from_pt_rec /= plus_n_Sm //.
+      * simpl. by destruct ptl'.
+  - destruct ptl as [|?? ptl ?? pt]; [contradiction|].
+    specialize (ptd_cost_build_from_pt_rec _ _ ptl). destruct ptl.
+    + apply eq_add_S. rewrite -ptd_cost_build_from_pt /=. ring.
+    + rewrite -ptd_cost_build_from_pt_rec //=. ring.
+Qed.
+
+Lemma ptd_cost_build_from_ptl {symbs word}
+      (ptl : parse_tree_list symbs word) (ptlz : ptl_zipper symbs word) :
+  ptlz_cost ptlz = ptd_cost (build_pt_dot_from_ptl ptl ptlz).
+Proof.
+  destruct ptlz=>//. apply eq_add_S. rewrite -ptd_cost_build_from_pt /=. ring.
+Qed.
+
+Lemma next_ptd_cost ptd:
+  match next_ptd ptd with
+  | None => ptd_cost ptd = 0
+  | Some ptd' => ptd_cost ptd = S (ptd_cost ptd')
+  end.
+Proof.
+  destruct ptd as [prod word ptl ptz|tok symbq wordq ptl ptlz] =>/=.
+  - generalize (Non_terminal_pt prod ptl). clear ptl.
+    destruct ptz as [|?? ptl ?? ptlz]=>// pt. by rewrite -ptd_cost_build_from_ptl.
+  - by rewrite -ptd_cost_build_from_ptl.
+Qed.
+
+Lemma next_ptd_iter_cost ptd log_n_steps :
+  match next_ptd_iter ptd log_n_steps with
+  | None => ptd_cost ptd < 2^log_n_steps
+  | Some ptd' => ptd_cost ptd = 2^log_n_steps + ptd_cost ptd'
+  end.
+Proof.
+  revert ptd. induction log_n_steps as [|log_n_steps IH]=>ptd /=.
+  - assert (Hptd := next_ptd_cost ptd). destruct next_ptd=>//. by rewrite Hptd.
+  - rewrite Nat.add_0_r. assert (IH1 := IH ptd). destruct next_ptd_iter as [ptd'|].
+    + specialize (IH ptd'). destruct next_ptd_iter as [ptd''|].
+      * by rewrite IH1 IH -!plus_assoc.
+      * rewrite IH1. by apply plus_lt_compat_l.
+    + by apply lt_plus_trans.
+Qed.
+
+(** We now prove the top-level parsing function. The only thing that
+  is left to be done is the initialization. To do so, we define the
+  initial dotted parse tree, depending on a full (top-level) parse tree. *)
+
+Variable full_pt : parse_tree (NT (start_nt init)) full_word.
+
+Theorem parse_complete log_n_steps:
+  match parse safe init (full_word ++ buffer_end) log_n_steps with
+  | Parsed_pr sem buff =>
+    sem = pt_sem full_pt /\ buff = buffer_end /\ pt_size full_pt <= 2^log_n_steps
+  | Timeout_pr => 2^log_n_steps < pt_size full_pt
+  | Fail_pr => False
+  end.
+Proof.
+  assert (Hstk : ptd_stack_compat (build_pt_dot_from_pt full_pt Top_ptz) []) by
+      by apply ptd_stack_compat_build_from_pt.
+  unfold parse.
+  assert (Hparse := parse_fix_next_ptd_iter _ _ log_n_steps (parse_subproof init) Hstk).
+  rewrite -ptd_buffer_build_from_pt -sem_build_from_pt /= in Hparse.
+  assert (Hcost := next_ptd_iter_cost (build_pt_dot_from_pt full_pt Top_ptz) log_n_steps).
+  destruct next_ptd_iter.
+  - destruct Hparse as (? & -> & ?). apply (f_equal S) in Hcost.
+    rewrite -ptd_cost_build_from_pt Nat.add_0_r in Hcost. rewrite Hcost.
+    apply le_lt_n_Sm, le_plus_l.
+  - rewrite Hparse. split; [|split]=>//. apply lt_le_S in Hcost.
+    by rewrite -ptd_cost_build_from_pt Nat.add_0_r in Hcost.
+Qed.
+
+End Completeness_Proof.
+
+End Make.
diff --git a/MenhirLib/Interpreter_correct.v b/MenhirLib/Interpreter_correct.v
new file mode 100644
index 00000000..1325f610
--- /dev/null
+++ b/MenhirLib/Interpreter_correct.v
@@ -0,0 +1,175 @@
+(****************************************************************************)
+(*                                                                          *)
+(*                                   Menhir                                 *)
+(*                                                                          *)
+(*           Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud         *)
+(*                                                                          *)
+(*  Copyright Inria. All rights reserved. This file is distributed under    *)
+(*  the terms of the GNU Lesser General Public License as published by the  *)
+(*  Free Software Foundation, either version 3 of the License, or (at your  *)
+(*  option) any later version, as described in the file LICENSE.            *)
+(*                                                                          *)
+(****************************************************************************)
+
+From Coq Require Import List Syntax.
+Require Import Alphabet.
+Require Grammar Automaton Interpreter.
+From Coq.ssr Require Import ssreflect.
+
+Module Make(Import A:Automaton.T) (Import Inter:Interpreter.T A).
+
+(** * Correctness of the interpreter **)
+
+(** We prove that, in any case, if the interpreter accepts returning a
+    semantic value, then this is a semantic value of the input **)
+
+Section Init.
+
+Variable init:initstate.
+
+(** [word_has_stack_semantics] relates a word with a stack, stating that the
+    word is a concatenation of words that have the semantic values stored in
+    the stack. **)
+Inductive word_has_stack_semantics:
+  forall (word:list token) (stack:stack), Prop :=
+  | Nil_stack_whss: word_has_stack_semantics [] []
+  | Cons_stack_whss:
+    forall (wordq:list token) (stackq:stack),
+      word_has_stack_semantics wordq stackq ->
+
+    forall (wordt:list token) (s:noninitstate)
+           (pt:parse_tree (last_symb_of_non_init_state s) wordt),
+
+    word_has_stack_semantics
+       (wordq++wordt) (existT noninitstate_type s (pt_sem pt)::stackq).
+
+(** [pop] preserves the invariant **)
+Lemma pop_spec_ptl A symbols_to_pop action word_stk stk (res : A) stk' :
+  pop_spec symbols_to_pop stk action stk' res ->
+  word_has_stack_semantics word_stk stk ->
+  exists word_stk' word_res (ptl:parse_tree_list symbols_to_pop word_res),
+    (word_stk' ++ word_res = word_stk)%list /\
+    word_has_stack_semantics word_stk' stk' /\
+    ptl_sem ptl action = res.
+Proof.
+  intros Hspec. revert word_stk.
+  induction Hspec as [stk sem|symbols_to_pop st stk action sem stk' res Hspec IH];
+    intros word_stk Hword_stk.
+  - exists word_stk, [], Nil_ptl. rewrite -app_nil_end. eauto.
+  - inversion Hword_stk. subst_existT.
+    edestruct IH as (word_stk' & word_res & ptl & ? & Hword_stk'' & ?); [eassumption|].
+    subst. eexists word_stk', (word_res ++ _)%list, (Cons_ptl ptl _).
+    split; [|split]=>//. rewrite app_assoc //.
+Qed.
+
+(** [reduce_step] preserves the invariant **)
+Lemma reduce_step_invariant (stk:stack) (prod:production) Hv Hi word buffer :
+  word_has_stack_semantics word stk ->
+  match reduce_step init stk prod buffer Hv Hi with
+  | Accept_sr sem buffer_new =>
+    exists pt : parse_tree (NT (start_nt init)) word,
+    buffer = buffer_new /\ pt_sem pt = sem
+  | Progress_sr stk' buffer_new =>
+    buffer = buffer_new /\ word_has_stack_semantics word stk'
+  | Fail_sr => True
+  end.
+Proof.
+  intros Hword_stk. unfold reduce_step.
+  match goal with
+  | |- context [pop_state_valid init ?stp stk ?x1 ?x2 ?x3 ?x4 ?x5] =>
+    generalize (pop_state_valid init stp stk x1 x2 x3 x4 x5)
+  end.
+  destruct pop as [stk' sem] eqn:Hpop=>/= Hv'.
+  apply pop_spec_ok in Hpop. apply pop_spec_ptl with (word_stk := word) in Hpop=>//.
+  destruct Hpop as (word1 & word2 & ptl & <- & Hword1 & <-).
+  generalize (reduce_step_subproof1 init stk prod Hv stk' (fun _ : True => Hv')).
+  destruct goto_table as [[st' EQ]|].
+  - intros _. split=>//.
+    change (ptl_sem ptl (prod_action prod)) with (pt_sem (Non_terminal_pt prod ptl)).
+    generalize (Non_terminal_pt prod ptl). rewrite ->EQ. intros pt. by constructor.
+  - intros Hstk'. destruct Hword1; [|by destruct Hstk'].
+    generalize (reduce_step_subproof0 init prod [] (fun _ : True => Hstk')).
+    simpl in Hstk'. rewrite -Hstk' // => EQ. rewrite cast_eq.
+    exists (Non_terminal_pt prod ptl). by split.
+Qed.
+
+(** [step] preserves the invariant **)
+Lemma step_invariant stk word buffer safe Hi :
+  word_has_stack_semantics word stk ->
+  match step safe init stk buffer Hi with
+  | Accept_sr sem buffer_new =>
+    exists word_new (pt:parse_tree (NT (start_nt init)) word_new),
+      (word ++ buffer = word_new ++ buffer_new)%buf /\
+      pt_sem pt = sem
+  | Progress_sr stk_new buffer_new =>
+    exists word_new,
+      (word ++ buffer = word_new ++ buffer_new)%buf /\
+      word_has_stack_semantics word_new stk_new
+  | Fail_sr => True
+  end.
+Proof.
+  intros Hword_stk. unfold step.
+  generalize (reduce_ok safe (state_of_stack init stk)).
+  destruct action_table as [prod|awt].
+  - intros Hv.
+    apply (reduce_step_invariant stk prod (fun _ => Hv) Hi word buffer) in Hword_stk.
+    destruct reduce_step=>//.
+    + destruct Hword_stk as (pt & <- & <-); eauto.
+    + destruct Hword_stk as [<- ?]; eauto.
+  - destruct buffer as [tok buffer]=>/=.
+    move=> /(_ (token_term tok)) Hv. destruct (awt (token_term tok)) as [st EQ|prod|]=>//.
+    + eexists _. split; [by apply app_buf_assoc with (l2 := [_])|].
+      change (token_sem tok) with (pt_sem (Terminal_pt tok)).
+      generalize (Terminal_pt tok). generalize [tok].
+      rewrite -> EQ=>word' pt /=. by constructor.
+    + apply (reduce_step_invariant stk prod (fun _ => Hv) Hi word (tok::buffer))
+        in Hword_stk.
+      destruct reduce_step=>//.
+      * destruct Hword_stk as (pt & <- & <-); eauto.
+      * destruct Hword_stk as [<- ?]; eauto.
+Qed.
+
+(** [step] preserves the invariant **)
+Lemma parse_fix_invariant stk word buffer safe log_n_steps Hi :
+  word_has_stack_semantics word stk ->
+  match proj1_sig (parse_fix safe init stk buffer log_n_steps Hi) with
+  | Accept_sr sem buffer_new =>
+    exists word_new (pt:parse_tree (NT (start_nt init)) word_new),
+      (word ++ buffer = word_new ++ buffer_new)%buf /\
+      pt_sem pt = sem
+  | Progress_sr stk_new buffer_new =>
+    exists word_new,
+      (word ++ buffer = word_new ++ buffer_new)%buf /\
+      word_has_stack_semantics word_new stk_new
+  | Fail_sr => True
+  end.
+Proof.
+  revert stk word buffer Hi.
+  induction log_n_steps as [|log_n_steps IH]=>/= stk word buffer Hi Hstk;
+    [by apply step_invariant|].
+  assert (IH1 := IH stk word buffer Hi Hstk).
+  destruct parse_fix as [[] Hi']=>/=; try by apply IH1.
+  destruct IH1 as (word' & -> & Hstk')=>//. by apply IH.
+Qed.
+
+(** The interpreter is correct : if it returns a semantic value, then the input
+    word has this semantic value.
+**)
+Theorem parse_correct safe buffer log_n_steps:
+  match parse safe init buffer log_n_steps with
+  | Parsed_pr sem buffer_new =>
+    exists word_new (pt:parse_tree (NT (start_nt init)) word_new),
+      buffer = (word_new ++ buffer_new)%buf /\
+      pt_sem pt = sem
+  | _ => True
+  end.
+Proof.
+  unfold parse.
+  assert (Hparse := parse_fix_invariant [] [] buffer safe log_n_steps
+                                        (parse_subproof init)).
+  destruct proj1_sig=>//. apply Hparse. constructor.
+Qed.
+
+End Init.
+
+End Make.
diff --git a/MenhirLib/Main.v b/MenhirLib/Main.v
new file mode 100644
index 00000000..f6158074
--- /dev/null
+++ b/MenhirLib/Main.v
@@ -0,0 +1,79 @@
+(****************************************************************************)
+(*                                                                          *)
+(*                                   Menhir                                 *)
+(*                                                                          *)
+(*           Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud         *)
+(*                                                                          *)
+(*  Copyright Inria. All rights reserved. This file is distributed under    *)
+(*  the terms of the GNU Lesser General Public License as published by the  *)
+(*  Free Software Foundation, either version 3 of the License, or (at your  *)
+(*  option) any later version, as described in the file LICENSE.            *)
+(*                                                                          *)
+(****************************************************************************)
+
+Require Grammar Automaton Interpreter_correct Interpreter_complete.
+From Coq Require Import Syntax Arith.
+
+Module Make(Export Aut:Automaton.T).
+Export Aut.Gram.
+Export Aut.GramDefs.
+
+Module Import Inter := Interpreter.Make Aut.
+Module Correct := Interpreter_correct.Make Aut Inter.
+Module Complete := Interpreter_complete.Make Aut Inter.
+
+Definition complete_validator:unit->bool := Complete.Valid.is_complete.
+Definition safe_validator:unit->bool := ValidSafe.is_safe.
+Definition parse (safe:safe_validator ()=true) init log_n_steps buffer :
+  parse_result (symbol_semantic_type (NT (start_nt init))):=
+  parse (ValidSafe.safe_is_validator safe) init buffer log_n_steps.
+
+(** Correction theorem. **)
+Theorem parse_correct
+  (safe:safe_validator ()= true) init log_n_steps buffer:
+  match parse safe init log_n_steps buffer with
+    | Parsed_pr sem buffer_new =>
+      exists word (pt : parse_tree (NT (start_nt init)) word),
+        buffer = (word ++ buffer_new)%buf /\
+        pt_sem pt = sem
+    | _ => True
+  end.
+Proof. apply Correct.parse_correct. Qed.
+
+(** Completeness theorem. **)
+Theorem parse_complete
+  (safe:safe_validator () = true) init log_n_steps word buffer_end:
+  complete_validator () = true ->
+  forall tree:parse_tree (NT (start_nt init)) word,
+  match parse safe init log_n_steps (word ++ buffer_end) with
+  | Fail_pr => False
+  | Parsed_pr sem_res buffer_end_res =>
+    sem_res = pt_sem tree /\ buffer_end_res = buffer_end /\
+    pt_size tree <= 2^log_n_steps
+  | Timeout_pr => 2^log_n_steps < pt_size tree
+  end.
+Proof.
+  intros. now apply Complete.parse_complete, Complete.Valid.complete_is_validator.
+Qed.
+
+(** Unambiguity theorem. **)
+Theorem unambiguity:
+  safe_validator () = true -> complete_validator () = true -> inhabited token ->
+  forall init word,
+  forall (tree1 tree2:parse_tree (NT (start_nt init)) word),
+    pt_sem tree1 = pt_sem tree2.
+Proof.
+  intros Hsafe Hcomp [tok] init word tree1 tree2.
+  pose (buf_end := cofix buf_end := (tok :: buf_end)%buf).
+  assert (Hcomp1 := parse_complete Hsafe init (pt_size tree1) word buf_end
+                                   Hcomp tree1).
+  assert (Hcomp2 := parse_complete Hsafe init (pt_size tree1) word buf_end
+                                   Hcomp tree2).
+  destruct parse.
+  - destruct Hcomp1.
+  - exfalso. eapply PeanoNat.Nat.lt_irrefl. etransitivity; [|apply Hcomp1].
+    eapply Nat.pow_gt_lin_r. constructor.
+  - destruct Hcomp1 as [-> _], Hcomp2 as [-> _]. reflexivity.
+Qed.
+
+End Make.
diff --git a/MenhirLib/Validator_classes.v b/MenhirLib/Validator_classes.v
new file mode 100644
index 00000000..c043cb73
--- /dev/null
+++ b/MenhirLib/Validator_classes.v
@@ -0,0 +1,74 @@
+(****************************************************************************)
+(*                                                                          *)
+(*                                   Menhir                                 *)
+(*                                                                          *)
+(*           Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud         *)
+(*                                                                          *)
+(*  Copyright Inria. All rights reserved. This file is distributed under    *)
+(*  the terms of the GNU Lesser General Public License as published by the  *)
+(*  Free Software Foundation, either version 3 of the License, or (at your  *)
+(*  option) any later version, as described in the file LICENSE.            *)
+(*                                                                          *)
+(****************************************************************************)
+
+From Coq Require Import List.
+From Coq.ssr Require Import ssreflect.
+Require Import Alphabet.
+
+Class IsValidator (P : Prop) (b : bool) :=
+  is_validator : b = true -> P.
+Hint Mode IsValidator + -.
+
+Instance is_validator_true : IsValidator True true.
+Proof. done. Qed.
+
+Instance is_validator_false : IsValidator False false.
+Proof. done. Qed.
+
+Instance is_validator_eq_true b :
+  IsValidator (b = true) b.
+Proof. done. Qed.
+
+Instance is_validator_and P1 b1 P2 b2 `{IsValidator P1 b1} `{IsValidator P2 b2}:
+  IsValidator (P1 /\ P2) (if b1 then b2 else false).
+Proof. split; destruct b1, b2; auto using is_validator. Qed.
+
+Instance is_validator_comparable_leibniz_eq A (C:Comparable A) (x y : A) :
+  ComparableLeibnizEq C ->
+  IsValidator (x = y) (compare_eqb x y).
+Proof. intros ??. by apply compare_eqb_iff. Qed.
+
+Instance is_validator_comparable_eq_impl A `(Comparable A) (x y : A) P b :
+  IsValidator P b ->
+  IsValidator (x = y -> P) (if compare_eqb x y then b else true).
+Proof.
+  intros Hval Val ->. rewrite /compare_eqb compare_refl in Val. auto.
+Qed.
+
+Lemma is_validator_forall_finite A P b `(Finite A) :
+  (forall (x : A), IsValidator (P x) (b x)) ->
+  IsValidator (forall (x : A), P x) (forallb b all_list).
+Proof.
+  move=> ? /forallb_forall.
+  auto using all_list_forall, is_validator, forallb_forall.
+Qed.
+(* We do not use an instance directly here, because we need somehow to
+   force Coq to instantiate b with a lambda. *)
+Hint Extern 2 (IsValidator (forall x : ?A, _) _) =>
+    eapply (is_validator_forall_finite _ _ (fun (x:A) => _))
+  : typeclass_instances.
+
+(* Hint for synthetizing pattern-matching. *)
+Hint Extern 2 (IsValidator (match ?u with _ => _ end) ?b0) =>
+    let b := fresh "b" in
+    unshelve notypeclasses refine (let b : bool := _ in _);
+      [destruct u; intros; shelve|];    (* Synthetize `match .. with` in the validator. *)
+    unify b b0;
+    unfold b; destruct u; clear b
+  : typeclass_instances.
+
+(* Hint for unfolding definitions. This is necessary because many
+  hints for IsValidator use [Hint Extern], which do not automatically
+  unfold identifiers. *)
+Hint Extern 100 (IsValidator ?X _) => unfold X
+  : typeclass_instances.
diff --git a/MenhirLib/Validator_complete.v b/MenhirLib/Validator_complete.v
new file mode 100644
index 00000000..ebb74500
--- /dev/null
+++ b/MenhirLib/Validator_complete.v
@@ -0,0 +1,394 @@
+(****************************************************************************)
+(*                                                                          *)
+(*                                   Menhir                                 *)
+(*                                                                          *)
+(*           Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud         *)
+(*                                                                          *)
+(*  Copyright Inria. All rights reserved. This file is distributed under    *)
+(*  the terms of the GNU Lesser General Public License as published by the  *)
+(*  Free Software Foundation, either version 3 of the License, or (at your  *)
+(*  option) any later version, as described in the file LICENSE.            *)
+(*                                                                          *)
+(****************************************************************************)
+
+From Coq Require Import List Syntax Derive.
+From Coq.ssr Require Import ssreflect.
+Require Automaton.
+Require Import Alphabet Validator_classes.
+
+Module Make(Import A:Automaton.T).
+
+(** We instantiate some sets/map. **)
+Module TerminalComparableM <: ComparableM.
+  Definition t := terminal.
+  Instance tComparable : Comparable t := _.
+End TerminalComparableM.
+Module TerminalOrderedType := OrderedType_from_ComparableM TerminalComparableM.
+Module StateProdPosComparableM <: ComparableM.
+  Definition t := (state*production*nat)%type.
+  Instance tComparable : Comparable t := _.
+End StateProdPosComparableM.
+Module StateProdPosOrderedType :=
+  OrderedType_from_ComparableM StateProdPosComparableM.
+
+Module TerminalSet := FSetAVL.Make TerminalOrderedType.
+Module StateProdPosMap := FMapAVL.Make StateProdPosOrderedType.
+
+(** Nullable predicate for symbols and list of symbols. **)
+Definition nullable_symb (symbol:symbol) :=
+  match symbol with
+  | NT nt => nullable_nterm nt
+  | _ => false
+  end.
+
+Definition nullable_word (word:list symbol) :=
+  forallb nullable_symb word.
+
+(** First predicate for non terminal, symbols and list of symbols, given as FSets. **)
+Definition first_nterm_set (nterm:nonterminal) :=
+  fold_left (fun acc t => TerminalSet.add t acc)
+    (first_nterm nterm) TerminalSet.empty.
+
+Definition first_symb_set (symbol:symbol) :=
+  match symbol with
+  | NT nt => first_nterm_set nt
+  | T t => TerminalSet.singleton t
+  end.
+
+Fixpoint first_word_set (word:list symbol) :=
+  match word with
+  | [] => TerminalSet.empty
+  | t::q =>
+    if nullable_symb t then
+      TerminalSet.union (first_symb_set t) (first_word_set q)
+    else
+      first_symb_set t
+  end.
+
+(** Small helper for finding the part of an item that is after the dot. **)
+Definition future_of_prod prod dot_pos : list symbol :=
+  (fix loop n lst :=
+    match n with
+    | O => lst
+    | S x => match loop x lst with [] => [] | _::q => q end
+    end)
+  dot_pos (rev' (prod_rhs_rev prod)).
+
+(** We build a fast map to store all the items of all the states. **)
+Definition items_map (_:unit): StateProdPosMap.t TerminalSet.t :=
+  fold_left (fun acc state =>
+    fold_left (fun acc item =>
+      let key := (state, prod_item item, dot_pos_item item) in
+        let data := fold_left (fun acc t => TerminalSet.add t acc)
+          (lookaheads_item item) TerminalSet.empty
+        in
+        let old :=
+          match StateProdPosMap.find key acc with
+          | Some x => x | None => TerminalSet.empty
+          end
+        in
+        StateProdPosMap.add key (TerminalSet.union data old) acc
+    ) (items_of_state state) acc
+  ) all_list (StateProdPosMap.empty TerminalSet.t).
+
+(** We need to avoid computing items_map each time we need it. To that
+  purpose, we declare a typeclass specifying that some map is equal to
+  items_map. *)
+Class IsItemsMap m := is_items_map : m = items_map ().
+
+(** Accessor. **)
+Definition find_items_map items_map state prod dot_pos : TerminalSet.t :=
+  match StateProdPosMap.find (state, prod, dot_pos) items_map with
+  | None => TerminalSet.empty
+  | Some x => x
+  end.
+
+Definition state_has_future state prod (fut:list symbol) (lookahead:terminal) :=
+  exists dot_pos:nat,
+    fut = future_of_prod prod dot_pos /\
+    TerminalSet.In lookahead (find_items_map (items_map ()) state prod dot_pos).
+
+(** Iterator over items. **)
+Definition forallb_items items_map (P:state -> production -> nat -> TerminalSet.t -> bool): bool:=
+  StateProdPosMap.fold (fun key set acc =>
+    match key with (st, p, pos) => (acc && P st p pos set)%bool end
+  ) items_map true.
+
+(** Typeclass instances for synthetizing the validator. *)
+
+Instance is_validator_subset S1 S2 :
+  IsValidator (TerminalSet.Subset S1 S2) (TerminalSet.subset S1 S2).
+Proof. intros ?. by apply TerminalSet.subset_2. Qed.
+
+(* While the specification of the validator always quantify over
+   possible lookahead tokens individually, the validator usually
+   handles lookahead sets directly instead, for better performances.
+
+   For instance, the validator for [state_has_future], which speaks
+   about one single lookahead token is a subset operation:
+*)
+Lemma is_validator_state_has_future_subset st prod pos lookahead lset im fut :
+  TerminalSet.In lookahead lset ->
+  fut = future_of_prod prod pos ->
+  IsItemsMap im ->
+  IsValidator (state_has_future st prod fut lookahead)
+              (TerminalSet.subset lset (find_items_map im st prod pos)).
+Proof.
+  intros ? -> -> HSS%TerminalSet.subset_2. exists pos. split=>//. by apply HSS.
+Qed.
+(* We do not declare this lemma as an instance, and use [Hint Extern]
+   instead, because the typeclass mechanism has trouble instantiating
+   some evars if we do not explicitely call [eassumption]. *)
+Hint Extern 2 (IsValidator (state_has_future _ _ _ _) _) =>
+  eapply is_validator_state_has_future_subset; [eassumption|eassumption || reflexivity|]
+: typeclass_instances.
+
+(* As said previously, we manipulate lookahead terminal sets instead of
+  lookahead individually. Hence, when we quantify over a lookahead set
+  in the specification, we do not do anything in the executable
+  validator.
+
+  This instance is used for [non_terminal_closed]. *)
+Instance is_validator_forall_lookahead_set lset P b:
+  (forall lookahead, TerminalSet.In lookahead lset -> IsValidator (P lookahead) b) ->
+  IsValidator (forall lookahead, TerminalSet.In lookahead lset -> P lookahead) b.
+Proof. unfold IsValidator. firstorder. Qed.
+
+
+(* Dually, we sometimes still need to explicitelly iterate over a
+  lookahead set. This is what this lemma allows.
+  Used only in [end_reduce]. *)
+Lemma is_validator_iterate_lset P b lookahead lset :
+  TerminalSet.In lookahead lset ->
+  IsValidator P (b lookahead) ->
+  IsValidator P (TerminalSet.fold (fun lookahead acc =>
+    if acc then b lookahead else false) lset true).
+Proof.
+  intros Hlset%TerminalSet.elements_1 Hval Val. apply Hval.
+  revert Val. rewrite TerminalSet.fold_1. generalize true at 1. clear -Hlset.
+  induction Hlset as [? l <-%compare_eq|? l ? IH]=> /= b' Val.
+  - destruct (b lookahead). by destruct b'. exfalso. by induction l; destruct b'.
+  - eauto.
+Qed.
+Hint Extern 100 (IsValidator _ _) =>
+  match goal with
+  | H : TerminalSet.In ?lookahead ?lset |- _ =>
+    eapply (is_validator_iterate_lset _ (fun lookahead => _) _ _ H); clear H
+  end
+: typeclass_instances.
+
+(* We often quantify over all the items of all the states of the
+   automaton. This lemma and the accompanying [Hint Resolve]
+   declaration allow generating the corresponding executable
+   validator.
+
+   Note that it turns out that, in all the uses of this pattern, the
+   first thing we do for each item is pattern-matching over the
+   future. This lemma also embbed this pattern-matching, which makes
+   it possible to get the hypothesis [fut' = future_of_prod prod (S pos)]
+   in the non-nil branch.
+
+   Moreover, note, again, that while the specification quantifies over
+   lookahead terminals individually, the code provides lookahead sets
+   instead. *)
+Lemma is_validator_forall_items P1 b1 P2 b2 im :
+  IsItemsMap im ->
+
+  (forall st prod lookahead lset pos,
+      TerminalSet.In lookahead lset ->
+      [] = future_of_prod prod pos ->
+      IsValidator (P1 st prod lookahead) (b1 st prod pos lset)) ->
+
+  (forall st prod pos lookahead lset s fut',
+      TerminalSet.In lookahead lset ->
+      fut' = future_of_prod prod (S pos) ->
+      IsValidator (P2 st prod lookahead s fut') (b2 st prod pos lset s fut')) ->
+
+  IsValidator (forall st prod fut lookahead,
+                  state_has_future st prod fut lookahead ->
+                  match fut with
+                  | [] => P1 st prod lookahead
+                  | s :: fut' => P2 st prod lookahead s fut'
+                  end)
+              (forallb_items im (fun st prod pos lset =>
+                 match future_of_prod prod pos with
+                 | [] => b1 st prod pos lset
+                 | s :: fut' => b2 st prod pos lset s fut'
+                 end)).
+Proof.
+  intros -> Hval1 Hval2 Val st prod fut lookahead (pos & -> & Hlookahead).
+  rewrite /forallb_items StateProdPosMap.fold_1 in Val.
+  assert (match future_of_prod prod pos with
+          | [] => b1 st prod pos (find_items_map (items_map ()) st prod pos)
+          | s :: fut' => b2 st prod pos (find_items_map (items_map ()) st prod pos) s fut'
+          end = true).
+  - unfold find_items_map in *.
+    assert (Hfind := @StateProdPosMap.find_2 _ (items_map ()) (st, prod, pos)).
+    destruct StateProdPosMap.find as [lset|]; [|by edestruct (TerminalSet.empty_1); eauto].
+    specialize (Hfind _ eq_refl). apply StateProdPosMap.elements_1 in Hfind.
+    revert Val. generalize true at 1.
+    induction Hfind as [[? ?] l [?%compare_eq ?]|??? IH]=>?.
+    + simpl in *; subst.
+      match goal with |- _ -> ?X = true => destruct X end; [done|].
+      rewrite Bool.andb_false_r. clear. induction l as [|[[[??]?]?] l IH]=>//.
+    + apply IH.
+  - destruct future_of_prod eqn:EQ. by eapply Hval1; eauto.
+    eapply Hval2 with (pos := pos); eauto; [].
+    revert EQ. unfold future_of_prod=>-> //.
+Qed.
+(* We need a hint for expplicitely instantiating b1 and b2 with lambdas. *)
+Hint Extern 0 (IsValidator
+                 (forall st prod fut lookahead,
+                     state_has_future st prod fut lookahead -> _)
+                 _) =>
+    eapply (is_validator_forall_items _ (fun st prod pos lset => _)
+                                      _ (fun st prod pos lset s fut' => _))
+  : typeclass_instances.
+
+(* Used in [start_future] only. *)
+Instance is_validator_forall_state_has_future im st prod :
+  IsItemsMap im ->
+  IsValidator
+    (forall look, state_has_future st prod (rev' (prod_rhs_rev prod)) look)
+    (let lookaheads := find_items_map im st prod 0 in
+     forallb (fun t => TerminalSet.mem t lookaheads) all_list).
+Proof.
+  move=> -> /forallb_forall Val look.
+  specialize (Val look (all_list_forall _)). exists 0. split=>//.
+  by apply TerminalSet.mem_2.
+Qed.
+
+(** * Validation for completeness **)
+
+(** The nullable predicate is a fixpoint : it is correct. **)
+Definition nullable_stable :=
+  forall p:production,
+    if nullable_word (prod_rhs_rev p) then
+      nullable_nterm (prod_lhs p) = true
+    else True.
+
+(** The first predicate is a fixpoint : it is correct. **)
+Definition first_stable:=
+  forall (p:production),
+    TerminalSet.Subset (first_word_set (rev' (prod_rhs_rev p)))
+                       (first_nterm_set (prod_lhs p)).
+
+(** The initial state has all the S=>.u items, where S is the start non-terminal **)
+Definition start_future :=
+  forall (init:initstate) (p:production),
+    prod_lhs p = start_nt init ->
+  forall (t:terminal),
+    state_has_future init p (rev' (prod_rhs_rev p)) t.
+
+(** If a state contains an item of the form A->_.av[[b]], where a is a
+    terminal, then reading an a does a [Shift_act], to a state containing
+    an item of the form A->_.v[[b]]. **)
+Definition terminal_shift :=
+  forall (s1:state) prod fut lookahead,
+    state_has_future s1 prod fut lookahead ->
+    match fut with
+    | T t::q =>
+      match action_table s1 with
+      | Lookahead_act awp =>
+        match awp t with
+        | Shift_act s2 _ =>
+          state_has_future s2 prod q lookahead
+        | _ => False
+        end
+      | _ => False
+      end
+    | _ => True
+    end.
+
+(** If a state contains an item of the form A->_.[[a]], then either we do a
+    [Default_reduce_act] of the corresponding production, either a is a
+    terminal (ie. there is a lookahead terminal), and reading a does a
+    [Reduce_act] of the corresponding production. **)
+Definition end_reduce :=
+  forall (s:state) prod fut lookahead,
+    state_has_future s prod fut lookahead ->
+    match fut with
+    | [] =>
+      match action_table s with
+      | Default_reduce_act p => p = prod
+      | Lookahead_act awt =>
+        match awt lookahead with
+        | Reduce_act p => p = prod
+        | _ => False
+        end
+      end
+    | _ => True
+    end.
+
+Definition is_end_reduce items_map :=
+  forallb_items items_map (fun s prod pos lset =>
+    match future_of_prod prod pos with
+    | [] =>
+      match action_table s with
+      | Default_reduce_act p => compare_eqb p prod
+      | Lookahead_act awt =>
+        TerminalSet.fold (fun lookahead acc =>
+          match awt lookahead with
+          | Reduce_act p => (acc && compare_eqb p prod)%bool
+          | _ => false
+          end) lset true
+      end
+    | _ => true
+    end).
+
+(** If a state contains an item of the form A->_.Bv[[b]], where B is a
+    non terminal, then the goto table says we have to go to a state containing
+    an item of the form A->_.v[[b]]. **)
+Definition non_terminal_goto :=
+  forall (s1:state) prod fut lookahead,
+    state_has_future s1 prod fut lookahead ->
+    match fut with
+    | NT nt::q =>
+      match goto_table s1 nt with
+      | Some (exist _ s2 _) =>
+        state_has_future s2 prod q lookahead
+      | None => False
+      end
+    | _ => True
+    end.
+
+Definition start_goto :=
+  forall (init:initstate),
+    match goto_table init (start_nt init) with
+    | None => True
+    | Some _ => False
+    end.
+
+(** Closure property of item sets : if a state contains an item of the form
+    A->_.Bv[[b]], then for each production B->u and each terminal a of
+    first(vb), the state contains an item of the form B->_.u[[a]] **)
+Definition non_terminal_closed :=
+  forall s1 prod fut lookahead,
+    state_has_future s1 prod fut lookahead ->
+    match fut with
+    | NT nt::q =>
+      forall p, prod_lhs p = nt ->
+        (if nullable_word q then
+           state_has_future s1 p (future_of_prod p 0) lookahead
+         else True) /\
+        (forall lookahead2,
+           TerminalSet.In lookahead2 (first_word_set q) ->
+             state_has_future s1 p (future_of_prod p 0) lookahead2)
+      | _ => True
+    end.
+
+(** The automaton is complete **)
+Definition complete :=
+  nullable_stable /\ first_stable /\ start_future /\ terminal_shift
+  /\ end_reduce /\ non_terminal_goto /\ start_goto /\ non_terminal_closed.
+
+Derive is_complete_0
+SuchThat (forall im, IsItemsMap im -> IsValidator complete (is_complete_0 im))
+As complete_0_is_validator.
+Proof. intros im. subst is_complete_0. instantiate (1:=fun im => _). apply _. Qed.
+
+Definition is_complete (_:unit) := is_complete_0 (items_map ()).
+Lemma complete_is_validator : IsValidator complete (is_complete ()).
+Proof. by apply complete_0_is_validator. Qed.
+
+End Make.
diff --git a/MenhirLib/Validator_safe.v b/MenhirLib/Validator_safe.v
new file mode 100644
index 00000000..2d2ea4b3
--- /dev/null
+++ b/MenhirLib/Validator_safe.v
@@ -0,0 +1,234 @@
+(****************************************************************************)
+(*                                                                          *)
+(*                                   Menhir                                 *)
+(*                                                                          *)
+(*           Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud         *)
+(*                                                                          *)
+(*  Copyright Inria. All rights reserved. This file is distributed under    *)
+(*  the terms of the GNU Lesser General Public License as published by the  *)
+(*  Free Software Foundation, either version 3 of the License, or (at your  *)
+(*  option) any later version, as described in the file LICENSE.            *)
+(*                                                                          *)
+(****************************************************************************)
+
+From Coq Require Import List Syntax Derive.
+From Coq.ssr Require Import ssreflect.
+Require Automaton.
+Require Import Alphabet Validator_classes.
+
+Module Make(Import A:Automaton.T).
+
+(** The singleton predicate for states **)
+Definition singleton_state_pred (state:state) :=
+  (fun state' => match compare state state' with Eq => true |_ => false end).
+
+(** [past_state_of_non_init_state], extended for all states. **)
+Definition past_state_of_state (state:state) :=
+  match state with
+  | Init _ => []
+  | Ninit nis => past_state_of_non_init_state nis
+  end.
+
+(** Concatenations of last and past **)
+Definition head_symbs_of_state (state:state) :=
+  match state with
+  | Init _ => []
+  | Ninit s =>
+    last_symb_of_non_init_state s::past_symb_of_non_init_state s
+  end.
+Definition head_states_of_state (state:state) :=
+  singleton_state_pred state::past_state_of_state state.
+
+(** * Validation for correctness **)
+
+(** Prefix predicate between two lists of symbols. **)
+Inductive prefix: list symbol -> list symbol -> Prop :=
+| prefix_nil: forall l, prefix [] l
+| prefix_cons: forall l1 l2 x, prefix l1 l2 -> prefix (x::l1) (x::l2).
+
+(** [prefix] is transitive **)
+Lemma prefix_trans:
+  forall (l1 l2 l3:list symbol), prefix l1 l2 -> prefix l2 l3 -> prefix l1 l3.
+Proof.
+  intros l1 l2 l3 H1 H2. revert l3 H2.
+  induction H1; [now constructor|]. inversion 1. subst. constructor. eauto.
+Qed.
+
+Fixpoint is_prefix (l1 l2:list symbol) :=
+  match l1, l2 with
+  | [], _ => true
+  | t1::q1, t2::q2 => (compare_eqb t1 t2 && is_prefix q1 q2)%bool
+  | _::_, [] => false
+  end.
+
+Instance prefix_is_validator l1 l2 : IsValidator (prefix l1 l2) (is_prefix l1 l2).
+Proof.
+  revert l2. induction l1 as [|x1 l1 IH]=>l2 Hpref.
+  - constructor.
+  - destruct l2 as [|x2 l2]=>//.
+    move: Hpref=> /andb_prop [/compare_eqb_iff -> /IH ?]. by constructor.
+Qed.
+
+(** If we shift, then the known top symbols of the destination state is
+    a prefix of the known top symbols of the source state, with the new
+    symbol added. **)
+Definition shift_head_symbs :=
+  forall s,
+    match action_table s with
+    | Lookahead_act awp => forall t,
+        match awp t with
+        | Shift_act s2 _ =>
+          prefix (past_symb_of_non_init_state s2) (head_symbs_of_state s)
+        | _ => True
+        end
+    | _ => True
+    end.
+
+(** When a goto happens, then the known top symbols of the destination state
+    is a prefix of the known top symbols of the source state, with the new
+    symbol added. **)
+Definition goto_head_symbs :=
+  forall s nt,
+    match goto_table s nt with
+    | Some (exist _ s2 _) =>
+      prefix (past_symb_of_non_init_state s2) (head_symbs_of_state s)
+    | None => True
+    end.
+
+(** We have to say the same kind of checks for the assumptions about the
+    states stack. However, theses assumptions are predicates. So we define
+    a notion of "prefix" over predicates lists, that means, basically, that
+    an assumption entails another **)
+Inductive prefix_pred: list (state->bool) -> list (state->bool) -> Prop :=
+  | prefix_pred_nil: forall l, prefix_pred [] l
+  | prefix_pred_cons: forall l1 l2 f1 f2,
+     (forall x, implb (f2 x) (f1 x) = true) ->
+     prefix_pred l1 l2 -> prefix_pred (f1::l1) (f2::l2).
+
+(** [prefix_pred] is transitive **)
+Lemma prefix_pred_trans:
+  forall (l1 l2 l3:list (state->bool)),
+  prefix_pred l1 l2 -> prefix_pred l2 l3 -> prefix_pred l1 l3.
+Proof.
+  intros l1 l2 l3 H1 H2. revert l3 H2.
+  induction H1 as [|l1 l2 f1 f2 Hf2f1]; [now constructor|].
+  intros l3. inversion 1 as [|??? f3 Hf3f2]. subst. constructor; [|now eauto].
+  intros x. specialize (Hf3f2 x). specialize (Hf2f1 x).
+  repeat destruct (_ x); auto.
+Qed.
+
+Fixpoint is_prefix_pred (l1 l2:list (state->bool)) :=
+  match l1, l2 with
+  | [], _ => true
+  | f1::q1, f2::q2 =>
+    (forallb (fun x => implb (f2 x) (f1 x)) all_list
+      && is_prefix_pred q1 q2)%bool
+  | _::_, [] => false
+  end.
+
+Instance prefix_pred_is_validator l1 l2 :
+  IsValidator (prefix_pred l1 l2) (is_prefix_pred l1 l2).
+Proof.
+  revert l2. induction l1 as [|x1 l1 IH]=>l2 Hpref.
+  - constructor.
+  - destruct l2 as [|x2 l2]=>//.
+    move: Hpref=> /andb_prop [/forallb_forall ? /IH ?].
+    constructor; auto using all_list_forall.
+Qed.
+
+(** The assumptions about state stack is conserved when we shift **)
+Definition shift_past_state :=
+  forall s,
+    match action_table s with
+    | Lookahead_act awp => forall t,
+        match awp t with
+        | Shift_act s2 _ =>
+          prefix_pred (past_state_of_non_init_state s2)
+                      (head_states_of_state s)
+        | _ => True
+        end
+    | _ => True
+    end.
+
+(** The assumptions about state stack is conserved when we do a goto **)
+Definition goto_past_state :=
+  forall s nt,
+    match goto_table s nt with
+    | Some (exist _ s2 _) =>
+      prefix_pred (past_state_of_non_init_state s2)
+                  (head_states_of_state s)
+    | None => True
+    end.
+
+(** What states are possible after having popped these symbols from the
+    stack, given the annotation of the current state ? **)
+Inductive state_valid_after_pop (s:state):
+  list symbol -> list (state -> bool) -> Prop :=
+  | state_valid_after_pop_nil1:
+    forall p pl, p s = true -> state_valid_after_pop s [] (p::pl)
+  | state_valid_after_pop_nil2:
+    forall sl, state_valid_after_pop s sl []
+  | state_valid_after_pop_cons:
+    forall st sq p pl, state_valid_after_pop s sq pl ->
+      state_valid_after_pop s (st::sq) (p::pl).
+
+Fixpoint is_state_valid_after_pop (state:state) (to_pop:list symbol) annot :=
+  match annot, to_pop with
+  | [], _ => true
+  | p::_, [] => p state
+  | p::pl, s::sl => is_state_valid_after_pop state sl pl
+  end.
+
+Instance impl_is_state_valid_after_pop_is_validator state sl pl P b :
+  IsValidator P b ->
+  IsValidator (state_valid_after_pop state sl pl -> P)
+              (if is_state_valid_after_pop state sl pl then b else true).
+Proof.
+  destruct (is_state_valid_after_pop state0 sl pl) eqn:EQ.
+  - intros ??. auto using is_validator.
+  - intros _ _ Hsvap. exfalso. induction Hsvap=>//; [simpl in EQ; congruence|].
+    by destruct sl.
+Qed.
+
+(** A state is valid for reducing a production when :
+      - The assumptions on the state are such that we will find the right hand
+        side of the production on the stack.
+      - We will be able to do a goto after having popped the right hand side.
+**)
+Definition valid_for_reduce (state:state) prod :=
+    prefix (prod_rhs_rev prod) (head_symbs_of_state state) /\
+    forall state_new,
+    state_valid_after_pop state_new
+      (prod_rhs_rev prod) (head_states_of_state state) ->
+    match goto_table state_new (prod_lhs prod) with
+    | None =>
+      match state_new with
+      | Init i => prod_lhs prod = start_nt i
+      | Ninit _ => False
+      end
+    | _ => True
+    end.
+
+(** All the states that does a reduce are valid for reduction **)
+Definition reduce_ok :=
+  forall s,
+    match action_table s with
+    | Lookahead_act awp =>
+      forall t, match awp t with
+                | Reduce_act p => valid_for_reduce s p
+                | _ => True
+                end
+    | Default_reduce_act p => valid_for_reduce s p
+    end.
+
+(** The automaton is safe **)
+Definition safe :=
+  shift_head_symbs /\ goto_head_symbs /\ shift_past_state /\
+  goto_past_state /\ reduce_ok.
+
+Derive is_safe
+SuchThat (IsValidator safe (is_safe ()))
+As safe_is_validator.
+Proof. subst is_safe. instantiate (1:=fun _ => _). apply _. Qed.
+
+End Make.