proposition: Lemma afold_right_implb_false_inv : forall a, afold_right bool true implb a = false -> 0 <? length a = true /\ (forall i, i <? length a - 1 = true -> a .[ i] = true) /\ a.[length a - 1] = false.
proof: Proof. intros a H; assert (Ba := to_Z_bounded (length a)); split; [ | split ]. revert H; unfold afold_right. case (reflect_eqb (length a) 0). intro Heq; rewrite Heq; discriminate. rewrite <- to_Z_eq, to_Z_0; intros Hlength _. rewrite ltb_spec, to_Z_0; lia. intro i; generalize (leb_0 i); revert H i; apply afold_right_ind. discriminate. intros _ _ i; rewrite leb_spec, ltb_spec; lia. intros b j; assert (Bj := to_Z_bounded j). rewrite 2!ltb_spec, to_Z_0; intros Hj1 Hj2 IH. unfold implb; case_eq (a.[j - 1]); [ | discriminate ]; intros Ha H; subst b; intro i. case (reflect_eqb i (j - 1)). intro Heq; subst i; intros; exact Ha. rewrite <- to_Z_eq, to_Z_sub_1_0 by lia; intro Hneq. rewrite leb_spec, to_Z_sub_1_0 by lia; intro Hji. apply IH; [ reflexivity | rewrite leb_spec; lia ]. revert H; unfold afold_right. case (reflect_eqb (length a) 0). discriminate. rewrite <- to_Z_eq, to_Z_0; intro Hlength. apply (foldi_ind _ (fun i b => b = false -> a.[length a - 1] = false)). rewrite leb_spec, to_Z_1; lia. tauto. intros i b; assert (Bi := to_Z_bounded i). rewrite leb_spec, to_Z_1; intro Hi1. rewrite ltb_spec; intros Hi2 IH. unfold implb at 1; case (a.[length a - 1 - i]); [ exact IH | discriminate ]. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz