證明Coq的nat的高斯定理

我想證明nat的高斯定理。證明Coq的nat的高斯定理

在普通（非精確）語言，它說：如果a劃分b*c和無的a的因素是在b那麼它們必須全部在c。

Require Import NPeano. 
Theorem Gauss_nat: forall (a b c:nat), gcd a b = 1 -> (a | (b*c)) -> (a | c).

定理已經爲整數Z定義，見here in the Coq manual。但我需要它的nat。到目前爲止，我已經得到的建議是使用的Bezout引理其中指出

Lemma Bezout: forall (a b c:Z), Z.gcd a b = c -> exists u v, u*a+v*b=c.

但是，我不能直接使用它nat小號自從係數u和v可能是負值，因此不成立爲nat。

是否還有另一個證明在證明中不使用整數？

編輯：

正如指出了由Mark Dickinson公司，定理和引理評論已經在勒柯克的圖書館。他們在NPeano，名爲Nat.gcd_bezout和Nat.gauss。

來源

2015-11-21 larsr

你能證明和使用的Bezout的基於NAT的版本：'FORALL（AB：NAT），存在紫外線，U * A = GCD ab + v * b'。 –

這將是完美的！你能否給出一個「回答」，指出一名基於自然力量的Bezout的Coq教授以及Gauss_nat如何跟隨它？ – larsr

（或者至少'bezout_nat'，我能夠通過使用它證明Gauss_nat ....） – larsr

如果您只是想獲得nat的結果，而不是真的避免使用Z，那麼您可以在標準庫中重新使用該證明。這裏是你如何能進行草圖，依靠兩個輔助引理：

Require Import NPeano. 
Require Import ZArith. 
Require Import ZArith.Znumtheory. 
Require Import Omega. 

Close Scope Z_scope. 

Lemma Zdiv_Ndiv a b : (a | b) <-> (Z.of_nat a | Z.of_nat b)%Z. 
Proof. Admitted. 

Lemma Zgcd_Ngcd a b : Z.of_nat (gcd a b) = Z.gcd (Z.of_nat a) (Z.of_nat b). 
Proof. Admitted. 

Theorem Gauss_nat a b c : gcd a b = 1 -> (a | (b*c)) -> (a | c). 
Proof. 
rewrite Zdiv_Ndiv, Zdiv_Ndiv, Nat2Z.inj_mul. 
intros H1 H2. 
assert (H3 : Z.of_nat (gcd a b) = 1%Z) by (rewrite H1; reflexivity). 
rewrite Zgcd_Ngcd in H3. 
apply (Gauss _ _ _ H2). 
now rewrite <- Zgcd_1_rel_prime. 
Qed.

來源

2015-11-21 08:41:52

謝謝，這是有用的 - 我偶爾想要一點點在Z和nat之間來回借用定理。（要明確處理所有的Z.to_nat和Z.from_nat和Nat2Z.inj_mul，看起來相當醜陋，但也許它比「魔術」轉換更好......） – larsr

證明Coq的nat的高斯定理

回答

相關問題