Mercurial > hg > Members > kono > Proof > automaton

changeset 160:57f2c04eb14c

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 Mon, 04 Jan 2021 11:56:14 +0900
parents 5530b3789e0c
children e5dc512f5306
files agda/gcd.agda agda/index.ind agda/prime.agda
diffstat 3 files changed, 97 insertions(+), 41 deletions(-) [+]
line wrap: on
line diff
--- a/agda/gcd.agda	Mon Jan 04 09:24:11 2021 +0900
+++ b/agda/gcd.agda	Mon Jan 04 11:56:14 2021 +0900
@@ -149,28 +149,29 @@
 gcd4 : ( n k : ℕ ) → 1 < n  → gcd n k ≡ k → k ≤ n
 gcd4 n k 1<n eq = subst (λ m → m ≤ n ) eq (gcd5 n k 1<n)
 
-record Comp ( m n : ℕ ) : Set where
+record Comp ( m : ℕ ) : Set where
    field
-       comp : ℕ
-       is-comp : n * comp ≡ m
+       compa : ℕ
+       compb : ℕ
+       is-comp : compb * compa ≡ m
 
 open Comp
 
-comp-n : ( m n : ℕ ) → Comp m n → Comp (m + n) n
-comp-n m n c = record { comp = suc (comp c) ; is-comp = 
+comp-n : ( n : ℕ ) → (c : Comp n ) → Comp (compa c + n) 
+comp-n n c = record { compa = suc (compa c) ; compb = n ; is-comp = 
    begin
-      n * suc (comp c)  ≡⟨ *-comm n (suc (comp c)) ⟩
-      n + comp c * n ≡⟨ +-comm n (comp c * n) ⟩
-      comp c * n + n ≡⟨ cong (λ k → k + n) ( *-comm (comp c) n) ⟩
-      (n * comp c) + n ≡⟨ cong (λ k → k + n) (is-comp c) ⟩ 
-      m + n ∎ 
+      n * suc (compa c)  ≡⟨ *-comm n (suc (compa c)) ⟩
+      n + compa c * n ≡⟨ +-comm n (compa c * n) ⟩
+      compa c * n + n ≡⟨ cong (λ k → k + n) ( *-comm (compa c) n) ⟩
+      (n * compa c) + n ≡⟨ cong (λ k → k + n) {!!} ⟩ 
+      compa c + n ∎ 
     } where open ≡-Reasoning
 
 gcdcomp : ( m n o : ℕ ) → 0 < n → Set
-gcdcomp m n o 0<n = gcd n m ≡ o → Comp n o 
+gcdcomp m n o 0<n = gcd n m ≡ o → Comp n  
 
 gcdcomp-eq : ( m o : ℕ ) (0<m : 0 < m)  → gcdcomp m m o 0<m
-gcdcomp-eq m o 0<m g = record { comp = 1 ; is-comp = gcdc0 g } where
+gcdcomp-eq m o 0<m g = record { compa = 1 ; compb = o ; is-comp = gcdc0 g } where
    gcdc0 : (g : gcd m m ≡ o) → o * 1 ≡ m
    gcdc0 g = begin
       o * 1 ≡⟨ cong (λ k → k * 1) (sym g) ⟩
@@ -178,6 +179,21 @@
       gcd m m  ≡⟨ gcdmm m m ⟩
       m ∎ where open ≡-Reasoning
 
+gcdmul+1 : ( m n : ℕ ) → gcd (m * n + 1) n ≡ 1
+gcdmul+1 zero n = gcd204 n
+gcdmul+1 (suc m) n = begin
+      gcd (suc m * n + 1) n ≡⟨⟩
+      gcd (n + m * n + 1) n ≡⟨ cong (λ k → gcd k n ) (begin
+         n + m * n + 1 ≡⟨ {!!}  ⟩
+         m * n + n + 1 ≡⟨ {!!}  ⟩
+         m * n + (n + 1)  ≡⟨ {!!}  ⟩
+         m * n + (1 + n)  ≡⟨ {!!}  ⟩
+         m * n + 1 + n ∎ 
+       ) ⟩
+      gcd (m * n + 1 + n) n ≡⟨ gcd2 (m * n + 1) n ⟩
+      gcd (m * n + 1) n ≡⟨ gcdmul+1 m n ⟩
+      1 ∎ where open ≡-Reasoning
+
 gcd3 : Set
 gcd3 = ( n k : ℕ ) → 1 < n → n < k + k → gcd n k ≡ k → n ≡ k 
 
--- a/agda/index.ind	Mon Jan 04 09:24:11 2021 +0900
+++ b/agda/index.ind	Mon Jan 04 11:56:14 2021 +0900
@@ -1,29 +1,31 @@
-<a href="automaton-text.agda"> automaton-text.agda </a><br>
-<a href="automaton.agda"> automaton.agda </a><br>
-<a href="cfg.agda"> cfg.agda </a><br>
-<a href="cfg1.agda"> cfg1.agda </a><br>
-<a href="chap0.agda"> chap0.agda </a><br>
-<a href="derive.agda"> derive.agda </a><br>
-<a href="epautomaton.agda"> epautomaton.agda </a><br>
-<a href="finiteSet.agda"> finiteSet.agda </a><br>
-<a href="flcagl.agda"> flcagl.agda </a><br>
-<a href="induction-ex.agda"> induction-ex.agda </a><br>
-<a href="lang-text.agda"> lang-text.agda </a><br>
-<a href="logic.agda"> logic.agda </a><br>
-<a href="nat.agda"> nat.agda </a><br>
-<a href="nfa-list.agda"> nfa-list.agda </a><br>
-<a href="nfa.agda"> nfa.agda </a><br>
-<a href="nfa136.agda"> nfa136.agda </a><br>
-<a href="omega-automaton.agda"> omega-automaton.agda </a><br>
-<a href="pushdown.agda"> pushdown.agda </a><br>
-<a href="puzzle.agda"> puzzle.agda </a><br>
-<a href="regex.agda"> regex.agda </a><br>
-<a href="regex1.agda"> regex1.agda </a><br>
-<a href="regop.agda"> regop.agda </a><br>
-<a href="regular-language.agda"> regular-language.agda </a><br>
-<a href="root2.agda"> root2.agda </a><br>
-<a href="sbconst.agda"> sbconst.agda </a><br>
-<a href="sbconst1.agda"> sbconst1.agda </a><br>
-<a href="sbconst2.agda"> sbconst2.agda </a><br>
-<a href="turing.agda"> turing.agda </a><br>
-<a href="utm.agda"> utm.agda </a><br>
+--title: list
+<a href=FSetUtil.agda> FSetUtil.agda </a><br>
+<a href=automaton-ex.agda> automaton-ex.agda </a><br>
+<a href=automaton.agda> automaton.agda </a><br>
+<a href=cfg.agda> cfg.agda </a><br>
+<a href=cfg1.agda> cfg1.agda </a><br>
+<a href=chap0.agda> chap0.agda </a><br>
+<a href=derive.agda> derive.agda </a><br>
+<a href=even.agda> even.agda </a><br>
+<a href=finiteSet.agda> finiteSet.agda </a><br>
+<a href=flcagl.agda> flcagl.agda </a><br>
+<a href=gcd.agda> gcd.agda </a><br>
+<a href=halt.agda> halt.agda </a><br>
+<a href=induction-ex.agda> induction-ex.agda </a><br>
+<a href=lang-text.agda> lang-text.agda </a><br>
+<a href=logic.agda> logic.agda </a><br>
+<a href=nat.agda> nat.agda </a><br>
+<a href=nfa.agda> nfa.agda </a><br>
+<a href=nfa136.agda> nfa136.agda </a><br>
+<a href=non-regular.agda> non-regular.agda </a><br>
+<a href=omega-automaton.agda> omega-automaton.agda </a><br>
+<a href=pushdown.agda> pushdown.agda </a><br>
+<a href=puzzle.agda> puzzle.agda </a><br>
+<a href=regex.agda> regex.agda </a><br>
+<a href=regex1.agda> regex1.agda </a><br>
+<a href=regular-concat.agda> regular-concat.agda </a><br>
+<a href=regular-language.agda> regular-language.agda </a><br>
+<a href=root2.agda> root2.agda </a><br>
+<a href=sbconst2.agda> sbconst2.agda </a><br>
+<a href=turing.agda> turing.agda </a><br>
+<a href=utm.agda> utm.agda </a><br>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/prime.agda	Mon Jan 04 11:56:14 2021 +0900
@@ -0,0 +1,38 @@
+module prime where
+
+open import Data.Nat 
+open import Data.Nat.Properties
+open import Data.Empty
+open import Data.Unit using (⊤ ; tt)
+open import Relation.Nullary
+open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Definitions
+
+open import gcd
+open import nat
+
+record Prime (i : ℕ ) : Set where
+   field
+      isPrime : ( j : ℕ ) → j < i → gcd i j ≡ 1
+
+prime? : ( i : ℕ) → Dec ( Prime i )
+prime? i = {!!}
+
+not-p : (i : ℕ) → ¬ Prime i → Comp i 
+not-p = {!!}
+
+prime-is-infinite : (max-prime : ℕ ) → ¬ ( (j : ℕ) → max-prime < j → ¬ Prime j ) 
+prime-is-infinite zero pmax = {!!}
+prime-is-infinite (suc m) pmax = {!!} where
+  factorial : (n : ℕ) → ℕ
+  factorial zero = 1
+  factorial (suc n) = (suc n) * (factorial n)
+  -- gcdmul+1 : gcd (m * n + 1) n ≡ 1
+  np : (i n j : ℕ) → ((i : ℕ) → Prime i → gcd i n ≡ 1) → Prime j → gcd (i * j ) n ≡ 1
+  np = {!!}
+  pf : (j : ℕ) → j < suc (factorial (suc m)) → gcd (suc (factorial (suc m))) j ≡ 1
+  pf j j<f with prime? j
+  ... | yes y = {!!}
+  ... | no non with not-p j non 
+  ... | t = {!!}
+