proposition: Lemma paren_balanced_hiding'_prefix__index_points_to_binop (str : StringLike.String) (n idx len : nat) (H_hiding : paren_balanced_hiding' (take len (drop n str)) 0) (H_points_to : index_points_to_binop n idx str) (H_pre_hiding : paren_balanced' (take idx (drop n str)) 0) (H_small : idx < min len (StringLike.length (drop n str))) : False.
proof: Proof. unfold index_points_to_binop in *. repeat match goal with | [ H : context[StringLike.get ?n ?str] |- _ ] => not constr_eq n 0; let H' := fresh in revert H; case_eq (StringLike.get n str); rewrite get_drop; intros | _ => progress destruct_head ex | _ => progress split_and | [ H : StringLike.get 0 _ = Some _ |- _ ] => apply get_0 in H | [ H : forall x, Some _ = Some x -> _ |- _ ] => specialize (H _ eq_refl) | [ H : ?idx < _, H' : context[drop (?n + ?idx) _] |- _ ] => replace (n + idx) with (idx + n) in H' by omega | [ H : ?idx < _, H' : context[drop (?idx + _) _] |- _ ] => rewrite <- drop_drop in H' | [ H : _ |- _ ] => progress rewrite ?take_length, ?drop_length in H | [ H : context[take _ (drop _ (take _ _))] |- _ ] => rewrite drop_take in H | [ H : is_true (take _ (take _ _) ~= [ _ ]) |- _ ] => rewrite take_take in H | [ H : is_true (_ ~= [ _ ]) |- _ ] => progress apply take_n_1_singleton in H | [ H : FirstChar.for_first_char _ _, H' : _ < _, H'' : _ < _ |- _ ] => apply FirstChar.for_first_char_exists in H; [ | rewrite !drop_length; clear -H' H''; omega ] | [ H : _ < min _ _ |- _ ] => apply Nat.min_glb_lt_iff in H end. eapply (paren_balanced_hiding'_prefix); [ exact H_hiding | exact H_pre_hiding | eassumption | eassumption | assumption ]. 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