proposition: Lemma afold_right_ind : forall A OP def V (P : int -> A -> Prop), (length V = 0 -> P 0 def) -> (0 <? length V = true -> P (length V - 1) (V.[length V - 1])) -> (forall a i, 0 <? i = true -> i <? length V = true -> P i a -> P (i - 1) (OP (V.[i - 1]) a)) -> P 0 (afold_right A def OP V).
proof: Proof. intros A OP def V P HP0 HP1 HPOP. assert (BV := to_Z_bounded (length V)). unfold afold_right. case (reflect_eqb (length V) 0); [ intro Heq; apply HP0; exact Heq | intro Hneq ]. rewrite <- to_Z_eq, to_Z_0 in Hneq. replace 0 with (length V - length V) at 1 by ring. apply (foldi_ind _ (fun i a => P (length V - i) a)). rewrite leb_spec, to_Z_1; lia. apply HP1; rewrite ltb_spec, to_Z_0; lia. intros i a; assert (Bi := to_Z_bounded i). rewrite leb_spec, to_Z_1, ltb_spec; intros Hi1 Hi2 IH. replace (length V - (i + 1)) with (length V - i - 1) by ring. replace (length V - 1 - i) with (length V - i - 1) by ring. apply HPOP; [ rewrite ltb_spec, to_Z_0, sub_spec, Z.mod_small; lia | rewrite ltb_spec, sub_spec, Z.mod_small; lia | exact IH ]. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz