proposition: Lemma tables_agree {HSLP : StringLikeProperties Char} {level str offset} : nth offset (map (fun ls => nth level ls None) (list_of_next_bin_ops' str)) None = compute_next_bin_op' (drop offset str) level.
proof: Proof. revert level offset. set (len := length str). generalize (eq_refl : length str = len). clearbody len. revert str. induction len; simpl; intros str Hlen level offset. { hnf. rewrite compute_next_bin_op'_nil, list_of_next_bin_ops'_nil by (rewrite ?drop_length; omega). destruct offset; reflexivity. } { specialize (IHlen (drop 1 str)). specialize_by (rewrite drop_length; omega). setoid_rewrite drop_drop in IHlen. t_eq. rewrite list_of_next_bin_ops'_recr. destruct (get 0 str) eqn:H'; [ | solve [ t ] ]. destruct offset as [|offset]. { rewrite compute_next_bin_op'_recr. rewrite drop_0, H'. unfold list_of_next_bin_ops'_step; simpl. rewrite drop_0. unfold compute_next_bin_op'_step, list_of_next_bin_ops'_step'. rewrite <- !IHlen; clear IHlen. repeat match goal with | [ |- context[if ?e then _ else _] ] => destruct e eqn:? | _ => progress t | _ => reflexivity end; match goal with | [ |- context[nth ?n (map ?f ?ls) _] ] => simpl rewrite <- (map_nth f ls nil n) end; destruct level; reflexivity. } { rewrite <- IHlen; clear IHlen. reflexivity. } } 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