proposition: Lemma pre_Fix_grammar_fixedpoint_correct_valid (P : default_nonterminal_carrierT -> state gdata -> Type) (Pinit : forall nt, is_true (is_valid_nonterminal initial_nonterminals_data nt) -> P nt ⊥) (IH : forall nt st v, st nt = v -> is_true (is_valid_nonterminal initial_nonterminals_data nt) -> P nt v -> P nt (v ⊔ step_constraints gdata st nt v)) : forall nt, is_true (is_valid_nonterminal initial_nonterminals_data nt) -> P nt (lookup_state (pre_Fix_grammar gdata initial_nonterminals_data) nt).
proof: Proof. specialize (fun nt st => IH nt st _ eq_refl). assert (Hvalid' : forall nt, is_true (is_valid_nonterminal initial_nonterminals_data nt) -> match FMapPositive.PositiveMap.find (nonterminal_to_positive nt) (aggregate_state_max gdata initial_nonterminals_data) with | Some v => P nt v | None => False end). { intros nt Hvalid. pose proof (find_aggregate_state_max_spec gdata G (nonterminal_to_positive nt)) as Hvalid'. rewrite nonterminal_to_positive_to_nonterminal in Hvalid'. edestruct Hvalid' as [Hvalid'0 Hvalid'1]. simpl in *. rewrite Hvalid'1 by (split; [ reflexivity | assumption ]). eauto. } pose proof (fun nt (pf : is_true (is_valid_nonterminal (@initial_nonterminals_data _ (@rdp_list_predata _ G)) nt)) => match eq_sym pf in (_ = b) return (if b then ⊥ else ⊤) = lookup_state (aggregate_state_max gdata initial_nonterminals_data) nt -> _ with | eq_refl => eq_rect _ (P nt) (Pinit _ pf) _ end (eq_sym (lookup_state_aggregate_state_max gdata G nt))) as Pinit'. unfold pre_Fix_grammar, pre_Fix_grammar_helper. let Rwf := lazymatch goal with |- context[Fix ?Rwf _ _ ?v] => Rwf end in let v := lazymatch goal with |- context[Fix Rwf _ _ ?v] => v end in pose proof (fun nt => IH nt (lookup_state v)) as IHv; specialize (fun nt pf => IHv nt pf (Pinit' _ pf)); induction (Rwf v) as [a Ha IHa]. rewrite Init.Wf.Fix_eq by (intros; edestruct Sumbool.sumbool_of_bool; trivial). edestruct Sumbool.sumbool_of_bool; [ intros; apply Pinit'; assumption | ]. fold (pre_Fix_grammar_helper (gdata := gdata) initial_nonterminals_data) in *. destruct (aggregate_state_eq a (aggregate_step a)) eqn:Heq. { intuition congruence. } { apply step_lt in Heq. intros nt. apply IHa; eauto; intros; try apply IH; repeat match goal with | _ => progress intros | _ => rewrite find_aggregate_step | _ => rewrite lookup_state_aggregate_step | _ => rewrite nonterminal_to_positive_to_nonterminal | _ => tauto | _ => assumption | _ => progress unfold lookup_state, PositiveMapExtensions.find_default, state, option_map, option_rect in * | [ H : forall nt, is_true (?P nt) -> _, H' : is_true (?P _) |- _ ] => specialize (H _ H') | [ |- ?P ?nt (_ ⊔ _) ] => apply P_lub | [ H : context[match ?e with _ => _ end] |- _ ] => destruct e eqn:? | [ |- context[match ?e with _ => _ end] ] => destruct e eqn:? end. } Qed.
imports: Fiat.Parsers.BaseTypes Fiat.Parsers.Splitters.RDPList Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Parsers.ContextFreeGrammar.Fix.Fix Fiat.Parsers.ContextFreeGrammar.Fix.Properties Fiat.Common