proposition: Lemma grec1up_correct (A := seq V) Fi (F : A -> nat -> A) Gi (G : A -> nat -> V) ai a si s n : (forall qi q m, RelP q qi -> RelP (F q m) (Fi qi m)) -> (forall qi q m, RelP q qi -> Rel (G q m) (Gi qi m)) -> RelP a ai -> RelP s si -> size s = size si -> RelP (grec1up F G a s n) (grec1up Fi Gi ai si n).
proof: Proof. move=> HF HG Ha Hs Hsize k. pose s1 := (size (grec1up F G a s n)).-1. case: (ltnP n k) => Hnk; first by rewrite !nth_default ?size_grec1up. have H1 : k = (size (grec1up F G a s k)).-1 by rewrite size_grec1up. have H2 : k = (size (grec1up Fi Gi ai si k)).-1 by rewrite size_grec1up. rewrite ?(@nth_grec1up_indep _ _ _ _ _ _ dv dv n k k) ?(@nth_grec1up_indep _ _ _ _ _ _ dt dt n k k) //. case: (ltnP k (size s)) => Hk. - have Hki : k < size si by rewrite -Hsize. rewrite ?(grec1up_init _ _ _ Hk, grec1up_init _ _ _ Hki) ?nth_take_dflt ltnn. exact: Hs. - have Hki : size si <= k by rewrite -Hsize. rewrite {4}H2 {2}H1 !nth_last !last_grec1up ?head_gloop1 // Hsize. apply: HG => j; set l := k - size si. elim: l j => [|l IHl] j /=; by [apply: Ha | apply: HF; apply: IHl]. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp