proposition: Lemma parse_to_sem_ind : forall r s k, normal r -> parse (r,s,k) = true -> exists s1 s2, s = s1 ++ s2 /\ sem r s1 /\ k s2 = true.
proof: Proof. Proof using. introv N P. sets_eq p: (r,s). gen r s k. induction_wf IH: parse_sub_wf p. intros. subst p. rewrite~ parse_fix in P. unfold Parse in P. destruct r; simpl in N; (try match type of N with _ /\ _ => destruct N end). false. exists (nil:text) s. splits~. destruct s; tryfalse. case_if; tryfalse. exists (n0::nil) s. subst. splits~. case_eq (parse (r1,s,k)); intros P1. forwards~ (s1&s2&E&S&P'): IH P1. auto 7. exists~ s1 s2. rewrite P1 in P. rew_bool in P. forwards~ (s1&s2&E&S&P'): IH P. auto 7. exists~ s1 s2. forwards~ (s1&s2&E&S&P'): IH P. auto. forwards~ (s3&s4&E'&S'&K): IH P'. auto. forwards M: text_sub_app E. subst s s2. exists (s1 ++ s3) s4. rew_list~. case_eq (k s); intros K. exists (nil:text) s. splits~. rewrite K in P. rew_bool in P. forwards~ (s1&s2&E&S&P'): IH P. auto. forwards~ (s3&s4&E'&S'&K'): IH P'; try solve [hnfs~]. forwards M: text_sub_app E. inverts M. auto. false. applys~ sem_productive S. apply* self_eq_app_r_inv. subst s s2. exists (s1++s3) s4. rew_list~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat