proposition: Lemma find_pre_Fix_grammar_to_lookup_state (nt : default_nonterminal_carrierT) : PositiveMap.find (nonterminal_to_positive nt) (pre_Fix_grammar initial_nonterminals_data) = if is_valid_nonterminal initial_nonterminals_data nt then Some (lookup_state (pre_Fix_grammar initial_nonterminals_data) nt) else None.
proof: Proof. let v := match goal with |- context[if ?v then _ else _] => v end in destruct v eqn:Hvalid. { apply find_pre_Fix_grammar in Hvalid. unfold lookup_state, PositiveMapExtensions.find_default, state in *; simpl in *. edestruct PositiveMap.find; [ reflexivity | congruence ]. } { destruct (PositiveMap.find (nonterminal_to_positive nt) (pre_Fix_grammar (@initial_nonterminals_data _ predata))) eqn:H; [ | reflexivity ]. rewrite (proj2 (find_pre_Fix_grammar _)) in Hvalid; congruence. } 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