proposition: Lemma pre_Fix_grammar_helper_commute v : aggregate_state_eq (pre_Fix_grammar_helper (aggregate_step v)) (aggregate_step (pre_Fix_grammar_helper v)).
proof: Proof. unfold pre_Fix_grammar_helper. induction (aggregate_state_lt_wf v) as [v H IHv]. 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. do 2 edestruct dec; try reflexivity; repeat match goal with | [ H : ?x = true |- _ ] => change (is_true x) in H end. { fold @pre_Fix_grammar_helper in *. rewrite <- pre_Fix_grammar_helper_fixed by assumption. assumption. } { match goal with | [ H : is_true (aggregate_state_eq ?x ?y), H' : context[?x] |- _ ] => rewrite <- H in H' end. congruence. } { apply IHv. apply step_lt; assumption. } 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