This commit is contained in:
Thomas Baruchel 2022-12-28 18:47:14 +01:00
parent 3a48fbe5d0
commit 7c7bc16120

View File

@ -556,8 +556,7 @@ Proof.
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. apply Nat.lt_succ_diag_r.
assumption.
assert (G: k = 0 \/ 0 < k). apply Nat.eq_0_gt_0_cases.
destruct G as [G1|G2].
assert (G: k = 0 \/ 0 < k). apply Nat.eq_0_gt_0_cases. destruct G as [G1|G2].
(* k = 0 *)
rewrite G1. rewrite Nat.mul_0_l. rewrite Nat.add_0_l.
@ -631,6 +630,293 @@ Qed.
Lemma tm_step_pred : forall (n k m : nat),
S (2*k) * 2^m < 2^n -> (
nth_error (tm_step n) (S (2*k) * 2^m)
= nth_error (tm_step n) (S (2*k) * 2^m - 1)
<-> odd m = true).
Proof.
intros n k m.
generalize n. induction m. rewrite Nat.pow_0_r. rewrite Nat.mul_1_r.
destruct n0. rewrite Nat.pow_0_r. rewrite Nat.lt_1_r.
intro H. apply Nat.neq_succ_0 in H. contradiction H.
rewrite Nat.odd_0. rewrite Nat.sub_succ. rewrite Nat.sub_0_r.
rewrite <- tm_step_double_index. intro H. split. intro I.
symmetry in I. apply tm_step_succ_double_index in I. contradiction I.
apply Nat.lt_succ_l in H. rewrite Nat.pow_succ_r' in H.
rewrite <- Nat.mul_lt_mono_pos_l in H. assumption. apply Nat.lt_0_2.
intro I. apply diff_false_true in I. contradiction I.
intro n0. intro I.
destruct n0. rewrite Nat.pow_0_r in I. rewrite Nat.lt_1_r in I.
rewrite Nat.mul_eq_0 in I. destruct I.
apply Nat.neq_succ_0 in H. contradiction H.
apply Nat.pow_nonzero in H. contradiction H. easy.
rewrite Nat.pow_succ_r'. rewrite Nat.mul_assoc.
replace (S (2*k) * 2) with (2* (S (2*k))).
rewrite <- Nat.mul_assoc. rewrite <- tm_step_double_index.
(* réécriture de I *)
rewrite Nat.pow_succ_r' in I.
rewrite Nat.pow_succ_r' in I.
rewrite Nat.mul_assoc in I.
replace (S (2*k) * 2) with (2* (S (2*k))) in I.
rewrite <- Nat.mul_assoc in I.
rewrite <- Nat.mul_lt_mono_pos_l in I.
assert (J := I). apply IHm in J.
assert (M: 0 < 2^m). destruct m. simpl. apply Nat.lt_0_1.
replace (0) with (0 ^ (S m)) at 1.
apply Nat.pow_lt_mono_l. apply Nat.neq_succ_0. apply Nat.lt_0_2.
apply Nat.pow_0_l. apply Nat.neq_succ_0.
assert (L: S (2 * k) * 2 ^ m - 1 < S (2 * k) * 2 ^ m).
replace (S (2 * k) * 2 ^ m) with (S (S (2 * k) * 2 ^ m - 1)) at 2.
apply Nat.lt_succ_diag_r.
rewrite <- Nat.sub_succ_l. rewrite Nat.sub_1_r. rewrite pred_Sn.
reflexivity. rewrite Nat.le_succ_l. apply Nat.mul_pos_pos.
apply Nat.lt_0_succ. assumption.
assert (N: 2 * (S (2 * k) * 2 ^ m) - 1 < length (tm_step (S n0))).
rewrite tm_size_power2.
rewrite <- Nat.le_succ_l. rewrite <- Nat.add_1_r.
rewrite Nat.sub_add. rewrite Nat.pow_succ_r'.
rewrite <- Nat.mul_le_mono_pos_l.
apply Nat.lt_le_incl. assumption. apply Nat.lt_0_2.
apply Nat.le_succ_l. apply Nat.mul_pos_pos. apply Nat.lt_0_2.
apply Nat.mul_pos_pos. apply Nat.lt_0_succ.
assumption.
assert (nth_error (tm_step n0) ((S (2 * k) * 2 ^ m) - 1)
<> nth_error (tm_step (S n0)) (S (2 * (S (2 * k) * 2 ^ m - 1)))).
apply tm_step_succ_double_index.
generalize I. generalize L. apply Nat.lt_trans.
replace (S (2 * (S (2 * k) * 2 ^ m - 1))) with (2 * (S (2*k) * 2^m) - 1) in H.
rewrite Nat.odd_succ. rewrite <- Nat.negb_odd. destruct (odd m).
split. intro K. rewrite <- K in H.
destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m));
destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m - 1)).
destruct J. replace (Some b) with (Some b0) in H. contradiction H.
reflexivity. symmetry. apply H1. reflexivity.
destruct J. replace (Some b) with (None : option bool) in H.
contradiction H. reflexivity. symmetry. apply H1. reflexivity.
destruct J. replace (None : option bool) with (Some b) in H.
contradiction H. reflexivity. symmetry. apply H1. reflexivity.
contradiction H. reflexivity.
destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m));
destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m - 1)).
intro K. simpl in K. apply diff_false_true in K. contradiction K.
intro K. simpl in K. apply diff_false_true in K. contradiction K.
intro K. simpl in K. apply diff_false_true in K. contradiction K.
intro K. simpl in K. apply diff_false_true in K. contradiction K.
rewrite nth_error_nth' with (d := false) in J.
rewrite nth_error_nth' with (d := false) in J.
rewrite nth_error_nth' with (d := false) in H.
rewrite nth_error_nth' with (d := false) in H.
rewrite nth_error_nth' with (d := false).
rewrite nth_error_nth' with (d := false).
destruct (nth (S (2 * k) * 2 ^ m) (tm_step n0) false);
destruct (nth (S (2 * k) * 2 ^ m - 1) (tm_step n0) false);
destruct (nth (2 * (S (2 * k) * 2 ^ m) - 1) (tm_step (S n0)) false).
simpl; split; reflexivity.
destruct J. rewrite H0 in H. contradiction H. reflexivity.
reflexivity.
simpl; split; reflexivity. contradiction H. reflexivity.
contradiction H. reflexivity.
simpl; split; reflexivity.
destruct J. rewrite H0 in H. contradiction H. reflexivity.
reflexivity.
simpl; split; reflexivity.
assumption.
rewrite tm_size_power2. assumption.
assumption.
rewrite tm_size_power2. generalize I. generalize L.
apply Nat.lt_trans.
rewrite tm_size_power2. generalize I. generalize L.
apply Nat.lt_trans.
rewrite tm_size_power2. assumption.
rewrite Nat.mul_sub_distr_l. rewrite Nat.mul_1_r.
rewrite <- Nat.sub_succ_l.
replace (S (2 * (S (2 * k) * 2 ^ m))) with (2 * (S (2 * k) * 2 ^ m) + 1).
rewrite <- Nat.add_cancel_r with (p := 1).
rewrite Nat.sub_add.
destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m));
destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m - 1));
destruct (nth_error (tm_step (S n0)) (2 * (S (2 * k) * 2 ^ m) - 1)).
destruct (b); destruct (b0); destruct (b1).
split. reflexivity. reflexivity.
destruct J. rewrite H0 in H. contradiction H. reflexivity.
reflexivity. simpl. split; reflexivity.
contradiction H. reflexivity. contradiction H. reflexivity.
simpl. split; reflexivity.
destruct J. rewrite H0 in H. contradiction H. reflexivity.
reflexivity. contradiction H. reflexivity.
destruct (b); destruct (b0). destruct J. rewrite H0.
split. intro J. inversion J. destruct H0. reflexivity.
intro J. simpl in J. symmetry in J. apply diff_false_true in J.
contradiction J. reflexivity.
split. intro K. inversion K.
apply Nat.lt_0_2. apply Nat.mul_comm.
Lemma tm_step_repeating_patterns :
forall (n m i j : nat),
i < 2^m -> j < 2^m
-> forall k, k < 2^n -> nth_error (tm_step m) i
= nth_error (tm_step m) j
<-> nth_error (tm_step (m+n)) (k * 2^m + i)
= nth_error (tm_step (m+n)) (k * 2^m + j).
induction m. rewrite Nat.pow_0_r. rewrite Nat.mul_1_r.
rewrite Nat.odd_0. rewrite Nat.sub_succ. rewrite Nat.sub_0_r.
destruct n. rewrite Nat.pow_0_r. rewrite Nat.lt_1_r.
intro H. apply Nat.neq_succ_0 in H. contradiction H.
rewrite <- tm_step_double_index. intro H. split. intro I.
symmetry in I. apply tm_step_succ_double_index in I. contradiction I.
apply Nat.lt_succ_l in H. rewrite Nat.pow_succ_r' in H.
rewrite <- Nat.mul_lt_mono_pos_l in H. assumption. apply Nat.lt_0_2.
intro I. apply diff_false_true in I. contradiction I.
intro H.
- induction m.
+ rewrite Nat.pow_0_r. rewrite Nat.mul_1_r.
rewrite Nat.odd_0. rewrite Nat.sub_succ. rewrite Nat.sub_0_r.
destruct n. rewrite Nat.pow_0_r in H. rewrite Nat.mul_1_r in H.
rewrite Nat.lt_1_r in H. apply Nat.neq_succ_0 in H. contradiction H.
rewrite <- tm_step_double_index.
split.
intro I. symmetry in I.
apply tm_step_succ_double_index in I. contradiction I.
rewrite Nat.pow_0_r in H. rewrite Nat.mul_1_r in H.
apply Nat.lt_succ_l in H. rewrite Nat.pow_succ_r' in H.
rewrite <- Nat.mul_lt_mono_pos_l in H. assumption. apply Nat.lt_0_2.
intro I. apply diff_false_true in I. contradiction I.
+
split.
- induction m.
+ rewrite Nat.pow_0_r. rewrite Nat.mul_1_r.
rewrite Nat.odd_0. rewrite Nat.sub_succ. rewrite Nat.sub_0_r.
destruct n. rewrite Nat.pow_0_r in H. rewrite Nat.mul_1_r in H.
rewrite Nat.lt_1_r in H. apply Nat.neq_succ_0 in H. contradiction H.
rewrite <- tm_step_double_index. intro I. symmetry in I.
apply tm_step_succ_double_index in I. contradiction I.
rewrite Nat.pow_0_r in H. rewrite Nat.mul_1_r in H.
apply Nat.lt_succ_l in H. rewrite Nat.pow_succ_r' in H.
rewrite <- Nat.mul_lt_mono_pos_l in H. assumption. apply Nat.lt_0_2.
+
Theorem tm_step_stable : forall (n m k : nat),
k < 2^n -> k < 2^m -> nth_error (tm_step n) k = nth_error (tm_step m) k.
Theorem tm_step_double_index : forall (n k : nat),
nth_error (tm_step n) k = nth_error (tm_step (S n)) (2*k).
Theorem tm_step_succ_double_index : forall (n k : nat),
k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step (S n)) (S (2*k)).
Require Import BinPosDef.
Require Import BinNatDef.
Lemma tm_step_double_index_pos : forall (p : positive),
nth_error (tm_step (Pos.size_nat p)) (Pos.to_nat p) =
nth_error (tm_step (S (Pos.size_nat p))) (Pos.to_nat (p~0)).
Proof.
intro p.
simpl.
Theorem tm_step_double_index : forall (n k : nat),
nth_error (tm_step n) k = nth_error (tm_step (S n)) (2*k).
(*
From a(0) to a(2n+1), there are n+1 terms equal to 0 and n+1 terms equal to 1 (see Hassan Tarfaoui link, Concours Général 1990). - Bernard Schott, Jan 21 2022
TODO Search "count_occ"
*)
Theorem tm_step_count_occ : forall (hd tl : list bool) (k : nat),
tm_step k = hd ++ tl -> even (length hd) = true
-> count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false.
Proof.
intros hd tl k. intros H I.
destruct k.
- assert (J: hd = nil). destruct hd. reflexivity.
simpl in H. inversion H.
symmetry in H2. apply app_eq_nil in H2.
destruct H2. rewrite H0 in I. simpl in I. inversion I.
rewrite J. reflexivity.
- rewrite <- tm_step_lemma in H.
generalize I. generalize H. induction hd.
reflexivity.
rewrite <- length_zero_iff_nil. simpl.
PeanoNat.Nat.neq_succ_0: forall n : nat, S n <> 0
(* TODO: supprimer head_2 *)
(* vérifier si les deux sont nécessaires *)
@ -654,19 +940,12 @@ Definition hamming_weight_n (x: N) :=
| Npos x => hamming_weight_positive x
end.
Lemma hamming_weight_remove_high : forall (x : N),
(0 < x)%N -> hamming_weight_n x = S (hamming_weight_n (x - 2^(N.log2 x))).
Proof.
intros x.
N.shiftl_spec_alt:
forall a n m : N, N.testbit (N.shiftl a n) (m + n) = N.testbit a m
Lemma hamming_weight_positive_nonzero : forall (x: positive),