proposition: Lemma paren_balanced'_split {HSLP : StringLikeProperties Char} (str : String) (n : nat) (level1 level2 : nat) (H1 : paren_balanced' (take n str) level1) (H2 : paren_balanced' (drop n str) level2) : paren_balanced' str (level1 + level2).
proof: Proof. revert n level1 level2 H1 H2. set (len := length str). generalize (eq_refl : length str = len). clearbody len. revert str. induction len as [|len IHlen]. { intros str Hlen ???. rewrite !paren_balanced'_nil by (rewrite ?drop_length, ?take_length, Hlen; destruct n; reflexivity). destruct level1, level2; simpl; intros; congruence. } { intros str Hlen ???. specialize (IHlen (drop 1 str)). specialize_by (rewrite drop_length; omega). specialize (IHlen (pred n)). destruct n as [|n]. { clear IHlen. rewrite drop_0. rewrite !paren_balanced'_nil by (rewrite ?drop_length, ?take_length, Hlen; reflexivity). destruct level1; simpl; intros; [ assumption | congruence ]. } { simpl in *. setoid_rewrite drop_drop in IHlen. setoid_rewrite take_drop in IHlen. rewrite !Nat.add_1_r in IHlen. specialize (fun H' level1 H => IHlen level1 level2 H H'). intros H1 H2. specialize_by assumption. rewrite paren_balanced'_recr in H1 |- *. rewrite get_take_lt in H1 by omega. destruct (get 0 str) eqn:H'. { unfold paren_balanced'_step in *. repeat match goal with | _ => progress simpl in * | [ |- context[if ?e then _ else _] ] => destruct e eqn:? | [ IHlen : forall level : nat, _ -> _, H : is_true (paren_balanced' _ _) |- _ ] => specialize (IHlen _ H) | [ IHlen : forall level : nat, _ -> _, H : paren_balanced' _ _ = true |- _ ] => specialize (IHlen _ H) | _ => solve [ eauto with nocore ] | [ H : is_true (andb _ _) |- _ ] => apply Bool.andb_true_iff in H | _ => progress split_and | [ |- is_true (andb _ _) ] => apply Bool.andb_true_iff | _ => congruence | _ => omega | [ H : context[bool_of_sumbool ?e] |- _ ] => destruct e; simpl in H | [ |- context[bool_of_sumbool ?e] ] => destruct e; simpl | [ |- _ /\ _ ] => split | [ H : context[pred ?x] |- _ ] => is_var x; destruct x end. } { apply no_first_char_empty in H'. omega. } } } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Parsers.Reachable.ParenBalanced.Core Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Common