proposition: Lemma dec_in_helper {ls it its offset len0_minus_len} (Hlen : (len0 - len0_minus_len) = 0 \/ offset + (len0 - len0_minus_len) <= length str) : iffT {n0 : nat & (In (min (length (substring offset (len0 - len0_minus_len) str)) n0) (map (min (length (substring offset (len0 - len0_minus_len) str))) ls) * minimal_parse_of_item (G := G) len0 valid (take n0 (substring offset (len0 - len0_minus_len) str)) it * minimal_parse_of_production (G := G) len0 valid (drop n0 (substring offset (len0 - len0_minus_len) str)) its)%type} {n0 : nat & (In n0 ls * (minimal_parse_of_item (G := G) len0 valid (substring offset (len0 - max (len0 - n0) len0_minus_len) str) it * minimal_parse_of_production (G := G) len0 valid (substring (offset + n0) (len0 - (len0_minus_len + n0)) str) its))%type}.
proof: Proof. rewrite Hlen_helper by assumption. split; first [ intros [n [[H0 H1] H2]] | intros [n [H0 [H1 H2]]] ]. { destruct (le_lt_dec (len0 - len0_minus_len) n) as [pf|pf]. { rewrite Nat.min_l in H0 by assumption. clear -H0 H1 H2 rdata cdata pf HSLP. induction ls as [|x xs IHxs]; destruct_head_hnf False. destruct (le_lt_dec (len0 - len0_minus_len) x). { exists x. repeat split. { left; reflexivity. } { eapply expand_minimal_parse_of_item_beq; [ .. | eassumption ]. rewrite take_take, <- Nat.sub_min_distr_l. rewrite !Nat.min_r by omega. reflexivity. } { eapply expand_minimal_parse_of_production_beq; [ .. | eassumption ]. rewrite drop_take, StringLike.drop_drop. rewrite Nat.sub_add_distr. apply bool_eq_empty; rewrite substring_length; apply Nat.min_case_strong; generalize dependent (len0 - len0_minus_len); intros; omega. } } { simpl in *. rewrite Nat.min_r in H0 by omega. destruct IHxs as [n' [IH0 [IH1 IH2]]]. { destruct H0; try omega; assumption. } { exists n'; repeat split; try assumption. right; assumption. } } } { exists n; repeat split; try assumption. { apply in_map_iff in H0. repeat match goal with | _ => progress destruct_head ex | _ => progress destruct_head and | [ H : context[min ?x ?y] |- _ ] => rewrite (Nat.min_r x y) in H by omega | _ => progress subst | [ H : min ?x ?y < ?x |- _ ] => revert H; apply (Nat.min_case_strong x y) | _ => intro | _ => omega | _ => assumption end. } { eapply expand_minimal_parse_of_item_beq; [ .. | eassumption ]. rewrite take_take. rewrite <- Nat.sub_min_distr_l, sub_twice. rewrite (Nat.min_r len0) by omega. reflexivity. } { eapply expand_minimal_parse_of_production_beq; [ .. | eassumption ]. rewrite drop_take, StringLike.drop_drop. rewrite (Nat.add_comm offset), Nat.sub_add_distr; reflexivity. } } } { exists n; repeat split; try assumption. { apply in_map; assumption. } { eapply expand_minimal_parse_of_item_beq; [ .. | eassumption ]. rewrite take_take. rewrite <- Nat.sub_min_distr_l, sub_twice. rewrite (Nat.min_comm len0), <- !Nat.min_assoc, (Nat.min_r len0) by omega. reflexivity. } { eapply expand_minimal_parse_of_production_beq; [ .. | eassumption ]. rewrite drop_take, StringLike.drop_drop. rewrite (Nat.add_comm offset), Nat.sub_add_distr. reflexivity. } } Defined.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Arith.EqNat Coq.Arith.Compare_dec Coq.Arith.Wf_nat Coq.ZArith.ZArith Fiat.Common.List.Operations Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BaseTypes Fiat.Parsers.GenericBaseTypes Fiat.Parsers.GenericCorrectnessBaseTypes Fiat.Parsers.StringLike.Properties Fiat.Parsers.MinimalParse Fiat.Parsers.CorrectnessBaseTypes Fiat.Parsers.BaseTypesLemmas Fiat.Parsers.ContextFreeGrammar.Properties Fiat.Parsers.WellFoundedParse Fiat.Parsers.MinimalParseOfParse Fiat.Parsers.GenericRecognizer Fiat.Parsers.GenericRecognizerExt Fiat.Common.Wf Fiat.Common.Wf1 Fiat.Common.List.ListFacts Fiat.Common.NatFacts Fiat.Common.UIP Fiat.Common