Mercurial > hg > Members > kono > Proof > automaton

changeset 165:6cb442050825

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 Sat, 13 Mar 2021 00:03:36 +0900
parents bee86ee07fff
children 159ad8b0104e
files agda/gcd.agda agda/root2.agda
diffstat 2 files changed, 55 insertions(+), 108 deletions(-) [+]
line wrap: on
line diff
--- a/agda/gcd.agda	Fri Mar 12 21:45:53 2021 +0900
+++ b/agda/gcd.agda	Sat Mar 13 00:03:36 2021 +0900
@@ -11,29 +11,17 @@
 open import nat
 open import logic
 
-gcd1 : ( i i0 j j0 : ℕ ) → ℕ
-gcd1 zero i0 zero j0 with <-cmp i0 j0
-... | tri< a ¬b ¬c = i0
-... | tri≈ ¬a refl ¬c = i0
-... | tri> ¬a ¬b c = j0
-gcd1 zero i0 (suc zero) j0 = 1
-gcd1 zero zero (suc (suc j)) j0 = j0
-gcd1 zero (suc i0) (suc (suc j)) j0 = gcd1 i0 (suc i0) (suc j) (suc (suc j))
-gcd1 (suc zero) i0 zero j0 = 1
-gcd1 (suc (suc i)) i0 zero zero = i0
-gcd1 (suc (suc i)) i0 zero (suc j0) = gcd1 (suc i) (suc (suc i))  j0 (suc j0)
-gcd1 (suc i) i0 (suc j) j0 = gcd1 i i0 j j0  
-
-gcd : ( i j : ℕ ) → ℕ
-gcd i j = gcd1 i i j j 
-
 record Factor (n m : ℕ ) : Set where
    field 
-      -- n<m : n ≤ m
       factor : ℕ
       remain : ℕ
       is-factor : factor * n + remain ≡ m
 
+record Dividable (n m : ℕ ) : Set where
+   field 
+      factor : ℕ
+      is-factor : factor * n + 0 ≡ m 
+
 open Factor
 
 open ≡-Reasoning
@@ -52,23 +40,43 @@
 ifzero : {k : ℕ } → (jf :  Factor k zero ) →  remain jf ≡ 0
 ifzero = {!!}
 
+gcd1 : ( i i0 j j0 : ℕ ) → ℕ
+gcd1 zero i0 zero j0 with <-cmp i0 j0
+... | tri< a ¬b ¬c = i0
+... | tri≈ ¬a refl ¬c = i0
+... | tri> ¬a ¬b c = j0
+gcd1 zero i0 (suc zero) j0 = 1
+gcd1 zero zero (suc (suc j)) j0 = j0
+gcd1 zero (suc i0) (suc (suc j)) j0 = gcd1 i0 (suc i0) (suc j) (suc (suc j))
+gcd1 (suc zero) i0 zero j0 = 1
+gcd1 (suc (suc i)) i0 zero zero = i0
+gcd1 (suc (suc i)) i0 zero (suc j0) = gcd1 (suc i) (suc (suc i))  j0 (suc j0)
+gcd1 (suc i) i0 (suc j) j0 = gcd1 i i0 j j0  
+
+gcd : ( i j : ℕ ) → ℕ
+gcd i j = gcd1 i i j j 
+
 gcd-gt : ( i i0 j j0 k : ℕ ) → (if : Factor k i) (i0f : Factor k i0 ) (jf : Factor k i ) (j0f : Factor k j0)
    → remain i0f ≡ 0 → remain j0f ≡  0
    → (remain if + i ) ≡ i0  → (remain jf + j ) ≡ j0
-   → Factor k ( gcd1 i i0 j j0 ) 
+   → Dividable k ( gcd1 i i0 j j0 ) 
 gcd-gt zero i0 zero j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 with <-cmp i0 j0
-... | tri< a ¬b ¬c = record { factor = factor i0f ; remain = 0 ; is-factor = ifk0 i0 k i0f i0=0 } 
-... | tri≈ ¬a refl ¬c = record { factor = factor i0f ; remain = 0 ; is-factor = ifk0 i0 k i0f i0=0 } 
-... | tri> ¬a ¬b c = record { factor = factor j0f ; remain = 0 ; is-factor = ifk0 j0 k j0f j0=0 } 
+... | tri< a ¬b ¬c = record { factor = factor i0f ; is-factor = ifk0 i0 k i0f i0=0 } 
+... | tri≈ ¬a refl ¬c = record { factor = factor i0f ;  is-factor = ifk0 i0 k i0f i0=0 } 
+... | tri> ¬a ¬b c = record { factor = factor j0f ;  is-factor = ifk0 j0 k j0f j0=0 } 
 gcd-gt zero i0 (suc zero) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!} -- can't happen
-gcd-gt zero zero (suc (suc j)) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = record { factor = factor j0f ; remain = 0 ; is-factor = ifk0 j0 k j0f j0=0 } 
+gcd-gt zero zero (suc (suc j)) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = record { factor = factor j0f ; is-factor = ifk0 j0 k j0f j0=0 } 
 gcd-gt zero (suc i0) (suc (suc j)) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 =  
     gcd-gt i0 (suc i0) (suc j) (suc (suc j))  k (decf i0f)  i0f (decf i0f)
        record { factor = factor jf ; remain = remain jf ; is-factor = {!!} } i0=0 {!!} {!!} {!!}  
 gcd-gt (suc zero) i0 zero j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!} -- can't happen
 gcd-gt (suc (suc i)) i0 zero zero k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!}
-gcd-gt (suc (suc i)) i0 zero (suc j0) k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!}
-gcd-gt (suc i) i0 (suc j) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!} -- gcd-gt i i0 j j0 k (decf if) i0f (decf jf) j0f ? ? ? ?
+gcd-gt (suc (suc i)) i0 zero (suc j0) k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 =
+     gcd-gt (suc i) (suc (suc i)) j0 (suc j0) k {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} 
+gcd-gt (suc zero) i0 (suc j) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = 
+     gcd-gt zero i0 j j0 k {!!} i0f {!!} j0f i0=0 j0=0 {!!} {!!}
+gcd-gt (suc (suc i)) i0 (suc j) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = 
+     gcd-gt (suc i) i0 j j0 k {!!} i0f {!!} j0f i0=0 j0=0 {!!} {!!}
 
 -- gcd26 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd (n - m) m
 -- gcd27 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n k ≡ k → k ≤ n
@@ -192,80 +200,3 @@
 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 : ℕ ) : Set where
-   field
-       compa : ℕ
-       compb : ℕ
-       is-comp : compb * compa ≡ m
-
-open Comp
-
-comp-n : ( n : ℕ ) → (c : Comp n ) → Comp (compa c + n) 
-comp-n n c = record { compa = compa c ; compb = suc (compb c) ; is-comp = 
-   begin
-      compa c + compb c * compa c ≡⟨ cong (λ k → compa c + k) (is-comp c) ⟩ 
-      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  
-
-gcdcomp-eq : ( m o : ℕ ) (0<m : 0 < m)  → gcdcomp m m o 0<m
-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) ⟩
-      gcd m m  * 1 ≡⟨ *-identityʳ _ ⟩
-      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 
-
-0<gcd : {i j : ℕ} → 0 < j → 0 < gcd j i
-0<gcd {zero} {zero} ()
-0<gcd {zero} {suc j} 0<j = subst (λ k → 0 < k ) (sym (gcd20 (suc j))) 0<j
-0<gcd {suc i} {suc j} (s≤s 0<j) = {!!}
-
-gcd23 : ( n m k : ℕ) → 1 < n → 1 < m  → gcd n k ≡ k → gcd m k ≡ k → k ≤ gcd n m 
-gcd23 n m k 1<n 1<m gn gm = gcd230 n n m m k k 1<n 1<m ≤-refl ≤-refl ≤-refl gn gm where
-     gcd232 : (i0 j0 k0 : ℕ) → (1 < i0) → k ≤ k0 → gcd1 0 i0 0 k0 ≡ suc k → gcd1 0 j0 0 k0 ≡ suc zero
-         → suc zero ≤ gcd1 0 i0 0 j0
-     gcd232 i0 j0 k0 1<i0 k<k0 gi gj = {!!}
-     gcd231 : (i0 k k0 : ℕ) → (1 < i0) → (suc k ≤ k0) → gcd1 0 i0 (suc k) k0 ≡ suc k → suc k ≤ i0
-     gcd231 i0 k k0 1<i0 sk<k0 gi = subst (λ m → m ≤ i0 ) gi ( gcd50 0 i0 (suc k) k0 1<i0 z≤n sk<k0 )
-     gcd230 : (i i0 j j0 k k0 : ℕ) → 1 < i0 → 1 < j0 → i ≤ i0 → j ≤ j0 → k ≤ k0  → gcd1 i i0 k k0 ≡ k → gcd1 j j0 k k0 ≡ k → k ≤ gcd1 i i0 j j0
-     gcd230 j i0 i j0 zero k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj = {!!}
-     gcd230 zero i0 zero j0 (suc k) k0 1<i 1<j i<i0 j<j0 k<k0 gi gj with <-cmp i0 j0
-     ... | tri< a ¬b ¬c = gcd231 i0 k k0 1<i k<k0 gi   -- k ≤ gcd1 zero i0 (suc j) j0
-     ... | tri≈ ¬a refl ¬c = gcd231 j0 k k0 1<i k<k0 gj 
-     ... | tri> ¬a ¬b c = gcd231 j0 k k0 1<j k<k0 gj 
-     gcd230 zero i0 (suc j) j0 (suc k) k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj = {!!}
-     gcd230 (suc i) i0 zero j0 (suc k) k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj = {!!}
-     gcd230 (suc zero) i0 (suc zero) j0 (suc zero) k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj =
-         gcd232 i0 j0 k0 1<i {!!} {!!} {!!}
-     gcd230 (suc zero) i0 (suc zero) j0 (suc (suc k)) k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj = {!!}
-     gcd230 (suc zero) i0 (suc (suc j)) j0 (suc k) k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj = {!!}
-     gcd230 (suc (suc i)) i0 (suc zero) j0 (suc k) k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj = {!!}
-     gcd230 (suc (suc i)) i0 (suc (suc j)) j0 (suc zero) k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj = {!!}
-     gcd230 (suc (suc i)) i0 (suc (suc j)) j0 (suc (suc k)) k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj = 
-          {!!} -- gcd230 (suc i) i0 (suc j) j0 (suc k) k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj 
-
-gcd24 : { n m k : ℕ} → n > 1 → m > 1 → k > 1 → gcd n k ≡ k → gcd m k ≡ k → ¬ ( gcd n m ≡ 1 )
-gcd24 {n} {m} {k} 1<n 1<m 1<k gn gm gnm = ⊥-elim ( nat-≡< (sym gnm) (≤-trans 1<k (gcd23 n m k 1<n 1<m gn gm  )))
-
--- a/agda/root2.agda	Fri Mar 12 21:45:53 2021 +0900
+++ b/agda/root2.agda	Sat Mar 13 00:03:36 2021 +0900
@@ -50,15 +50,27 @@
 ... | tri≈ ¬a b ¬c = cong suc b
 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym eq) (s≤s (<-trans (<-plus c) (<-plus-0 (s≤s (<-plus c ))))))
 
