proposition: Lemma nth_error_default_to_nonterminal nt_idx : List.nth_error (pregrammar_productions G) nt_idx = if nt_idx <? List.length (pregrammar_productions G) then Some (default_to_nonterminal nt_idx, Lookup_idx G nt_idx) else None.
proof: Proof. destruct (nt_idx <? List.length (pregrammar_productions G)) eqn:Hlt. { apply Nat.ltb_lt in Hlt. unfold Lookup_idx, default_to_nonterminal. rewrite !nth_error_nth. repeat match goal with | _ => reflexivity | _ => discriminate | _ => omega | _ => break_innermost_match_step | _ => progress subst | _ => progress destruct_head' sig | _ => progress destruct_head' and | [ H : ?x = Some ?y, H' : ?x = Some ?z |- _ ] => assert (y = z) by congruence; (subst y || subst z) | [ H : ?x = Some _ |- ?x = _ ] => rewrite H | [ H : List.nth_error (List.map _ _) _ = Some _ |- _ ] => apply ListFacts.nth_error_map'_strong in H | [ H : List.nth_error (List.map ?f ?ls) ?idx = None |- _ ] => let H' := fresh in destruct (List.nth_error ls idx) eqn:H'; [ eapply List.map_nth_error in H'; rewrite H in H'; congruence | clear H ] | _ => progress destruct_head' prod | [ |- None = Some _ ] => exfalso | [ H : List.nth_error _ _ = None |- False ] => apply List.nth_error_None in H end. } { apply List.nth_error_None. apply Nat.ltb_ge in Hlt; assumption. } 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