proposition: Lemma list_of_next_bin_ops'_opt_correct (str : String) : list_of_next_bin_ops'_opt str = (nth 0 (map Some (list_of_next_bin_ops' str)) None, tl (map (fun ls => nth 0 ls None) (list_of_next_bin_ops' str))).
proof: Proof. change list_of_next_bin_ops'_opt with list_of_next_bin_ops'_opt0. unfold list_of_next_bin_ops', list_of_next_bin_ops'_opt0. set (len := length str). generalize (eq_refl : length str = len). clearbody len. revert str. induction len; intros str H'. { rewrite !fold_nil by assumption; reflexivity. } { specialize (IHlen (drop 1 str)). specialize_by (rewrite drop_length; omega). rewrite !(fold_recr _ _ str). destruct (get 0 str) eqn:H''. { unfold list_of_next_bin_ops'_step_opt at 1. rewrite !IHlen; clear IHlen. unfold list_of_next_bin_ops'_step'_opt. generalize (fold list_of_next_bin_ops'_step [] (drop 1 str)). intros ls'. unfold list_of_next_bin_ops'_step. unfold list_of_next_bin_ops'_step'. repeat match goal with | [ |- context[if ?e then _ else _] ] => destruct e eqn:? | _ => progress cbv beta | [ |- context[fst (?x, ?y)] ] => change (fst (x, y)) with x | [ |- context[snd (?x, ?y)] ] => change (snd (x, y)) with y | [ |- context[nth 0 (?x::?xs) ?v] ] => change (nth 0 (x::xs) v) with x | [ |- (_, _) = (_, _) ] => apply f_equal2 | [ |- context[map ?f (?x::?xs)] ] => change (map f (x::xs)) with (f x :: map f xs) | [ |- Some _ = Some _ ] => apply f_equal | [ |- _::_ = _::_ ] => apply f_equal2 | _ => reflexivity | [ |- context[nth 0 (map Some ?ls) None] ] => is_var ls; destruct ls end. } { 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