--- gcd24 : { n m k : ℕ} → n > 1 → m > 1 → k > 1 → gcd n k ≡ k → gcd m k ≡ k → ¬ ( gcd n m ≡ 1 )
-
-gcd-even : { n m : ℕ} → Even n → Even m → Even ( gcd n m )
-gcd-even {n} {m} en em = record { j = {!!} ; is-twice = {!!} } where
-   gcd-even1 : ( n m : ℕ) → Even n → Even m → Even ( gcd n m )
-   gcd-even1 n m gn gm = {!!}
+open Factor
 
 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 = gcd24 {n} {m} n>1 m>1 (s≤s (s≤s z≤n)) (even→gcd=2 rot7 (rot5 n>1)) (even→gcd=2 ( even^2 {m} ( rot1)) (rot5 m>1))where
+root2-irrational n m n>1 m>1 2nm = rot13 ( gcd-gt n n m m 2 f2 f2 f2 fm {!!} {!!} {!!} {!!}) where 
+    rot13 : {m : ℕ } → Dividable 2 m →  m ≡ 1 → ⊥
+    rot13 d refl with Dividable.is-factor d
+    ... | t = {!!}
+    rot11 : {m : ℕ } → even m → Factor 2 m 
+    rot11 {zero} em = record { factor = 0 ; remain = 0 ; is-factor = refl }
+    rot11 {suc zero} ()
+    rot11 {suc (suc m) } em = record { factor = suc (factor fc ) ; remain = remain fc ; is-factor = isfc } where
+       fc : Factor 2 m
+       fc = rot11 {m} em
+       isfc : suc (factor fc) * 2 + remain fc ≡ suc (suc m)
+       isfc = begin
+          suc (factor fc) * 2 + remain fc ≡⟨ cong (λ k →  k + remain fc) (*-distribʳ-+ 2 1 (factor fc)) ⟩
+          ((1 * 2) +  (factor fc)* 2 ) + remain fc ≡⟨⟩
+          ((1 + 1) +  (factor fc)* 2 ) + remain fc ≡⟨ cong (λ k → k + remain fc) (+-assoc 1  1 _ ) ⟩
+          (1 + (1 +  (factor fc)* 2 )) + remain fc ≡⟨⟩
+          suc (suc ((factor fc * 2) + remain fc )) ≡⟨ cong (λ x → suc (suc x)) (is-factor fc) ⟩
+          suc (suc m) ∎ where open ≡-Reasoning
     rot5 : {n : ℕ} → n > 1 → n > 0
     rot5 {n} lt = <-trans a<sa lt 
     rot1 : even ( m * m )
@@ -81,4 +93,8 @@
           2 * (Even.j E * m)  ∎ ) where open ≡-Reasoning
     rot7 : even n  
     rot7 =  even^2 {n} (subst (λ k → even k) (sym rot3) ((n*even {Even.j E} {m} ( even^2 {m} ( rot1 )))))
+    f2 : Factor 2 n
+    f2 = rot11 rot7
+    fm : Factor 2 m
+    fm = record { factor = Even.j E ; remain = 0 ; is-factor = {!!} }