proposition: Lemma foldr_correct fv ft sv st : RelP sv st -> (forall xv yv, Rel xv dt -> Rel yv dt -> Rel (fv xv yv) dt) -> (forall xt yt, Rel dv xt -> Rel dv yt -> Rel dv (ft xt yt)) -> (forall xv xt yv yt, Rel xv xt -> Rel yv yt -> Rel (fv xv yv) (ft xt yt)) -> Rel (foldr fv dv sv) (foldr ft dt st).
proof: Proof. move=> Hs H0t H0v Hf. elim: sv st Hs => [ | xv sv IH1] st Hs /=. - elim: st Hs => [ | xt st IH2] Hs //=. apply: H0v; first by move/(_ 0): Hs. by apply: IH2 => k; move/(_ k.+1): Hs; rewrite /= nth_nil. - case: st Hs => [ | xt st] Hs /=. + apply: H0t; first by move/(_ 0): Hs. change dt with (foldr ft dt [::]). apply/IH1 => k. by move/(_ k.+1): Hs; rewrite /= nth_nil. + apply: Hf; first by move/(_ 0): Hs. apply: IH1. move=> k; by move/(_ k.+1): Hs. Qed.
imports: Coq(Rdefinitions Raxioms RIneq Rbasic_fun) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq bigop) MathComp1or2