proposition: Lemma pre_Fix_grammar_fixedpoint : aggregate_state_eq pre_Fix_grammar (aggregate_step pre_Fix_grammar).
proof: Proof. unfold pre_Fix_grammar, pre_Fix_grammar_helper. generalize aggregate_state_max; intro a. rewrite Init.Wf.Fix_eq at 1 by (intros; edestruct dec; trivial). edestruct dec as [pf|pf]. { rewrite Init.Wf.Fix_eq at 1 by (intros; edestruct dec; trivial). edestruct dec; [ | congruence ]. assumption. } { induction (aggregate_state_lt_wf a) as [?? IH]. rewrite Init.Wf.Fix_eq at 1 by (intros; edestruct dec; trivial). symmetry; rewrite Init.Wf.Fix_eq at 1 by (intros; edestruct dec; trivial); symmetry. rewrite pf; simpl. edestruct dec as [pf'|pf']. { rewrite Init.Wf.Fix_eq at 1 by (intros; edestruct dec; trivial). rewrite pf'; simpl. assumption. } { apply IH; try assumption; []; clear IH. unfold Basics.flip, aggregate_state_lt, PositiveMapExtensions.lift_ltb. setoid_rewrite pf; simpl; rewrite andb_true_r. pose proof (fun x => aggregate_state_lub_correct x (aggregate_prestep x)) as H'. unfold aggregate_step in *. edestruct H'; eassumption. } } 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