proposition: Lemma rdp_list_to_production_opt_sig x : { f : _ | rdp_list_to_production (G := G) x = f }.
proof: Proof. eexists. set_evars. unfold rdp_list_to_production at 1. cbv beta iota delta [Carriers.default_to_production productions production]. simpl @Lookup. match goal with | [ |- (let a := ?av in let b := @?bv a in let c := @?cv a b in let d := @?dv a b c in let e := @?ev a b c d in @?v a b c d e) = ?R ] => change (Let_In av (fun a => Let_In (bv a) (fun b => Let_In (cv a b) (fun c => Let_In (dv a b c) (fun d => Let_In (ev a b c d) (fun e => v a b c d e))))) = R); cbv beta end. lazymatch goal with | [ |- Let_In ?x ?P = ?R ] => subst R; refine (@Let_In_Proper _ _ x _ _ _); intro; set_evars end. unfold Lookup_idx. symmetry; rewrite_map_nth_rhs; symmetry. repeat match goal with | [ |- context G[@Let_In ?A ?B ?k ?f] ] => first [ let h := head k in constr_eq h @nil | constr_eq k 0 | constr_eq k (snd (snd x)) ]; test pose f; let c := constr:(@Let_In A B k) in let c' := (eval unfold Let_In' in c) in let G' := context G[c' f] in change G'; simpl end. rewrite drop_all by (simpl; omega). unfold productions, production. rewrite <- nth'_nth at 1. rewrite map_map; simpl. match goal with | [ H := ?e |- _ ] => is_evar e; subst H end. match goal with | [ |- nth' ?a ?ls ?d = ?e ?a ] => refine (_ : inner_nth' a ls d = (fun a' => inner_nth' a' _ d) a); cbv beta; apply f_equal2; [ clear a | reflexivity ] end. etransitivity. { apply (_ : Proper (pointwise_relation _ _ ==> eq ==> eq) (@List.map _ _)); [ intro | reflexivity ]. do 2 match goal with | [ |- Let_In ?x ?P = ?R ] => refine (@Let_In_Proper _ _ x _ _ _); intro end. etransitivity. { symmetry; rewrite_map_nth_rhs; symmetry. unfold Let_In' at 2 3 4; simpl. set_evars. rewrite drop_all by (simpl; omega). unfold Let_In'. rewrite <- nth'_nth. change @nth' with @inner_nth'. subst_body; reflexivity. } reflexivity. } reflexivity. Defined.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Strings.String Coq.Arith.Compare_dec Coq.Arith.Wf_nat Coq.Arith.PeanoNat Fiat.Common.List.Operations Fiat.Common.List.ListMorphisms Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ContextFreeGrammar.Properties Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Parsers.BaseTypes Fiat.Parsers.BaseTypesLemmas Fiat.Parsers.CorrectnessBaseTypes Fiat.Common Fiat.Common.Wf Fiat.Common.Wf2 Fiat.Common.Telescope.Core Fiat.Parsers.GenericRecognizerExt Fiat.Parsers.BooleanRecognizer Fiat.Parsers.BooleanRecognizerExt Fiat.Parsers.BooleanRecognizerCorrect Fiat.Parsers.Splitters.RDPList Fiat.Parsers.ContextFreeGrammar.Valid Fiat.Parsers.ContextFreeGrammar.ValidReflective Fiat.Parsers.ContextFreeGrammar.Reflective Fiat.Parsers.ContextFreeGrammar.ReflectiveLemmas Fiat.Parsers.RecognizerPreOptimized Fiat.Common.Match Fiat.Common.List.ListFacts Fiat.Common.Equality Fiat.Common.SetoidInstances Fiat.Common.List.ListMorphisms Fiat.Common.OptionFacts Fiat.Common.BoolFacts Fiat.Common.NatFacts Fiat.Common.Sigma Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties