proposition: Lemma find_pre_Fix_grammar (nt : default_nonterminal_carrierT) : is_valid_nonterminal initial_nonterminals_data nt <-> PositiveMap.find (nonterminal_to_positive nt) (pre_Fix_grammar initial_nonterminals_data) <> None.
proof: Proof. unfold pre_Fix_grammar, pre_Fix_grammar_helper. assert (H : PositiveMap.find (nonterminal_to_positive nt) (aggregate_state_max initial_nonterminals_data) <> None <-> is_valid_nonterminal initial_nonterminals_data nt). { pose proof (find_aggregate_state_max_spec (nonterminal_to_positive nt)) as H. rewrite nonterminal_to_positive_to_nonterminal in H. edestruct PositiveMap.find. { edestruct H as [H0 H1]; clear H. intuition congruence. } { specialize (H ⊥). intuition congruence. } } rewrite <- H; clear H. generalize dependent (aggregate_state_max initial_nonterminals_data); intro a; intros. induction (aggregate_state_lt_wf a) as [?? IH]. rewrite Init.Wf.Fix_eq at 1 by (intros; edestruct dec; trivial). edestruct dec as [pf|pf]; [ reflexivity | ]. rewrite <- IH by (apply step_lt; assumption). rewrite find_aggregate_step. unfold option_map; split; fold_andb_t. Qed.
imports: Coq.Init.Wf Coq.Numbers.BinNums Coq.Arith.Arith Coq.FSets.FMapPositive Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.Splitters.RDPList Fiat.Parsers.BaseTypes Fiat.Parsers.ContextFreeGrammar.Fix.Definitions Fiat.Parsers.ContextFreeGrammar.Fix.Properties Fiat.Common.FMapExtensions.Wf Fiat.Common Fiat.Common.OptionFacts Fiat.Common.SetoidInstances