proposition: Lemma find_aggregate_state_max_rdp_spec k v : PositiveMap.find k aggregate_state_max = Some v <-> (v = ⊥ /\ rdp_list_is_valid_nonterminal initial_nonterminals_data (positive_to_nonterminal k)).
proof: Proof. unfold aggregate_state_max in *. generalize dependent initial_nonterminals_data; intros ls. induction ls as [|x xs IHxs]. { simpl in *. autorewrite with aggregate_step_db in *. intuition (tauto || congruence || eauto). } { simpl in *. autorewrite with aggregate_step_db in *. edestruct PositiveMap.E.eq_dec; subst; autorewrite with aggregate_step_db in *; auto using eq_refl with nocore. { repeat intuition (congruence || subst || eauto). } { intuition (congruence || subst || eauto). { apply orb_true_iff; intuition. } { do 2 match goal with | [ H : is_true (orb _ _) |- _ ] => apply orb_true_iff in H | [ H : _ |- _ ] => setoid_rewrite Nat.eqb_eq in H end. repeat intuition (congruence || subst || (autorewrite with aggregate_step_db in * ) || eauto). } } } 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