Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • hamelin/jscoq-light
  • rousselin/jscoq-light
2 results
Show changes
Showing
with 3565 additions and 0 deletions
.PHONY: all get
all:
# not parallel: some Dune dependency mixup with generating META file
dune build -j1
# addon-equations
Coq-Equations addon plugin for jsCoq
(rule
(targets coq-pkgs)
(deps
(package teach)
(:pkg-json teach-pkg.json))
(action
(run jscoq build %{pkg-json})))
(dirs workdir)
\ No newline at end of file
{
"name": "@jscoq/teach",
"description": "Teach coq",
"version": "0.1.0",
"files": ["README.md", "coq-pkgs"],
"repository": {
"type": "git",
"url": "https://gitlab.inria.fr/dhamelin/test-jscoq-addon"
},
"license": "AGPL-3.0-or-later"
}
{
"rootdir": "workdir",
"builddir": "coq-pkgs",
"projects": {
"teach": {
"theories": {
"prefix": "Teach"
}
}
}
}
.DS_Store
.~lock*
*.swp
*.aux
*.fdb_latexmk
*.fls
*.log
*.out
*.synctex.gz
*.toc
*.vrb
_minted*
*.nav
*.snm
*.vo
*.vok
*.vos
*.glob
*.bbl
*.blg
.*.aux
.*.cache
*cache
.*Makefile.d
*Makefile*
coq-num-analysis
article.pdf
(lang dune 2.5)
(using coq 0.2)
(name teach)
\ No newline at end of file
opam-version: "2.0"
version: "8.16.dev"
build: [
[make "-j%{jobs}%"]
]
install: [
[make "install"]
]
depends: [
"coq" { >= "8.16~" & < "8.17~" }
"ocamlfind" {build}
]
(**
This file is part of the coq-teach library
Copyright (C) Boldo, Clément, Hamelin, Mayero, Rousselin
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
From Coq.ZArith Require Import BinInt Znumtheory.
From Coq Require Import Classical.
From Coq Require Import List.
Import ListNotations.
From Teach Require Import Zmod_div Zprime.
Export Znumtheory(prime).
(** * Preliminary lemmas and types for arithmetics exercises *)
#[local] Open Scope Z.
(** ** Missing lemmas about modular arithmetics *)
(** ** Numbers as non-empty strings of decimal digits *)
Inductive Digit :=
d0 | d1 | d2 | d3 | d4 | d5 | d6 | d7 | d8 | d9.
Definition Z_of_Digit (c : Digit) :=
match c with
d0 => 0
| d1 => 1
| d2 => 2
| d3 => 3
| d4 => 4
| d5 => 5
| d6 => 6
| d7 => 7
| d8 => 8
| d9 => 9
end.
Inductive Digits :=
| dsingleton (x : Digit) (* Un seul chiffre | A single digit *)
| dcons (x : Digit) (xs : Digits). (* Un chiffre suivi d'autres chiffres | A digit followed by other digits *)
(* Coercion dsingleton : Digit >-> Digits. *)
(*
= Ctrl+Shift+u 27EA
= Ctrl+Shift+u 27EB
*)
Notation "⟪ x ⟫" := (dsingleton x).
Notation "⟪ x ; .. ; w ; z ⟫" := (dcons x .. (dcons w (dsingleton z)) ..).
(* When compared to List.length, digits_len returns a Z rather than a nat *)
(* L'avantage par rapport à List.length : on renvoie un Z plutôt qu'un nat *)
Fixpoint digits_len (l : Digits): Z :=
match l with
| dsingleton _ => 1
| dcons _ xs => (digits_len xs) + 1
end.
(* = Ctrl+Shift+u 266F *)
Notation "♯ x" := (digits_len x) (at level 40).
Fixpoint digits_sum (cs : Digits) : Z :=
match cs with
| dsingleton d => Z_of_Digit d
| dcons x xs => (Z_of_Digit x) + (digits_sum xs)
end.
Fixpoint Z_of_Digits (l : Digits): Z :=
match l with
| dsingleton d => (Z_of_Digit d)
| dcons x xs => (Z_of_Digit x)*10^(xs) + (Z_of_Digits xs)
end.
Fixpoint shiftr (d : Digits) :=
match d with
| dsingleton d' => dsingleton d0
| dcons h (dsingleton d') => dsingleton h
| dcons h t => dcons h (shiftr t)
end.
Fixpoint digits_canon (l : Digits) : Digits :=
match l with
| dcons d0 xs => digits_canon xs
| l => l
end.
Definition first_digit (xs : Digits) : Digit :=
match xs with
| dsingleton d => d
| dcons x _ => x
end.
Fixpoint last_digit (xs : Digits) : Digit :=
match xs with
| dsingleton d => d
| dcons _ xs => last_digit xs
end.
Definition findall {E} (P : E -> Prop) :=
{ l : list E | (Forall P l /\ (forall (x : E), P x -> In x l)) }.
Ltac atomize H := destruct H as [H | H]; [| try atomize H].
Definition not_In {E : Type} (x : E) (l : list E) := ~ In x l.
(** ** Missing lemmas about modular arithmetics *)
Module Z.
(* TODO: Is it really needed ? *)
Lemma square_opp (x : Z) : (- x) * (- x) = x * x.
Proof. rewrite Z.mul_opp_opp. reflexivity. Qed.
Lemma le_square_r (k : Z) : k <= k * k.
Proof.
destruct (Z.nonpos_pos_cases k) as [H | H].
- apply Z.le_trans with (1 := H); exact (Z.square_nonneg k).
- rewrite <-(Z.mul_1_l k) at 1; apply Z.mul_le_mono_pos_r; [exact H |].
apply Z.le_succ_l in H; rewrite Z.one_succ; exact H.
Qed.
Lemma mod_decomp (a b r : Z) (h : a mod b = r) :
exists k, a = b * k + r.
Proof.
destruct (Z.eq_dec b 0) as [-> | I].
- exists a; rewrite Z.mul_0_l, Z.add_0_l.
rewrite Z.mod_0_r in h; rewrite h; reflexivity.
- exists (a / b); rewrite <-h; exact (Z.div_mod a b).
Qed.
Lemma zero_or_ge_1 (n : Z) : n <= - 1 \/ n = 0 \/ 1 <= n.
Proof.
destruct n as [| p | p].
- right; left; reflexivity.
- right; right; apply Pos2Z.pos_le_pos; exact (Pos.le_1_l p).
- left; apply Pos2Z.neg_le_neg; exact (Pos.le_1_l p).
Qed.
Lemma div_eucl_unique (a b q q' r r' : Z) :
b <> 0 -> a = b * q + r -> a = b * q' + r' -> 0 <= r < b -> 0 <= r' < b
-> q = q' /\ r = r'.
Proof.
intros bn0 eq eq' ineq ineq'.
rewrite eq in eq'.
apply Z.add_move_r in eq'; rewrite <-Z.add_sub_assoc in eq'.
apply eq_sym, Z.add_move_l in eq'.
rewrite <-Z.mul_sub_distr_l in eq'.
assert (- b < b * (q - q') < b) as key. {
rewrite <-eq'; split.
- apply Z.lt_add_lt_sub_l, (Z.lt_le_trans _ 0); [| now apply ineq'].
apply Z.lt_add_lt_sub_r; rewrite Z.sub_opp_r, Z.add_0_l; now apply ineq.
- apply Z.lt_sub_lt_add_l, (Z.lt_le_trans _ b); [now apply ineq' |].
rewrite <-(Z.add_0_l b) at 1; apply Z.add_le_mono_r; now apply ineq.
}
assert (q - q' = 0) as qq'. {
apply Z.abs_lt in key.
assert (0 < b) as Ib. {
apply Z.le_lt_trans with (2 := key).
exact (Z.abs_nonneg _).
}
rewrite Z.abs_mul, Z.abs_eq in key by (now apply Z.lt_le_incl).
apply Z.abs_0_iff.
destruct (zero_or_ge_1 (Z.abs (q - q'))) as [I |[-> | I]].
- exfalso; apply Z.le_ngt with (1:= Z.abs_nonneg (q - q')).
apply Z.le_lt_trans with (1 := I).
exact (Pos2Z.neg_is_neg _).
- reflexivity.
- exfalso; apply Z.lt_nge with (1 := key).
apply Z.le_mul_diag_r; [exact Ib | exact I].
}
rewrite qq', Z.mul_0_r in eq'; split.
- now apply Z.sub_move_0_r.
- now apply eq_sym, Z.sub_move_0_r.
Qed.
(*
Lemma div_ (a b q r : Z) :
b <> 0 -> a = b * q + r -> 0 <= r < b -> q = a / b /\ r = a mod b.
Proof.
intros h1 h2 h3.
Search (?a = ?b * ?q + ?r) (?r = ?a mod ?b).
Search (?a = ?b * ?q + ?r) (?q = ?a / ?b).
pose proof (Z.div_unique_pos a b q r h3 h2) as h4.
pose proof (
split.
*
*)
Lemma digits_sum_suiv (c : Digit) (cs : Digits) : digits_sum (dcons c cs) = (Z_of_Digit c) + digits_sum cs.
Proof. reflexivity. Qed.
Lemma Z_of_Digits_dsingleton (d : Digit) :
Z_of_Digits (dsingleton d) = Z_of_Digit d.
Proof. reflexivity. Qed.
Lemma Z_of_Digits_dcons (h : Digit) (t : Digits) :
Z_of_Digits (dcons h t) = (Z_of_Digit h) * 10 ^(t) + (Z_of_Digits t).
Proof. reflexivity. Qed.
Lemma shiftr_dsingleton (d : Digit) :
shiftr (dsingleton d) = dsingleton d0.
Proof. reflexivity. Qed.
Lemma shiftr_two_digits (d d' : Digit) :
shiftr (dcons d (dsingleton d')) = dsingleton d.
Proof. reflexivity. Qed.
Lemma shiftr_digits (h h' : Digit) (t : Digits) :
shiftr (dcons h (dcons h' t)) = dcons h (shiftr (dcons h' t)).
Proof. reflexivity. Qed.
Lemma digits_len_digit (d : Digit) : digits_len (dsingleton d) = 1.
Proof. reflexivity. Qed.
Lemma digits_len_digits (h : Digit) (t : Digits) :
digits_len (dcons h t) = (digits_len t) + 1.
Proof. reflexivity. Qed.
Lemma digits_sum_digit (d : Digit) :
digits_sum (dsingleton d) = (Z_of_Digit d).
Proof. reflexivity. Qed.
Lemma digits_sum_digits (h : Digit) (t : Digits) :
digits_sum (dcons h t) = (Z_of_Digit h) + digits_sum t.
Proof. reflexivity. Qed.
Lemma digits_len_shiftr_digits (h : Digit) (t : Digits) :
digits_len (shiftr (dcons h t)) = digits_len t.
Proof.
revert h; induction t as [d | d t' IH].
- intros h; rewrite shiftr_two_digits, 2!digits_len_digit; reflexivity.
- intros h; rewrite shiftr_digits, 2digits_len_digits, IH; reflexivity.
Qed.
Lemma digits_len_nneg (d : Digits) : 0 <= digits_len d.
Proof.
induction d as [d | h t IH].
- rewrite digits_len_digit; exact (Z.le_0_1).
- rewrite digits_len_digits; apply Z.add_nonneg_nonneg;
[exact IH | exact Z.le_0_1].
Qed.
Lemma digits_canon_correct (l : Digits) : Z_of_Digits l = Z_of_Digits (digits_canon l).
Proof.
induction l as [x | h t IH]; [reflexivity |].
destruct h; [simpl; exact IH | reflexivity..].
Qed.
Lemma last_digit_digit (d : Digit) :
last_digit (dsingleton d) = d.
Proof. reflexivity. Qed.
Lemma last_digit_digits (h : Digit) (t : Digits) :
last_digit (dcons h t) = last_digit t.
Proof. reflexivity. Qed.
Lemma decimal_decomposition (n : Digits) :
Z_of_Digits n = 10 * (Z_of_Digits (shiftr n)) + (Z_of_Digit (last_digit n)).
Proof.
induction n as [d | h t IH].
- reflexivity.
- destruct t as [d | h' t'].
+ rewrite shiftr_two_digits, last_digit_digits, last_digit_digit.
rewrite Z_of_Digits_dcons, digits_len_digit, Z.pow_1_r.
rewrite !Z_of_Digits_dsingleton, Z.mul_comm; reflexivity.
+ rewrite shiftr_digits, Z_of_Digits_dcons, digits_len_digits.
rewrite (Z_of_Digits_dcons h), last_digit_digits, IH.
rewrite digits_len_shiftr_digits, Z.add_assoc; f_equal.
rewrite Z.mul_add_distr_l; f_equal.
rewrite Z.pow_add_r; [| exact (digits_len_nneg _) | exact Z.le_0_1].
rewrite Z.pow_1_r, Z.mul_assoc, Z.mul_comm; reflexivity.
Qed.
Lemma digits_canon_nonzero (l : Digits) :
(digits_canon l) = d0 \/ first_digit (digits_canon l) <> d0.
Proof.
induction l as [x | h t [IH0 | IHn0]].
- destruct x; [left; reflexivity | right; intros H; discriminate H..].
- destruct h; [left; simpl; exact IH0 | right; intros H; discriminate H..].
- right; destruct h; simpl; [exact IHn0 | intros H; discriminate H..].
Qed.
Lemma In_dec {E : Type} (x : E) (l : list E) :
(In x l) \/ (not_In x l).
Proof.
induction l as [|y l [IH | IH]]; [right; intros [] |..].
- left; right; exact IH.
- destruct (classic (y = x)) as [-> | H].
+ left; left; reflexivity.
+ right; intros [H' | H']; [exact (H H') | exact (IH H')].
Qed.
Definition primeb_correct := Z.primeb_correct.
Definition not_prime_0 := not_prime_0.
Definition pair_equal_spec := pair_equal_spec.
Definition is_nonneg := Pos2Z.is_nonneg.
Definition prime_divisors := prime_divisors.
Definition prime_ge_2 := prime_ge_2.
Definition add_1_r := Z.add_1_r.
Definition add_mod := Z.add_mod.
Definition add_opp_diag_r := Z.add_opp_diag_r.
Definition divide_0_l := Z.divide_0_l.
Definition divide_add_cancel_l := Z.divide_add_cancel_l.
Definition divide_add_cancel_r := Z.divide_add_cancel_r.
Definition divide_add_r := Z.divide_add_r.
Definition divide_factor_l := Z.divide_factor_l.
Definition divide_factor_r := Z.divide_factor_r.
Definition divide_mul_l := Z.divide_mul_l.
Definition divide_mul_r := Z.divide_mul_r.
Definition divide_opp_r := Z.divide_opp_r.
Definition divide_pos_le := Z.divide_pos_le.
Definition divide_refl := Z.divide_refl.
Definition gauss := Z.gauss.
Definition mod_0_l := Z.mod_0_l.
Definition mod_divide := Z.mod_divide.
Definition mul_1_r := Z.mul_1_r.
Definition mul_assoc := Z.mul_assoc.
Definition mul_comm := Z.mul_comm.
Definition mul_mod := Z.mul_mod.
Definition mul_succ_r := Z.mul_succ_r.
Definition pow_1_l := Z.pow_1_l.
Definition pow_m1_l_odd := Z.pow_m1_l_odd.
Definition pow_mod := Z.pow_mod.
Definition divide_mul_cancel_l := Z.divide_mul_cancel_l.
End Z.
(* Tactics *)
Import Z.
Fixpoint range_pos (a b : Z) (n: nat) (acc: list Z) {struct n} : list Z :=
match n with
| O => a :: acc
| S n' => range_pos a (b-1) n' (cons b acc)
end.
Fixpoint range_neg (a b : Z) (n: nat) (acc: list Z) {struct n} : list Z :=
match n with
| O => b :: acc
| S n' => range_neg (a+1) b n' (cons a acc)
end.
Definition range (a b : Z) : list Z :=
if a <=? b
then range_pos a b (Z.to_nat (b-a)) nil
else range_neg b a (Z.to_nat (a-b)) nil
.
#[local]
Ltac false_solv := match goal with
| [H : False |- _ ] => destruct H
end.
#[local]
Ltac casparcas' H := destruct H as [H | H]; [| try casparcas' H; try false_solv ].
#[local]
Ltac casparcas x l H :=
specialize (In_dec x l) as H; unfold In in H; unfold not_In in H; destruct H as [H|H]; [casparcas' H|].
(*Ltac casparcas_range x a b H :=
specialize (In_dec x (range a b)) as H; remember x as __x' in H; simpl in H; subst __x'; unfold In in H; unfold not_In in H; destruct H as [H|H]; [casparcas' H|]. *)
#[local]
Ltac casparcas_range x a b H :=
specialize (In_dec x (range a b)) as H; remember x as __x' in H; destruct H as [H|H];
[ unfold In in H; simpl in H; subst __x'; casparcas' H | unfold not_In in H; simpl in H; subst __x' ].
(*
La tactique `study` est conçue pour rendre plus simple l'analyse des valeurs d'une expression
Si on a un but de la forme Γ G, et une expression E : T, alors on peut utilise la tactique
`study E in [a_1,a_2,...,a_n] as H` qui génerera (n+1) buts: le premier est:
Γ,H:E <> a1 /\ E <> a2 /\ ... /\ E <> a_n G
Autrement dit, on doit prouver le but quand on sait que l'expression E
n'est égale à aucun des élements de la liste d'expression qu'on a donné.
Le second but est Γ,H:E = a1 G, le troisième Γ,H:E = a2 G ... et ainsi de suite jusqu Γ,H:E = an G
Cette tactique est particulièrement utile dans le contexte des exercices sur la divisibilité, où étudier
les restes possibles d'une division euclidienne est courant pour prouver certaines propriétés.
~~~~
The study tactic is designed to make it easier to analyse the different possibles values of an expression
If we have a goal of the form Γ G, and an expression E : T, then we can use the tactic
`study E in [a_1,a_2,...,a_n] as H` to generate (n+1) goals: the first one is
Γ,H:E <> a1 /\ E <> a2 /\ ... /\ E <> a_n G : We have to prove the goal when we know that E is not in the list of expression.
The second goal is Γ,H:E = a1 G, third is Γ,H:E = a2 G and so on until Γ,H:E = an G
This tactic is useful in the context of divisibility, where studying the range of remainder is common to
prove some properties.
*)
Tactic Notation "study" constr(x) "in" constr(l) "as" simple_intropattern(H) := casparcas x l H.
(*
`study E between a and b as H` est un sucre syntaxique pour `study E in [a,a+1,a+2,...,b] as H` (si a <= b) ou `[a,a-1,a-2,...,b]` (si a > b)
Il est courant d'analyser des intervalles continus lorsqu'on travaille sur la divisibilité:
Ce raccourcis permet dviter de faire des erreurs en listant les valeurs possibles d'un intervalle.
~~~
`study E between a and b as H` is a syntax sugar for `study E in [a,a+1,a+2,...,b] as H` (if a <= b) or [a,a-1,a-2,...,b] (if a > b)
It is common to have contiguous ranges when working with divisibility:
This syntax makes it less error-prone to list all possible values in a range.
*)
Tactic Notation "study" constr(x) "between" constr(a) "and" constr(b) "as" simple_intropattern(H) := casparcas_range x a b H.
Add Search Blacklist "Coq".
Require Import Zify.
This diff is collapsed.
(**
This file is part of the coq-teach library
Copyright (C) Boldo, Clément, Hamelin, Mayero, Rousselin
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Additional results on [nat], the type of Peano natural numbers. *)
From Coq Require Import PeanoNat Compare_dec.
Local Open Scope nat_scope.
Section Nat_eq_Compl.
(** ** Compléments sur lgalité. / Complements on equality. *)
Lemma nat_neq_0_1 : 0 <> 1.
Proof. exact (Nat.neq_0_succ 0). Qed.
Lemma nat_eq_1_equiv n : n = 1 <-> n <> 0 /\ n <= 1.
Proof.
split.
+ intros; subst; split. apply not_eq_sym, nat_neq_0_1. apply Nat.le_refl.
+ intros [H1 H2]; apply Nat.le_1_r in H2; destruct H2; subst. contradict H1.
all: reflexivity.
Qed.
Lemma nat_pred_neq_0 n : pred n <> 0 <-> n <> 0 /\ n <> 1.
Proof.
split.
+ intros H; split; contradict H; subst; reflexivity.
+ intros [H0 H1] H. destruct n. contradict H0; reflexivity.
rewrite Nat.pred_succ in H. contradict H1; subst; reflexivity.
Qed.
End Nat_eq_Compl.
Section Nat_ineq_Compl.
(** ** Compléments sur les inégalités. / Complements on inequalities. *)
Lemma nat_le_S_l m n : S m <= n -> m <= n.
Proof.
intros H. apply Nat.le_trans with (S m). 2: assumption.
apply Nat.le_succ_diag_r.
Qed.
Lemma nat_le_1_S n : 1 <= S n.
Proof. rewrite <- Nat.succ_le_mono; apply Nat.le_0_l. Qed.
(* "_wnl" means "when (something is) not last", here "when m <> S n". *)
Lemma nat_le_S_wnl m n : m <= S n -> m <> S n -> m <= n.
Proof.
intros H1 H2; apply Nat.nlt_ge; contradict H2.
apply Nat.le_antisymm. 2: apply Nat.le_succ_l. all: assumption.
Qed.
(* "_wnl" means "when (something is) not last", here "when m <> n". *)
Lemma nat_lt_S_wnl m n : m < S n -> m <> n -> m < n.
Proof.
intros H1 H2; apply Nat.nle_gt; contradict H2.
apply Nat.le_antisymm. apply Nat.lt_succ_r. all: assumption.
Qed.
(* "_wnf" means "when (something is) not first", here "when n <> S m". *)
Lemma nat_lt_S_wnf m n : m < n -> n <> S m -> S m < n.
Proof.
intros H1 H2; apply Nat.nle_gt; contradict H2.
apply Nat.le_antisymm. 2: apply Nat.le_succ_l. all: assumption.
Qed.
Lemma nat_S2_gt_1 n : 1 < S (S n).
Proof.
induction n. apply Nat.lt_1_2.
apply Nat.lt_trans with (S (S n)). assumption.
apply Nat.lt_succ_diag_r.
Qed.
Lemma nat_lt_le_dec m n : {m < n} + {n <= m}.
Proof. destruct (le_lt_dec n m). right; assumption. left; assumption. Qed.
End Nat_ineq_Compl.
Section Nat_add_Compl.
(** ** Compléments sur l'addition. / Complements on addition. *)
Lemma nat_add_0_r_equiv m n : m = m + n <-> n = 0.
Proof.
split; intros H.
+ rewrite <- (Nat.add_0_l n), <- (Nat.sub_diag m) at 1.
rewrite <- Nat.add_sub_swap, <- H, Nat.sub_diag.
reflexivity. apply Nat.le_refl.
+ subst; apply eq_sym, Nat.add_0_r.
Qed.
Lemma nat_add_0_l_equiv m n : n = m + n <-> m = 0.
Proof. rewrite Nat.add_comm. apply nat_add_0_r_equiv. Qed.
Lemma nat_add_S_pred m n : n <> 0 -> S m + pred n = m + n.
Proof.
intros; rewrite Nat.add_pred_r, Nat.add_succ_l. 2: assumption.
apply Nat.pred_succ.
Qed.
Lemma nat_add_pred_S m n : m <> 0 -> pred m + S n = m + n.
Proof.
intros; rewrite Nat.add_pred_l, Nat.add_succ_r. 2: assumption.
apply Nat.pred_succ.
Qed.
(* Partial contrapositive of Nat.eq_add_1.
"_wn0" means "when (something is) not 0", here "when m <> 0 /\ n <> 0". *)
Lemma nat_eq_add_1_contra_wn0 m n : m <> 0 -> n <> 0 -> m < n -> m + n <> 1.
Proof.
intros H1 H2 H; contradict H1; apply Nat.eq_add_1 in H1.
destruct H1 as [[Hm Hn] | [Hm Hn]]; subst. contradict H2. all: reflexivity.
Qed.
(* Partial contrapositive of Nat.eq_add_1.
"_wn1" means "when (something is) not 1", here "when n <> 1". *)
Lemma nat_eq_add_1_contra_wn1 m n : n <> 1 -> m < n -> m + n <> 1.
Proof.
intros Hn H; contradict Hn; apply Nat.eq_add_1 in Hn.
destruct Hn as [[Hm Hn] | [Hm Hn]]; subst. 2: reflexivity.
contradict H. apply Nat.nlt_ge, Nat.le_0_1.
Qed.
Lemma nat_lt_add_l_S m n p : m <= p -> m < n + S p.
Proof. rewrite <- Nat.lt_succ_r; apply Nat.lt_lt_add_l. Qed.
(* "_wn0" means "when (something is) not 0", here "when n <> 0". *)
Lemma nat_lt_add_l_wn0 m n p : n <> 0 -> m <= p -> m < n + p.
Proof.
intros Hn H. rewrite <- (Nat.succ_pred n). 2: assumption.
rewrite Nat.add_succ_comm. apply nat_lt_add_l_S. assumption.
Qed.
Lemma nat_add_lt_l_S m n : m + n < m + S n.
Proof. apply Nat.add_lt_mono_l, Nat.lt_succ_diag_r. Qed.
Lemma nat_lt_add_S m n p : p < m + n -> p < m + S n.
Proof.
intros. apply Nat.lt_trans with (m + n). assumption. apply nat_add_lt_l_S.
Qed.
Lemma nat_le_add_r_lt_S m n : m <= m + n < m + S n.
Proof. split. apply Nat.le_add_r. apply nat_add_lt_l_S. Qed.
Lemma nat_le_lt_add_S m n p : m <= p < m + n -> m <= p < m + S n.
Proof. intros [H1 H2]. split. assumption. apply nat_lt_add_S. assumption. Qed.
Lemma nat_lt_add_succ_r m n p : m < n + S p <-> m <= n + p.
Proof. rewrite <- Nat.lt_succ_r. rewrite Nat.add_succ_r. apply iff_refl. Qed.
Lemma nat_le_lt_add_succ_r m n p : m <= p < m + S n <-> m <= p <= m + n.
Proof. rewrite nat_lt_add_succ_r. apply iff_refl. Qed.
End Nat_add_Compl.
Section Nat_sub_Compl.
(** ** Compléments sur la soustraction. / Complements on subtraction. *)
Lemma nat_sub_0_eq m n : m - n = 0 /\ n - m = 0 <-> m = n.
Proof.
rewrite !Nat.sub_0_le; split.
+ intros [H1 H2]; apply Nat.le_antisymm; assumption.
+ intros; subst; split; apply Nat.le_refl.
Qed.
Lemma nat_sub_S_1 n : S n - 1 = n.
Proof. rewrite Nat.sub_1_r, Nat.pred_succ. reflexivity. Qed.
Lemma nat_pred_sub m n : pred (m - n) = pred m - n.
Proof.
revert m; induction n.
+ intros; rewrite !Nat.sub_0_r. reflexivity.
+ intros; rewrite !Nat.sub_succ_r. rewrite IHn; reflexivity.
Qed.
Lemma nat_sub2 m n p : p <= n -> n <= m -> m - (n - p) = m - n + p.
Proof.
intros H1 H2; apply Nat.add_sub_eq_r.
rewrite Nat.add_sub_assoc. 2: assumption.
rewrite <- Nat.add_assoc, (Nat.add_comm p), Nat.add_assoc.
rewrite <- Nat.add_sub_assoc. 2: apply Nat.le_refl.
rewrite Nat.sub_diag, Nat.add_0_r.
apply Nat.sub_add; assumption.
Qed.
Lemma nat_sub_0_le m n : m <= n -> m - n = 0.
Proof. intros; apply Nat.sub_0_le; assumption. Qed.
Lemma nat_sub_0_lt m n : m < n -> m - n = 0.
Proof. intros; apply nat_sub_0_le, Nat.lt_le_incl; assumption. Qed.
Lemma nat_sub_n0_lt m n : m - n <> 0 <-> n < m.
Proof.
split. 2: apply Nat.sub_gt.
intros H; apply Nat.nle_gt. contradict H. apply Nat.sub_0_le; assumption.
Qed.
Lemma nat_sub_lt_mono_rev m n p q : p <= q -> m - p < n - q -> m < n.
Proof.
intros H1 H2. destruct (le_lt_dec q n) as [H3 | H3].
2: { contradict H2. apply Nat.nlt_ge. replace (n - q) with 0.
apply Nat.le_0_l. apply eq_sym, Nat.sub_0_le, Nat.lt_le_incl. assumption. }
destruct (le_lt_dec p m) as [H4 | H4].
2: { apply Nat.lt_le_trans with p. assumption.
apply Nat.le_trans with q; assumption. }
specialize (Nat.add_le_lt_mono _ _ _ _ H1 H2).
rewrite Nat.add_comm. rewrite (Nat.add_comm q).
rewrite !Nat.sub_add. 2,3: assumption. tauto.
Qed.
Lemma nat_sub_add_eq_l m n p : n <= m -> m - n = p -> p + n = m.
Proof.
revert n p. induction m.
+ intros n p. rewrite Nat.le_0_r. intros Hn; subst.
rewrite Nat.sub_diag, Nat.add_0_r. intros; subst. reflexivity.
+ intros n p. destruct n.
- intros _; rewrite Nat.sub_0_r, Nat.add_0_r. intros; subst. reflexivity.
- rewrite <- Nat.succ_le_mono, Nat.sub_succ.
intros H1 H2. rewrite <- (IHm _ _ H1 H2). apply Nat.add_succ_r.
Qed.
Lemma nat_sub_add_eq_r m n p : n <= m -> m - n = p -> n + p = m.
Proof. rewrite Nat.add_comm. apply nat_sub_add_eq_l. Qed.
Lemma nat_le_lt_add_sub m n p : m <= p < m + n -> 0 <= p - m < n.
Proof.
intros [H1 H2]; split.
+ apply Nat.le_0_l.
+ apply (Nat.add_lt_mono_l _ _ m). rewrite Nat.add_comm.
rewrite Nat.sub_add. all: assumption.
Qed.
End Nat_sub_Compl.
Section Nat_mul_Compl.
(** ** Compléments sur la multiplication. / Complements on multiplication. *)
Lemma nat_le_mul_S_l m n : m <= S n * m.
Proof. apply Nat.le_add_r. Qed.
Lemma nat_le_mul_S_r m n : m <= m * S n.
Proof. rewrite Nat.mul_comm; apply nat_le_mul_S_l. Qed.
Lemma nat_lt_mul_S_l m n : 0 < m -> 0 < n -> m < S n * m.
Proof. intros; apply Nat.lt_add_pos_r, Nat.mul_pos_pos; assumption. Qed.
Lemma nat_lt_mul_S_r m n : 0 < m -> 0 < n -> m < m * S n.
Proof. rewrite Nat.mul_comm; apply nat_lt_mul_S_l. Qed.
Lemma nat_lt_1_mul_pos_sym m n : 1 < m -> 0 < n -> 1 < n * m.
Proof. rewrite Nat.mul_comm. apply Nat.lt_1_mul_pos. Qed.
End Nat_mul_Compl.
Section Nat_div_Compl.
(** ** Compléments sur la division. / Complements on division. *)
Lemma nat_div_mul_sym a b : b <> 0 -> b * a / b = a.
Proof. rewrite Nat.mul_comm. apply Nat.div_mul. Qed.
Lemma nat_div_mul_eq a b q : b <> 0 -> Nat.divide b a -> q = a / b -> a = b * q.
Proof.
intros Hb [p Hp] Hq. subst. rewrite Nat.div_mul. 2: assumption.
apply Nat.mul_comm.
Qed.
End Nat_div_Compl.
Module Nat.
Import PeanoNat.Nat.
(** ** Some results from Nat.Div0 and Nat.Lcm0
These are mostly lemmas taking advantage of the fact that
[forall (a : nat), a / 0 = 0 /\ a mod 0 = a]
This really makes proofs simpler.
These lemmas are not available in Coq 8.16 and anyway it is better to mask
the corresponding lemmas in PeanoNat.Nat. *)
(* Not available in 8.16. *)
Lemma mod_0_r (a : nat) : a mod 0 = a.
Proof. reflexivity. Qed.
(* Not available in 8.16. *)
Lemma div_0_r (a : nat) : a / 0 = 0.
Proof. reflexivity. Qed.
(* Not available in 8.16, better than Nat.div_mod, alternative div_mod_eq. *)
Lemma div_mod (a b : nat) : a = b * (a / b) + a mod b.
Proof. exact (div_mod_eq a b). Qed.
(* Better than Nat.mod_eq. *)
Lemma mod_eq (a b : nat) : a mod b = a - b * (a / b).
Proof.
symmetry; apply Nat.add_sub_eq_l; rewrite <-div_mod; reflexivity.
Qed.
(* Better than Nat.mod_same. *)
Lemma mod_same (a : nat) : a mod a = 0.
Proof.
rewrite mod_eq; destruct (Nat.eq_dec a 0) as [-> | nE]; [reflexivity |].
rewrite (div_same a nE), Nat.mul_1_r, Nat.sub_diag; reflexivity.
Qed.
(* Better than Nat.mod_mul. *)
Lemma mod_mul (a b : nat) : a * b mod b = 0.
Proof.
destruct (Nat.eq_dec b 0) as [-> | nE].
- rewrite Nat.mul_0_r, mod_0_r; reflexivity.
- rewrite mod_eq, (div_mul a b nE), Nat.mul_comm, Nat.sub_diag; reflexivity.
Qed.
Lemma mod_le (a b : nat) : a mod b <= a.
Proof. rewrite mod_eq; now apply (Nat.le_sub_l). Qed.
Lemma div_le_mono (a b c : nat) : a <= b -> a / c <= b / c.
Proof.
destruct (Nat.eq_dec c 0) as [-> | nE%Nat.neq_0_lt_0].
- intros _; rewrite 2!div_0_r; exact (Nat.le_refl 0).
- intros [I | ->]%Nat.le_lteq; [| exact (Nat.le_refl _)].
apply ->Nat.lt_succ_r; apply (Nat.mul_lt_mono_pos_l c _ _ nE).
rewrite Nat.mul_succ_r.
apply (Nat.add_lt_mono_r _ _ (a mod c)); rewrite <-div_mod.
apply Nat.lt_trans with (1 := I); rewrite (div_mod b c) at 1.
rewrite <-Nat.add_assoc; apply Nat.add_lt_mono_l.
apply Nat.lt_lt_add_r, Nat.mod_upper_bound, Nat.neq_0_lt_0; exact nE.
Qed.
Lemma mul_div_le (a b : nat) : b * (a / b) <= a.
Proof. rewrite (div_mod a b) at 2; exact (Nat.le_add_r _ _). Qed.
Lemma div_exact (a b : nat) : (a = b * (a / b)) <-> a mod b = 0.
Proof.
rewrite (div_mod a b) at 1; rewrite <-(Nat.add_0_r (b * (a / b))) at 2.
exact (add_cancel_l _ _ _).
Qed.
(* Replaces divide_div_mul_exact, alternative is Lcm0.divide_div_mul_exact. *)
Lemma divide_div_mul_exact (a b c : nat) :
divide b a -> c * a / b = c * (a / b).
Proof.
destruct (eq_dec b 0) as [-> | Hb].
- intros ->%divide_0_l. rewrite 2!div_0_r, mul_0_r; reflexivity.
- intros [q ->]; rewrite mul_assoc, 2!div_mul by (exact Hb); reflexivity.
Qed.
(* Replaces div_mul_cancel_l, alternative is Div0.div_mul_cancel_l. *)
Lemma div_mul_cancel_l (a b c : nat) : c <> 0 -> c * a / (c * b) = a / b.
Proof.
destruct (eq_dec b 0) as [-> | nE].
- rewrite mul_0_r, 2!div_0_r; intros _; reflexivity.
- intros H%neq_0_lt_0; symmetry; apply (div_unique _ _ _ (c * (a mod b))).
+ apply mul_lt_mono_pos_l; [exact H | exact (mod_upper_bound _ _ nE)].
+ rewrite (div_mod_eq a b) at 1; rewrite mul_add_distr_l, !mul_assoc;
reflexivity.
Qed.
(* Replaces mod_divide, alternative is Lcm0.mod_divide. *)
Lemma mod_divide (a b : nat) : a mod b = 0 <-> divide b a.
Proof.
pose proof (div_mod_eq a b); split.
- intros E; rewrite E, add_0_r, mul_comm in H; exists (a / b); exact H.
- destruct (eq_dec b 0) as [-> | I%neq_0_lt_0].
+ intros ->%divide_0_l; rewrite mod_0_r; reflexivity.
+ intros [q Hq]; rewrite <-(add_0_r (q * b)) in Hq.
rewrite mul_comm in Hq; apply mod_unique, eq_sym in Hq;
[exact Hq | exact I].
Qed.
End Nat.
Section Nat2_Compl.
(** Compléments sur [nat * nat]. / Complements on [nat * nat]. *)
(* Principe d'induction double. / Double induction principle. *)
Lemma nat_ind2 (P : nat -> nat -> Prop) :
P 0 0 ->
(forall m n, P m n -> P (S m) n) ->
(forall m n, P m n -> P m (S n)) ->
forall m n, P m n.
Proof.
intros H00 HSl HSr; induction m; intros n.
+ induction n. assumption. apply HSr; assumption.
+ apply HSl, IHm.
Qed.
(* Principe d'induction double pour une propriété symétrique. /
Double induction principle for a symmetric property. *)
Lemma nat_ind2_sym (P : nat -> nat -> Prop) :
(forall m n, P m n -> P n m) ->
P 0 0 ->
(forall m n, P m n -> P (S m) n) ->
forall m n, P m n.
Proof.
intros HP P00 HS; apply nat_ind2.
+ assumption.
+ assumption.
+ intros; apply HP, HS, HP; assumption.
Qed.
(* Décidabilité de deux égalités. / Decidability of two equalities. *)
Lemma nat_eq2_dec (m1 n1 m2 n2 : nat) :
{ m1 = n1 /\ m2 = n2 } + { m1 <> n1 \/ m2 <> n2 }.
Proof.
destruct (Nat.eq_dec m1 n1) as [H1 | H1].
destruct (Nat.eq_dec m2 n2) as [H2 | H2].
+ left; split; assumption.
+ right; right; assumption.
+ right; left; assumption.
Qed.
(* Décidabilité d'une égalité et d'une inégalité (large). /
Decidability of an equality and a (large) inequality. *)
Lemma nat_eq_le2_dec (m1 n1 m2 n2 : nat) :
{ m1 = n1 /\ m2 <= n2 } + { m1 <> n1 \/ n2 < m2 }.
Proof.
destruct (Nat.eq_dec m1 n1) as [H1 | H1].
destruct (le_lt_dec m2 n2) as [H2 | H2].
+ left; split; assumption.
+ right; right; assumption.
+ right; left; assumption.
Qed.
(* Décidabilité d'une égalité et d'une inégalité (stricte). /
Decidability of an equality and a (strict) inequality. *)
Lemma nat_eq_l2t_dec (m1 n1 m2 n2 : nat) :
{ m1 = n1 /\ m2 < n2 } + { m1 <> n1 \/ n2 <= m2 }.
Proof.
destruct (Nat.eq_dec m1 n1) as [H1 | H1].
destruct (nat_lt_le_dec m2 n2) as [H2 | H2].
+ left; split; assumption.
+ right; right; assumption.
+ right; left; assumption.
Qed.
End Nat2_Compl.
(**
This file is part of the coq-teach library
Copyright (C) Boldo, Clément, Hamelin, Mayero, Rousselin
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Support for factorials in [nat], the type of Peano natural numbers. *)
From Coq Require Import PeanoNat Compare_dec.
From Teach Require Import Nat_Compl.
Local Open Scope nat_scope.
Section Fact_Def.
(* Factorielle de n. / Factorial of n.
fact n = 1 * 2 * ... * (n - 1) * n. *)
Fixpoint fact (n : nat) : nat :=
match n with
| O => 1
| S n' => fact n' * S n'
end.
End Fact_Def.
Section Fact_Facts.
Lemma fact_0 : fact 0 = 1.
Proof. reflexivity. Qed.
Lemma fact_1 : fact 1 = 1.
Proof. reflexivity. Qed.
Lemma fact_S n : fact (S n) = fact n * S n.
Proof. reflexivity. Qed.
Lemma fact_pred n : fact n = fact (S n) / S n.
Proof. rewrite fact_S, Nat.div_mul. reflexivity. discriminate. Qed.
Lemma fact_gt_0 n : 0 < fact n.
Proof.
induction n. apply Nat.lt_0_1.
rewrite fact_S; apply Nat.mul_pos_pos. apply IHn. apply Nat.lt_0_succ.
Qed.
Lemma fact_neq_0 n : fact n <> 0.
Proof. apply Nat.neq_0_lt_0, fact_gt_0. Qed.
Lemma fact_mul_neq_0 m n : fact m * fact n <> 0.
Proof. apply Nat.neq_mul_0; split; apply fact_neq_0. Qed.
Lemma fact_mul2_neq_0 m n p : fact m * fact n * fact p <> 0.
Proof. apply Nat.neq_mul_0; split. apply fact_mul_neq_0. apply fact_neq_0. Qed.
Lemma fact_S_div n : fact (S n) / fact n = S n.
Proof. rewrite fact_S. apply nat_div_mul_sym, fact_neq_0. Qed.
Lemma fact_S_div_alt n : 0 < n -> fact n / fact (pred n) = n.
Proof.
intros Hn; rewrite <- (Nat.succ_pred n). apply fact_S_div.
apply Nat.neq_0_lt_0; assumption.
Qed.
Lemma fact_gt_1 n : 1 < n -> 1 < fact n.
Proof.
destruct n. easy.
intros; rewrite fact_S; apply nat_lt_1_mul_pos_sym. assumption.
apply fact_gt_0.
Qed.
Lemma fact_eq_1_equiv n : fact n = 1 <-> n = 0 \/ n = 1.
Proof.
apply iff_sym; split.
+ intros [Hn | Hn]; subst. apply fact_0. apply fact_1.
+ destruct (lt_dec 1 n) as [Hn | Hn]; intros Hn1.
- contradict Hn1. apply not_eq_sym, Nat.lt_neq, fact_gt_1. assumption.
- apply Nat.le_1_r. apply Nat.nlt_ge. assumption.
Qed.
(* "_wn1" means "when (something is) not 1", here "when n <> 1". *)
Lemma fact_eq_1_wn1 n : n <> 1 -> fact n = 1 -> n = 0.
Proof.
intros H1; rewrite fact_eq_1_equiv; intros [H2 | H2]; subst. 2: contradict H1.
all: reflexivity.
Qed.
Lemma fact_le m n : m <= n -> fact m <= fact n.
Proof.
intros H; induction H as [| n H IH]. apply Nat.le_refl.
rewrite fact_S. apply Nat.le_trans with (fact n). assumption.
apply nat_le_mul_S_r.
Qed.
(* "_w0" means "when (something is) 0", here "when m = 0". *)
Lemma fact_lt_w0 m n : m = 0 -> n <> 1 -> m < n -> fact m < fact n.
Proof.
intros H0 H1 H; subst. rewrite fact_0; apply fact_gt_1.
apply Nat.nle_gt. contradict H1. apply Nat.le_antisymm. assumption.
apply Nat.le_succ_l. assumption.
Qed.
Lemma fact_lt_S n : n <> 0 -> fact n < fact (S n).
Proof.
intros Hn. rewrite fact_S. apply nat_lt_mul_S_r. apply fact_gt_0.
apply Nat.neq_0_lt_0. assumption.
Qed.
(* "_wn0" means "when (something is) not 0", here "when m <> 0". *)
Lemma fact_lt_wn0 m n : m <> 0 -> m < n -> fact m < fact n.
Proof.
intros Hm H; induction H as [| n H IH]. apply fact_lt_S; assumption.
apply Nat.lt_trans with (fact n). assumption.
apply fact_lt_S. apply Nat.neq_0_lt_0, Nat.le_lt_trans with m.
+ apply Nat.le_0_l.
+ apply Nat.lt_le_trans with (S m). 2: assumption.
apply Nat.lt_succ_diag_r.
Qed.
Lemma fact_lt m n : m + n <> 1 -> m < n -> fact m < fact n.
Proof.
intros H; destruct (Nat.eq_dec m 0).
+ subst. apply fact_lt_w0. reflexivity. assumption.
+ apply fact_lt_wn0. assumption.
Qed.
(* "_w0" means "when (something is) 0", here "when m * n = 0". *)
Lemma fact_inj_w0 m n : m * n = 0 -> m + n <> 1 -> fact m = fact n -> m = n.
Proof.
rewrite Nat.mul_eq_0. intros [Hm | Hn]; subst; rewrite fact_0.
+ intros. rewrite fact_eq_1_wn1; easy.
+ rewrite Nat.add_0_r. apply fact_eq_1_wn1.
Qed.
(* "_w0" means "when (something is) 0", here "when m * n <> 0". *)
Lemma fact_inj_wn0 m n : m <> 0 -> n <> 0 -> fact m = fact n -> m = n.
Proof.
intros Hm Hn H1. destruct (Nat.eq_dec m n) as [| H2]. assumption.
apply not_eq in H2. contradict H1. destruct H2 as [H | H].
+ apply Nat.lt_neq, fact_lt. apply nat_eq_add_1_contra_wn0. all: assumption.
+ apply not_eq_sym, Nat.lt_neq, fact_lt. apply nat_eq_add_1_contra_wn0.
all: assumption.
Qed.
Lemma fact_inj m n : m + n <> 1 -> fact m = fact n -> m = n.
Proof.
intros H1. destruct (Nat.eq_dec (m * n) 0) as [H0 | H0].
+ apply fact_inj_w0; assumption.
+ apply Nat.neq_mul_0 in H0. destruct H0 as [Hm Hn].
apply fact_inj_wn0; assumption.
Qed.
Lemma fact_mod_0 m n : m <= n -> (fact n) mod (fact m) = 0.
Proof.
intros H. apply Nat.mod_divide.
revert m H. induction n as [| n IHn].
+ intros m H. apply Nat.le_0_r in H. subst. exists 1. reflexivity.
+ intros m [H | ->]%Nat.le_lteq; [| exact (Nat.divide_refl _)].
apply ->Nat.lt_succ_r in H; apply IHn in H.
apply Nat.divide_trans with (1 := H).
exists (S n); rewrite fact_S, Nat.mul_comm; reflexivity.
Qed.
Lemma fact_divide n p : S p <= n -> Nat.divide (S p) (fact n).
Proof.
intros H1; induction n. contradict H1; apply Nat.nle_succ_0.
rewrite fact_S. destruct (le_lt_dec (S p) n) as [H2 | H2].
+ apply Nat.divide_mul_l. apply IHn. assumption.
+ replace (S p) with (S n). apply Nat.divide_factor_r.
apply Nat.le_antisymm. 2: assumption.
apply Nat.le_succ_l. assumption.
Qed.
End Fact_Facts.
(**
This file is part of the coq-teach library
Copyright (C) Boldo, Clément, Hamelin, Mayero, Rousselin
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Support for iterated summations in [nat], the type of Peano natural
numbers. *)
(* Strong induction is needed. *)
From Coq Require Import PeanoNat Wf_nat Compare_dec.
From Teach Require Import Nat_Compl.
Local Open Scope nat_scope.
Section Sum_Def.
(* Somme de n termes à partir de a. / Sum of n terms from a.
sum_n a n f = f a + f (a + 1) + ... + f (a + n - 1).
n = 0 -> sum_n a n f = 0. *)
Fixpoint sum_n (a n : nat) (f : nat -> nat) : nat :=
match n with
| O => 0
| S n' => sum_n a n' f + f (a + n')
end.
(*
Definition sum_range (a b : nat) (f: nat -> nat) := sum_n a (S b-a) f.
*)
(* Somme de a à b inclus. / Sum from a to b included.
sum_range a b f = f a + f (a + 1) + ... + f (b - 1) + f b.
b < a -> sum_range a b f = 0. *)
Definition sum_range (a b : nat) (f : nat -> nat) : nat :=
if le_lt_dec a b then sum_n a (b - a + 1) f else 0.
Definition sum_range_bis (a b : nat) (f: nat -> nat) : nat := sum_n a (S b - a) f.
Lemma sum_range_correct_l a b f :
a <= b -> sum_range a b f = sum_n a (b - a + 1) f.
Proof.
intros H; unfold sum_range. destruct (le_lt_dec _ _). reflexivity.
contradict H. apply Nat.nle_gt; assumption.
Qed.
Lemma sum_range_correct_r a b f : b < a -> sum_range a b f = 0.
Proof.
intros H; unfold sum_range. destruct (le_lt_dec _ _). 2: reflexivity.
contradict H. apply Nat.nlt_ge; assumption.
Qed.
Lemma sum_n_eq a n f : 0 < a + n -> sum_n a n f = sum_range a (a + n - 1) f.
Proof.
intros H. destruct (Nat.eq_dec n 0) as [Hn | Hn].
+ subst. rewrite sum_range_correct_r. reflexivity.
rewrite Nat.add_0_r in *. rewrite Nat.sub_1_r.
apply Nat.lt_pred_l. apply Nat.neq_0_lt_0. assumption.
+ assert (Hn1 : 1 <= n). apply Nat.le_succ_l, Nat.neq_0_lt_0. assumption.
assert (H1 : a <= a + n - 1).
rewrite <- Nat.add_sub_assoc. apply Nat.le_add_r. assumption.
rewrite sum_range_correct_l. 2: assumption.
replace (_ + 1) with n. reflexivity.
rewrite <- Nat.add_sub_swap. 2: assumption.
rewrite <- (Nat.add_sub_assoc a). 2: assumption.
rewrite <- Nat.add_assoc. rewrite Nat.sub_add. 2: assumption.
rewrite Nat.add_comm. rewrite Nat.add_sub. reflexivity.
Qed.
Lemma sum_range_0_l n f : sum_range 0 n f = sum_n 0 (S n) f.
Proof.
rewrite sum_range_correct_l. 2: apply Nat.le_0_l.
rewrite Nat.sub_0_r, Nat.add_1_r. reflexivity.
Qed.
End Sum_Def.
Section Sum_Facts.
Lemma sum_n_ext a n f1 f2 :
(forall k, a <= k < a + n -> f1 k = f2 k) -> sum_n a n f1 = sum_n a n f2.
Proof.
intro H. induction n. reflexivity.
simpl. rewrite IHn.
+ rewrite H. reflexivity. apply nat_le_add_r_lt_S.
+ intros k Hk. apply H. apply nat_le_lt_add_S. assumption.
Qed.
Lemma sum_range_ext a b f1 f2 :
(forall k, a <= k <= b -> f1 k = f2 k) -> sum_range a b f1 = sum_range a b f2.
Proof.
destruct (le_lt_dec a b) as [H | H].
+ intros Hf. rewrite !sum_range_correct_l. 2,3: assumption.
apply sum_n_ext. intros k [Hk1 Hk2]. apply Hf. split. assumption.
revert Hk2. rewrite Nat.add_1_r. rewrite Nat.add_succ_r, Nat.lt_succ_r.
rewrite Nat.add_comm. rewrite Nat.sub_add. easy. assumption.
+ intros _. rewrite !sum_range_correct_r. reflexivity. all: assumption.
Qed.
Lemma sum_n_0 a f : sum_n a 0 f = 0.
Proof. reflexivity. Qed.
Lemma sum_n_1 a f : sum_n a 1 f = f a.
Proof. unfold sum_n. rewrite Nat.add_0_l, Nat.add_0_r. reflexivity. Qed.
(* (S n) est le successeur de n, c'est-à-dire (n + 1). /
(S n) is the successor of n, ie (n + 1). *)
Lemma sum_n_ind_r a n f : sum_n a (S n) f = sum_n a n f + f (a + n).
Proof. reflexivity. Qed.
Lemma sum_n_ind_l a n f : sum_n a (S n) f = f a + sum_n (S a) n f.
Proof.
revert a.
apply (lt_wf_ind n).
clear n.
intros n IHn a. rewrite sum_n_ind_r. destruct n.
+ rewrite !Nat.add_0_r. reflexivity.
+ rewrite IHn. 2: apply Nat.lt_succ_diag_r.
rewrite sum_n_ind_r. rewrite Nat.add_succ_comm, Nat.add_assoc. reflexivity.
Qed.
Lemma sum_n_ind (P : nat -> Prop) a n f :
P 0 -> (forall i j, P i -> P j -> P (i + j)) ->
(forall i, a <= i < a + n -> P (f i)) ->
P (sum_n a n f).
Proof.
intros HP0 HP Hf. induction n.
+ rewrite sum_n_0. assumption.
+ rewrite sum_n_ind_r. apply HP.
- apply IHn. intros i Hi. apply Hf. apply nat_le_lt_add_S. assumption.
- apply Hf. apply nat_le_add_r_lt_S.
Qed.
Lemma sum_n_concat a n1 n2 f :
sum_n a n1 f + sum_n (a + n1) n2 f = sum_n a (n1 + n2) f.
Proof.
revert a n2 f; induction n1.
+ intros. rewrite sum_n_0, Nat.add_0_l. f_equal. easy.
+ intros a n2 f. rewrite Nat.add_succ_comm. rewrite <- IHn1.
rewrite sum_n_ind_r. rewrite sum_n_ind_l. rewrite Nat.add_succ_r.
apply eq_sym, Nat.add_assoc.
Qed.
Lemma sum_n_split m n a f :
m <= n -> sum_n a n f = sum_n a m f + sum_n (a + m) (n - m) f.
Proof.
intros H. rewrite sum_n_concat. rewrite Nat.add_comm. rewrite Nat.sub_add.
reflexivity. assumption.
Qed.
Lemma sum_n_extract i a n f :
i < n -> sum_n a n f = sum_n a i f + f (a + i) + sum_n (a + S i) (n - S i) f.
Proof.
intros Hi. rewrite (sum_n_split i). 2: apply Nat.lt_le_incl; assumption.
rewrite <- Nat.add_assoc. f_equal.
rewrite Nat.add_succ_r. rewrite <- sum_n_ind_l. f_equal.
rewrite Nat.sub_succ_r. rewrite Nat.succ_pred. reflexivity.
apply Nat.sub_gt. assumption.
Qed.
Lemma sum_n_le a n f g :
(forall i, a <= i < a + n -> f i <= g i) -> sum_n a n f <= sum_n a n g.
Proof.
intros H. induction n.
+ rewrite !sum_n_0. apply Nat.le_refl.
+ rewrite !sum_n_ind_r. apply Nat.add_le_mono. 2: apply H, nat_le_add_r_lt_S.
apply IHn. intros i Hi. apply H. apply nat_le_lt_add_S. assumption.
Qed.
Lemma sum_n_lt a n f g :
(forall i, a <= i < a + n -> f i <= g i) ->
(exists i, a <= i < a + n /\ f i < g i) ->
sum_n a n f < sum_n a n g.
Proof.
revert a f g. induction n; intros a f g H1 [i [Hi H2]].
+ destruct Hi as [Hi1 Hi2]. contradict Hi2.
rewrite Nat.add_0_r. apply Nat.nlt_ge. assumption.
+ rewrite (sum_n_extract (i - a) _ _ f), (sum_n_extract (i - a) _ _ g).
2,3: apply nat_le_lt_add_sub; assumption.
destruct Hi as [Hi1 Hi2]. apply Nat.add_lt_le_mono.
2: { apply sum_n_le. intros j [Hj1 Hj2]. apply H1. split.
+ apply Nat.le_trans with (a + S (i - a)). apply Nat.le_add_r. assumption.
+ apply Nat.lt_le_trans with (a + S (i - a) + (S n - S (i - a))). assumption.
rewrite Nat.sub_succ. rewrite <- Nat.add_assoc. rewrite Nat.add_succ_l.
rewrite (Nat.add_comm (i - a)). rewrite Nat.sub_add. apply Nat.le_refl.
apply Nat.le_sub_le_add_l. apply nat_lt_add_succ_r. assumption. }
apply Nat.add_le_lt_mono.
2: { replace (a + (i - a)) with i. assumption.
rewrite Nat.add_comm. rewrite Nat.sub_add. reflexivity. assumption. }
apply sum_n_le. intros j [Hj1 Hj2]. apply H1. split. assumption.
apply Nat.lt_trans with i. 2: assumption.
rewrite <- (Nat.sub_add a i). 2: assumption.
rewrite Nat.add_comm. assumption.
Qed.
Lemma sum_n_eq_0 a n f :
(forall i, a <= i < a + n -> f i = 0) -> sum_n a n f = 0.
Proof.
intros H. apply trans_eq with (sum_n a n (fun _ => 0)).
+ apply sum_n_ext. assumption.
+ clear; revert a; induction n. reflexivity.
intros a; rewrite sum_n_ind_l. rewrite IHn. reflexivity.
Qed.
Lemma sum_range_eq_0 a b f :
(forall i, a <= i <= b -> f i = 0) -> sum_range a b f = 0.
Proof.
intros Hf. destruct (le_lt_dec a b) as [H | H].
2: { apply sum_range_correct_r. assumption. }
rewrite sum_range_correct_l. 2: assumption.
apply sum_n_eq_0. intros i [Hi1 Hi2]. apply Hf. split. assumption.
apply Nat.lt_succ_r. replace (S b) with (a + (b - a + 1)). assumption.
rewrite Nat.add_1_r. rewrite <- Nat.sub_succ_l. 2: assumption.
rewrite Nat.add_comm. rewrite Nat.sub_add. reflexivity.
apply Nat.le_trans with b. assumption. apply Nat.le_succ_diag_r.
Qed.
Lemma sum_n_eq_0_rev a n f :
sum_n a n f = 0 -> forall i, a <= i < a + n -> f i = 0.
Proof.
induction n.
+ rewrite Nat.add_0_r. intros _ i [Hi1 Hi2].
contradict Hi1. apply Nat.nle_gt. assumption.
+ rewrite sum_n_ind_r. rewrite Nat.eq_add_0.
intros [H1 H2] i Hi1. destruct (Nat.eq_dec i (a + n)) as [Hi2 | Hi2].
- subst. assumption.
- apply IHn. assumption.
destruct Hi1 as [Hi1a Hi1b]. split. assumption.
apply nat_lt_S_wnl. 2: assumption.
rewrite <- Nat.add_succ_r. assumption.
Qed.
Lemma sum_n_eq_0_equiv a n f :
sum_n a n f = 0 <-> forall i, a <= i < a + n -> f i = 0.
Proof. split. apply sum_n_eq_0_rev. apply sum_n_eq_0. Qed.
Lemma sum_n_neq_0 a n f :
(exists i, a <= i < a + n /\ f i <> 0) -> sum_n a n f <> 0.
Proof.
intros [i [Hi Hf]]. contradict Hf.
apply (sum_n_eq_0_rev a n). all: assumption.
Qed.
Lemma sum_n_add a n f g :
sum_n a n f + sum_n a n g = sum_n a n (fun i => f i + g i).
Proof.
induction n. reflexivity.
rewrite !sum_n_ind_r. rewrite <- IHn. rewrite 2!Nat.add_assoc. f_equal.
rewrite <- Nat.add_assoc. rewrite (Nat.add_comm (f _)). apply Nat.add_assoc.
Qed.
Lemma sum_n_sub a n f g :
(forall i, a <= i < a + n -> g i <= f i) ->
sum_n a n f - sum_n a n g = sum_n a n (fun i => f i - g i).
Proof.
intros H. induction n. reflexivity.
rewrite !sum_n_ind_r. rewrite <- IHn.
2: { intros i Hi. apply H. apply nat_le_lt_add_S. assumption. }
rewrite Nat.sub_add_distr. rewrite Nat.add_sub_assoc.
2: { apply H. apply nat_le_add_r_lt_S. }
rewrite Nat.add_sub_swap.
2: { apply sum_n_le. intros i Hi. apply H. apply nat_le_lt_add_S. assumption. }
reflexivity.
Qed.
Lemma sum_n_mul_add_distr_l a n f c :
c * sum_n a n f = sum_n a n (fun i => c * f i).
Proof.
induction n. apply Nat.mul_0_r.
rewrite !sum_n_ind_r. rewrite <- IHn. apply Nat.mul_add_distr_l.
Qed.
Lemma sum_n_mul_add_distr_r a n f c :
sum_n a n f * c = sum_n a n (fun i => f i * c).
Proof.
rewrite Nat.mul_comm. rewrite sum_n_mul_add_distr_l.
apply sum_n_ext. intros; apply Nat.mul_comm.
Qed.
Lemma sum_n_shift_l t a n f :
t <= a -> sum_n a n f = sum_n (a - t) n (fun i => f (i + t)).
Proof.
intros Ht. induction n. reflexivity.
rewrite !sum_n_ind_r. rewrite IHn.
replace (a - t + n + t) with (a + n). reflexivity.
rewrite (Nat.add_comm (a - t)). rewrite <- Nat.add_assoc.
rewrite Nat.sub_add. 2: assumption.
apply Nat.add_comm.
Qed.
Lemma sum_n_shift_r t a n f :
sum_n a n f = sum_n (a + t) n (fun i => f (i - t)).
Proof.
rewrite (sum_n_shift_l t (a + t)). 2: apply Nat.le_add_l.
rewrite Nat.add_sub. apply sum_n_ext.
intros. rewrite Nat.add_sub. reflexivity.
Qed.
Lemma sum_n_reverse a n f :
sum_n a n f = sum_n a n (fun i => f (2 * a + n - 1 - i)).
Proof.
induction n. rewrite !sum_n_0; reflexivity.
rewrite sum_n_ind_r, sum_n_ind_l, (sum_n_shift_l 1 (S a)). 2: apply nat_le_1_S.
rewrite nat_sub_S_1. replace (_ - a) with (a + n).
2: { rewrite <- Nat.double_twice, <- Nat.add_sub_assoc. 2: apply nat_le_1_S.
unfold Nat.double. rewrite nat_sub_S_1, (Nat.add_comm (_ + _)).
rewrite <- Nat.add_sub_assoc. 2: apply Nat.le_add_r.
rewrite Nat.add_sub. apply Nat.add_comm. }
rewrite Nat.add_comm. f_equal. rewrite IHn. apply sum_n_ext.
intros i Hi. f_equal. rewrite (Nat.add_comm i), Nat.sub_add_distr.
do 2 f_equal. rewrite <- Nat.add_sub_assoc. 2: apply nat_le_1_S.
rewrite nat_sub_S_1. reflexivity.
Qed.
End Sum_Facts.
(**
This file is part of the coq-teach library
Copyright (C) Boldo, Clément, Hamelin, Mayero, Rousselin
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Missing basic lemmas for the type [positive] of binary positive integers *)
From Coq Require Import PArith.BinPos.
Module Pos.
Local Open Scope positive_scope.
Lemma neq_1_lt_1 (p : positive) : p <> 1 <-> (1 < p).
Proof.
split; [| now intros H H'; apply (Pos.lt_irrefl p); rewrite H' at 1].
destruct p as [p | p |]; [| | intros C; exfalso; apply C]; reflexivity.
Qed.
Lemma le_le_succ_r (n m : positive) :
n <= m -> n <= Pos.succ m.
Proof.
intros H; apply Pos.le_trans with (1 := H).
apply Pos.lt_le_incl; exact (Pos.lt_succ_diag_r _).
Qed.
Lemma le_succ_r (n m : positive) :
(n <= Pos.succ m) <-> n <= m \/ n = Pos.succ m.
Proof.
split.
- now intros [I%Pos.lt_succ_r | ->]%Pos.le_lteq; [left | right; reflexivity].
- intros [I | ->]; [apply le_le_succ_r; exact I | exact (Pos.le_refl _)].
Qed.
Lemma two_succ : 2 = Pos.succ 1.
Proof. reflexivity. Qed.
Lemma le_2_succ (n : positive) : 2 <= Pos.succ n.
Proof. rewrite two_succ, <-Pos.succ_le_mono; exact (Pos.le_1_l _). Qed.
End Pos.
(**
This file is part of the coq-teach library
Copyright (C) Boldo, Clément, Hamelin, Mayero, Rousselin
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
From Coq Require Import ZArith.BinInt.
From Teach Require Import Pos_Compl.
Module Pos.
Local Open Scope positive_scope.
Definition primeb_pos_aux (p : positive) (fuel : positive) : bool.
Proof.
induction fuel as [| fuel' IH'] using Pos.peano_rect.
- exact true.
- destruct (Z.pos p mod (Z.pos (Pos.succ fuel')) =? 0)%Z eqn:E.
+ exact false.
+ exact IH'.
Defined.
Lemma primeb_pos_aux_succ (p : positive) (fuel : positive) :
primeb_pos_aux p (Pos.succ fuel) =
if (Z.pos p mod (Z.pos (Pos.succ fuel)) =? 0)%Z then false else
primeb_pos_aux p fuel.
Proof.
unfold primeb_pos_aux;
rewrite Pos.peano_rect_succ;
destruct (Z.pos p mod (Z.pos (Pos.succ fuel)) =? 0)%Z eqn:E; reflexivity.
Qed.
Lemma primeb_pos_aux_correct (p : positive) (fuel : positive) :
primeb_pos_aux p fuel = true <->
forall (n : positive), (2 <= n <= fuel)%positive ->
(Z.pos p mod (Z.pos n) =? 0)%Z = false.
Proof.
split; induction fuel as [| fuel' IH'] using Pos.peano_rect.
- intros _ n [C1 C2]; exfalso.
pose proof (Pos.le_trans _ _ _ C1 C2) as C.
unfold Pos.le in C; apply C; reflexivity.
- intros H n [In In'].
rewrite primeb_pos_aux_succ in H.
destruct (Z.pos p mod (Z.pos (Pos.succ fuel')) =? 0)%Z eqn:E; simpl in H.
+ discriminate H.
+ apply Pos.le_succ_r in In' as [In' | En].
* apply IH'; [exact H |]; split; assumption.
* rewrite En; exact E.
- intros _; reflexivity.
- intros H.
rewrite primeb_pos_aux_succ.
destruct (Z.pos p mod (Z.pos (Pos.succ fuel')) =? 0)%Z eqn:E; simpl.
+ rewrite <-E; rewrite H; [reflexivity |]; split; [| exact (Pos.le_refl _)].
exact (Pos.le_2_succ _).
+ apply IH'; intros n [In In']; apply H; split; [exact In |].
apply Pos.le_le_succ_r; exact In'.
Qed.
End Pos.
(**
This file is part of the coq-teach library
Copyright (C) Boldo, Clément, Hamelin, Mayero, Rousselin
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Worksheet on binomial coefficients.
These are:
- general statements from library modules Nat_Sum, Nat_Factorial and
Nat_Binomial that are equipped with guidance comments for students, and
solution(s) for teachers;
- alternate proofs general results from the library modules;
- proofs that hypotheses of general results are optimal;
- or specific statements or questions.
Note that provided script prepsheet will replace lines from marker
(* Begin solution for the teacher. *)
to next marker (included)
(* End solution for the teacher. *)
by "Admitted.", and will remove lines from marker
(* Begin other solution for the teacher. *)
to next marker (included)
(* End other solution for the teacher. *)
That way, both teacher and student versions of the file are compiling, and
teachers can verify the validity of the provided solution(s). *)
From Teach Require Import WS_Helper.
Section Statements_From_Lib.
Search "vandermonde".
(*fr Faire la preuve du lemme suivant et remplacer "Admitted" par "Qed". *)
(*en Fill the proof of next lemma and replace "Admitted" by "Qed". *)
Lemma binom_sum_sqr n :
sum_range 0 n (fun k => (binom n k) ^ 2) = binom (2 * n) n.
Proof.
(*fr Transformer (2*n) en une somme. *)
(*en Transform (2*n) into a sum. *)
(*fr Utiliser l'identité de Vandermonde. *)
(*en Use Vandermonde's identity. *)
(*fr Réduire lgalite de somme à lgalité des fonctions. *)
(*en Reduce equality on sums to equality on functions. *)
(*fr Utiliser la symétrie des coefficients binomiaux. *)
(*en Use symmetry of binomial coefficients. *)
(*fr Ne pas oublier les conditions d'application des lemmes utilisés. *)
(*en Do not forget application conditions of used lemmas. *)
(* Begin solution for the teacher. *)
(* Without automation. *)
replace (2 * n) with (n + n) by apply double_twice.
rewrite binom_vandermonde.
apply sum_range_ext. intros k [_ Hk].
rewrite <- binom_sym. 2: assumption.
rewrite pow_2_r. reflexivity.
Qed.
(* End solution for the teacher. *)
(* Begin other solution for the teacher. *)
(* With automation. *)
Lemma binom_sum_sqr_with_auto n :
sum_range 0 n (fun k => (binom n k) ^ 2) = binom (2 * n) n.
Proof.
replace (2 * n) with (n + n) by lia.
rewrite binom_vandermonde.
apply sum_range_ext. intros k Hk.
rewrite <- binom_sym by lia.
now rewrite pow_2_r.
Qed.
(* End other solution for the teacher. *)
(*enFill the proof of next lemma and replace "Admitted" by "Qed". *)
(*fr Faire la preuve du lemme suivant et remplacer "Admitted" par "Qed". *)
(*enFill the proof of next lemma and replace "Admitted" by "Qed". *)
Lemma binom_sum n : sum_range 0 n (fun k => binom n k) = 2 ^ n.
Proof.
(*fr Transformer 2 en une somme. *)
(*en Transform 2 into a sum. *)
(*fr Utiliser la formule du binome. *)
(*en Use binomial theorem. *)
(*fr Reduire l'egalite de somme a l'egalite des fonctions. *)
(*en Reduce equality on sums to equality on functions. *)
(* Begin solution for the teacher. *)
(* Without automation. *)
replace 2 with (1+1) by reflexivity.
rewrite binom_formula.
apply sum_range_ext. intros k Hk.
rewrite !pow_1_l.
rewrite !mul_1_r. reflexivity.
Qed.
(* End solution for the teacher. *)
(* Begin other solution for the teacher. *)
(* With automation. *)
Lemma binom_sum_with_auto n : sum_range 0 n (fun k => binom n k) = 2 ^ n.
Proof.
replace 2 with (1+1) by easy.
rewrite binom_formula.
apply sum_range_ext. intros k Hk.
rewrite !pow_1_l; lia.
Qed.
(* End other solution for the teacher. *)
End Statements_From_Lib.
Section Alternate_Proofs.
(*fr Preuve alternative de la formule du pion. *)
(*en Alternate proof of the committee-chair identity. *)
Lemma binom_committee_chair_alt n k :
S k * binom n (S k) = n * binom (n - 1) k.
Proof.
destruct n. now simpl.
destruct (le_lt_dec (S k) (S n)) as [h1|]. 2: rewrite 2!binom_eq_0; lia.
symmetry.
rewrite binom_fact_div_wn0 by lia.
replace (S n - 1) with n by lia.
rewrite <- divide_div_mul_exact.
* rewrite mul_comm, <- fact_S.
rewrite <- div_mul_cancel_l with (c := S k) by lia.
rewrite mul_assoc.
rewrite (mul_comm _ (fact k)), <- fact_S.
replace (n - k) with (S n - S k) by lia.
rewrite divide_div_mul_exact.
+ now rewrite <- binom_fact_div_wn0.
+ apply mod_divide.
apply fact_sub_mod_0; lia.
* apply mod_divide.
apply fact_sub_mod_0; lia.
Qed.
End Alternate_Proofs.
Section Optimality_Of_Hypotheses.
(*fr Prouver que les hypothèses des lemmes suivants sont optimales : *)
(*en Prove that hypotheses of the following lemmas are optimal: *)
(* binom_S_l, binom_S_r, binom_pred, binom_eq_0, binom_gt_0, binom_neq_0,
binom_le_alt, binom_lt_S, binom_lt, binom_lt_alt, binom_gt_1,
binom_committee_chair_iter, binom_fact, binom_fact_div, binom_sym,
binom_cancellation_alt. *)
(*fr Indication : ces lemmes sont de la forme (P -> Q). Il faut donc prouver
lquivalence (P <-> Q), ou juste l'implication dans l'autre sens (Q -> P),
ou plutôt la contraposée de cette dernière (~ P -> ~ Q). *)
(*en Hint: these lemmas are of the form (P -> Q). It is thus a matter of proving
either the equivalence (P <-> Q), or just the reverse implication (Q -> P),
or rather the contrapositive of the latter (~ P -> ~ Q). *)
(* "_rev_contra" means the contrapositive of the reverse implication. *)
Lemma binom_S_l_rev_contra n k :
k = 0 -> binom (S n) k <> binom n (pred k) + binom n k.
Proof.
intros; subst. simpl.
rewrite !binom_0_r.
apply lt_neq, lt_1_2.
Qed.
(*fr Ici, P est de la forme (~ P1 \/ ~ P2), sa négation est donc (P1 /\ P2). *)
(*en Here, P is of the form (~ P1 \/ ~ P2), thus its negation is (P1 /\ P2). *)
Lemma binom_S_r_rev_contra n k :
n = 0 /\ k = 0 -> binom n (S k) <> binom (pred n) k + binom (pred n) (S k).
Proof.
intros [Hn Hk]; subst. simpl.
apply nat_neq_0_1.
Qed.
Lemma binom_pred_rev_contra n k :
n = 0 /\ k = 1 \/ k = 0 ->
binom n k <> binom (pred n) (pred k) + binom (pred n) k.
Proof.
intros [[Hn Hk] | Hk].
+ subst. simpl. apply nat_neq_0_1.
+ subst. rewrite !binom_0_r. apply not_eq_S, nat_neq_0_1.
Qed.
Lemma binom_eq_0_rev_contra n k : k <= n -> binom n k <> 0.
Proof. apply binom_neq_0. Qed.
Lemma binom_gt_0_rev_contra n k : n < k-> binom n k <= 0.
Proof. rewrite le_0_r. apply binom_eq_0. Qed.
Lemma binom_neq_0_rev_contra n k : n < k -> binom n k = 0.
Proof. apply binom_eq_0. Qed.
(*fr Ici, P est de la forme (P1 \/ P2 \/ P3), sa négation est donc
(~ P1 /\ ~ P2 /\ ~ P3). *)
(*en Here, P is of the form (P1 \/ P2 \/ P3), thus its negation is
(~ P1 /\ ~ P2 /\ ~ P3). *)
Lemma binom_le_alt_rev_contra n1 n2 k :
(k <> 0 /\ k <= n1 /\ n2 < n1) -> binom n2 k < binom n1 k.
Proof.
intros [Hk1 [Hk2 Hn]]. apply binom_lt. 2: assumption. split. 2: assumption.
apply neq_0_lt_0. assumption.
Qed.
(*fr Ici, P est de la forme (P1 /\ P2), sa négation est donc (~ P1 \/ ~ P2). *)
(*en Here, P is of the form (P1 /\ P2), thus its negation is (~ P1 \/ ~ P2). *)
Lemma binom_lt_S_rev_contra n k :
(k <= 0 \/ S n < k) -> binom (S n) k <= binom n k.
Proof.
intros [Hk | H].
+ rewrite le_0_r in Hk. subst. simpl. rewrite binom_0_r. apply le_refl.
+ rewrite binom_eq_0. apply le_0_l. assumption.
Qed.
(*fr Ici, P est de la forme (P1 /\ P2 /\ P3), sa négation est donc
(~ P1 \/ ~ P2 \/ ~ P3). *)
(*en Here, P is of the form (P1 /\ P2 /\ P3), thus its negation is
(~ P1 \/ ~ P2 \/ ~ P3). *)
Lemma binom_lt_rev_contra n1 n2 k :
(k <= 0 \/ n2 < k \/ n2 <= n1) -> binom n2 k <= binom n1 k.
Proof. rewrite le_0_r. apply binom_le_alt. Qed.
(*fr Ici, P est de la forme (P1 /\ P2), sa négation est donc (~ P1 \/ ~ P2). *)
(*en Here, P is of the form (P1 /\ P2), thus its negation is (~ P1 \/ ~ P2). *)
Lemma binom_gt_1_rev_contra n k : k <= 0 \/ n <= k -> binom n k <= 1.
Proof.
rewrite le_0_r. intros [H | H].
+ subst. rewrite binom_0_r. apply le_refl.
+ destruct (le_lt_eq_dec _ _ H) as [H' | H'].
- rewrite binom_eq_0. apply le_0_l. assumption.
- subst. rewrite binom_diag. apply le_refl.
Qed.
(*fr Ici, P est de la forme (~ P1 \/ P2), sa négation est donc (P1 /\ ~ P2). *)
(*en Here, P is of the form (~ P1 \/ P2), thus its negation is (P1 /\ ~ P2). *)
Lemma binom_committee_chair_iter_rev_contra n k i :
(k = 0 /\ n < i) ->
fact (k + i) * fact (n - i) * binom n (k + i) <>
fact n * fact k * binom (n - i) k.
Proof.
intros [Hk H]; subst. simpl.
rewrite binom_eq_0. 2: assumption.
rewrite mul_0_r.
rewrite nat_sub_0_lt. 2: assumption. simpl.
rewrite !mul_1_r.
apply not_eq_sym, fact_neq_0.
Qed.
Lemma binom_fact_rev_contra n k :
n < k -> binom n k * (fact k * fact (n - k)) <> fact n.
Proof.
intros H.
rewrite binom_eq_0. 2: assumption. simpl.
apply not_eq_sym, fact_neq_0.
Qed.
(*fr Ici, P est de la forme (~ P1 \/ ~ P2), sa négation est donc (P1 /\ P2). *)
(*en Here, P is of the form (~ P1 \/ ~ P2), thus its negation is (P1 /\ P2). *)
Lemma binom_fact_div_rev_contra n k :
(n = 0 /\ k = 1) -> binom n k <> fact n / (fact k * fact (n - k)).
Proof. intros [Hn Hk]; subst. simpl. apply nat_neq_0_1. Qed.
Lemma binom_sym_rev_contra n k : n < k -> binom n k <> binom n (n - k).
Proof.
intros H.
rewrite binom_eq_0. 2: assumption.
rewrite nat_sub_0_lt. 2: assumption.
rewrite binom_0_r.
apply nat_neq_0_1.
Qed.
(*fr Ici, P est de la forme (P1 \/ P2), sa négation est donc (~ P1 /\ ~ P2). *)
(*en Here, P is of the form (P1 \/ P2), thus its negation is (~ P1 /\ ~ P2). *)
Lemma binom_cancellation_alt_rev_contra n k i :
k < i /\ i <= n ->
binom n k * binom k i <> binom n i * binom (n - i) (k - i).
Proof.
intros [H1 H2].
rewrite (binom_eq_0 k i H1). rewrite mul_0_r.
apply not_eq_sym, neq_mul_0. split; apply binom_neq_0.
+ assumption.
+ apply sub_le_mono_r.
apply lt_le_incl, lt_le_trans with i.
all: assumption.
Qed.
End Optimality_Of_Hypotheses.
Section Specific_Statements.
(*fr L'exercice suivant provient de *)
(*en The following exercise is taken from *)
(* Hyperbole Terminale - Spécialité Mathématiques, Nathan, 2020 (in French). *)
(*fr Résoudre (binom n 5 = 17 (binom n 4)) avec (n >= 5).
Indication : essayer n = 89. *)
(*en Solve (binom n 5 = 17 (binom n 4)) with (n >= 5).
Hint: try n = 89. *)
Lemma binom_ex01a : exists n, 5 <= n /\ binom n 5 = 17 * binom n 4.
Proof.
exists 89. split.
+ apply sub_0_le. rewrite 5!sub_succ. apply sub_0_l.
+ apply (mul_cancel_l _ _ 5). discriminate.
rewrite binom_mul_S_r. rewrite 4!sub_succ, sub_0_r, mul_assoc. reflexivity.
Qed.
Lemma binom_ex01b n : binom n 5 = 17 * binom n 4 -> n < 5 \/ n = 89.
Proof.
destruct (nat_lt_le_dec n 5) as [Hn | Hn].
+ intros _; left. assumption.
+ assert (Hn' : 4 <= n).
apply le_trans with 5. apply le_succ_diag_r. assumption.
rewrite <- (mul_cancel_l _ _ 5). 2: discriminate.
rewrite binom_mul_S_r. rewrite mul_assoc. rewrite mul_cancel_r.
2: apply binom_neq_0; assumption.
intros H. apply nat_sub_add_eq_l in H. 2: assumption.
right. subst. reflexivity.
Qed.
End Specific_Statements.
This diff is collapsed.
(**
This file is part of the coq-teach library
Copyright (C) Boldo, Clément, Hamelin, Mayero, Rousselin
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Useful exports for the provided worksheet.
This includes the lists of results on natural numbers from Arith.PeanoNat.Nat
that are used in modules Nat_Sum, Nat_Factorial and Nat_Binomial.
Usage: tune exports and definitions to your needs, and import the resulting
module in the worksheet. *)
From Coq Require Import Arith.PeanoNat.
From Coq Require Export Arith.Compare_dec.
From Coq Require Export Lia.
Export (notations) Nat.
(* Helper for results on natural numbers used in Nat_Sum. *)
Export Nat (eq_add_0, eq_dec).
Export Nat (le_0_l, le_refl, le_succ_diag_r, le_succ_l, le_trans, lt_pred_l,
lt_succ_diag_r, lt_succ_r, neq_0_lt_0, nle_gt, nlt_ge).
Export Nat (add_0_l, add_0_r, add_1_r, add_assoc, add_comm, add_sub,
add_sub_assoc, add_sub_swap, add_succ_comm, add_succ_r, sub_0_r,
sub_1_r, sub_add, sub_add_distr, sub_diag, sub_succ, sub_succ_l).
Export Nat (add_le_mono, le_add_l, le_add_r).
Export Nat (mul_0_r, mul_add_distr_l, mul_comm).
(* Helper for results on natural numbers used in Nat_Factorial. *)
Export Nat (eq_dec, succ_pred).
Export Nat (le_0_l, le_0_r, le_1_r, le_antisymm, le_lt_trans, le_refl,
le_succ_l, le_trans, nle_gt, nle_succ_0).
Export Nat (lt_0_1, lt_0_succ, lt_le_trans, lt_neq, lt_succ_diag_r, lt_trans,
neq_0_lt_0, nlt_ge).
Export Nat (add_0_r).
Export Nat (mul_1_r, mul_assoc, mul_comm, mul_eq_0, mul_pos_pos, neq_mul_0).
Export Nat (div_mul, divide_factor_r, divide_mul_l, mod_divides).
(* Helper for results on natural numbers used in Nat_Binomial. *)
Export Nat (eq_dec, pred_succ, succ_pred).
Export Nat (le_0_l, le_0_r, le_antisymm, le_refl, le_trans, le_succ_diag_r,
le_succ_le_pred, le_trans).
Export Nat (lt_0_1, lt_0_succ, lt_1_r, lt_le_incl, lt_neq, lt_succ_diag_r,
lt_succ_lt_pred, lt_succ_r, lt_trans, neq_0_lt_0, nle_gt, nlt_ge,
succ_le_mono, succ_lt_mono).
Export Nat (add_0_l, add_0_r, add_1_l, add_1_r, add_assoc, add_comm, add_sub,
add_sub_swap, add_succ_comm, add_succ_r, sub_0_l, sub_0_le,
sub_0_r, sub_1_r, sub_add, sub_diag, sub_succ_l, sub_succ_r).
Export Nat (add_lt_mono_r, add_pos_l, le_add_l, lt_add_pos_l, lt_lt_add_l).
Export Nat (mul_0_l, mul_0_r, mul_1_l, mul_1_r, mul_assoc, mul_cancel_l,
mul_comm, mul_succ_l).
Export Nat (double_twice, mul_add_distr_l, mul_add_distr_r).
Export Nat (div_mul, div_small, mod_divides).
Export Nat (pow_0_r, pow_1_l, pow_2_r, pow_succ_r').
(* Helper for results on natural numbers used in exercises. *)
Export Nat (lt_1_2).
Export Nat (add_sub_eq_l, add_succ_l, sub_le_mono_r).
Export Nat (mul_cancel_r, mul_le_mono_l, mul_le_mono_pos_r, mul_sub_distr_r).
Export Nat (div_mul_cancel_l, div_unique_exact, divide_div_mul_exact,
mod_divide).
Export Nat (pow_inj_l, pow_le_mono_l, pow_mul_l).
From Teach Require Export Nat_Compl Nat_Sum Nat_Factorial.
From Teach Require Import Nat_Binomial.
Export Nat_Binomial (binom, binom_vandermonde, binom_sym, binom_formula, binom_eq_0, binom_fact_div_wn0,
fact_sub_mod_0, binom_0_r, binom_neq_0, binom_lt, binom_le_alt, binom_diag, binom_mul_S_r).
Export Nat_Compl.Nat.
Definition formule_du_pion := binom_committee_chair.
Definition committee_chair_identity := binom_committee_chair.
Definition formule_de_vandermonde := binom_vandermonde.
Definition vandermonde_identity := binom_vandermonde.
(**
This file is part of the coq-teach library
Copyright (C) Boldo, Clément, Hamelin, Mayero, Rousselin
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
From Coq.ZArith Require Import BinInt Wf_Z.
(** ** Missing lemmas about modular arithmetics in Z *)
Module Z.
#[local] Open Scope Z.
(** Below are lemmas either missing, or with unnecessary hypotheses, or wrong
name in the standard library. *)
Lemma div_eucl_0_r (a : Z) : Z.div_eucl a 0 = (0, a).
Proof. destruct a as [| a | a]; reflexivity. Qed.
Lemma div_eucl_0_l (b : Z) : Z.div_eucl 0 b = (0, 0).
Proof. reflexivity. Qed.
(* Alternative: Zdiv.Zmod_0_r *)
Lemma mod_0_r (a : Z) : a mod 0 = a.
Proof.
pose proof (div_eucl_0_r a) as E.
unfold "mod"; rewrite E; reflexivity.
Qed.
(* Alternative: Zdiv.Zdiv_0_r *)
Lemma div_0_r (a : Z) : a / 0 = 0.
Proof.
pose proof (div_eucl_0_r a) as E.
unfold "/"; rewrite E; reflexivity.
Qed.
(* Alternative: Zdiv.Zmod_0_l, better than Z.mod_0_l *)
Lemma mod_0_l (b : Z) : 0 mod b = 0.
Proof.
pose proof (div_eucl_0_l b) as E.
unfold "mod"; rewrite E; reflexivity.
Qed.
(* Alternative: Zdiv.Zdiv_0_l, better than Z.div_0_l *)
Lemma div_0_l (b : Z) : 0 / b = 0.
Proof.
pose proof (div_eucl_0_l b) as E.
unfold "/"; rewrite E; reflexivity.
Qed.
(* Better version of Z.div_mod *)
Lemma div_mod (a b : Z) : a = b * (a / b) + a mod b.
Proof.
destruct (Z.eq_dec b 0) as [-> | E].
- rewrite div_0_r, mod_0_r; reflexivity.
- exact (Z.div_mod a b E).
Qed.
(* Better version of Z.mod_mul, better name than Zdiv.Z_mod_mult
Note that (a * b) / b = a is not valid in general if b = 0. *)
Lemma mod_mul (a b : Z) : (a * b) mod b = 0.
Proof.
pose proof (div_mod (a * b) b) as eq.
destruct (Z.eq_dec b 0) as [-> | Eb].
- rewrite mod_0_r, Z.mul_0_r; reflexivity.
- rewrite Z.div_mul, (Z.mul_comm b a) in eq by (exact Eb).
rewrite <-(Z.add_0_r (a * b)) in eq at 1.
apply Z.add_reg_l in eq; symmetry; exact eq.
Qed.
(* Better version of Znumtheory.Zmod_divide and Z.mod_divide, both have
the extra hypothesis [(b <> 0)], Z.mod_divide is an equivalence. *)
Lemma mod_divide (a b : Z) : a mod b = 0 <-> (b | a).
Proof.
pose proof (div_mod a b) as eq; split.
- intros H; rewrite H, Z.add_0_r, Z.mul_comm in eq; exists (a / b); exact eq.
- intros [q ->]; exact (mod_mul _ _).
Qed.
(* Better version of Z.add_mod *)
Lemma add_mod (a b n : Z) : (a + b) mod n = (a mod n + b mod n) mod n.
Proof.
destruct (Z.eq_dec n 0) as [-> | H].
- rewrite !mod_0_r; reflexivity.
- exact (Z.add_mod a b n H).
Qed.
(* NOTE: Z.mul_mod but without the unnecessary hypothesis *)
Lemma mul_mod (a b n : Z) : (a * b) mod n = (a mod n * (b mod n)) mod n.
Proof.
destruct (Z.eq_dec n 0) as [-> | H]; [now rewrite !Z.mod_0_r |].
exact (Z.mul_mod a b n H).
Qed.
(* NOTE: Z.mul_mod_idemp_r but without the unnecessary hypothesis *)
Lemma mul_mod_idemp_r (a b n : Z) : (a * (b mod n)) mod n = (a * b) mod n.
Proof.
destruct (Z.eq_dec n 0) as [-> | H].
- rewrite !Z.mod_0_r; reflexivity.
- rewrite Z.mul_mod_idemp_r by (exact H); reflexivity.
Qed.
(* Currently not in the stdlib *)
Lemma pow_mod (a k n : Z) : (a ^ k) mod n = ((a mod n) ^ k) mod n.
Proof.
destruct (Z.neg_nonneg_cases k).
- rewrite 2Z.pow_neg_r by (assumption); reflexivity. (* <- ugly *)
- apply (Wf_Z.natlike_ind (fun k => a ^ k mod n = (a mod n) ^ k mod n)); (* <- ugly *)
[rewrite 2Z.pow_0_r; reflexivity | | exact H].
intros x Hx IH; rewrite 2Z.pow_succ_r, mul_mod, IH by (assumption).
rewrite mul_mod_idemp_r; reflexivity.
Qed.
(* Currently does not exist in the stdlib, note the unfortunate condition *)
Lemma pow_m1_l_odd (n : Z) : (0 <= n) -> Z.Odd n -> (- 1) ^ n = - 1.
Proof.
intros H H'.
replace (- 1) with (- (1)) by reflexivity. (* <- ugly *)
rewrite Z.pow_opp_odd by (exact H').
rewrite Z.pow_1_l by exact H; reflexivity.
Qed.
Lemma gcd_ge_1 (a b : Z) : a <> 0 \/ b <> 0 -> 1 <= Z.gcd a b.
Proof.
intros Hab; rewrite Z.one_succ; apply Z.le_succ_l, Z.le_neq; split.
- exact (Z.gcd_nonneg _ _).
- intros [Ha Hb]%eq_sym%Z.gcd_eq_0; destruct Hab as [Ha' | Hb'];
[exact (Ha' Ha) | exact (Hb' Hb)].
Qed.
Lemma gt_1_neq_0 (n : Z) : 1 < n -> n <> 0.
Proof.
intros H1 H2; apply (Z.lt_asymm 1 n); [exact H1 | rewrite H2; exact Z.lt_0_1].
Qed.
Lemma ge_1_gt_0 (n : Z) : 1 <= n -> 0 < n.
Proof. rewrite Z.one_succ; intros H%Z.le_succ_l; exact H. Qed.
Lemma gt_1_gt_0 (n : Z) : 1 < n -> 0 < n.
Proof. intros H; apply Z.lt_trans with (1 := Z.lt_0_1); exact H. Qed.
(* Equivalence in Z.divide_add_cancel_r *)
(* NOTE: the stdlib is inconsistent in the naming of "cancel_l" or "cancel_r"
lemmas, most of the times "l" or "r" refers to the position of the canceled
operand, but sometimes (see [Z.divide_add_cancel_r]) it refers to the position
of the uncanceled operand.
See also the ouput of [Search "cancel_r"].
We chose "l" or "r" to denote the position of the canceled operand as we believe
it's probably what the user expects. *)
Lemma divide_add_cancel_l (n m p : Z) : (n | m) -> (n | m + p) <-> (n | p).
Proof.
intros H; split.
- exact (Z.divide_add_cancel_r _ _ _ H).
- exact (Z.divide_add_r _ _ _ H).
Qed.
Lemma divide_add_cancel_r (n m p : Z) : (n | m) -> (n | p + m) <-> (n | p).
Proof. rewrite Z.add_comm; exact (divide_add_cancel_l _ _ _). Qed.
(* Equivalence in Gauss lemma *)
Lemma divide_mul_cancel_l (n m p : Z) :
Z.gcd n m = 1 -> (n | m * p) <-> (n | p).
Proof.
intros H; split.
- intros H'; exact (Z.gauss _ _ _ H' H).
- clear H; exact (Z.divide_mul_r _ _ _).
Qed.
Lemma divide_mul_cancel_r (n m p : Z) :
Z.gcd n m = 1 -> (n | p * m) <-> (n | p).
Proof. rewrite Z.mul_comm; exact (divide_mul_cancel_l _ _ _). Qed.
End Z.
(**
This file is part of the coq-teach library
Copyright (C) Boldo, Clément, Hamelin, Mayero, Rousselin
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
From Coq Require Import ZArith.BinInt Znumtheory.
From Teach Require Import Zmod_div Pos_prime Pos_Compl.
(** * Additional lemmas and functions about primality in Z *)
(** Remark: the definition of the [prime] predicate (Prop-valued) is in
ZArith.Znumtheory. It is quite surprising and not very practical. *)
Module Z.
(* Alternative (better) definitions of prime *)
Lemma prime_no_strict_divisor (p : Z) :
prime p <-> 1 < p /\ forall a, (a | p) -> a = -1 \/ a = 1 \/ a = p \/ a = - p.
Proof.
split; intros H.
- pose proof H as [H1 H2]; split; [exact H1 |].
exact (Znumtheory.prime_divisors p H).
- destruct H as [H1 H2]; constructor; [exact H1 |].
intros n Hn; apply Znumtheory.Zgcd_1_rel_prime.
apply Z.le_antisymm; cycle 1;
[apply Z.gcd_ge_1; right; apply Z.gt_1_neq_0; exact H1 |].
apply Z.le_ngt; intros H.
pose proof (Z.gcd_divide_r n p) as Hdiv.
pose proof (Z.gcd_nonneg n p) as Ig.
pose proof (Z.gcd_divide_l n p) as Hdivn.
specialize (H2 _ Hdiv) as [C | [C | [C | C]]].
+ rewrite C in Ig; apply Z.le_ngt in Ig; now apply Ig.
+ rewrite C in H; apply (Z.lt_irrefl 1); exact H.
+ rewrite C in Hdivn.
apply Z.divide_pos_le, Z.le_ngt in Hdivn; [| now apply Z.ge_1_gt_0, Hn].
now apply Hdivn, Hn.
+ rewrite C in Ig; apply Z.le_ngt in Ig.
apply Ig, Z.opp_neg_pos, Z.gt_1_gt_0; exact H1.
Qed.
Lemma prime_no_strict_divisor_below (p : Z) :
prime p <-> 1 < p /\ forall a, 1 < a < p -> ~ (a | p).
Proof.
split.
- intros H; pose proof H as [H1 H2]; split; [exact H1 |]; intros a Ha Hdiv.
apply prime_no_strict_divisor in H as [_ H].
specialize (H a Hdiv) as [C | [C | [C | C]]]; rewrite C in Ha.
+ destruct Ha as [Ha _]; now apply (Z.lt_asymm (-1) 1).
+ destruct Ha as [Ha _]; apply (Z.lt_irrefl 1); exact Ha.
+ destruct Ha as [_ Ha]; apply (Z.lt_irrefl p); exact Ha.
+ destruct Ha as [Ha _]; apply (Z.lt_asymm (- p) 1); [| exact Ha].
now apply Z.lt_trans with (2 := Z.lt_0_1), Z.opp_neg_pos, Z.gt_1_gt_0.
- intros [Ip Hp]; apply prime_no_strict_divisor; split; [exact Ip |].
intros a Hdiv; enough (Z.abs a = 1 \/ Z.abs a = p) as C. {
destruct C as [C | C].
+ destruct (Z.abs_or_opp_abs a) as [C' | C']; [right; left | left];
rewrite C'; [exact C |]; rewrite C; exact (Pos2Z.opp_pos _).
+ right; right; destruct (Z.abs_or_opp_abs a) as [C' | C'];
[left | right]; rewrite C', C; reflexivity.
}
apply Z.divide_abs_l in Hdiv.
pose proof (Z.abs_nonneg a) as [I1 | E1]%Z.le_lteq; cycle 1. {
exfalso; rewrite <-E1 in Hdiv; apply Z.divide_0_l in Hdiv;
rewrite Hdiv in Ip; apply (Z.lt_asymm 0 1 (Z.lt_0_1)); exact Ip.
}
pose proof (Z.gt_1_gt_0 p Ip) as Hpgt0.
pose proof (Z.divide_pos_le (Z.abs a) p Hpgt0 Hdiv) as I2.
assert (Z.abs a = 1 \/ 1 < Z.abs a) as [Ha | Ha]. {
apply Z.le_succ_l in I1; rewrite <-Z.one_succ in I1.
apply Z.le_lteq in I1 as [H | H]; [right | left; symmetry]; exact H.
}
+ left; exact Ha.
+ apply Z.le_lteq in I2 as [I2 | E2]; [| right; exact E2].
exfalso; apply (Hp (Z.abs a)); [| exact Hdiv]; split; assumption.
Qed.
Lemma divisor_le_sqrt (n m p : Z) :
0 <= n -> n = m * p -> m <= Z.sqrt n \/ p <= Z.sqrt n.
Proof.
intros H1 Hdiv.
destruct (Z.le_ge_cases m 0) as [Im | Im]. {
left; apply Z.le_trans with (1 := Im); exact (Z.sqrt_nonneg _).
}
destruct (Z.le_ge_cases p 0) as [Ip | Ip]. {
right; apply Z.le_trans with (1 := Ip); exact (Z.sqrt_nonneg _).
}
destruct (Z.le_ge_cases m p) as [Imp | Imp]; [left | right].
- apply Z.sqrt_le_square; [exact H1 | exact Im |].
apply Z.mul_le_mono_nonneg_l with (1 := Im) in Imp; rewrite <-Hdiv in Imp;
exact Imp.
- apply Z.sqrt_le_square; [exact H1 | exact Ip |].
apply Z.mul_le_mono_nonneg_r with (1 := Ip) in Imp; rewrite <-Hdiv in Imp;
exact Imp.
Qed.
Lemma prime_no_strict_divisor_below_sqrt (p : Z) :
prime p <-> 1 < p /\ forall a, 1 < a <= Z.sqrt p -> ~ (a | p).
Proof.
split.
- intros [Ip Hp]%prime_no_strict_divisor_below; split; [exact Ip |].
intros a [Ia Ia']; apply Hp; split; [exact Ia |].
apply Z.le_lt_trans with (1 := Ia').
apply Z.sqrt_lt_lin; exact Ip.
- intros [Ip Hp]; apply prime_no_strict_divisor_below; split; [exact Ip |].
intros a [Ia Ia'] [q Hq].
pose proof Hq as Hdiv; apply divisor_le_sqrt in Hdiv; cycle 1. {
apply Z.lt_le_incl, Z.gt_1_gt_0; exact Ip.
}
destruct Hdiv as [Hdiv | Hdiv].
+ assert (1 < q) as Iq. {
apply Z.lt_nge; intros C.
apply (Z.mul_le_mono_nonneg_r _ _ a) in C; cycle 1. {
apply Z.lt_le_incl, Z.lt_trans with (1 := Z.lt_0_1); exact Ia.
}
rewrite <-Hq, Z.mul_1_l in C; apply Z.le_ngt in C; apply C; exact Ia'.
}
pose proof (conj Iq Hdiv) as Iq'; specialize (Hp _ Iq'); apply Hp.
exists a; rewrite Z.mul_comm; exact Hq.
+ pose proof (conj Ia Hdiv) as Ia''; specialize (Hp _ Ia''); apply Hp.
exists q; exact Hq.
Qed.
Definition primeb (n : Z) : bool :=
match n with
| Z.neg p => false
| 0 => false
| Z.pos p =>
match p with
| 1%positive => false
| _ => Pos.primeb_pos_aux p (Z.to_pos (Z.sqrt (Z.pos p)))
end
end.
Lemma Private_test_primeb :
primeb (- 5) = false /\
primeb (- 4) = false /\
primeb (- 3) = false /\
primeb (- 2) = false /\
primeb (- 1) = false /\
primeb 0 = false /\
primeb 1 = false /\
primeb 2 = true /\
primeb 3 = true /\
primeb 4 = false /\
primeb 5 = true /\
primeb 6 = false /\
primeb 7 = true /\
primeb 8 = false /\
primeb 9 = false /\
primeb 10 = false /\
primeb 11 = true /\
primeb 12 = false /\
primeb 13 = true /\
primeb 14 = false /\
primeb 15 = false /\
primeb 16 = false /\
primeb 17 = true /\
primeb 18 = false /\
primeb 19 = true /\
primeb 65537 = true /\
primeb 65533 = false /\
primeb 939391 = true. (* /\
primeb 479001599 = true. *)
Proof. repeat split; reflexivity. Qed.
Lemma primeb_correct (n : Z) : primeb n = true <-> prime n.
Proof.
unfold primeb; split; destruct n as [| p | p].
- intros H; discriminate H.
- enough (forall p, (p <> 1)%positive ->
Pos.primeb_pos_aux p (Z.to_pos (Z.sqrt (Z.pos p))) = true ->
prime (Z.pos p)) as key. {
destruct p as [p' | p' |]; [| | intros H; discriminate H]; apply key;
unfold Pos.le; intros H; discriminate H.
}
intros q Hq.
intros H; rewrite Pos.primeb_pos_aux_correct in H. (* apply fails *)
apply Z.prime_no_strict_divisor_below_sqrt; split. {
apply Pos2Z.pos_lt_pos, Pos.neq_1_lt_1; exact Hq.
}
intros a [Ha Ha']; intros Hdiv%Z.mod_divide%Z.eqb_eq.
destruct a as [| a | a]; [discriminate Ha | | discriminate Ha].
lapply (H a); [rewrite Hdiv; intros contra; discriminate contra |].
split.
+ rewrite Pos.two_succ; apply Pos.le_succ_l; exact Ha.
+ exact Ha'.
- intros H; discriminate H.
- intros [H _]; easy.
- enough (forall p, (p <> 1)%positive -> prime (Z.pos p) ->
Pos.primeb_pos_aux p (Z.to_pos (Z.sqrt (Z.pos p))) = true) as key. {
now intros Hp; destruct p as [p | p |];
[apply key.. | apply not_prime_1 in Hp].
}
intros q Hq Pq; apply Pos.primeb_pos_aux_correct; intros n Hn.
apply Z.prime_no_strict_divisor_below_sqrt in Pq as [_ Pq].
apply Z.eqb_neq; intros Hdiv%Z.mod_divide.
specialize (Pq (Z.pos n)); apply Pq; [| exact Hdiv].
destruct Hn as [H2%Pos2Z.pos_le_pos Hsqrt%Pos2Z.pos_le_pos].
split.
* apply Z.le_succ_l; rewrite <-Z.two_succ; exact H2.
* rewrite Z2Pos.id in Hsqrt; [exact Hsqrt | now apply Z.sqrt_pos].
- now intros [I _]; contradict I.
Qed.
End Z.