Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: NGcd.v Sprache: Unknown

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(** Properties of the greatest common divisor *)

Require Import NAxioms NSub NZGcd.

Module Type NGcdProp
(Import A : NAxiomsSig')
(Import B : NSubProp A).

Include NZGcdProp A A B.

(** Results concerning divisibility*)

Definition divide_1_r n : (n | 1) -> n == 1
:= divide_1_r_nonneg n (le_0_l n).

Definition divide_antisym n m : (n | m) -> (m | n) -> n == m
:= divide_antisym_nonneg n m (le_0_l n) (le_0_l m).

Lemma divide_add_cancel_r : forall n m p, (n | m) -> (n | m + p) -> (n | p).
Proof.
intros n m p (q,Hq) (r,Hr).
exists (r-q). rewrite mul_sub_distr_r, <- Hq, <- Hr.
now rewrite add_comm, add_sub.
Qed.

Lemma divide_sub_r : forall n m p, (n | m) -> (n | p) -> (n | m - p).
Proof.
intros n m p H H'.
destruct (le_ge_cases m p) as [LE|LE].
apply sub_0_le in LE. rewrite LE. apply divide_0_r.
apply divide_add_cancel_r with p; trivial.
now rewrite add_comm, sub_add.
Qed.

(** Properties of gcd *)

Definition gcd_0_l n : gcd 0 n == n := gcd_0_l_nonneg n (le_0_l n).
Definition gcd_0_r n : gcd n 0 == n := gcd_0_r_nonneg n (le_0_l n).
Definition gcd_diag n : gcd n n == n := gcd_diag_nonneg n (le_0_l n).
Definition gcd_unique' n m p := gcd_unique n m p (le_0_l p).
Definition gcd_unique_alt' n m p := gcd_unique_alt n m p (le_0_l p).
Definition divide_gcd_iff' n m := divide_gcd_iff n m (le_0_l n).

Lemma gcd_add_mult_diag_r : forall n m p, gcd n (m+p*n) == gcd n m.
Proof.
intros. apply gcd_unique_alt'.
intros. rewrite gcd_divide_iff. split; intros (U,V); split; trivial.
apply divide_add_r; trivial. now apply divide_mul_r.
apply divide_add_cancel_r with (p*n); trivial.
now apply divide_mul_r. now rewrite add_comm.
Qed.

Lemma gcd_add_diag_r : forall n m, gcd n (m+n) == gcd n m.
Proof.
intros n m. rewrite <- (mul_1_l n) at 2. apply gcd_add_mult_diag_r.
Qed.

Lemma gcd_sub_diag_r : forall n m, n<=m -> gcd n (m-n) == gcd n m.
Proof.
intros n m H. symmetry.
rewrite <- (sub_add n m H) at 1. apply gcd_add_diag_r.
Qed.

(** On natural numbers, we should use a particular form
  for the Bezout identity, since we don't have full subtraction. *)

Definition Bezout n m p := exists a b, a*n == p + b*m.

Instance Bezout_wd : Proper (eq==>eq==>eq==>iff) Bezout.
Proof.
unfold Bezout. intros x x' Hx y y' Hy z z' Hz.
setoid_rewrite Hx. setoid_rewrite Hy. now setoid_rewrite Hz.
Qed.

Lemma bezout_1_gcd : forall n m, Bezout n m 1 -> gcd n m == 1.
Proof.
intros n m (q & r & H).
apply gcd_unique; trivial using divide_1_l, le_0_1.
intros p Hn Hm.
apply divide_add_cancel_r with (r*m).
now apply divide_mul_r.
rewrite add_comm, <- H. now apply divide_mul_r.
Qed.

(** For strictly positive numbers, we have Bezout in the two directions. *)

Lemma gcd_bezout_pos_pos : forall n, 0<n -> forall m, 0<m ->
Bezout n m (gcd n m) /\ Bezout m n (gcd n m).
Proof.
intros n Hn. rewrite <- le_succ_l, <- one_succ in Hn.
pattern n. apply strong_right_induction with (z:=1); trivial.
unfold Bezout. solve_proper.
clear n Hn. intros n Hn IHn.
intros m Hm. rewrite <- le_succ_l, <- one_succ in Hm.
pattern m. apply strong_right_induction with (z:=1); trivial.
unfold Bezout. solve_proper.
clear m Hm. intros m Hm IHm.
destruct (lt_trichotomy n m) as [LT|[EQ|LT]].
(* n < m *)
destruct (IHm (m-n)) as ((a & b & EQ), (a' & b' & EQ')).
rewrite one_succ, le_succ_l.
apply lt_add_lt_sub_l; now nzsimpl.
apply sub_lt; order'.
split.
exists (a+b). exists b.
rewrite mul_add_distr_r, EQ, mul_sub_distr_l, <- add_assoc.
rewrite gcd_sub_diag_r by order.
rewrite sub_add. reflexivity. apply mul_le_mono_l; order.
exists a'. exists (a'+b').
rewrite gcd_sub_diag_r in EQ' by order.
rewrite (add_comm a'), mul_add_distr_r, add_assoc, <- EQ'.
rewrite mul_sub_distr_l, sub_add. reflexivity. apply mul_le_mono_l; order.
(* n = m *)
rewrite EQ. rewrite gcd_diag.
split.
exists 1. exists 0. now nzsimpl.
exists 1. exists 0. now nzsimpl.
(* m < n *)
rewrite gcd_comm, and_comm.
apply IHn; trivial.
now rewrite <- le_succ_l, <- one_succ.
Qed.

Lemma gcd_bezout_pos : forall n m, 0<n -> Bezout n m (gcd n m).
Proof.
intros n m Hn.
destruct (eq_0_gt_0_cases m) as [EQ|LT].
rewrite EQ, gcd_0_r. exists 1. exists 0. now nzsimpl.
now apply gcd_bezout_pos_pos.
Qed.

(** For arbitrary natural numbers, we could only say that at least
  one of the Bezout identities holds. *)

Lemma gcd_bezout : forall n m,
Bezout n m (gcd n m) \/ Bezout m n (gcd n m).
Proof.
intros n m.
destruct (eq_0_gt_0_cases n) as [EQ|LT].
right. rewrite EQ, gcd_0_l. exists 1. exists 0. now nzsimpl.
left. now apply gcd_bezout_pos.
Qed.

Lemma gcd_mul_mono_l :
  forall n m p, gcd (p * n) (p * m) == p * gcd n m.
Proof.
intros n m p.
apply gcd_unique'.
apply mul_divide_mono_l, gcd_divide_l.
apply mul_divide_mono_l, gcd_divide_r.
intros q H H'.
destruct (eq_0_gt_0_cases n) as [EQ|LT].
rewrite EQ in *. now rewrite gcd_0_l.
destruct (gcd_bezout_pos n m) as (a & b & EQ); trivial.
apply divide_add_cancel_r with (p*m*b).
now apply divide_mul_l.
rewrite <- mul_assoc, <- mul_add_distr_l, add_comm, (mul_comm m), <- EQ.
rewrite (mul_comm a), mul_assoc.
now apply divide_mul_l.
Qed.

Lemma gcd_mul_mono_r :
forall n m p, gcd (n*p) (m*p) == gcd n m * p.
Proof.
intros. rewrite !(mul_comm _ p). apply gcd_mul_mono_l.
Qed.

Lemma gauss : forall n m p, (n | m * p) -> gcd n m == 1 -> (n | p).
Proof.
intros n m p H G.
destruct (eq_0_gt_0_cases n) as [EQ|LT].
rewrite EQ in *. rewrite gcd_0_l in G. now rewrite <- (mul_1_l p), <- G.
destruct (gcd_bezout_pos n m) as (a & b & EQ); trivial.
rewrite G in EQ.
apply divide_add_cancel_r with (m*p*b).
now apply divide_mul_l.
rewrite (mul_comm _ b), mul_assoc. rewrite <- (mul_1_l p) at 2.
rewrite <- mul_add_distr_r, add_comm, <- EQ.
now apply divide_mul_l, divide_factor_r.
Qed.

Lemma divide_mul_split : forall n m p, n ~= 0 -> (n | m * p) ->
exists q r, n == q*r /\ (q | m) /\ (r | p).
Proof.
intros n m p Hn H.
assert (G := gcd_nonneg n m). le_elim G.
destruct (gcd_divide_l n m) as (q,Hq).
exists (gcd n m). exists q.
split. now rewrite mul_comm.
split. apply gcd_divide_r.
destruct (gcd_divide_r n m) as (r,Hr).
rewrite Hr in H. rewrite Hq in H at 1.
rewrite mul_shuffle0 in H. apply mul_divide_cancel_r in H; [|order].
apply gauss with r; trivial.
apply mul_cancel_r with (gcd n m); [order|].
rewrite mul_1_l.
rewrite <- gcd_mul_mono_r, <- Hq, <- Hr; order.
symmetry in G. apply gcd_eq_0 in G. destruct G as (Hn',_); order.
Qed.

(** TODO : relation between gcd and division and modulo *)

(** TODO : more about rel_prime (i.e. gcd == 1), about prime ... *)

End NGcdProp.

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: NGcd.v Sprache: Unknown

[ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ]

^© Kompilation durch diese Firma