proposition: Lemma rdp_list_remove_nonterminal_dec : forall ls prods, @rdp_list_is_valid_nonterminal ls prods = true -> @rdp_list_nonterminals_listT_R (@rdp_list_remove_nonterminal ls prods) ls.
proof: Proof. intros ls prods H. unfold rdp_list_is_valid_nonterminal, rdp_list_nonterminals_listT_R, rdp_list_remove_nonterminal, ltof in *. fix_eqs. apply list_in_bl in H; [ | solve [ intros; apply Nat.eqb_eq; trivial ] ]. match goal with | [ H : In ?prods ?ls |- context[filter ?f ?ls] ] => assert (~In prods (filter f ls)) end. { intro H'. apply filter_In in H'. destruct H' as [? H']. rewrite Nat.eqb_refl in H'. simpl in *; congruence. } { match goal with | [ |- context[filter ?f ?ls] ] => generalize dependent f; intros end. induction ls; simpl in *; try congruence. repeat match goal with | [ |- context[if ?x then _ else _] ] => destruct x; simpl in * | [ H : _ \/ _ |- _ ] => destruct H | _ => progress subst | [ H : ~(_ \/ _) |- _ ] => apply Decidable.not_or in H | [ H : _ /\ _ |- _ ] => destruct H | [ H : ?x <> ?x |- _ ] => exfalso; apply (H eq_refl) | _ => apply (fun n m => (proj1 (Nat.succ_lt_mono n m))) | _ => apply (fun n m => (proj1 (Nat.succ_le_mono n m))) | _ => apply filter_list_dec | [ H : _ -> _ -> ?G |- ?G ] => apply H; auto end. } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.ZArith.ZArith Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.BaseTypes Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Common Fiat.Common.Equality Fiat.Common.List.Operations Fiat.Common.List.ListFacts