proposition: Lemma FirstStep_preopt : refineADT (string_spec G HSL) rindexed_spec.
proof: Proof. refine (transitivityT _ _ _ _ FirstStep_helper_1). refine (transitivityT _ _ _ _ FirstStep_helper_2). unfold rindexed_spec', expanded_fallback_list', split_list_is_complete_alt. econstructor 1 with (AbsR := (fun r_o r_n => r_o =s r_n)); do_Iterate_Ensemble_BoundedIndex_equiv; try assumption; intros; [ setoid_subst_rel beq; try reflexivity.. | ]. { erewrite char_at_matches_correct by eassumption; reflexivity. } { apply unsafe_get_correct; assumption. } unfold split_list_is_complete_idx, split_list_is_complete, expanded_fallback_list'_body in *. intros. match goal with | [ H : context[length (substring ?n ?m ?s)] |- _ ] => let H' := fresh in assert (H' : length (substring n m s) = m) by (rewrite substring_length; fin_common; rewrite Nat.min_r by omega; omega); rewrite !H' in H |- * end. repeat match goal with | [ H : context[to_production_opt] |- _ ] => rewrite to_production_opt_correct in H | [ H : context[forall_reachable_productions_if_eq] |- _ ] => rewrite forall_reachable_productions_if_eq_correct_reachable in H by first [ assumption | exact _ ] | _ => progress simpl in * | _ => progress unfold rdp_list_to_production in * | [ H : default_to_production ?p = ?x :: ?xs, H' : context[?x::?xs] |- _] => rewrite <- H in H' | [ H : context[match ?e with _ => _ end], H' : ?e = _::_ |- _ ] => rewrite H' in H | [ H : context[match ?e with _ => _ end] |- _ ] => is_var e; destruct e | _ => progress unfold If_Then_Else, option_rect in * | [ H : context[match ?e with _ => _ end] |- _ ] => destruct e eqn:? | _ => unfold rdp_list_production_carrier_valid in *; congruence end. { fin2. } { fin2. } { fin2. } { repeat match goal with | [ H : parse_of_production _ _ (_::_) |- _ ] => (inversion H; clear H) | _ => progress subst | _ => erewrite <- has_only_terminals_length by eassumption | [ H : context[List.length _] |- _ ] => erewrite <- has_only_terminals_length in H by eassumption | _ => progress safe_setoid_subst_beq_r | _ => progress destruct_head or; try solve [ fin2 ]; [] | [ H : ?x = ?y |- _ ] => is_var y; subst y | [ H : ?x = ?y |- _ ] => is_var x; subst x | _ => rewrite Nat.min_r by omega | _ => progress fin2 | [ H : ?x = ?x |- _ ] => clear H end; repeat match goal with | [ H : _ = _ :> nat |- _ ] => revert H | [ H : _ <= _ |- _ ] => revert H end; clear -HSLP; intros; rewrite !drop_length, !substring_length, Nat.min_r, Nat.add_sub by omega; repeat match goal with | [ H : context[min] |- _ ] => revert H; apply Nat.min_case_strong | [ H : ?x = 1, H' : context[?x] |- _ ] => rewrite H in H' | [ H : ?x = 1 |- context[?x] ] => rewrite H | [ H : ?x <= ?y |- context[?x - ?y] ] => replace (x - y) with 0 by omega | _ => rewrite Nat.sub_0_r | _ => intro | _ => progress subst | [ H : ?x - ?y = ?z |- ?x - ?z = ?y ] => clear -H; omega | [ |- context[?x - ?y - (?x - ?z - ?y)] ] => replace (x - z - y) with (x - y - z) by omega | [ |- context[S (?x - S ?y)] ] => rewrite (Nat.sub_succ_r x y) | _ => progress rewrite ?sub_twice, ?Nat.sub_0_r | _ => erewrite <- S_pred by eassumption | _ => rewrite Nat.min_r by omega | _ => rewrite Nat.min_l by omega | _ => reflexivity end. } { repeat match goal with | [ H : parse_of_production _ _ (_::_) |- _ ] => (inversion H; clear H) | _ => progress subst | [ H : collapse_length_result ?e = Some _ |- _ ] => (revert H; case_eq e; simpl; [ try (intros; congruence).. ]; []) | _ => intro | [ H : length_of_any ?G _ ?nt = _, p : parse_of_item _ ?str (NonTerminal ?nt) |- _ ] => (pose proof (has_only_terminals_parse_of_item_length eq_refl H p); clear H) end; fin2. } { repeat match goal with | _ => progress fin_common | [ H : forall x y, ?z = x::y -> _, H' : ?x = _::_ |- _ ] => specialize (H _ _ H') | [ H : length ?x = _, H' : context[length ?x] |- _ ] => rewrite H in H' | _ => progress specialize_by assumption | _ => progress specialize_by (left; reflexivity) | _ => progress specialize_by (right; assumption) | [ H : context[length (substring _ 0 _)] |- _ ] => rewrite substring_length in H | _ => solve [ eauto with nocore ] | _ => progress safe_setoid_subst_beq_r | _ => progress specialize_by (exact eq_refl) | [ H : ?x = ?y |- _ ] => is_var y; progress subst y end. } { repeat match goal with | [ H : parse_of_production _ _ (_::_) |- _ ] => (inversion H; clear H) | _ => progress subst | [ H : collapse_length_result ?e = Some _ |- _ ] => (revert H; case_eq e; simpl; [ try (intros; congruence).. ]; []) | _ => intro | [ H : length_of_any ?G _ ?nt = _, p : parse_of_item _ ?str (NonTerminal ?nt) |- _ ] => (pose proof (has_only_terminals_parse_of_item_length eq_refl H p); clear H) end; fin2. } { repeat match goal with | _ => progress fin_common | [ H : forall x y, ?z = x::y -> _, H' : ?x = _::_ |- _ ] => specialize (H _ _ H') | [ H : length ?x = _, H' : context[length ?x] |- _ ] => rewrite H in H' | _ => progress specialize_by assumption | _ => progress specialize_by (left; reflexivity) | _ => progress specialize_by (right; assumption) | _ => solve [ eauto with nocore ] | _ => progress safe_setoid_subst_beq_r | _ => progress specialize_by (exact eq_refl) | [ H : ?x = ?y |- _ ] => is_var y; progress subst y 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