proposition: Lemma lookup_state_aggregate_state_max nt : lookup_state (aggregate_state_max initial_nonterminals_data) nt = if is_valid_nonterminal initial_nonterminals_data nt then ⊥ else default_value.
proof: Proof. unfold lookup_state, PositiveMapExtensions.find_default, option_rect. destruct (PositiveMap.find (nonterminal_to_positive nt) (aggregate_state_max (@initial_nonterminals_data _ predata))) eqn:H; [ | ]; setoid_rewrite H. { simpl in *. apply find_aggregate_state_max_spec in H. rewrite nonterminal_to_positive_to_nonterminal in H. destruct H as [? H']; subst; simpl in *; rewrite H'; intuition. } { match goal with |- context[if ?e then _ else _] => destruct e eqn:H' end; [ | reflexivity ]. pose proof (find_aggregate_state_max_spec (nonterminal_to_positive nt) ⊥) as H''. rewrite nonterminal_to_positive_to_nonterminal, H' in H''. destruct H'' as [_ H'']. rewrite H'' in H by intuition. 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