proposition: Lemma expanded_fallback_list'_ext'' (P1 P2 : String -> nat -> nat -> production_carrierT -> production _ -> production_carrierT -> production _ -> list nat -> Prop) str offset len idx dummy (H : production_carrier_valid idx -> forall splits, P2 str offset len idx (to_production idx) idx (to_production idx) splits -> P1 str offset len idx (to_production idx) idx (to_production idx) splits) : refine (expanded_fallback_list' P1 str offset len idx dummy) (expanded_fallback_list' P2 str offset len idx dummy).
proof: Proof. unfold expanded_fallback_list', expanded_fallback_list'_body. rewrite !forall_reachable_productions_if_eq_correct; try exact _; [ rewrite !to_production_opt_correct | intro y; rewrite !to_production_opt_correct.. ]; [ repeat match goal with | [ |- ?R ?x ?x ] => reflexivity | [ |- context[match ?e with _ => _ end] ] => destruct e eqn:? | _ => progress subst | _ => progress simpl in * | _ => progress unfold If_Then_Else, option_rect in * | [ |- refine (a <- _; _) (b <- _; _) ] => apply refine_under_bind_both; [ | reflexivity ] | [ |- refine { a : _ | _ } { b : _ | _ } ] => apply refine_pick_pick | _ => progress specialize_by (exact eq_refl) | _ => solve [ eauto with nocore ] | [ H : rdp_list_to_production idx = ?x |- context[?x] ] => rewrite <- H | [ H : rdp_list_to_production idx = ?x, H' : context[?x] |- _ ] => rewrite <- H in H' | [ H : context[match ?e with _ => _ end] |- _ ] => destruct e eqn:? | _ => discriminate | [ H : ret_pick _ = ret_pick _ |- _ ] => inversion H; clear H end | repeat match goal with | [ |- is_true true ] => reflexivity | [ |- context[@production_carrier_valid ?A ?B ?idx] ] => destruct (@production_carrier_valid A B idx) eqn:? | _ => intro | _ => discriminate | [ H : ?x = true, H' : ?x = false |- _ ] => exfalso; clear -H H'; symmetry in H; pose proof (eq_trans H H'); clear H H' | [ H : invalid = match ?p with _ => _ end |- _ ] => destruct p | _ => progress unfold If_Then_Else in * | _ => progress unfold option_rect in * | _ => progress simpl in * end.. ]. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Arith.PeanoNat Coq.Lists.List Fiat.Parsers.BaseTypes Fiat.Parsers.Splitters.RDPList Fiat.Parsers.ParserInterface Fiat.Parsers.ParserADTSpecification Fiat.Parsers.ContextFreeGrammar.Equality Fiat.Parsers.ContextFreeGrammar.Properties Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ContextFreeGrammar.Precompute Fiat.Parsers.Refinement.FixedLengthLemmas Fiat.ADTNotation.BuildADT Fiat.ADTNotation.BuildADTSig Fiat.ADT.ComputationalADT Fiat.ADTRefinement Fiat.ADTRefinement.BuildADTRefinements.HoneRepresentation Fiat.ADTRefinement.GeneralBuildADTRefinements Fiat.Common Fiat.Common.Equality Fiat.Common.StringBound Fiat.Common.ilist Fiat.Common.IterateBoundedIndex Fiat.Common.List.FlattenList Fiat.Common.List.ListMorphisms Fiat.Common.List.ListFacts Fiat.Common.NatFacts Fiat.Common.StringFacts Fiat.Common.LogicFacts Fiat.Common.LogicMorphisms Fiat.Computation.SetoidMorphisms Fiat.Common.List.ListMorphisms Fiat.Common.Instances Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Common Fiat.Common.Enumerable Fiat.Common.Enumerable.BoolProp Fiat.Common.Enumerable.ReflectiveForall Fiat.Common.Enumerable.ReflectiveForallStaged