proposition: Lemma afold_right_implb_true_inv : forall a, afold_right bool true implb a = true -> length a = 0 \/ (exists i, i <? length a - 1 = true /\ a.[i] = false) \/ (forall i, i <? length a = true -> a.[i] = true).
proof: Proof. intros a H; cut (length a = 0 \/ (exists i, 0 <=? i = true /\ i <? length a - 1 = true /\ a.[i] = false) \/ (forall i, 0 <=? i = true -> i <? length a = true -> a.[i] = true)). clear H; intro H; destruct H as [ H | H ]. left; tauto. destruct H as [ H | H ]. destruct H as [ i [ Hi1 Hi2 ] ]. right; left; exists i; tauto. right; right; intro i; apply H; apply leb_0. assert (Ba := to_Z_bounded (length a)). revert H; apply afold_right_ind. left; tauto. rewrite ltb_spec, to_Z_0; intro Hlength. intro Ha; right; right. intro i; assert (Bi := to_Z_bounded i). rewrite leb_spec, to_Z_sub_1_0 by lia; intro Hi1. rewrite ltb_spec; intro Hi2. replace i with (length a - 1) by (rewrite <- to_Z_eq, to_Z_sub_1_0; lia); exact Ha. intros b i; assert (Bi := to_Z_bounded i). rewrite ltb_spec, to_Z_0; intro Hi1. rewrite ltb_spec; intros Hi2 IH. case_eq (a.[i - 1]); unfold implb. intros Ha Hb; destruct (IH Hb) as [ Heq | H ]; clear IH. rewrite Heq in Hi2; lia. destruct H as [ [ j [ Hij Hj ] ] | H ]. right; left; exists j. split; [ | exact Hj ]. revert Hij; rewrite 2!leb_spec, to_Z_sub_1_0; lia. right; right; intro j. rewrite leb_spec, sub_spec, to_Z_1, Z.mod_small by lia; intro Hij. rewrite ltb_spec; intro Hj. case (reflect_eqb j (i - 1)). intro Heq; rewrite Heq; exact Ha. rewrite <- to_Z_eq, to_Z_sub_1_0 by lia; intro Hneq. apply H; [ rewrite leb_spec; lia | rewrite ltb_spec; lia ]. intros Ha _; right; left; exists (i - 1). split; [ rewrite leb_spec; lia | ]. split; [ rewrite ltb_spec, 2!to_Z_sub_1_0; lia | exact Ha ]. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz