Mercurial > hg > Members > kono > Proof > automaton

changeset 230:a72bcc6eadad

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
prime done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 24 Jun 2021 11:02:58 +0900
parents fb080920c104
children 54977cc189e6
files automaton-in-agda/src/gcd.agda automaton-in-agda/src/prime.agda
diffstat 2 files changed, 43 insertions(+), 41 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda	Thu Jun 24 00:37:46 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Thu Jun 24 11:02:58 2021 +0900
@@ -508,39 +508,21 @@
       Dividable.factor d * k + 0  ≡⟨ Dividable.is-factor d ⟩
       i  ∎ ) 0<i ) where open ≡-Reasoning
 
-gcd-≤ : ( i j  : ℕ ) → i ≤ j → gcd i j ≤ j
-gcd-≤ zero zero z≤n = ≤-refl
-gcd-≤ 0 (suc j) z≤n = subst (λ k → k ≤ suc j ) (trans (sym (gcd20 (suc j))) (gcdsym  {suc j} {zero})) ≤-refl
-gcd-≤ (suc i) (suc j) (s≤s i<j) = begin
+m*n=m→n : {m n : ℕ } → 0 < m → m * n ≡ m * 1 → n ≡ 1
+m*n=m→n {suc m} {n} (s≤s lt) eq = *-cancelˡ-≡ m eq 
+
+gcd-≤ : ( i j  : ℕ ) → 0 < i → i ≤ j → gcd i j ≤ i
+gcd-≤ zero _ () z≤n 
+gcd-≤ (suc i) (suc j) _ (s≤s i<j) = begin
       gcd (suc i) (suc j)   ≡⟨ sym m*1=m ⟩
       gcd (suc i) (suc j) * 1  ≤⟨ *-monoʳ-≤ (gcd (suc i) (suc j)) (f-div>0 d (s≤s z≤n)) ⟩
       gcd (suc i) (suc j) * f  ≡⟨ +-comm 0 _ ⟩
       gcd (suc i) (suc j) * f  + 0  ≡⟨ cong (λ k → k + 0) (*-comm (gcd (suc i) (suc j)) _  ) ⟩
-      Dividable.factor (proj2 (gcd-dividable (suc i) (suc j))) * gcd (suc i) (suc j) + 0 ≡⟨ Dividable.is-factor (proj2 (gcd-dividable (suc i) (suc j)))  ⟩
-      suc j  ∎ where
-          d = proj2 (gcd-dividable (suc i) (suc j))
-          f = Dividable.factor (proj2 (gcd-dividable (suc i) (suc j)))
+      Dividable.factor (proj1 (gcd-dividable (suc i) (suc j))) * gcd (suc i) (suc j) + 0 ≡⟨ Dividable.is-factor (proj1 (gcd-dividable (suc i) (suc j)))  ⟩
+      suc i  ∎ where
+          d = proj1 (gcd-dividable (suc i) (suc j))
+          f = Dividable.factor (proj1 (gcd-dividable (suc i) (suc j)))
           open ≤-Reasoning
 
-m*n=m→n : {m n : ℕ } → 0 < m → m * n ≡ m * 1 → n ≡ 1
-m*n=m→n {suc m} {n} (s≤s lt) eq = *-cancelˡ-≡ m eq 
-
-gcd-< : ( i j  : ℕ ) → 0 < i → i < j → gcd i j < j
-gcd-<  i j  0<i  i<j with <-cmp ( gcd i j ) j
-... | tri< a ¬b ¬c = a
-... | tri≈ ¬a b ¬c = ⊥-elim (g111 (Dividable.factor (proj1 (gcd-dividable i j)))
-                 (subst (λ k → (Dividable.factor (proj1 (gcd-dividable i j))) * k + 0 ≡ i ) b (Dividable.is-factor (proj1 (gcd-dividable i j))))) where
-   g111 : (f : ℕ) → f * j + 0 ≡ i → ⊥
-   g111 zero eq = nat-≡<  eq 0<i
-   g111 (suc zero) eq = nat-≡< (sym eq) (begin
-       suc i ≤⟨ i<j ⟩
-       j ≡⟨ trans (+-comm 0 _) (+-comm 0 _) ⟩
-       1 * j + 0 ∎ )  where open ≤-Reasoning
-   g111 (suc (suc f)) eq = nat-≡< (sym eq) ( begin
-       suc i ≤⟨ i<j ⟩
-       j ≡⟨ +-comm  0 _  ⟩
-       j + 0 ≤⟨ +-monoʳ-≤ j z≤n ⟩
-       j + ((j + f * j) + 0) ≡⟨ sym (+-assoc j _ _) ⟩
-       j + (j + f * j) + 0 ≡⟨ refl ⟩
-       suc (suc f) * j + 0 ∎ )  where open ≤-Reasoning
-... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> (gcd-≤ i j (<to≤ i<j)) c )
+gcd-≥ : ( i j  : ℕ ) → 0 < i → i ≤ j → gcd j i ≤ i
+gcd-≥ i j 0<i i≤j = subst (λ k → k ≤ i) (gcdsym {i} {j}) ( gcd-≤ i j 0<i i≤j )
--- a/automaton-in-agda/src/prime.agda	Thu Jun 24 00:37:46 2021 +0900
+++ b/automaton-in-agda/src/prime.agda	Thu Jun 24 11:02:58 2021 +0900
@@ -49,37 +49,57 @@
 open _∧_
 
 data Factoring (m : ℕ ) : (n : ℕ) → Set where
-     findFactor : (n : ℕ) → ( (j : ℕ ) → m ≤ j → j < n → gcd n j ≡ 1  ) → Factoring m n
+     findFactor : (n : ℕ) → m ≤ n → ( (j : ℕ ) → m ≤ j → j < n → gcd n j ≡ 1  ) → Factoring m n
      skipFactor : (n : ℕ) → n < m →  Factoring m n
 
 nonPrime : { n : ℕ } → 1 < n → ¬ Prime n → NonPrime n
-nonPrime {n} 1<n np = np1 n n np 1<n (findFactor n (λ j n≤j j<n → ⊥-elim (nat-≤>  n≤j j<n ) )) where
+nonPrime {n} 1<n np = np1 n n np 1<n (findFactor n ≤-refl (λ j n≤j j<n → ⊥-elim (nat-≤>  n≤j j<n ) )) where
     mg1 :  (n m : ℕ )→ ( (j : ℕ ) → m < j → j < n → gcd n j ≡ 1  ) →  gcd n m ≡ 1 → (j : ℕ) → m ≤ j → j < n → gcd n j ≡ 1
     mg1 n m mg gcd j m<j j<n with <-cmp m j
     ... | tri< a ¬b ¬c = mg j a j<n  
     ... | tri≈ ¬a refl ¬c = gcd
     ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> m<j c)
     np1 : ( n m : ℕ ) → ¬ Prime n → 1 < n → Factoring m n → NonPrime n
-    np1 n zero np 1<n (findFactor n  mg ) = ⊥-elim ( np record { isPrime = λ j lt _ → mg j z≤n lt ; p>1 = 1<n } ) -- zero < j , j < n
-    np1 n (suc m) np 1<n (findFactor n  mg) with <-cmp ( gcd n m ) 1
+    np1 n zero np 1<n (findFactor n m≤n mg ) = ⊥-elim ( np record { isPrime = λ j lt _ → mg j z≤n lt ; p>1 = 1<n } ) -- zero < j , j < n
+    np1 n (suc m) np 1<n (findFactor n m≤n mg) with <-cmp ( gcd n m ) 1
     ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> ( gcd>0 n m (<-trans (s≤s z≤n) 1<n) 0<m ) a ) where
          0<m : 0 < m
          0<m with <-cmp 0 m
          ... | tri< a ¬b ¬c = a
          ... | tri≈ ¬a refl ¬c = ⊥-elim ( nat-<> a (subst (λ k → 1 < k) (sym (gcd20 n)) 1<n ))
