From becbd874aeee6a6e73139d56c97e23f29c35a727 Mon Sep 17 00:00:00 2001 From: vblot <24938579+vblot@users.noreply.github.com> Date: Wed, 23 Jun 2021 13:51:01 +0200 Subject: foldi_iter --- src/Misc.v | 52 +++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 39 insertions(+), 13 deletions(-) diff --git a/src/Misc.v b/src/Misc.v index ff2366a..91ff342 100644 --- a/src/Misc.v +++ b/src/Misc.v @@ -351,27 +351,53 @@ Proof. rewrite leb_spec, sub_spec, Z.mod_small; lia. Qed. -Definition foldi {A : Type} (f : int -> A -> A) (from to : int) (a : A) : A := - let fix foldi_rec (n : nat) (a : A) : A := - match n with - | O => a - | S m => foldi_rec m (f (to - of_Z (Z.of_nat n)) a) - end in - foldi_rec (Z.to_nat (to_Z to) - Z.to_nat (to_Z from))%nat a. +Definition firstr i := negb((i land 1) == 0). +Fixpoint recr_aux (n:nat)(A:Type)(case0:A)(caserec:bool->int->A->A) + (i:int) : A := + match n with + | O => case0 + | S next => + if i == 0 then + case0 + else + let si := i >> 1 in + caserec (firstr i) si (recr_aux next A case0 caserec si) + end. +Definition recr := recr_aux size. +Definition iter_int63 i A f := + recr (A->A) (fun x => x) + (fun b si rec => if b + then fun x => f (rec (rec x)) + else fun x => rec (rec x)) + i. + +Definition foldi_cont + {A B : Type} + (f : int -> (A -> B) -> A -> B) + (from to : int) + (cont : A -> B) : A -> B := + if to <= from then + cont + else + let (_,r) := iter_int63 (to - from) _ (fun (jy: (int * (A -> B))%type) => + let (j,y) := jy in (j - 1, f (j - 1) y) + ) (to, cont) in r. + +Definition foldi {A} (f:int -> A -> A) from to := + foldi_cont (fun i cont a => cont (f i a)) from to (fun a => a). Lemma foldi_ge : forall A f from to (a:A), to <= from = true -> foldi f from to a = a. Proof. - intros A f from to a; unfold foldi. - assert (Bfrom := to_Z_bounded from); assert (Bto := to_Z_bounded to). - rewrite leb_spec, Z2Nat.inj_le by lia; intro Hle. - replace (_ - _)%nat with O by lia; tauto. + intros A f from to a; unfold foldi, foldi_cont. + intro H; rewrite H; reflexivity. Qed. Lemma foldi_lt_l : forall A f from to (a:A), from < to = true -> foldi f from to a = foldi f (from + 1) to (f from a). Proof. - intros A f from to a; rewrite ltb_spec; intro Hlt; unfold foldi. +Admitted. +(* intros A f from to a; rewrite ltb_spec; intro Hlt; unfold foldi, foldi_cont. assert (Bfrom := to_Z_bounded from); assert (Bto := to_Z_bounded to). rewrite <- Nat.sub_succ. rewrite Nat.sub_succ_l by (rewrite Nat.le_succ_l, <- Z2Nat.inj_lt; lia); f_equal. @@ -381,7 +407,7 @@ Proof. rewrite Nat.sub_succ, <- Z2Nat.inj_sub, Z2Nat.id by lia. apply to_Z_inj; rewrite sub_spec, of_Z_spec, <- 2!sub_spec; f_equal; ring. Qed. - + *) Lemma foldi_lt_r : forall A f from to (a:A), from < to = true -> foldi f from to a = f (to - 1) (foldi f from (to - 1) a). Proof. -- cgit From 772f19d20ec6af11259c1aea2095547944d63086 Mon Sep 17 00:00:00 2001 From: vblot <24938579+vblot@users.noreply.github.com> Date: Wed, 16 Feb 2022 15:20:43 +0100 Subject: simpler foldi_iter --- src/Misc.v | 293 ++++++++++++++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 251 insertions(+), 42 deletions(-) diff --git a/src/Misc.v b/src/Misc.v index 91ff342..8f082f1 100644 --- a/src/Misc.v +++ b/src/Misc.v @@ -351,63 +351,272 @@ Proof. rewrite leb_spec, sub_spec, Z.mod_small; lia. Qed. -Definition firstr i := negb((i land 1) == 0). -Fixpoint recr_aux (n:nat)(A:Type)(case0:A)(caserec:bool->int->A->A) - (i:int) : A := +Lemma bit_sub1_0 : forall i, bit (i - 1) 0 = negb (bit i 0). +Proof. +intro i. +cut (b2i (bit (i - 1) 0) = b2i (negb (bit i 0))). +generalize (bit (i - 1) 0) (negb (bit i 0)); intros b1 b2. +destruct b1; destruct b2; simpl; rewrite <- eqb_spec; trivial; discriminate. +replace (b2i (negb (bit i 0))) with (1 - bit i 0); [ | destruct (bit i 0); reflexivity ]. +rewrite <- to_Z_eq. +rewrite sub_spec, to_Z_1. +rewrite 2!bit_0_spec. +rewrite sub_spec, to_Z_1. +case_eq (i == 0). +rewrite eqb_spec; intro Hi; rewrite Hi; reflexivity. +rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_0. +generalize (to_Z_bounded i). +intros Hi1 Hi2. +rewrite (Zmod_small _ wB); [ | lia ]. +assert (0 <= to_Z i mod 2 < 2)%Z. +apply Z_mod_lt; lia. +rewrite (Zmod_small _ wB); [ | lia ]. +rewrite 2!Zmod_even. +rewrite Z.even_sub. +case (Z.even (to_Z i)). +reflexivity. +reflexivity. +Qed. + +Lemma sub1_lsr : forall i, i <> 0 -> (i - 1) >> 1 = if bit i 0 then i >> 1 else i >> 1 - 1. +intro i. +rewrite <- to_Z_eq, to_Z_0; intro Hi0. +assert (Hi : (0 < to_Z i < wB)%Z). +generalize (to_Z_bounded i); lia. +clear Hi0. +rewrite <- to_Z_eq. +rewrite lsr_spec, to_Z_sub_1_0, to_Z_1; [ | lia ]. +case_eq (bit i 0); intro Hibit. +rewrite lsr_spec, to_Z_1. +change (2 ^ 1)%Z with 2%Z. +rewrite to_Z_split. +rewrite Hibit. +rewrite <- Z.add_sub_assoc. +change (to_Z true) with 1%Z. +replace (1 - 1)%Z with 0%Z by ring. +rewrite 2!Z.div_add_l; [ reflexivity | lia | lia ]. +rewrite to_Z_sub_1_0. +rewrite lsr_spec, to_Z_1. +change (2 ^ 1)%Z with 2%Z. +rewrite to_Z_split. +rewrite Hibit. +rewrite <- Z.add_sub_assoc. +change (to_Z false) with 0%Z. +rewrite 2!Z.div_add_l; [ | lia | lia ]. +rewrite <- Z.add_sub_assoc; reflexivity. +rewrite lsr_spec. +change (2 ^ to_Z 1)%Z with 2%Z. +apply Z.div_str_pos. +split; [ lia | ]. +cut (to_Z i <> 1)%Z; [ lia | ]. +change 1%Z with (to_Z 1). +rewrite to_Z_eq. +intro H; rewrite H in Hibit; discriminate. +Qed. + +Lemma pow2_lsr : forall i n, + (to_Z i < 2 ^ Z.of_nat (S n))%Z -> (to_Z (i >> 1) < 2 ^ Z.of_nat n)%Z. +Proof. +intros i n Hi. +rewrite lsr_spec. +change (2 ^ to_Z 1)%Z with 2%Z. +apply (Zmult_lt_reg_r _ _ 2); [ lia | ]. +rewrite Zmult_comm. +apply (Z.le_lt_trans _ (to_Z i)). +apply Z.mul_div_le; lia. +rewrite <- two_power_nat_equiv in *. +rewrite two_power_nat_S in Hi. +rewrite Zmult_comm; assumption. +Qed. + +Lemma pow2_size : forall i, (to_Z i < 2 ^ Z.of_nat size)%Z. +Proof. +intro i. +change (2 ^ Z.of_nat size)%Z with wB. +generalize (to_Z_bounded i); lia. +Qed. + +Fixpoint iter_int63_aux (n : nat) (i : int) (A : Type) (f : A -> A) : A -> A := match n with - | O => case0 - | S next => - if i == 0 then - case0 - else - let si := i >> 1 in - caserec (firstr i) si (recr_aux next A case0 caserec si) + | O => fun x => x + | S n => + if i == 0 then fun x => x + else let g := iter_int63_aux n (i >> 1) A f in + fun x => if bit i 0 then f (g (g x)) else g (g x) end. -Definition recr := recr_aux size. -Definition iter_int63 i A f := - recr (A->A) (fun x => x) - (fun b si rec => if b - then fun x => f (rec (rec x)) - else fun x => rec (rec x)) - i. - -Definition foldi_cont - {A B : Type} - (f : int -> (A -> B) -> A -> B) + +Definition iter_int63 := iter_int63_aux size. + +Lemma iter_int63_aux_comm : forall n i A f a, + (to_Z i < 2 ^ Z.of_nat n)%Z -> + iter_int63_aux n i A f (f a) = f (iter_int63_aux n i A f a). +Proof. +intros n i A f; revert i; induction n. +intros i a Hi. +assert (i = 0). +rewrite <- to_Z_eq, to_Z_0. +generalize (to_Z_bounded i); lia. +reflexivity. +intros i a Hi; simpl. +case (i == 0); [ reflexivity | ]. +rewrite IHn; [ | apply pow2_lsr; assumption]. +rewrite IHn; [ | apply pow2_lsr; assumption]. +case (bit i 0); reflexivity. +Qed. + +Lemma iter_int63_comm : forall i A f a, + iter_int63 i A f (f a) = f (iter_int63 i A f a). +Proof. +intros i A f a. +unfold iter_int63. +apply iter_int63_aux_comm. +apply pow2_size. +Qed. + +Lemma iter_int63_aux_S : forall n i A f a, + (0 < to_Z i < 2 ^ Z.of_nat n)%Z -> + iter_int63_aux n i A f a = f (iter_int63_aux n (i - 1) A f a). +Proof. +intros n i A f; revert i; induction n; intros i a Hi. +{ + lia. +} +simpl. +replace (i == 0) with false. +{ + rewrite bit_sub1_0, sub1_lsr. + { + case_eq (bit i 0); simpl. + { + intros _. + case_eq (i == 1). + { + rewrite eqb_spec; intro H; rewrite H in *; clear i H. + case n; reflexivity. + } + rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_1; intro Hi1. + replace (i - 1 == 0) with false. + { + reflexivity. + } + symmetry. + rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_sub_1_0, to_Z_0; lia. + } + intro Hibit. + case_eq (i == 1). + { + rewrite eqb_spec; intro H; rewrite H in *; clear i H; discriminate. + } + rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_1; intro Hi1. + replace (i - 1 == 0) with false. + { + case_eq (i == 2). + { + rewrite eqb_spec; intro H; rewrite H in *; clear i H. + destruct n; [ lia | ]. + case n; reflexivity. + } + rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq. + change (to_Z 2) with 2%Z; intro Hi2. + rewrite (IHn (i >> 1)). + { + rewrite (IHn (i >> 1)). + { + f_equal. + apply iter_int63_aux_comm. + replace (i >> 1 - 1) with ((i - 1) >> 1). + { + apply pow2_lsr. + rewrite to_Z_sub_1_0; lia. + } + rewrite sub1_lsr, Hibit; [ reflexivity | ]. + rewrite <- to_Z_eq, to_Z_0; lia. + } + split. + { + rewrite lsr_spec, to_Z_1. + change (2 ^ 1)%Z with 2%Z. + apply Z.div_str_pos; lia. + } + apply pow2_lsr; lia. + } + split. + { + rewrite lsr_spec, to_Z_1. + change (2 ^ 1)%Z with 2%Z. + apply Z.div_str_pos; lia. + } + apply pow2_lsr; lia. + } + symmetry. + rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_sub_1_0, to_Z_0; lia. + } + rewrite <- to_Z_eq, to_Z_0; lia. +} +symmetry. +rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_0; lia. +Qed. + +Lemma iter_int63_S : forall i A f a, 0 < i = true -> iter_int63 i A f a = f (iter_int63 (i - 1) A f a). +Proof. +intros i A f a. +rewrite ltb_spec, to_Z_0; intro Hi. +unfold iter_int63. +apply iter_int63_aux_S. +split; [ lia | ]. +apply pow2_size. +Qed. + +Definition foldi + {A : Type} + (f : int -> A -> A) (from to : int) - (cont : A -> B) : A -> B := + (a : A) + : A := if to <= from then - cont + a else - let (_,r) := iter_int63 (to - from) _ (fun (jy: (int * (A -> B))%type) => - let (j,y) := jy in (j - 1, f (j - 1) y) - ) (to, cont) in r. - -Definition foldi {A} (f:int -> A -> A) from to := - foldi_cont (fun i cont a => cont (f i a)) from to (fun a => a). + let (_,r) := iter_int63 (to - from) _ (fun (jy: (int * A)%type) => + let (j,y) := jy in (j + 1, f j y) + ) (from, a) in r. Lemma foldi_ge : forall A f from to (a:A), to <= from = true -> foldi f from to a = a. Proof. - intros A f from to a; unfold foldi, foldi_cont. + intros A f from to a; unfold foldi. intro H; rewrite H; reflexivity. Qed. Lemma foldi_lt_l : forall A f from to (a:A), from < to = true -> foldi f from to a = foldi f (from + 1) to (f from a). Proof. -Admitted. -(* intros A f from to a; rewrite ltb_spec; intro Hlt; unfold foldi, foldi_cont. - assert (Bfrom := to_Z_bounded from); assert (Bto := to_Z_bounded to). - rewrite <- Nat.sub_succ. - rewrite Nat.sub_succ_l by (rewrite Nat.le_succ_l, <- Z2Nat.inj_lt; lia); f_equal. - rewrite to_Z_add_1_wB, Z.add_1_r, Z2Nat.inj_succ by lia; reflexivity. - f_equal. - rewrite <- Nat.sub_succ_l by (rewrite Nat.le_succ_l, <- Z2Nat.inj_lt; lia). - rewrite Nat.sub_succ, <- Z2Nat.inj_sub, Z2Nat.id by lia. - apply to_Z_inj; rewrite sub_spec, of_Z_spec, <- 2!sub_spec; f_equal; ring. -Qed. - *) +intros A f from to a Hfromto. +pose proof (to_Z_bounded from) as Hfrom. +pose proof (to_Z_bounded to) as Hto. +unfold foldi. +rewrite leb_negb_gtb. +rewrite Hfromto; simpl. +rewrite ltb_spec in Hfromto. +case_eq (to <= from + 1). +rewrite leb_spec, to_Z_add_1_wB; [ | lia ]. +intro Htofrom. +assert (H : to = from + 1). +rewrite <- to_Z_eq. +rewrite to_Z_add_1_wB; lia. +rewrite H; clear H. +replace (from + 1 - from) with 1 by ring. +rewrite iter_int63_S; [ | reflexivity ]. +change (1 - 1) with 0. +reflexivity. +replace (to - (from + 1)) with (to - from - 1) by ring. +rewrite iter_int63_S. +rewrite (iter_int63_comm _ _ + (fun jy : int * A => let (j, y) := jy in (j + 1, f j y)) + (from, a)). +reflexivity. +rewrite ltb_spec, to_Z_0, sub_spec, Zmod_small; lia. +Qed. + Lemma foldi_lt_r : forall A f from to (a:A), from < to = true -> foldi f from to a = f (to - 1) (foldi f from (to - 1) a). Proof. -- cgit