Mercurial > hg > Members > kono > Proof > automaton

changeset 199:4a83abf7b822

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 17 Jun 2021 22:42:36 +0900
parents 4b452c9d7e7b
children a5c8a90615be
files automaton-in-agda/src/gcd.agda automaton-in-agda/src/prime.agda automaton-in-agda/src/root2.agda
diffstat 3 files changed, 66 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda	Thu Jun 17 17:16:36 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Thu Jun 17 22:42:36 2021 +0900
@@ -30,6 +30,12 @@
 FtoD : {n m : ℕ} → (fc : Factor n m) → remain fc ≡ 0 → Dividable n m 
 FtoD {n} {m} record { factor = f ; remain = r ; is-factor = fa } refl = record { factor = f ; is-factor = fa }
 
+--decD : {n m : ℕ} → Dec (Dividable n m)
+--decD = {!!}
+
+--divdable^2 : ( n k : ℕ ) → Dividable k ( n * n ) → Dividable k n
+--divdable^2 n k dn2 = {!!}
+
 decf : { n k : ℕ } → ( x : Factor k (suc n) ) → Factor k n
 decf {n} {k} record { factor = f ; remain = r ; is-factor = fa } = 
  decf1 {n} {k} f r fa where
@@ -278,3 +284,7 @@
       gcd (m * n + 1) n ≡⟨ gcdmul+1 m n ⟩
       1 ∎ where open ≡-Reasoning
 
+div+1 : { i k : ℕ } → k > 1 →  Dividable k i →  ¬ Dividable k (suc i)  
+div+1 {i} {k} k>1 d d1 = div1 k>1 div+11 where
+   div+11 : Dividable k 1
+   div+11 = subst (λ g → Dividable k g) (minus+y-y {1} {i} ) ( proj2 (div-div k>1 d d1  ) )
--- a/automaton-in-agda/src/prime.agda	Thu Jun 17 17:16:36 2021 +0900
+++ b/automaton-in-agda/src/prime.agda	Thu Jun 17 22:42:36 2021 +0900
@@ -21,31 +21,69 @@
    field
       factor : ℕ
       prime : Prime factor
+      p>0 : factor > 1
       dividable : Dividable factor n
 
-isPrime : ( n : ℕ ) → Dec ( Prime n )
-isPrime = {!!}
+PrimeP : ( n : ℕ ) → Dec ( Prime n )
+PrimeP 0 = yes record { isPrime = λ j () }
+PrimeP (suc n) = isPrime1 (suc n) n a<sa (λ i m<i i<n → {!!} ) where
+   isPrime1 : ( n m : ℕ ) → m < n → ( (i : ℕ) → m ≤ i → i < n  →  gcd n i ≡ 1 )  → Dec ( Prime n )
+   isPrime1 n zero m<n lt = yes record { isPrime = λ j j<i → lt j z≤n {!!} }
+   isPrime1 n (suc m) m<n lt with <-cmp (gcd n (suc m)) 1
+   ... | tri< a ¬b ¬c = {!!}
+   ... | tri≈ ¬a b ¬c = isPrime1 n m {!!} {!!}
+   ... | tri> ¬a ¬b c = no ( λ p → nat-≡< (sym (Prime.isPrime p (suc m) {!!} )) c )
 
-nonPrime : ( n : ℕ ) → ¬ Prime n → NonPrime n
-nonPrime n np = np1 n (λ j n≤j j<n → ⊥-elim (nat-≤>  n≤j j<n ) ) where
+nonPrime : { n : ℕ } → ¬ Prime n → NonPrime n
+nonPrime {n} np = np1 n (λ j n≤j j<n → ⊥-elim (nat-≤>  n≤j j<n ) ) where
     np1 : ( m : ℕ ) → ( (j : ℕ ) → m ≤ j → j < n → gcd n j ≡ 1  ) → NonPrime n
     np1 zero mg = ⊥-elim ( np record { isPrime = λ j lt → mg j z≤n lt } ) -- zero < j , j < n
     np1 (suc m) mg with <-cmp ( gcd n (suc m) ) 1
     ... | tri< a ¬b ¬c = {!!}
     ... | tri≈ ¬a b ¬c = np1 m {!!}
-    ... | tri> ¬a ¬b c = record { factor = gcd n (suc m) ; prime = {!!} ; dividable = record { factor = {!!} ; is-factor = {!!} } }
+    ... | tri> ¬a ¬b c = record { factor = gcd n (suc m) ; prime = {!!} ; p>0 = c ; dividable = record { factor = {!!} ; is-factor = {!!} } }
+
 
 prime-is-infinite : (max-prime : ℕ ) → ¬ ( (j : ℕ) → max-prime < j → ¬ Prime j ) 
 prime-is-infinite zero pmax = pmax 1 {!!} record { isPrime = λ n lt → {!!} }
-prime-is-infinite (suc m) pmax = pmax (suc (factorial (suc m))) f>m record { isPrime = λ n lt → fact n lt } where
+prime-is-infinite (suc m) pmax = getPrime where -- pmax (suc (factorial (suc m))) f>m {!!} where
   factorial : (n : ℕ) → ℕ
   factorial zero = 1
   factorial (suc n) = (suc n) * (factorial n)
