Mercurial > hg > Members > kono > Proof > automaton

changeset 200:a5c8a90615be

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 Fri, 18 Jun 2021 07:54:25 +0900
parents 4a83abf7b822
children db05b4df5b67
files automaton-in-agda/src/prime.agda
diffstat 1 files changed, 67 insertions(+), 33 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/prime.agda	Thu Jun 17 22:42:36 2021 +0900
+++ b/automaton-in-agda/src/prime.agda	Fri Jun 18 07:54:25 2021 +0900
@@ -13,22 +13,22 @@
 
 record Prime (i : ℕ ) : Set where
    field
+      p>0 : i > 1
       isPrime : ( j : ℕ ) → j < i → gcd i j ≡ 1
 
-open ≡-Reasoning
 
 record NonPrime ( n : ℕ ) : Set where
    field
       factor : ℕ
       prime : Prime factor
-      p>0 : factor > 1
       dividable : Dividable factor n
 
 PrimeP : ( n : ℕ ) → Dec ( Prime n )
-PrimeP 0 = yes record { isPrime = λ j () }
+PrimeP 0 = no (λ p → ⊥-elim ( nat-<> (Prime.p>0 p) (s≤s z≤n))) 
+PrimeP 1 = no (λ p → ⊥-elim ( nat-≤> (Prime.p>0 p) (s≤s (≤-refl))))
 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 zero m<n lt = yes record { isPrime = λ j j<i → lt j z≤n {!!} ; p>0 = {!!} }
    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 {!!} {!!}
@@ -37,53 +37,87 @@
 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 zero mg = ⊥-elim ( np record { isPrime = λ j lt → mg j z≤n lt ; p>0 = {!!} } ) -- 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 = {!!} ; p>0 = c ; dividable = record { factor = {!!} ; is-factor = {!!} } }
+    ... | tri> ¬a ¬b c = record { factor = gcd n (suc m) ; prime = {!!} ;  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 = getPrime where -- pmax (suc (factorial (suc m))) f>m {!!} where
+prime-is-infinite zero pmax = pmax 3 (s≤s z≤n) record { isPrime = λ n lt → {!!} ; p>0 = {!!} }
+prime-is-infinite (suc m) pmax = getPrime 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 )
+  prime<max : (n : ℕ ) → Prime n → n < suc (suc m)
+  prime<max n p with <-cmp n (suc m) 
+  ... | tri< a ¬b ¬c = ≤-trans a refl-≤s 
+  ... | tri≈ ¬a refl ¬c = ≤-refl 
+  ... | tri> ¬a ¬b c = ⊥-elim ( pmax n c p ) 
+  factorial-mono : (n : ℕ) → factorial n ≤ factorial (suc n)
+  factorial-mono n = begin
+     factorial n  ≤⟨ x≤x+y ⟩
+     factorial n + n * factorial n ≡⟨ refl ⟩
+     (suc n) * factorial n  ≡⟨ refl ⟩
+     factorial (suc n)  ∎  where open ≤-Reasoning
+  factorial≥1 : {m : ℕ} → 1 ≤ factorial m
+  factorial≥1 {zero} = ≤-refl
+  factorial≥1 {suc m} = begin
+     1 ≤⟨ s≤s z≤n ⟩
+     (suc m) * 1 ≤⟨  *-monoʳ-≤ (suc m) (factorial≥1 {m}) ⟩
+     (suc m) * factorial m ≡⟨ refl ⟩
+     factorial (suc m)  ∎  where open ≤-Reasoning
+  factorial⟩m : (m : ℕ) → m ≤ factorial m
+  factorial⟩m zero = z≤n
+  factorial⟩m (suc m) = begin
+     suc m ≡⟨ cong suc (+-comm 0 _) ⟩
+     1 * suc m ≡⟨ *-comm 1 _ ⟩
+     (suc m) * 1 ≤⟨  *-monoʳ-≤ (suc m) (factorial≥1 {m}) ⟩
+     (suc m) * factorial m  ≡⟨ refl ⟩
+     factorial (suc m)  ∎  where open ≤-Reasoning
+  -- *-monoˡ-≤ (suc m) {!!}
   f>m :  suc m < suc (factorial (suc m))