-    ... | tri≈ ¬a b ¬c = np1 n m np 1<n (findFactor n (mg1 n m mg b ) )
+    ... | tri≈ ¬a b ¬c = np1 n m np 1<n (findFactor n (≤-trans refl-≤s m≤n) (mg1 n m mg b ) )
     ... | tri> ¬a ¬b c with PrimeP ( gcd n m )
     ... | yes y = record { factor = gcd n m ; prime = y ;  dividable = proj1 (gcd-dividable n m ) }
-    ... | no ngcd with np1 (gcd n m) m ngcd c (skipFactor (gcd n m) {!!}) 
-    ... | cc = record { factor = NonPrime.factor cc ; prime = NonPrime.prime cc ; dividable =
+    ... | no ngcd = np2 where
+         skip-case : NonPrime (gcd n m) → NonPrime n
+         skip-case  cc = record { factor = NonPrime.factor cc ; prime = NonPrime.prime cc ; dividable =
                           record { factor = (Dividable.factor (proj1 (gcd-dividable n m))) * (Dividable.factor (NonPrime.dividable cc))
-                              ; is-factor = {!!} } } -- cc : NonPrime (gcd n m )
+                              ; is-factor = begin
+             Dividable.factor (proj1 (gcd-dividable n m)) * Dividable.factor (NonPrime.dividable cc) * NonPrime.factor cc + 0 ≡⟨ refl ⟩
+             g * d * p + 0 ≡⟨ +-comm _ 0 ⟩
+             g * d * p  ≡⟨ *-assoc g d p  ⟩
+             g * (d * p)  ≡⟨ cong (λ k → g * k ) (+-comm 0 _) ⟩
+             g * (d * p + 0)  ≡⟨ cong (λ k → g * k ) (Dividable.is-factor (NonPrime.dividable cc) ) ⟩
+             g * gcd n m  ≡⟨ +-comm 0 _ ⟩
+             g * gcd n m + 0 ≡⟨ Dividable.is-factor (proj1 (gcd-dividable n m)) ⟩
+             n ∎  }} where
+                open ≡-Reasoning
+                g =  Dividable.factor (proj1 (gcd-dividable n m))
+                d =  Dividable.factor (NonPrime.dividable cc)
+                p = NonPrime.factor cc
+         np2 :  NonPrime n
+         np2 with <-cmp (gcd n m) m
+         ... | tri< a ¬b ¬c = skip-case (np1 (gcd n m) m ngcd c (skipFactor (gcd n m) a ))
+         ... | tri≈ ¬a b ¬c = skip-case (np1 (gcd n m) m ngcd c
+              (subst (λ k → Factoring m k) (sym b) (findFactor m ≤-refl (λ j n≤j j<n → ⊥-elim (nat-≤>  n≤j j<n) ))))
+         ... | tri> ¬a ¬b' c with <-cmp 0 m
+         ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> (gcd-≥ m n a (≤-trans refl-≤s m≤n)) c )
+         ... | tri≈ ¬a' b' ¬c = ⊥-elim ( np record { isPrime = λ j lt 0<j → mg j (subst (λ k → k < j) b' 0<j) lt ; p>1 = 1<n } ) -- suc m ≤ j
     np1 n zero np 1<n (skipFactor n ())
     np1 n (suc m) np 1<n  (skipFactor n n<m) with <-cmp m n
     ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a n<m) 
-    ... | tri> ¬a ¬b c = np1 n m np 1<n  (skipFactor n c) 
-    ... | tri≈ ¬a refl ¬c with np1 n m np 1<n (findFactor m (λ j n≤j j<n → ⊥-elim (nat-≤>  n≤j j<n) ))
-    ... | np2 = np1 n m np 1<n (findFactor m (λ j n≤j j<n → ⊥-elim (nat-≤>  n≤j j<n)))
+    ... | tri> ¬a ¬b c    = np1 n m np 1<n (skipFactor n c) 
+    ... | tri≈ ¬a refl ¬c = np1 n m np 1<n (findFactor m ≤-refl (λ j n≤j j<n → ⊥-elim (nat-≤>  n≤j j<n) ))
 
 
 prime-is-infinite : (max-prime : ℕ ) → ¬ ( (j : ℕ) → max-prime < j → ¬ Prime j )