proposition: Lemma rdp_list_production_tl_correct : forall p, rdp_list_to_production (rdp_list_production_tl p) = tl (rdp_list_to_production p).
proof: Proof. unfold rdp_list_to_production, rdp_list_production_tl, default_production_tl, default_to_production; simpl. intros [? [? p]]; rewrite tl_drop; simpl. do 2 try match goal with | [ |- context[match ?e with _ => _ end] ] => destruct e eqn:?; simpl end; repeat match goal with | _ => destruct p; reflexivity | _ => assumption | _ => omega | [ H : leb _ _ = false |- _ ] => apply leb_iff_conv in H | [ H : ?x < 1 |- _ ] => assert (x = 0) by omega; clear H | [ H : ?x = 0 |- context[?x] ] => rewrite H | [ H : ?x = nil |- context[?x] ] => rewrite H | [ H : List.length ?x = 0 |- _ ] => assert (x = nil) by (destruct x; simpl in *; trivial; discriminate); clear H | _ => progress simpl in * | _ => reflexivity | [ H : _ < S _ |- _ ] => apply le_S_n in H | _ => rewrite drop_all by assumption | [ |- nil = drop _ _ ] => symmetry; apply drop_all | [ |- context[List.length (tl ?x)] ] => destruct x eqn:? end. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.ZArith.ZArith Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.BaseTypes Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Common Fiat.Common.Equality Fiat.Common.List.Operations Fiat.Common.List.ListFacts