-  f>m = {!!}
-  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
+  f>m = begin
+     suc (suc m)  ≡⟨ cong (λ k → 1 + suc k ) (+-comm _ m) ⟩
+     suc (1 + 1 * m)  ≡⟨ cong (λ k → suc (1 + k )) (*-comm 1 m)  ⟩
+     suc (1 + m * 1)  ≤⟨ s≤s (s≤s (*-monoʳ-≤ m  (factorial≥1 {m}) )) ⟩
+     suc (1 + m * factorial m) ≤⟨ s≤s  (+-monoˡ-≤ _ (factorial≥1 {m})) ⟩
+     suc (factorial m + m * factorial m)  ≡⟨ refl ⟩
+     suc (factorial (suc m)) ∎  where open ≤-Reasoning
+  fact< : (n : ℕ) → 0 < n → n < suc (suc m) → Dividable n ( factorial (suc m) )
+  fact< n 0<n n<m = record { factor = F.f1 (fact1 m init1) ? ? ? ; is-factor = last  } where
+     record F (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 = {!!} }
+          f1 : (n : ℕ ) → 0 < n →  n < suc (suc m ) → ℕ
+          is-f1 : (0<n : 0 < n ) →  (n<m : n < suc (suc m )) → f1 n 0<n n<m * n ≡ factorial (suc m)
+     init0 : (n : ℕ) → 0 < n → n < 2 → 1 * n ≡ factorial 1
+     init0 (suc zero) (s≤s lt) (s≤s (s≤s z≤n)) = refl
+     init : F 0
+     init = record { f1 = ? ; is-f1 = λ 0<n lt → init0 n 0<n lt } where
+     init1 : F ( m - m )
+     init1 = subst (λ k → F k ) (sym (minus<=0 {m} ≤-refl)) init
+     fact1 : (j : ℕ ) → F ((suc m) - suc j) → F j  
+     fact1 zero f = record { f1 = ? ;  is-f1 = fact2 } where
+        fact3 : 0 < n → n < suc (suc m) →  F.f1 f n ? ? * n ≡ factorial (suc m)
+        fact3 = ? -- F.is-f1 f ? ? 
+        fact2 : 0 < n → n < 2 → F.f1 f n ? ? * n ≡ factorial 1
+        fact2 = {!!}
      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)
+     ... | tri< a ¬b ¬c = record { f1 = ? ;  is-f1 = {!!} }
+     ... | tri≈ ¬a refl ¬c = record { f1 = ? ;  is-f1 = λ lt → {!!} }
+     ... | tri> ¬a ¬b c = record { f1 = ? ;  is-f1 = λ lt → {!!} }
+     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) {!!} ⟩
+         F.f1 (fact1 m init1) ? ? ? * n + 0 ≡⟨ +-comm _ 0 ⟩
+         F.f1 (fact1 m init1) ? ? ? * n ≡⟨ F.is-f1 (fact1 m init1) 0<n n<m ⟩
          factorial (suc m) ∎  where open ≡-Reasoning
   fact : (n : ℕ) → Prime n → Dividable n ( factorial (suc m) )
-  fact n p = fact< n ( prime<max n p )
+  fact n p = fact< n (<-trans (s≤s z≤n) (Prime.p>0 p)) ( 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
+  ... | no np = div+1 (Prime.p>0 (NonPrime.prime p1)) (fact (NonPrime.factor p1) (NonPrime.prime p1) ) (NonPrime.dividable p1) where
       p1 : NonPrime  ( suc (factorial (suc m)) )
       p1 = nonPrime  np