proposition: Lemma pre_Fix_grammar_fixedpoint_correct_stronger' (P : default_nonterminal_carrierT -> state gdata -> Type) (Pbot : forall nt, is_true (is_valid_nonterminal initial_nonterminals_data nt) -> P nt ⊥) (Ptop : forall nt, is_valid_nonterminal initial_nonterminals_data nt = false -> P nt ⊤) (IH : forall nt st, (forall nt', is_valid_nonterminal initial_nonterminals_data nt' = false -> st nt' = ⊤) -> (forall nt', P nt' (st nt')) -> P nt (st nt ⊔ step_constraints gdata st nt (st nt))) : 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. assert (Htop : forall nt', is_valid_nonterminal initial_nonterminals_data nt' = false -> lookup_state (aggregate_state_max gdata initial_nonterminals_data) nt' = ⊤). { intros nt' Hinvalid. simpl rewrite lookup_state_aggregate_state_max; simpl in *; rewrite Hinvalid. reflexivity. } 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 rewrite Hvalid'1; [ | split; [ reflexivity | assumption ] ]. eauto. } pose proof (fun nt => match is_valid_nonterminal (@initial_nonterminals_data _ (@rdp_list_predata _ G)) nt as b return is_valid_nonterminal (@initial_nonterminals_data _ (@rdp_list_predata _ G)) nt = b -> (if b then ⊥ else ⊤) = lookup_state (aggregate_state_max gdata initial_nonterminals_data) nt -> _ with | true => fun pf => eq_rect _ (P nt) (Pbot _ pf) _ | false => fun pf => eq_rect _ (P nt) (Ptop _ pf) _ end eq_refl (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 => IHv nt Htop Pinit'); 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. simpl @nonterminal_carrierT in *. 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 subst | _ => progress unfold lookup_state, PositiveMapExtensions.find_default, state, option_map, option_rect in * | [ H : ?A -> ?B, H' : ?A |- _ ] => specialize (H H') | [ H : is_true true -> _ |- _ ] => specialize (H eq_refl) | [ |- is_true true ] => reflexivity | [ |- is_true false ] => exfalso | [ |- ?P ?nt (_ ⊔ _) ] => apply P_lub | _ => rewrite top_lub_l | [ H : Some _ = Some _ |- _ ] => inversion H; clear H | [ H : forall nt : default_nonterminal_carrierT, _ |- _ ] => repeat match goal with | [ nt' : default_nonterminal_carrierT |- _ ] => unique pose proof (H nt') | [ H' : context[is_valid_nonterminal _ ?nt'] |- _ ] => unique pose proof (H nt') | [ |- context[is_valid_nonterminal _ ?nt'] ] => unique pose proof (H nt') end; clear H | [ H : forall a b, is_true (is_valid_nonterminal ?ls ?nt) -> _ |- _ ] => destruct (is_valid_nonterminal ls nt) eqn:? | [ P_lub : forall a b, _ -> _ -> _ -> ?P ?nt (_ ⊔ _) |- ?P ?nt (_ ⊔ _) ] => apply P_lu | [ 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