proposition: Lemma default_find_to_nonterminal idx : List.first_index_error (string_beq (default_to_nonterminal idx)) valid_nonterminals = bool_rect (fun _ => option _) (Some idx) (None) (Compare_dec.leb (S idx) (List.length valid_nonterminals)).
proof: Proof. pose proof (nonterminals_unique G) as HNoDup. hnf in HNoDup. unfold pregrammar_nonterminals in *. destruct (Compare_dec.leb (S idx) (List.length valid_nonterminals)) eqn:H0; simpl; [ apply Compare_dec.leb_complete in H0 | apply Compare_dec.leb_complete_conv in H0 ]. { generalize dependent idx. unfold default_to_nonterminal, default_to_nonterminal, Valid_nonterminals, grammar_of_pregrammar, pregrammar_nonterminals. replace valid_nonterminals with (uniquize string_beq valid_nonterminals) by (rewrite HNoDup; reflexivity). induction valid_nonterminals as [|x xs IHxs]. { simpl; intros; omega. } { simpl. simpl in *. destruct (list_bin string_beq x (uniquize string_beq xs)) eqn:H''; try assumption. { apply (f_equal (@List.length _)) in HNoDup. simpl in *. pose proof (uniquize_shorter xs string_beq) as H'. rewrite HNoDup in H'. exfalso; clear -H'. omega. } apply (f_equal (@List.tl _)) in HNoDup; simpl in *. specialize (IHxs HNoDup). intros [|idx]. { simpl. rewrite (string_lb eq_refl); trivial. } { simpl; intros H'. specialize (IHxs idx (proj2 (Nat.succ_le_mono _ _) H')). rewrite first_index_helper_first_index_error, IHxs by omega. apply first_index_error_Some_correct in IHxs. repeat match goal with | _ => exact (@string_lb) | _ => progress simpl in * | [ H : and _ _ |- _ ] => destruct H | [ H : ex _ |- _ ] => destruct H | [ |- context[if ?E then _ else _] ] => destruct E eqn:? | _ => reflexivity | [ |- Some _ = Some _ ] => apply f_equal | [ |- 0 = S _ ] => exfalso | [ H : string_beq _ _ = true |- _ ] => apply string_bl in H | _ => progress subst | [ H : _ = ?x |- _ ] => is_var x; subst x | [ H : S _ = S _ |- _ ] => apply (f_equal pred) in H | [ H : List.length (uniquize _ _) = List.length _ |- _ ] => apply uniquize_length in H | [ H : uniquize ?beq ?ls = ?ls, H' : context[uniquize ?beq ?ls] |- _ ] => rewrite H in H' | [ H : list_bin _ _ _ = false |- False ] => rewrite list_in_lb in H; [ discriminate | | ] | [ |- List.In (List.nth _ _ _) _ ] => apply List.nth_In; omega | [ |- context[List.nth_error ?n ?ls] ] => destruct (List.nth_error n ls) eqn:? | _ => congruence | _ => progress unfold BoolFacts.Bool.bool_rect_nodep in * end. } } } { unfold default_to_nonterminal, default_to_nonterminal. simpl. rewrite List.nth_overflow by omega. apply first_index_error_None_correct; intros elem H''. destruct (string_beq some_invalid_nonterminal elem) eqn:H'''; trivial. apply string_bl in H'''. subst. apply some_invalid_nonterminal_invalid' in H''; destruct H''. } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Common.Enumerable Fiat.Common.Enumerable.BoolProp Fiat.Common.List.Operations Fiat.Common.List.ListFacts Fiat.Common.Equality Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Common.Gensym Fiat.Common.Tactics.BreakMatch Fiat.Common.Tactics.DestructHead