proposition: Lemma refine_opt2_fold_right_no_unif base ls : make_tower_no_unif base ls (fun x => x) (refine (x0 <- opt2.fold_right (fun x else_case => If test x Then test_true x Else else_case) base ls; r_o x0) retv).
proof: Proof. pose proof (refine_opt2_fold_right base ls) as H. induction ls as [|x xs IHxs]. { exact H. } { simpl in *. repeat match goal with | _ => assumption | [ |- context[If test ?x Then _ Else _] ] => destruct (test x) eqn:? | _ => progress simpl in * | [ |- context[match ?e with _ => _ end] ] => destruct e eqn:? | _ => apply make_tower_const; reflexivity | _ => apply make_tower_no_unif_const; first [ reflexivity | assumption ] | _ => progress intros | _ => progress specialize_by (exact eq_refl) | _ => progress specialize_by assumption | _ => solve [ eauto with nocore ] end. } Qed.
imports: Coq.Strings.String Fiat.Common.List.ListFacts Fiat.ADTNotation.BuildADT Fiat.ADTNotation.BuildADTSig Fiat.ADT.ComputationalADT Fiat.ADTRefinement Fiat.ADTRefinement.BuildADTRefinements.HoneRepresentation Fiat.Parsers.ParserADTSpecification Fiat.Parsers.Refinement.IndexedAndAtMostOneNonTerminalReflective Fiat.Parsers.StringLike.Core Fiat.Parsers.ContextFreeGrammar.Precompute Fiat.Parsers.BaseTypes Fiat.Parsers.Splitters.RDPList Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Parsers.ContextFreeGrammar.PreNotations