+  prime<max : (n : ℕ ) → Prime n → n < suc m
+  prime<max n p with <-cmp n m
+  ... | tri< a ¬b ¬c = <-trans a {!!} --  suc n ≤ suc m → suc n ≤ m
+  ... | tri≈ ¬a refl ¬c = ⊥-elim ( pmax n {!!} p )
+  ... | tri> ¬a ¬b c = ⊥-elim ( pmax n {!!} p )
   f>m :  suc m < suc (factorial (suc m))
   f>m = {!!}
-  factm : (n m : ℕ ) → n < (suc m) →  Dividable n (factorial m )
-  factm = {!!}
-  fact : (n : ℕ ) → n < (suc (factorial (suc m))) →   gcd (suc (factorial (suc m))) n ≡ 1
-  fact n lt = fact12  (nonPrime (factorial (suc m )) ( pmax (factorial (suc m )) {!!} )) where
-       fact12 : NonPrime (factorial (suc m)) → gcd (suc (factorial (suc m))) n ≡ 1
-       fact12 np = {!!}
+  fact< : (n : ℕ) → n < suc m → Dividable n ( factorial (suc m) )
+  fact< n n<m = record { factor = F.f1 (fact1 m init1) ; is-factor = last  } where
+     record F ( n m : ℕ) : Set where
+        field
+          f1 : ℕ
+          is-f1 : ( n < m ) → f1 * n ≡ factorial (suc m)
+     init : F n 0
+     init = record { f1 = 1 ; is-f1 = {!!} }
+     init1 : F n ( m - m )
+     init1 = subst (λ k → F n k ) (sym (minus<=0 {m} ≤-refl)) init
+     fact1 : (j : ℕ ) → F n ((suc m) - suc j) → F n j  
+     fact1 zero f = record { f1 = F.f1 f ;  is-f1 = {!!} }
+     fact1 (suc j) f with <-cmp n j
+     ... | tri< a ¬b ¬c = record { f1 = F.f1 f * (suc j) ;  is-f1 = {!!} }
+     ... | tri≈ ¬a b ¬c = record { f1 = F.f1 f ;  is-f1 = {!!} }
+     ... | tri> ¬a ¬b c = record { f1 = F.f1 f * (suc j) ;  is-f1 = {!!} }
+     last : F.f1 (fact1 m init1 ) * n + 0 ≡ factorial (suc m)
+     last = begin
+         F.f1 (fact1 m init1) * n + 0 ≡⟨ +-comm _ 0 ⟩
+         F.f1 (fact1 m init1) * n ≡⟨ F.is-f1 (fact1 m init1) {!!} ⟩
+         factorial (suc m) ∎  where open ≡-Reasoning
+  fact : (n : ℕ) → Prime n → Dividable n ( factorial (suc m) )
+  fact n p = fact< n ( prime<max n p )
+  -- div+1 : { i k : ℕ } → k > 1 →  Dividable k i →  ¬ Dividable k (suc i)
+  getPrime : ⊥
+  getPrime with PrimeP ( suc (factorial (suc m)) )
+  ... | yes p = pmax _ f>m p 
+  ... | no np = div+1 (NonPrime.p>0 p1) (fact (NonPrime.factor p1) (NonPrime.prime p1) ) (NonPrime.dividable p1) where
+      p1 : NonPrime  ( suc (factorial (suc m)) )
+      p1 = nonPrime  np
--- a/automaton-in-agda/src/root2.agda	Thu Jun 17 17:16:36 2021 +0900
+++ b/automaton-in-agda/src/root2.agda	Thu Jun 17 22:42:36 2021 +0900
@@ -53,12 +53,11 @@
 
 open Factor
 
--- gcd-div : ( i j k : ℕ ) → (if : Factor k i) (jf : Factor k j )
---    → remain if ≡ 0 → remain jf ≡  0
+-- gcd-div : ( i j k : ℕ ) → (if : Dividable k i) (jf : Dividable k j )
 --    → Dividable k ( gcd i  j )
 
 root2-irrational : ( n m : ℕ ) → n > 1 → m > 1  →  2 * n * n ≡ m * m  → ¬ (gcd n m ≡ 1)
-root2-irrational n m n>1 m>1 2nm = rot13 ( gcd-div n m 2 (s≤s (s≤s z≤n)) {!!} {!!} ) where 
+root2-irrational n m n>1 m>1 2nm = rot13 ( gcd-div n m 2 (s≤s (s≤s z≤n)) dn dm ) where 
     rot13 : {m : ℕ } → Dividable 2 m →  m ≡ 1 → ⊥
     rot13 d refl with Dividable.factor d | Dividable.is-factor d
     ... | zero | ()
@@ -112,5 +111,9 @@
          Even.j E * 2  ≡⟨  *-comm (Even.j E) 2  ⟩
          2 * Even.j E  ≡⟨  sym ( Even.is-twice E )  ⟩
          m ∎  where open ≡-Reasoning
+    dn : Dividable 2 n
+    dn = record { factor = factor f2 ; is-factor = subst (λ k → factor f2 * 2 + k ≡ n ) (f3 n rot7) (is-factor f2)  }
+    dm : Dividable 2 m
+    dm = record { factor = factor fm ; is-factor = is-factor fm }