proposition: Lemma refine_binop_table' (H_nt_hiding : forall str', parse_of_item G str' (NonTerminal nt) -> paren_balanced_hiding str') : retT table.
proof: Proof. intros ls H. computes_to_inv; subst. apply PickComputes. specialize (Htable n). hnf; cbv zeta. intros Hlen it' its' Heq idx' Hsmall Hreachable pit pits; simpl. rewrite length_helper by assumption. inversion Heq; subst it' its'; clear Heq. specialize (H_nt_hiding _ pit). unfold paren_balanced_hiding in *. set (s_str := (substring n m str) : @StringLike.String _ HSLM) in *. destruct (Compare_dec.zerop (StringLike.length (drop idx' s_str))) as [iszero|isnonzero]. { rewrite drop_length in iszero. assert (lenequal : idx' = StringLike.length s_str) by omega. subst. destruct (nth n table None) eqn:nth_equals. { destruct (Compare_dec.le_lt_dec (StringLike.length s_str) n0) as [|g]. { rewrite Nat.min_l by assumption. left. reflexivity. } { exfalso. destruct (Htable n0) as [some_impl _]. pose (some_impl nth_equals) as Hn0. destruct Hn0 as [Hn0_binop Hn0_balanced]. apply paren_balanced_hiding_impl_paren_balanced' in Hn0_balanced. subst s_str. rewrite take_take in H_nt_hiding. refine (paren_balanced_hiding'_prefix__index_points_to_binop _ H_nt_hiding Hn0_binop Hn0_balanced _). rewrite <- Nat.min_assoc. rewrite <- take_length. rewrite Nat.min_idempotent. assumption. } } { rewrite Nat.min_idempotent. tauto. } } destruct Hlen as [Hlen|Hlen]. { subst s_str m; exfalso; revert isnonzero. rewrite drop_length, substring_length; apply Nat.min_case_strong; simpl; intros; omega. } subst s_str. rewrite take_take in H_nt_hiding. inversion pits as [|idx'' pat pats H_parse_item H_parse_production Hits]. { subst. simpl in *. tauto. } assert (take 1 (drop idx' (substring n m str)) ~= [ch]). { destruct (possible_first_terminals_of_production its) eqn:terminals. { simpl in *. tauto. } { pose proof (possible_first_ascii_parse_of_production pits) as H_first_char. apply FirstChar.first_char_in_exists in H_first_char. { destruct H_first_char as [ch0 [take_equals in_list] ]. rewrite terminals in in_list. clear terminals. set (ls := (a :: l)) in *. induction ls; destruct pf; destruct in_list; subst; tauto. } { omega. } } } repeat match goal with | [ H : context[length (drop _ (substring _ _ _))] |- _ ] => rewrite drop_length in H end. unfold list_of_next_bin_ops_spec'' in *. destruct (List.nth n table None) as [idx|]. { edestruct Htable as [ [Htable0 Htable1] _]; clear Htable; [ reflexivity | ]. left. destruct (Compare_dec.lt_eq_lt_dec idx idx') as [ [?|?]|?]; [ | subst; apply Nat.min_r; omega | ]; exfalso. { apply paren_balanced_hiding_impl_paren_balanced' in Htable1; [ | exact _ .. ]. eapply paren_balanced_hiding'_prefix__index_points_to_binop; try eassumption. rewrite <- take_length, <- take_take, take_length. apply Nat.min_case_strong; intros; try assumption; omega. } { apply paren_balanced_hiding_impl_paren_balanced' in H_nt_hiding; [ | exact _ .. ]. eapply (paren_balanced_hiding'_prefix); [ exact Htable1 | exact H_nt_hiding | | | eassumption ]. { apply Nat.min_case_strong; omega. } { rewrite Nat.min_l by (rewrite substring_length, Nat.min_r in Hsmall by omega; omega). rewrite drop_take, take_take in H. apply take_n_1_singleton in H. assumption. } } } { simpl. pose proof (fun idx => proj2 (Htable idx) eq_refl) as Htable'. clear Htable. apply paren_balanced_hiding_impl_paren_balanced' in H_nt_hiding. specialize (Htable' _ H_nt_hiding). unfold index_not_points_to_binop in *. apply FirstChar.for_first_char_exists in Htable'; [ | solve [ repeat match goal with | _ => rewrite Nat.min_l in Hsmall by omega | _ => rewrite Nat.min_l in isnonzero by omega | _ => rewrite Nat.min_l by assumption | [ H : is_true (_ ~= [ _ ]) |- _ ] => apply length_singleton in H | [ H : _ |- _ ] => progress rewrite ?drop_length, ?take_length in H | _ => progress rewrite ?drop_length, ?take_length | [ H : min _ _ = _ |- _ ] => revert H; apply Nat.min_case_strong; clear; intros; omega | _ => omega end ] ]. destruct Htable' as [ch' [Ht0 Ht1] ]. rewrite substring_length, Nat.min_r, Nat.add_sub in Hsmall by omega. repeat match goal with | _ => rewrite Nat.min_idempotent | [ |- _ \/ False ] => left | [ H : 0 < ?x - ?y |- ?x = ?y ] => exfalso | [ H : context[min] |- _ ] => rewrite Nat.min_r in H by omega | [ H : context[min] |- _ ] => rewrite Nat.min_l in H by omega | [ H : is_true (is_char (substring _ _ (substring _ _ _)) _) |- _ ] => rewrite substring_substring in H; apply take_n_1_singleton in H | [ H : context[(?x + ?y)%nat], H' : context[(?y + ?x)%nat] |- _ ] => not constr_eq x y; replace (y + x) with (x + y) in H' by omega | [ H : is_true (?str ~= [ ?ch ])%string_like, H' : is_true (?str ~= [ ?ch' ])%string_like |- _ ] => assert (ch = ch') by (eapply singleton_unique; eassumption); clear H' | _ => progress subst | _ => congruence end. } 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