proposition: Lemma rdp_list_remove_nonterminal_2 : forall ls ps ps', rdp_list_is_valid_nonterminal (rdp_list_remove_nonterminal ls ps) ps' = false <-> rdp_list_is_valid_nonterminal ls ps' = false \/ ps = ps'.
proof: Proof. unfold rdp_list_is_valid_nonterminal, rdp_list_remove_nonterminal. fix_eqs. repeat match goal with | _ => exfalso; congruence | _ => reflexivity | _ => progress subst | _ => intro | [ H : @eq bool ?x ?y -> False |- _ ] => apply Bool.eq_true_not_negb in H | [ H : context[In _ (filter _ _)] |- _ ] => rewrite filter_In in H | [ H : _ /\ _ |- _ ] => destruct H | [ H : ?T, H' : ~?T |- _ ] => destruct (H' H) | [ |- true = false \/ _ ] => right | [ |- ?x = ?x \/ _ ] => left; reflexivity | [ H : ~(_ /\ ?x = ?x) |- _ ] => specialize (fun y => H (conj y eq_refl)) | [ H : ~(?T /\ _), H' : ?T |- _ ] => specialize (fun y => H (conj H' y)) | [ H : (?T /\ _) -> False, H' : ?T |- _ ] => specialize (fun y => H (conj H' y)) | [ H : _ \/ _ |- _ ] => destruct H | [ |- _ <-> _ ] => split | [ H : context[match ?E with left _ => _ | right _ => _ end] |- _ ] => destruct E | [ |- context[match ?E with left _ => _ | right _ => _ end] ] => destruct E | [ H : _ |- _ ] => rewrite Bool.negb_involutive in H | [ H : string_beq _ _ = true |- _ ] => apply string_bl in H | [ H : context[string_beq ?x ?x] |- _ ] => rewrite (string_lb (eq_refl x)) in H | _ => progress simpl in * | [ H : list_bin _ _ _ = true |- _ ] => apply list_in_bl in H; [ | solve [ intros; apply (fun n m => (proj1 (Nat.eqb_eq n m))); trivial ] ] | [ |- list_bin _ _ _ = true ] => apply list_in_lb | [ |- context[list_bin ?x ?y ?z = false] ] => case_eq (list_bin x y z) | [ H : list_bin _ _ _ = false |- _ ] => apply Bool.not_true_iff_false in H | [ H : list_bin _ _ _ <> true |- _ ] => specialize (fun pf H' => H (list_in_lb pf H')) | [ H : ?A -> ?B |- _ ] => let H' := fresh in assert (H' : A) by (intros; subst; rewrite ?Nat.eqb_refl; reflexivity); specialize (H H'); clear H' | [ H : Nat.eqb _ _ = true |- _ ] => apply (fun n m => (proj1 (Nat.eqb_eq n m))) in H | [ H : context[Nat.eqb ?x ?x] |- _ ] => rewrite Nat.eqb_refl in H 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