proposition: Lemma related_pre_Fix_grammar_gen (HRtop : R ⊤ ⊤) (HRbot : R ⊥ ⊥) (HRtopR : forall x y, R x ⊤ -> R (x ⊔ y) ⊤) (HRtopL : forall x y, R ⊤ x -> R ⊤ (x ⊔ y)) (HRstep : forall st st' k, aggregate_state_relation st st' -> R (lookup_state st k ⊔ step_constraints gdata0 (lookup_state st) k (lookup_state st k)) (lookup_state st' k ⊔ step_constraints gdata1 (lookup_state st') k (lookup_state st' k))) (R_Proper : Proper (state_beq ==> state_beq ==> iff) R) : aggregate_state_relation (pre_Fix_grammar gdata0 initial_nonterminals_data) (pre_Fix_grammar gdata1 initial_nonterminals_data).
proof: Proof. pose proof (related_aggregate_state_max initial_nonterminals_data HRbot) as H. unfold aggregate_state_relation in *. rewrite PositiveMapExtensions.lift_relation_hetero_iff in *. rewrite <- ?PositiveMapExtensions.lift_relation_hetero_iff in H. intro k. rewrite !find_pre_Fix_grammar_to_lookup_state' in *. fold predata. destruct (@is_valid_nonterminal _ predata (@initial_nonterminals_data _ predata) (positive_to_nonterminal k)) eqn:Hv; [ | exact I ]. unfold pre_Fix_grammar, pre_Fix_grammar_helper in *. fold predata. assert (Hfind : forall k, PositiveMap.find k (aggregate_state_max gdata0 initial_nonterminals_data) = None <-> PositiveMap.find k (aggregate_state_max gdata1 initial_nonterminals_data) = None). { intro; rewrite !find_aggregate_state_max_exact. break_match; split; congruence. } generalize dependent (aggregate_state_max gdata0 initial_nonterminals_data). generalize dependent (aggregate_state_max gdata1 initial_nonterminals_data). intro a; induction (aggregate_state_lt_wf a) as [st' Hacc IH]. intro st. intros H' Hfind; revert H'. rewrite Init.Wf.Fix_eq at 1 by (intros; edestruct dec; trivial). set (FIX := Fix) at 1. rewrite Init.Wf.Fix_eq at 1 by (intros; edestruct dec; trivial). subst FIX. assert (Hfind_all : forall k, (PositiveMap.find k st = None <-> PositiveMap.find k (aggregate_step st') = None) /\ (PositiveMap.find k (aggregate_step st) = None <-> PositiveMap.find k st' = None) /\ (PositiveMap.find k (aggregate_step st) = None <-> PositiveMap.find k (aggregate_step st') = None) /\ (PositiveMap.find k (aggregate_step (aggregate_step st)) = None <-> PositiveMap.find k st' = None) /\ (PositiveMap.find k (aggregate_step (aggregate_step st)) = None <-> PositiveMap.find k (aggregate_step st') = None)). { let k := fresh in intro k; specialize (Hfind k). rewrite !find_aggregate_step; unfold option_map; break_match; intuition congruence. } assert (forall k, PositiveMap.find k st = None <-> PositiveMap.find k (aggregate_step st') = None) by apply Hfind_all. assert (forall k, PositiveMap.find k (aggregate_step st) = None <-> PositiveMap.find k st' = None) by apply Hfind_all. assert (forall k, PositiveMap.find k (aggregate_step st) = None <-> PositiveMap.find k (aggregate_step st') = None) by apply Hfind_all. assert (forall k, PositiveMap.find k (aggregate_step (aggregate_step st)) = None <-> PositiveMap.find k st' = None) by apply Hfind_all. assert (forall k, PositiveMap.find k (aggregate_step (aggregate_step st)) = None <-> PositiveMap.find k (aggregate_step st') = None) by apply Hfind_all. do 2 edestruct dec. { rewrite PositiveMapExtensions.lift_relation_hetero_iff. unfold lookup_state, PositiveMapExtensions.find_default. intro Hfind'. let k := match goal with |- context[PositiveMap.find ?k _] => k end in specialize (Hfind' k). do 2 edestruct PositiveMap.find; simpl; assumption. } { specialize (fun y Hy => IH y Hy st). rewrite Init.Wf.Fix_eq in IH by (intros; edestruct dec; trivial). edestruct dec; [ | congruence ]. intro Hfind'; apply IH; clear IH; auto using step_lt; []. unfold aggregate_state_eq in *. unfold PositiveMapExtensions.lift_eqb in *. match goal with | [ H : PositiveMapExtensions.lift_brelation state_beq ⊤ ?x ?y = true |- PositiveMapExtensions.lift_relation_hetero _ _ _ ?x _ ] => change (is_true (PositiveMapExtensions.lift_brelation state_beq ⊤ x y)) in H; rewrite H end. rewrite PositiveMapExtensions.lift_relation_hetero_iff. unfold lookup_state, PositiveMapExtensions.find_default. intro k'; specialize (Hfind k'); rewrite !find_aggregate_step. unfold option_map; break_innermost_match; auto; try solve [ intuition congruence ]; []. repeat match goal with | [ |- context[?s ⊔ step_constraints ?data ?lookup ?k ?s] ] => is_var s; replace s with (lookup k) by (unfold lookup_state, PositiveMapExtensions.find_default, option_rect; rewrite positive_to_nonterminal_to_positive; rewrite_hyp; reflexivity) end. auto. } { clear IH Hfind_all Hacc. intro Hrel. assert (Hrel' : PositiveMapExtensions.lift_relation_hetero R ⊤ ⊤ (aggregate_step st) st'). { unfold aggregate_state_eq, PositiveMapExtensions.lift_eqb in *. match goal with | [ H : PositiveMapExtensions.lift_brelation state_beq ⊤ ?x ?y = true |- PositiveMapExtensions.lift_relation_hetero _ _ _ _ ?x ] => change (is_true (PositiveMapExtensions.lift_brelation state_beq ⊤ x y)) in H; rewrite H end. pose proof Hrel as Hrel'. rewrite PositiveMapExtensions.lift_relation_hetero_iff in Hrel' |- *. unfold lookup_state, PositiveMapExtensions.find_default. intro k'; pose proof (Hrel' k'); rewrite !find_aggregate_step. unfold option_map; break_innermost_match; auto; try solve [ intuition congruence ]; []. repeat match goal with | [ |- context[?s ⊔ step_constraints ?data ?lookup ?k ?s] ] => is_var s; replace s with (lookup k) by (unfold lookup_state, PositiveMapExtensions.find_default, option_rect; rewrite positive_to_nonterminal_to_positive; rewrite_hyp; reflexivity) end. auto. } revert dependent st'. generalize dependent (aggregate_step st); intros a _. intros; clear dependent st; revert dependent st'. induction (aggregate_state_lt_wf a) as [st Hacc IH]. intro st'. intros. rewrite Init.Wf.Fix_eq at 1 by (intros; edestruct dec; trivial). edestruct dec. { unfold lookup_state, PositiveMapExtensions.find_default. rewrite positive_to_nonterminal_to_positive. lazymatch goal with | [ H : PositiveMapExtensions.lift_relation_hetero _ _ _ _ _ |- _ ] => revert H end. rewrite PositiveMapExtensions.lift_relation_hetero_iff. intro Hrel. repeat match goal with | [ H : forall k : PositiveMap.key, _ |- context[PositiveMap.find ?k' _] ] => specialize (H k') end. unfold state in *. unfold option_map, option_rect; break_match; auto; intuition congruence. } { specialize (fun y Hy => IH y Hy st'). specialize (IH (aggregate_step st)). apply IH; clear IH; auto using step_lt; [ let k := fresh in intro k; repeat match goal with | [ H : forall k' : PositiveMap.key, _ |- _ ] => specialize (H k) end; rewrite !find_aggregate_step; unfold option_map; break_innermost_match; intuition congruence.. | ]. { unfold aggregate_state_eq, PositiveMapExtensions.lift_eqb, state in *. lazymatch goal with | [ H : PositiveMapExtensions.lift_brelation state_beq ⊤ ?x ?y = true |- PositiveMapExtensions.lift_relation_hetero _ _ _ _ ?x ] => change (is_true (PositiveMapExtensions.lift_brelation state_beq ⊤ x y)) in H; rewrite H end. lazymatch goal with | [ H : PositiveMapExtensions.lift_relation_hetero _ _ _ _ _ |- _ ] => generalize H end. rewrite !PositiveMapExtensions.lift_relation_hetero_iff. let k := fresh in intros Hrel k; specialize (Hrel k); revert Hrel. rewrite !find_aggregate_step; unfold option_map, state; break_innermost_match; auto. repeat match goal with | [ |- context[?s ⊔ step_constraints ?data ?lookup ?k ?s] ] => is_var s; replace s with (lookup k) by (unfold lookup_state, PositiveMapExtensions.find_default, option_rect; rewrite positive_to_nonterminal_to_positive; rewrite_hyp; reflexivity) end. auto. } } } { intro Hfind'; apply IH; clear IH; auto using step_lt; []. pose proof Hfind' as Hfind''. rewrite PositiveMapExtensions.lift_relation_hetero_iff in Hfind' |- *. intro k'; specialize (Hfind' k'). rewrite !find_aggregate_step. unfold option_map; break_innermost_match; auto. repeat match goal with | [ |- context[?s ⊔ step_constraints ?data ?lookup ?k ?s] ] => is_var s; replace s with (lookup k) by (unfold lookup_state, PositiveMapExtensions.find_default, option_rect; rewrite positive_to_nonterminal_to_positive; rewrite_hyp; reflexivity) end. auto. } 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.Parsers.ContextFreeGrammar.Fix.Fix Fiat.Common.FMapExtensions.Wf Fiat.Common Fiat.Common.OptionFacts Fiat.Common.SetoidInstances