proposition: Lemma has_only_terminals_length {its str} (H0 : @has_only_terminals _ its) (H1 : parse_of_production G str its) : length str = List.length its.
proof: Proof. induction H1 as [ | ? ? ? ? pit pits IH ]; simpl in *; trivial. rewrite drop_length in IH. dependent destruction pit. { match goal with | [ H : context[(_ ~= [ _ ])%string_like] |- _ ] => apply length_singleton in H end. rewrite <- IH by assumption; clear IH. repeat match goal with | _ => intro | [ H : context[length (take _ _)] |- _ ] => rewrite take_length in H | [ H : context[length (drop _ _)] |- _ ] => rewrite drop_length in H | [ H : min ?x ?y = 1 |- _ ] => is_var x; destruct x | [ H : min (S ?x) ?y = 1 |- _ ] => is_var x; destruct x | [ H : min (S (S ?x)) ?y = 1 |- _ ] => revert H; apply (Nat.min_case_strong (S (S x)) y) | [ H : context[min _ 0] |- _ ] => rewrite Nat.min_0_r in H | [ H : context[min 0 _] |- _ ] => rewrite Nat.min_0_l in H | [ H : 0 = 1 |- _ ] => exfalso; clear -H; discriminate | [ H : S (S _) = 1 |- _ ] => exfalso; clear -H; discriminate | [ H : ?x = 1, H' : context[?x] |- _ ] => rewrite H in H' | [ H : ?x = 1 |- context[?x] ] => rewrite H | [ H : min ?x ?y = 1 |- _ ] => revert H; apply (Nat.min_case_strong x y) | _ => omega end. } { exfalso. unfold is_true in *. discriminate. } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Arith.PeanoNat Coq.Lists.List Fiat.Parsers.BaseTypes Fiat.Parsers.Splitters.RDPList Fiat.Parsers.ParserInterface Fiat.Parsers.ParserADTSpecification Fiat.Parsers.ContextFreeGrammar.Equality Fiat.Parsers.ContextFreeGrammar.Properties Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ContextFreeGrammar.Precompute Fiat.Parsers.Refinement.FixedLengthLemmas Fiat.ADTNotation.BuildADT Fiat.ADTNotation.BuildADTSig Fiat.ADT.ComputationalADT Fiat.ADTRefinement Fiat.ADTRefinement.BuildADTRefinements.HoneRepresentation Fiat.ADTRefinement.GeneralBuildADTRefinements Fiat.Common Fiat.Common.Equality Fiat.Common.StringBound Fiat.Common.ilist Fiat.Common.IterateBoundedIndex Fiat.Common.List.FlattenList Fiat.Common.List.ListMorphisms Fiat.Common.List.ListFacts Fiat.Common.NatFacts Fiat.Common.StringFacts Fiat.Common.LogicFacts Fiat.Common.LogicMorphisms Fiat.Computation.SetoidMorphisms Fiat.Common.List.ListMorphisms Fiat.Common.Instances Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Common Fiat.Common.Enumerable Fiat.Common.Enumerable.BoolProp Fiat.Common.Enumerable.ReflectiveForall Fiat.Common.Enumerable.ReflectiveForallStaged