proposition: Lemma length_helper {n' m' table} (Hlen : m' = 0 \/ n' + m' <= length str) : match List.nth n' table None with | Some idx => idx | None => m' end = match List.nth n' table None with | Some idx => idx | None => length (substring n' m' str) end.
proof: Proof. destruct (List.nth n' table None); try reflexivity. rewrite substring_length. destruct Hlen; subst; simpl; apply Nat.min_case_strong; omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.ZArith.ZArith Fiat.Computation.Refinements.General Fiat.Common Fiat.Common.Equality Fiat.Common.List.Operations Fiat.Computation.Refinements.General Fiat.Parsers.Reachable.ParenBalanced.Core Fiat.Parsers.Reachable.ParenBalancedHiding.Core Fiat.Parsers.Refinement.DisjointRulesCommon Fiat.Parsers.Refinement.BinOpBrackets.ParenBalanced Fiat.Parsers.Refinement.BinOpBrackets.MakeBinOpTable Fiat.Parsers.Refinement.BinOpBrackets.ParenBalancedLemmas Fiat.Parsers.Refinement.BinOpBrackets.ParenBalancedGrammar Fiat.Parsers.Refinement.PossibleTerminalsSets Fiat.Parsers.ParserInterface Fiat.Parsers.BaseTypes Fiat.Parsers.ContextFreeGrammar.Valid Fiat.Parsers.ContextFreeGrammar.ValidProperties Fiat.Parsers.ContextFreeGrammar.ValidReflective Fiat.Parsers.Splitters.RDPList Fiat.Parsers.Reachable.ParenBalanced.Core Fiat.Parsers.Refinement.PreTactics Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Parsers.Refinement.DisjointLemmas