proposition: Lemma afold_left_ind : forall A OP def V (P : int -> A -> Prop), (length V = 0 -> P 0 def) -> (0 <? length V = true -> P 1 (V.[0])) -> (forall a i, 0 <? i = true -> i <? length V = true -> P i a -> P (i + 1) (OP a (V.[i]))) -> P (length V) (afold_left A def OP V).
proof: Proof. intros A OP def V P HP0 HP1 HPOP. assert (BV := to_Z_bounded (length V)). unfold afold_left. case (reflect_eqb (length V) 0); [ intro Heq; rewrite Heq; tauto | intro Hneq ]. rewrite <- to_Z_eq, to_Z_0 in Hneq. apply foldi_ind. 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. apply HPOP; [ rewrite ltb_spec, to_Z_0; lia | rewrite ltb_spec; lia | exact IH ]. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz