proposition: Lemma sext_wneg_natToWord'': forall sz1 sz2 n, pow2 sz1 <= 2 * n < pow2 (S sz1) -> sext (natToWord sz1 n) sz2 = natToWord (sz1 + sz2) (pow2 (sz1+sz2) - (pow2 sz1 - n)).
proof: Proof. induction sz1; intros. - unfold pow2 in H. lia. - unfold sext in *. assert (@wmsb (S sz1) (natToWord (S sz1) n) false = true) as E. { apply wmsb_1. rewrite wordToNat_natToWord_idempotent'; (unfold pow2 in *; fold pow2 in *; lia). } rewrite E. match goal with | |- _ = $ ?a => remember a as b end. simpl. unfold natToWord. f_equal. + subst b. rewrite mod2sub. * rewrite mod2sub. { replace (S sz1 + sz2) with (S (sz1 + sz2)) by lia. simpl. do 2 rewrite mod2_pow2_twice. do 2 rewrite Bool.xorb_false_l. reflexivity. } simpl in *. lia. * rewrite pow2_add_mul in *. unfold pow2 in *. fold pow2 in *. apply Nat.le_trans with (m := 2 * pow2 sz1); [lia|]. rewrite <- Nat.mul_assoc. apply Nat.mul_le_mono_l. rewrite <- Nat.mul_1_r at 1. apply Nat.mul_le_mono_l. apply one_le_pow2. + fold natToWord. specialize (IHsz1 sz2 (Nat.div2 n)). assert (Nat.div2 b = pow2 (sz1 + sz2) - (pow2 sz1 - (Nat.div2 n))) as D2. { rewrite minus_minus. - subst b. replace (S sz1 + sz2) with (S (sz1 + sz2)) by lia. unfold pow2. fold pow2. rewrite minus_minus. * rewrite <- Nat.mul_sub_distr_l. rewrite <- (Nat.add_comm n). rewrite div2_plus_2. apply Nat.add_comm. * rewrite pow2_add_mul. clear IHsz1. unfold pow2 in *. fold pow2 in *. split; [lia|]. apply Nat.mul_le_mono_l. rewrite <- Nat.mul_1_r at 1. apply Nat.mul_le_mono_l. apply one_le_pow2. - unfold pow2 in H. fold pow2 in H. split. * pose proof (@div2_compat_lt_l (pow2 sz1) n) as P. lia. * rewrite pow2_add_mul. clear IHsz1. rewrite <- Nat.mul_1_r at 1. apply Nat.mul_le_mono_l. apply one_le_pow2. } rewrite D2. destruct sz1 as [|sz1']. * simpl in H. assert (n=1) by lia. subst n. simpl in D2. simpl. apply wones_natToWord. * assert (n <= S (2 * Nat.div2 n))%nat. { destruct (even_odd_destruct n) as [[m C]|[m C]]; subst n. - rewrite Nat.div2_double. constructor. constructor. - replace (2 * m + 1) with (S (2 * m)) by lia. rewrite Nat.div2_succ_double. constructor. } rewrite <- IHsz1. { assert (@wmsb (S sz1') (natToWord (S sz1') (Nat.div2 n)) false = true) as F. { apply wmsb_1_natToWord. unfold pow2 in *. fold pow2 in *. assert (2 * Nat.div2 n <= n)%nat by apply two_times_div2_bound. clear -H H0 H1. lia. } { rewrite F. reflexivity. } } { assert (2 * Nat.div2 n <= n)%nat by apply two_times_div2_bound. clear -H H0 H1. unfold pow2 in *. fold pow2 in *. lia. } Qed.
imports: Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Classes.Equivalence Coq.Arith.PeanoNat Coq.ZArith.BinInt  Coq.Arith.Arith Coq.NArith.NArith Coq.Bool.Bool Coq.ZArith.ZArith Coq.Logic.Eqdep_dec Coq.Logic.EqdepFacts Coq.Program.Tactics Coq.Program.Equality Coq.setoid_ring.Ring Coq.setoid_ring.Ring_polynom bbv.Nomega bbv.ZLib bbv.NatLib bbv.NLib bbv.N_Z_nat_conversions bbv.DepEq bbv.DepEqNat bbv.ReservedNotations Coq.micromega.Lia