proposition: Lemma seq_foldri_correct fv ft sv st (zv := [::]) (zt := [::]) i : RelP sv st -> (forall xv yv i, Rel xv dt -> RelP yv zt -> RelP (fv xv i yv) zt) -> (forall xt yt i, Rel dv xt -> RelP zv yt -> RelP zv (ft xt i yt)) -> (forall xv xt yv yt i, Rel xv xt -> RelP yv yt -> RelP (fv xv i yv) (ft xt i yt)) -> RelP (foldri fv zv sv i) (foldri ft zt st i).
proof: Proof. move=> Hs H0t H0v Hf. elim: sv st Hs i => [ | xv sv IH1] st Hs i /=. - elim: st Hs i => [ | xt st IH2] Hs i //=. 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 zt with (foldri ft zt [::] i.+1). 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