ペル方程式の解の存在をCoqで証明してみた
初めに
この記事はTheorem Proving Advent Calendar 2011の８日目の記事です。
以前、ペル方程式の解の存在証明をCoqで書いたので、その紹介をしようと思います。
anarchy proofでPell's equationとして投稿されていた問題です。
ちなみにFormalizing 100 theorems in Coqというリストがあるのですが、
そこには、まだCoqで証明されてない命題として載っているようなので(39. Solutions to Pell’s Equation)、Coqで証明されたのは初めてかもしれないです。
この記事の内容は、証明方針と証明してみた感想等を述べるのが目的で、Coq自体についての解説等はないのでご了承下さい。
証明する主張
「nを0より大きい整数で平方数でないとすると、x*x-n*y*y=1となる整数x,yでy≠0となるものが存在する。」
具体例としては次のようなものとなります。
n=2のとき(x,y)=(3,2) など.
n=3のとき(x,y)=(2,1) など.
n=5のとき(x,y)=(9,4) など.
coqで主張を書くと
forall (n: Z), n > 0 -> { x:Z & { y:Z | x*x - n*y*y = 1 /\ y <> 0 }} + { m:Z | n = m * m }.
となります。
方針
ペル方程式の解の存在を証明する方法は色々あると思いますが、今回は比較的Coqで表現しやすいと思われる次の証明を使います。
証明
を以下で定義します。
ただし、最後の式のs,t,uはM2T(a,b,c,d)=(s,t,u)です。
このとき実はM2T(f(a,b,c,d))=h(M2T(a,b,c,d))となっていることが分かります。
ここで例として、n=10の場合にf^k(1,0,0,1)とM2T(f^k(1,0,0,1))=h^k(M2T(1,0,0,1))を計算してみます。
k,f^k(1,0,0,1),M2T(f^k(1,0,0,1))=h^k(1,0,-10)を各行ごとに書いています。
0, (1,0,0,1), (1,0,-10)
1, (1,0,1,1), (1,1,-9)
2, (1,0,2,1), (1,2,-6)
3, (1,0,3,1), (1,3,-1)
4, (4,1,3,1), (6,2,-1)
5, (7,2,3,1), (9,1,-1)
6, (10,3,3,1), (10,0,-1)
7, (13,4,3,1), (9,-1,-1)
8, (16,5,3,1), (6,-2,-1)
9, (19,6,3,1), (1,-3,-1)
10, (19,6,22,7), (1,-2,-6)
11, (19,6,41,13), (1,-1,-9)
12, (19,6,60,19), (1,0,-10)
13, (19,6,79,25), (1,1,-9)
...
一番右の数字の三つ組みに注目するとt*t-s*u=n, s>0, u<0 が成り立っていることが分かります。
このようなs,t,uの組みは有限通りしかありません。また、hはこのような(s,t,u)の組み全体の集合に対する自己全単射です。
よって、右側に現れる三つ組みは途中で最初の(1,0,-n)に戻ってきてループするということです。（今回の例ではk=12）。
(s,t,u)=(1,0,-n)のときの(a,b,c,d)の値はM2T(a,b,c,d)=(1,0,-n)を満たすので、特にa*a-n*b*b=1となります。
(今回の例では(a,b,c,d)=(19,6,60,19) )。
最後に示さなくてはいけないことはb!=0となることですが、左側の数字は大きくなり続けるので、k=0を除いてb=0とはなりえません（後で詳しく書きます）。
coqで証明を書く
実際に上の方針をためにCoqで証明する主な内容は必要があります。
- Aが有限集合でxがAの元で、f:A→Aが単射ならあるk>0が存在してf^k(x)=x
- t*t-s*u=n, s>0, u<0 を満たすs,t,uは有限個
- k!=0ならb!=0
実は２と３が一番苦労した部分です。
まず、Coqで集合を現すのに、A:SetとP:A→Propの組みであらわすことにしました。Pが成り立つようなAの元全体を(A,P)で表すって事です。
１の主張を書くため、まず次の定義を書きます。
Definition injective_sub {A}{B} (P:A->Prop) (f:A->B) := forall (x y:A), P x -> P y -> f x = f y -> x=y. Definition finite_sub (X:Set) (P:X -> Prop) :={f:X -> nat &{n | injective_sub P f /\ forall x, f x < n } }. Definition well_def{A}{B} (f:A ->B)(P:A -> Prop) (Q:B -> Prop) := forall x:A , P x -> Q (f x).
injecttive_sub P f はfが単射となることを表します。
finite_sub X P は(X,P)が有限集合となることを表します。
well_def f P Q はfがWell-definedな写像となることを表します。
このあたりの部分はStandard-LibraryのCoq.Setsあたりを使ったほうが賢明だったかもしれないです。
Hypothesis hy1: finite_sub X P . Hypothesis hy2: well_def f P P. Hypothesis hy3: injective_sub P f. Hypothesis hy4: P x0.
↑の仮定の下で次を示します。
Fixpoint iterate{A} (n:nat) (f:A->A) (x:A) :=match n with | 0 => x | S m => f (iterate m f x) end. Lemma loop_sub: {n:nat | 0<n /\ iterate n f x0 = x0}.
↑を示すために使ったのが以下の定義と補題です。
Definition skip m n:= if (le_lt_dec m n) then S n else n. Definition skip_inv m n:= if (le_lt_dec m n) then (match n with | 0 => 0 | S k => k end) else n. Lemma skip_id:forall m n,skip_inv m (skip m n) = n. Lemma skip_lem:forall m n,m <> skip m n. Lemma php0:forall (n:nat) (f:nat -> nat) , {m | n <= f m} + {x:nat & {y| x<>y /\ f x=f y}}. Lemma php:forall (n:nat) (f:nat -> nat) , {m | n <= f m} + {x:nat & {y| x<y /\ f x=f y}}. Lemma loop_sub_iter: forall m, P (iterate m f x0). Lemma loop_sub0:{m:nat &{ n | m<n /\ iterate m f x0 = iterate n f x0}}.
まず iterate m f x0 = iterate n f x0 となるm
Let reg_t (t:Tri):Prop:=match t with |tri s t u => s>0 /\ u<0 /\ t*t-s*u=n end.
示したいことは次の補題です。
Lemma psub1:finite_sub Tri reg_t.
実はこのLemmaの証明だけに３００行近くかかっています。
このLemmaの証明は主に２パートに分かれていて、第一パートで有限集合の積の有限性を証明し(コードでいうとSection P2Nの内部)、第二パートでそれを使って、不等式を処理したりしながら有限性を示しています。証明自体はかなり冗長で気合で乗り切った部分です。
あまりうまい方法ではないですが、うまい方法を求めてぐだぐだ悩み続けるよりは、冗長な方針でもいいからとにかく書いてみるのがいいと思います。
最後に３の部分です。
右側の数字(s,t,u)が(1,0,-n)に戻ったとき、左側の数字(a,b,c,d)が(a,b)!=(1,0)となっていることを示す必要があります。
自明だと思えるような主張ですが、(a,b)!=(1,0)となる理由を書き出すと次のようなり、意外とステップ数が多いことが分かります。
- (a,b,c,d)は常にa>=1,b>=0,c>=0,d>=1である。またk!=0を除いてc>=1である。
- (a,b,c,d)->(a,b,a+c,b+d)の変換のみを繰り返していると、(s,t,u)のtが大きくなり続けて途中で矛盾する。
- よって、途中で(a,b,c,d)->(a+c,b+d,c,d)の変換が必ず入る。
- ↑の変換後は常にb>=1を満たす。
というわけでb!=1を示すのは思ったより面倒です。一つ一つ丁寧に証明していけば証明が完了します。
まとめ
- 人に説明するときなら自明の一言で済ませたくなる部分でも、Coqで証明するには非常に面倒だったりする。
- 逆に、数学的に一番キーポイントだと思える部分がCoqで書くとほんの数行だったりする。
コード
最後に少し長いですが、Coqコードを載せておきます。anarchy proof に投稿したものに「若干の変更＋Show Scriptコマンドによる整形」を行ったものです。
Require Import ZArith Znumtheory Arith. Open Scope Z_scope. (* facts about finite set *) Open Scope nat_scope. Fixpoint iterate{A} (n:nat) (f:A->A) (x:A) :=match n with | 0 => x | S m => f (iterate m f x) end. Definition skip m n:= if (le_lt_dec m n) then S n else n. Definition skip_inv m n:= if (le_lt_dec m n) then (match n with | 0 => 0 | S k => k end) else n. Lemma skip_id:forall m n,skip_inv m (skip m n) = n. intros. unfold skip in |- *. destruct le_lt_dec. unfold skip_inv in |- *. destruct le_lt_dec. auto. omega. unfold skip_inv in |- *. destruct le_lt_dec. omega. auto. Qed. Lemma skip_lem:forall m n,m <> skip m n. intros. unfold skip in |- *. destruct le_lt_dec; omega. Qed. Lemma php0:forall (n:nat) (f:nat -> nat) , {m | n <= f m} + {x:nat & {y| x<>y /\ f x=f y}}. induction n. left. exists 0. omega. intro. case (IHn f). intro. destruct s. destruct (eq_nat_dec (f x) n). destruct (IHn (fun k => f (skip x k))); destruct s. destruct (eq_nat_dec (f (skip x x0)) n). right. exists x. exists (skip x x0). split. apply skip_lem. omega. left. exists (skip x x0). omega. destruct s. destruct a. right. exists (skip x x0). exists (skip x x1). split. intro. assert (x0 = x1). rewrite <- (skip_id x x0) in |- *. rewrite <- (skip_id x x1) in |- *. rewrite H1 in |- *. auto. auto. auto. left. exists x. omega. auto. Qed. Lemma php:forall (n:nat) (f:nat -> nat) , {m | n <= f m} + {x:nat & {y| x<y /\ f x=f y}}. intros. destruct (php0 n f). auto. destruct s as (x, (y, (H1, H2))). right. destruct (le_lt_dec x y). exists x. exists y. omega. exists y. exists x. omega. Qed. Definition injective_sub {A}{B} (P:A->Prop) (f:A->B) := forall (x y:A), P x -> P y -> f x = f y -> x=y. Definition finite_sub (X:Set) (P:X -> Prop) :={f:X -> nat &{n | injective_sub P f /\ forall x, f x < n } }. Definition well_def{A}{B} (f:A ->B)(P:A -> Prop) (Q:B -> Prop) := forall x:A , P x -> Q (f x). Section LOOP. Variable (X:Set) (f:X->X) (x0:X) (P:X -> Prop). Hypothesis hy1: finite_sub X P . Hypothesis hy2: well_def f P P. Hypothesis hy3: injective_sub P f. Hypothesis hy4: P x0. Lemma loop_sub_iter: forall m, P (iterate m f x0). induction m; simpl in |- *; auto. Qed. Lemma loop_sub0:{m:nat &{ n | m<n /\ iterate m f x0 = iterate n f x0}}. destruct hy1 as (inj, (upper, (H1, H2))). clear hy1 hy2. destruct (php upper (fun n => inj (iterate n f x0))). destruct s as (m, H3). assert (inj (iterate m f x0) < upper). apply H2. exists 0. exists 0. apply False_ind. omega. destruct s as (x, (y, (H3, H4))). exists x. exists y. split. auto. apply H1; try apply loop_sub_iter. auto. Qed. Lemma minus:forall m n,n<=m -> {k | m=n+k}. intros. exists (m - n). omega. Qed. Lemma loop_sub: {n:nat | 0<n /\ iterate n f x0 = x0}. destruct loop_sub0 as (m1, (m2, (H1, H2))). assert (forall n, n <= m1 -> iterate (m1 - n) f x0 = iterate (m2 - n) f x0). induction n. intro. assert (forall mm, mm - 0 = mm). intro. omega. rewrite H0, H0 in |- *. auto. intro. apply hy3; try apply loop_sub_iter. assert (forall mm, S n <= mm -> mm - n = S (mm - S n)). intro. omega. rewrite H0, H0 in IHn; try omega. simpl in IHn. apply IHn. omega. exists (m2 - m1). split. omega. rewrite <- (H m1) in |- *. replace (m1 - m1) with 0 by omega. auto. omega. Qed. End LOOP. Check loop_sub. Lemma p_fin_inj:forall X Y P Q f ,finite_sub Y Q -> well_def f P Q -> injective_sub P f -> finite_sub X P. unfold finite_sub in |- *. unfold injective_sub in |- *. unfold well_def in |- *. intros. destruct H. exists (fun xx => x (f xx)). destruct s. exists x0. destruct a. split. intros. apply H1. auto. auto. apply H. apply H0. auto. apply H0. auto. auto. intro. apply H2. Qed. Definition prod_prop{A}{B}(P:A->Prop)(Q:B->Prop)(z:(A*B)%type):= let (x,y) := z in P x /\ Q y. Section aP2N. Variable xs:nat. Definition P2N x y:=x+y*xs. Lemma p_p2n1 x1 x2 y1 y2:x1<xs -> x2<xs -> y1<y2 -> P2N x1 y1 < P2N x2 y2. intros. unfold P2N in |- *. assert {dy : _ | y2 = dy + 1 + y1}. exists (y2 - y1 - 1). omega. destruct H2. rewrite e in |- *. replace ((x + 1 + y1) * xs) with (x * xs + y1 * xs + xs) by ring. assert (0 <= x * xs). apply le_O_n. omega. Qed. Lemma p_p2n3 x1 x2 y1 y2:x1<xs -> x2<xs -> P2N x1 y1 =P2N x2 y2 -> y1=y2. intros. destruct (lt_eq_lt_dec y1 y2). destruct s. assert (P2N x1 y1 < P2N x2 y2). apply p_p2n1. auto. omega. auto. omega. auto. assert (P2N x2 y2 < P2N x1 y1). apply p_p2n1. auto. omega. auto. omega. Qed. Lemma p_p2n4 x1 x2 y1 y2 :x1<xs -> x2 <xs -> P2N x1 y1 = P2N x2 y2 -> x1 =x2 /\ y1=y2. intros. assert (y1 = y2). apply (p_p2n3 x1 x2 y1 y2); omega. split. unfold P2N in H1. rewrite H2 in H1. omega. auto. Qed. Definition P2Nprod z:=match z with (x,y) => P2N x y end. Definition regular_prod (z:nat*nat):=match z with (x,y) => x<xs end. Lemma p_p2n5 z1 z2:regular_prod z1 -> regular_prod z2 -> P2Nprod z1 = P2Nprod z2 -> z1=z2. intros z1 z2 H1 H2 H. destruct z1 as (x1, y1). destruct z2 as (x2, y2). unfold regular_prod in *. assert (x1 = x2 /\ y1 = y2). apply p_p2n4; auto. destruct H0. auto. Qed. End aP2N. Check P2Nprod. Lemma p_fin_prod:forall X Y P Q , finite_sub X P -> finite_sub Y Q -> finite_sub ( (X*Y)%type ) (prod_prop P Q). intros. destruct H as (jx, (xs, (HX1, HX2))). destruct H0 as (jy, (ys, (HY1, HY2))). exists (fun z => match z with | pair x y => P2Nprod xs (jx x, jy y) end). exists (ys * xs). split. unfold injective_sub in |- *. intros z1 z2 H1 H2 H. destruct z1 as (x1, y1). destruct z2 as (x2, y2). assert (x1 = x2 /\ y1 = y2). assert ((jx x1, jy y1) = (jx x2, jy y2)). apply (p_p2n5 xs); simpl in |- *; auto. inversion H0. split; [ apply HX1 | apply HY1 ]; destruct H1; destruct H2; auto. destruct H0. rewrite H0, H3 in |- *. auto. intro. destruct x as (x, y). unfold P2Nprod in |- *. unfold P2N in |- *. assert (jx x < xs). apply HX2. assert (jy y < ys). apply HY2. assert (S (jy y) * xs <= ys * xs). apply mult_le_compat_r; omega. simpl in H1. omega. Qed. Open Scope Z_scope. Inductive perfect_square : Z -> Prop := ps_intro : forall n, perfect_square (n * n). Lemma perfect_square_dec: forall n, { m | n=m*m} + {~perfect_square n}. intros. destruct (Z_eq_dec (Zsqrt_plain n * Zsqrt_plain n) n). left. rewrite <- e in |- *. exists (Zsqrt_plain n). auto. right. intro. destruct H. destruct (Z_lt_dec 0 n). rewrite Zsqrt_square_id in n0. omega. omega. replace (n * n) with (- n * - n) in n0 by ring. rewrite Zsqrt_square_id in n0. omega. omega. Qed. Lemma sqpos:forall n, 0<>n -> 0<n*n. intros. destruct (Z_lt_dec 0 n). apply Zmult_lt_0_compat; auto. replace (n * n) with (- n * - n) by ring. apply Zmult_lt_0_compat; omega. Qed. Section A. Variable n:Z. Hypothesis pos:n>0. Hypothesis psn:~(perfect_square n). Inductive Tri: Set := | tri (s t u:Z) :Tri. Inductive Mat: Set := |mat (a b c d:Z):Mat. Let M2T (m:Mat) := match m with |mat a b c d => tri (a*a-n*b*b) (a*c-n*b*d) (c*c-n*d*d) end. Let f (m:Mat) := match m with |mat a b c d =>match M2T(m) with |tri s t u => if (Z_lt_dec 0 (s+t+t+u)) then mat (a+c) (b+d) c d else mat a b (a+c) (b+d) end end. Let reg_t (t:Tri):Prop:=match t with |tri s t u => s>0 /\ u<0 /\ t*t-s*u=n end. Definition h t:=match t with |tri s t u => if (Z_lt_dec 0 (s+t+t+u)) then tri (s+t+t+u) (t+u) u else tri s (s+t) (s+t+t+u) end. Definition h_inv t:=match t with |tri s t u => if (Z_lt_dec 0 (s-t-t+u)) then tri (s-t-t+u) (t-u) u else tri s (-s+t) (s-t-t+u) end. Definition Z2:=(Z*Z)%type. Definition Z3:=(Z*Z*Z)%type. Definition prZ z:=0<=z<=n+n. Definition prZ2 z2:=match z2 with | (a,b) => 0<=a<=n+n /\ 0<=b<=n+n end. Definition prZ3 z3:=match z3 with | (a,b,c) => 0<a<=n /\ 0<=b<=n+n /\ 0<c<=n end. Definition prZ3em t :=match t with | tri s t u =>(s,t+n,-u) end. Lemma p_fin_prod2:forall (X Y:Set) (P:X -> Prop) (Q:Y->Prop) (R:(X*Y)%type -> Prop), finite_sub X P -> finite_sub Y Q -> (forall x y , R (x,y) -> P x /\ Q y) -> finite_sub (X*Y) R. intros. assert (finite_sub (X * Y) (prod_prop P Q)). apply p_fin_prod; auto. unfold finite_sub in |- *. unfold finite_sub in H2. destruct H2 as (f00). destruct s as (n00). exists f00. exists n00. split. destruct a. unfold injective_sub in |- *. unfold injective_sub in H2. unfold prod_prop in H2. intros r1 r2. intros. destruct r1 as (x1, y1). destruct r2 as (x2, y2). apply H2. apply H1; auto. apply H1; auto. auto. apply a. Qed. Lemma pzn:forall n,0<=n -> Z_of_nat (Zabs_nat n) = n. intros. destruct n0. simpl in |- *. auto. simpl in |- *. rewrite Zpos_eq_Z_of_nat_o_nat_of_P in |- *. auto. assert (Zneg p < 0). apply Zlt_neg_0. omega. Qed. Definition embzn zup z:= if (Z_le_dec z zup) then (if Z_le_dec 0 z then Zabs_nat z else 0%nat )else 0%nat. Definition ZNP:=Zpos_eq_Z_of_nat_o_nat_of_P. Lemma psubz:finite_sub Z prZ. unfold prZ in |- *. unfold finite_sub in |- *. assert (0 < n + n). omega. revert H. generalize (n + n). intros. exists (embzn z). exists (1 + Zabs_nat z)%nat. unfold injective_sub in |- *. split. intros. unfold embzn in H2. destruct Z_le_dec; destruct Z_le_dec; try omega. destruct Z_le_dec; try destruct Z_le_dec; try omega. rewrite <- pzn in |- *. rewrite <- (pzn x) in |- *. auto. omega. omega. unfold embzn in |- *. intro. destruct Z_le_dec; try destruct Z_le_dec; try omega. unfold Zabs_nat in |- *. destruct x. omega. destruct z. omega. apply inj_lt_rev. rewrite inj_plus in |- *. rewrite <- ZNP in |- *. rewrite <- ZNP in |- *. replace (Z_of_nat 1) with 1 . omega. auto. assert (Zneg p0 < 0). apply Zlt_neg_0. omega. assert (Zneg p < 0). apply Zlt_neg_0. omega. Qed. Lemma psub10:finite_sub Z3 prZ3. apply (p_fin_prod2 Z2 Z prZ2 prZ). apply (p_fin_prod2 Z Z prZ prZ). exact psubz. exact psubz. unfold prZ2 in |- *. unfold prZ in |- *. intros. omega. exact psubz. destruct x. unfold prZ3 in |- *. unfold prZ2 in |- *. unfold prZ in |- *. intros. omega. Qed. Lemma sqpos2:forall x,0<=x*x. intro. destruct (Z_zerop x). rewrite e in |- *. simpl in |- *. omega. assert (0 < x * x). apply sqpos. omega. omega. Qed. Lemma sql0:forall x , 0<=x -> x*x<=n -> -n<=x<=n. intros. destruct (Z_zerop x). omega. destruct (Z_le_dec x n). omega. assert (x * n < x * x). apply Zmult_lt_compat_l; omega. assert (1 * n <= x * n). apply Zmult_le_compat_r; omega. omega. Qed. Lemma sql1:forall x , x*x<=n -> -n<=x<=n. intros. destruct (Z_lt_dec x 0). cut (- n <= - x <= n). intro. omega. apply sql0. omega. replace (- x * - x) with (x * x) by ring. omega. apply sql0; omega. Qed. Lemma sql2:forall x y,0<x -> 0<y -> x*y<=n -> x<=n. intros. destruct (Z_le_dec x n). omega. assert (n * 1 <= n * y). apply Zmult_le_compat_l; omega. assert (n * y < x * y). apply Zmult_lt_compat_r; omega. omega. Qed. Lemma psub1:finite_sub Tri reg_t. apply (p_fin_inj Tri Z3 reg_t prZ3 prZ3em). exact psub10. unfold well_def in |- *. intros. destruct x. unfold reg_t in H. unfold prZ3em in |- *. unfold prZ3 in |- *. destruct H. assert (0 <= t * t). apply sqpos2. assert (s * u < 0). assert (0 < s * - u). apply Zmult_lt_0_compat; omega. replace (s * u) with (- (s * - u)) by ring. omega. assert (- n <= t <= n). apply sql1. omega. assert (s * - u <= n). replace (s * - u) with (- (s * u)) by ring. omega. split. assert (s <= n). apply (sql2 s (- u)); omega. omega. split. omega. split. omega. apply (sql2 (- u) s). omega. omega. replace (- u * s) with (s * - u) by ring. omega. unfold injective_sub in |- *. intros. unfold prZ3em in H1. destruct x. destruct y. injection H1. intros. assert (s = s0 /\ t = t0 /\ u = u0) by complete omega. destruct H5. destruct H6. rewrite H5, H6, H7 in |- *. auto. Qed. Lemma psub2:well_def h reg_t reg_t. unfold well_def in |- *. unfold reg_t in |- *. intros. destruct x. unfold h in |- *. destruct H. destruct H0. destruct Z_lt_dec; split. omega. split. omega. rewrite <- H1 in |- *. ring. omega. split. destruct (Z_zerop (s + t + t + u)). assert (s = - t - t - u). omega. rewrite H2 in H1. apply False_ind. apply psn. replace n with ((t + u) * (t + u)) . apply ps_intro. rewrite <- H1 in |- *. ring. omega. rewrite <- H1 in |- *. ring. Qed. Lemma pp_inj_tri :forall s1 s2 t1 t2 u1 u2 , s1=s2 -> t1=t2 -> u1=u2 -> tri s1 t1 u1 = tri s2 t2 u2. intros. rewrite H, H0, H1 in |- *. auto. Qed. Lemma h_id:forall t, (reg_t t) -> h_inv (h t) = t. intros. destruct t. unfold h in |- *. unfold h_inv in |- *. unfold reg_t in H. destruct Z_lt_dec. destruct Z_lt_dec. apply pp_inj_tri; omega. apply False_ind; omega. destruct Z_lt_dec. apply pp_inj_tri; omega. apply pp_inj_tri; omega. Qed. Lemma psub3:injective_sub reg_t h. unfold injective_sub in |- *. intros. rewrite <- h_id in |- *. rewrite <- (h_id x) in |- *. rewrite H1 in |- *. auto. auto. auto. Qed. Lemma loop_h:{ k:nat | (0<k)%nat /\ iterate k h (tri 1 0 (-n) ) = (tri 1 0 (-n))}. apply loop_sub with reg_t. exact psub1. exact psub2. exact psub3. unfold reg_t in |- *. split. omega. split. omega. ring. Qed. Definition K:=(proj1_sig loop_h). Definition Finalmat:=iterate K f (mat 1 0 0 1). Definition X:=match Finalmat with | mat a b c d => a end. Definition Y:=match Finalmat with |mat a b c d => b end. Definition X2:=match Finalmat with |mat a b c d => c end. Definition Y2:=match Finalmat with |mat a b c d => d end. Lemma loopK : (0<K)%nat /\ iterate K h (tri 1 0 (-n)) = tri 1 0 (-n). exact (proj2_sig loop_h). Qed. Lemma loopK_1: (0<K)%nat. apply loopK. Qed. Lemma loopK_2:iterate K h (tri 1 0 (-n)) = tri 1 0 (-n). apply loopK. Qed. Lemma eq_Finalmat:mat X Y X2 Y2 = Finalmat. unfold X, Y, X2, Y2 in |- *. destruct Finalmat. auto. Qed. Lemma pp1 m:M2T(f(m)) = h( M2T(m)). destruct m. unfold f in |- *. unfold h in |- *. unfold M2T in |- *. destruct Z_lt_dec; apply pp_inj_tri; ring. Qed. Lemma pp2:M2T Finalmat = tri 1 0 (-n). rewrite <- loopK_2 in |- *. unfold Finalmat in |- *. generalize K. induction n0. unfold iterate in |- *. unfold M2T in |- *. replace (1 * 1 - n * 0 * 0) with 1 by ring. replace (1 * 0 - n * 0 * 1) with 0 by ring. replace (0 * 0 - n * 1 * 1) with (- n) by ring. auto. simpl in |- *. rewrite <- IHn0 in |- *. apply pp1. Qed. Definition reg1_m m:=match m with |mat a b c d =>a>0 /\ b>0 /\ c>=0 /\ d>0 end. Definition reg2_m m:=match m with |mat a b c d =>a>0 /\ b>=0 /\ c>0 /\ d>0 end. Definition reg3_m m:={reg1_m m} + {reg2_m m}. Lemma f_dec:forall a b c d, {f (mat a b c d) = mat (a+c) (b+d) c d} + {f (mat a b c d) = mat a b (a+c) (b+d)}. intros. unfold f in |- *. destruct M2T. destruct (Z_lt_dec 0 (s + t + t + u)). left. auto. right. auto. Qed. Lemma pp3_1: forall m,reg1_m m -> reg1_m (f m). destruct m. destruct (f_dec a b c d); rewrite e in |- *; unfold reg1_m in |- *; omega. Qed. Lemma pp3_2: forall m,reg2_m m -> reg2_m (f m). destruct m. destruct (f_dec a b c d); rewrite e in |- *; unfold reg2_m in |- *; omega. Qed. Lemma pp3_3:forall m,reg3_m m -> reg3_m (f m). intros. unfold reg3_m in |- *. destruct H. left. apply pp3_1. auto. right. apply pp3_2. auto. Qed. Lemma pp3_4:reg3_m Finalmat. unfold Finalmat in |- *. assert (0 < K)%nat. exact loopK_1. induction K. left. apply False_ind. omega. destruct (zerop n0). rewrite e in |- *. unfold iterate in |- *. destruct (f_dec 1 0 0 1); rewrite e0 in |- *. left. unfold reg1_m in |- *. omega. right. unfold reg2_m in |- *. omega. simpl in |- *. apply pp3_3. auto. Qed. Lemma pp4: 1=(X*X - n*Y*Y) /\ 0 = (X*X2 - n*Y*Y2) /\ (-n) =(X2*X2 - n*Y2*Y2) . assert (tri 1 0 (- n) = tri (X * X - n * Y * Y) (X * X2 - n * Y * Y2) (X2 * X2 - n * Y2 * Y2)). rewrite <- pp2 in |- *. rewrite <- eq_Finalmat in |- *. unfold M2T in |- *. auto. injection H. auto. Qed. Lemma pp3_5:X<>1 /\ Y<>0. destruct pp4. destruct H0. destruct pp3_4; rewrite <- eq_Finalmat in r. unfold reg1_m in r. split. destruct (Z_eq_dec X 1). rewrite e in H. replace (1 * 1) with 1 in H by ring. assert (n * Y * Y = 0). omega. replace (n * Y * Y) with (n * (Y * Y)) in H2 by ring. assert (n = 0). apply (Zmult_integral_l (Y * Y)). assert (0 < Y * Y). apply sqpos. omega. omega. auto. omega. auto. omega. unfold reg2_m in r. destruct (Z_zerop Y). rewrite e in H0. replace (n * 0 * Y2) with 0 in H0 by ring. assert (X = 0). apply (Zmult_integral_l X2); omega. omega. split. destruct (Z_eq_dec X 1). rewrite e in H. replace (1 * 1) with 1 in H by ring. assert (n * Y * Y = 0). omega. replace (n * Y * Y) with (n * (Y * Y)) in H2 by ring. assert (n = 0). apply (Zmult_integral_l (Y * Y)). assert (0 < Y * Y). apply sqpos. omega. omega. auto. omega. auto. auto. Qed. Lemma pell_eq:{ x:Z & { y:Z | x*x - n*y*y = 1 /\ x <> 1 /\ y <> 0 }}. exists X. exists Y. split. symmetry in |- *. apply pp4. apply pp3_5. Qed. End A. Theorem Pell's_equation: forall (n: Z), n > 0 -> { x:Z & { y:Z | x*x - n*y*y = 1 /\ x <> 1 /\ y <> 0 }} + { m:Z | n = m * m }. Proof. intros. destruct (perfect_square_dec n). auto. left. apply pell_eq. auto. auto. Qed.
