proposition: Lemma cell_of_next_bin_ops_spec''_compute_next_bin_op' {HSLP : StringLikeProperties Char} {level str offset idx} : cell_of_next_bin_ops_spec'' level (compute_next_bin_op' (drop offset str) level) str offset idx.
proof: Proof. revert level offset idx. set (len := length str). generalize (eq_refl : length str = len). clearbody len. revert str. induction len; simpl; intros str Hlen level offset idx. { hnf. rewrite compute_next_bin_op'_nil by (rewrite drop_length; omega). repeat split; intros. { apply index_points_to_binop_nil; omega. } { congruence. } { apply index_not_points_to_binop_nil; omega. } } { specialize (IHlen (drop 1 str)). specialize_by (rewrite drop_length; omega). setoid_rewrite drop_drop in IHlen; t_eq. destruct offset as [|offset]; [ | solve [ eauto using cell_of_next_bin_op_spec''_S_offset with nocore ] ]. rewrite drop_0. specialize (fun level => IHlen level 0). split. { specialize (fun level => IHlen level (pred idx)). destruct idx as [|idx]. { clear IHlen. rewrite compute_next_bin_op'_recr. unfold compute_next_bin_op'_step. repeat match goal with | [ |- context[match ?e with _ => _ end] ] => destruct e eqn:? end; t. } { rewrite compute_next_bin_op'_recr. repeat match goal with | [ |- context[match ?e with _ => _ end] ] => destruct e eqn:? end; [ | solve [ t ] ]. rewrite paren_balanced_hiding'_recr. repeat match goal with | [ |- context[match ?e with _ => _ end] ] => destruct e eqn:? end; [ | solve [ t ] ]. unfold compute_next_bin_op'_step, paren_balanced_hiding'_step, paren_balanced'_step, cell_of_next_bin_ops_spec'' in *. repeat match goal with | _ => progress t | [ |- context[match ?e with _ => _ end] ] => destruct e eqn:? | [ H : context[match ?e with _ => _ end] |- _ ] => destruct e eqn:? end. } } { specialize (fun level => IHlen level (pred idx)). destruct idx as [|idx]. { clear IHlen. rewrite compute_next_bin_op'_recr, paren_balanced'_recr. unfold compute_next_bin_op'_step, paren_balanced'_step. repeat match goal with | [ |- context[match ?e with _ => _ end] ] => destruct e eqn:? end; t. } { simpl in *. rewrite compute_next_bin_op'_recr. repeat match goal with | [ |- context[match ?e with _ => _ end] ] => destruct e eqn:? end; [ | solve [ t ] ]. rewrite paren_balanced'_recr. repeat match goal with | [ |- context[match ?e with _ => _ end] ] => destruct e eqn:? end; [ | solve [ t ] ]. unfold compute_next_bin_op'_step, paren_balanced'_step, cell_of_next_bin_ops_spec'' in *. repeat match goal with | _ => progress t | [ |- context[match ?e with _ => _ end] ] => destruct e eqn:? | [ H : context[match ?e with _ => _ end] |- _ ] => destruct e eqn:? end. } } } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.ZArith.ZArith Fiat.Common Fiat.Common.List.Operations Fiat.Common.List.ListFacts Fiat.Common.SetoidInstances Fiat.Parsers.Reachable.ParenBalanced.Core Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Parsers.StringLike.FirstChar Fiat.Parsers.Refinement.BinOpBrackets.ParenBalanced