Mercurial > hg > Members > kono > Proof > automaton

changeset 213:9aec75fa796c

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, 21 Jun 2021 08:08:08 +0900
parents cb36711e8b06
children 906b43b94228
files automaton-in-agda/src/gcd.agda
diffstat 1 files changed, 46 insertions(+), 64 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda	Mon Jun 21 00:43:09 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Mon Jun 21 08:08:08 2021 +0900
@@ -188,59 +188,31 @@
     suc f * k ≡⟨ +-comm 0 _ ⟩
     suc f * k + 0 ∎  )) where open ≤-Reasoning  
 
+div+div : { i j k : ℕ } →  Dividable k i →  Dividable k j → Dividable k (i + j) ∧ Dividable k (j + i)
+div+div {i} {j} {k} di dj = ⟪ div+div1 , subst (λ g → Dividable k g) (+-comm i j) div+div1 ⟫ where
+      fki = Dividable.factor di
+      fkj = Dividable.factor dj
+      div+div1 : Dividable k (i + j)
+      div+div1 = record { factor = fki + fkj  ; is-factor = ( begin 
+          (fki + fkj) * k + 0 ≡⟨ +-comm _ 0 ⟩
+          (fki + fkj) * k  ≡⟨ *-distribʳ-+ k fki _ ⟩
+          fki * k + fkj * k  ≡⟨ cong₂ ( λ i j → i + j ) (+-comm 0 (fki * k)) (+-comm 0 (fkj * k)) ⟩
+          (fki * k + 0) + (fkj * k + 0) ≡⟨ cong₂ ( λ i j → i + j ) (Dividable.is-factor di) (Dividable.is-factor dj) ⟩
+          i + j  ∎ ) } where
+             open ≡-Reasoning  
+
 div-div : { i j k : ℕ } → k > 1 →  Dividable k i →  Dividable k j → Dividable k (i - j) ∧ Dividable k (j - i)
-div-div {i} {j} {suc k} k>1 di dj = div-div0 di dj where
-   div-div1 : {i j : ℕ}   →  Dividable (suc k) i →  Dividable (suc k) j → i < j  → Dividable (suc k) (j - i)
-   div-div1 {i} {j} record { factor = fi ; is-factor = fai } record { factor = fj ; is-factor = faj } i<j =
-            subst (λ g →  Dividable (suc k) g ) div-div3 ( div-div2 fj fi fi<fj ) where
-      fi<fj : fi < fj
-      fi<fj with <-cmp fi fj
-      ... | tri< a ¬b ¬c = a
-      ... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< (cong (λ g → g * suc k + 0) b) (begin
-             suc (fi * suc k + 0)  ≡⟨ cong suc fai ⟩
-             suc i  ≤⟨ i<j ⟩
-             j  ≡⟨ sym faj ⟩
-             fj * suc k + 0 ∎  )) where open ≤-Reasoning  
-      ... | tri> ¬a ¬b c = ⊥-elim ( nat-<> (*-monoˡ-< k c ) (begin
-             suc (fi * suc k) ≡⟨ +-comm 0 _ ⟩
-             suc (fi * suc k + 0) ≡⟨ cong suc fai ⟩
-             suc i ≤⟨ i<j ⟩
-             j ≡⟨ sym faj ⟩
-             fj * suc k + 0 ≡⟨ +-comm _ 0 ⟩
-             fj * suc k ∎  )) where open ≤-Reasoning  
-      div-div3 : (fj * suc k) - (fi * suc k) ≡ j - i
-      div-div3 = begin (fj * suc k) - (fi * suc k) ≡⟨  cong₂ (λ g h → g - h) (+-comm 0 (fj * suc k)) (+-comm 0 (fi * suc k)) ⟩
-          (fj * suc k + 0) - (fi * suc k + 0) ≡⟨  cong₂ (λ g h → g - h) faj  fai ⟩
-          j - i ∎  where open ≡-Reasoning  
-      div-div2 : (fj fi : ℕ) → fi < fj → Dividable (suc k) ((fj * suc k) - (fi * suc k))
-      div-div2 zero fi i<j = subst (λ g → Dividable (suc k) g) (begin
-          0 ≡⟨ sym (minus<=0 {0} {fi * suc k} z≤n ) ⟩
-          0 -  (fi * suc k) ≡⟨ refl ⟩
-          (zero * suc k) - (fi * suc k) ∎ ) div0
-          where open ≡-Reasoning  
-      div-div2 (suc fj) fi i<j with <-cmp fi fj
-      ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c i<j  )
-      ... | tri≈ ¬a refl ¬c = record { factor = 1 ; is-factor = (begin
-             1 * suc k + 0 ≡⟨ +-comm _ 0 ⟩
-               1 * suc k ≡⟨ cong suc (+-comm _ 0) ⟩
-             suc k ≡⟨ sym (minus+y-y {suc k} {fj * suc k}) ⟩
-             (suc k + fj * suc k) - (fj * suc k) ≡⟨ refl ⟩
-             (suc (k + fj * suc k)) - (fj * suc k) ∎  )} where open ≡-Reasoning  
-      ... | tri< fi<fj ¬b ¬c = record { factor = suc (Dividable.factor (div-div2 fj fi fi<fj )) ; is-factor = ( begin 
-          suc (Dividable.factor (div-div2 fj fi fi<fj )) * suc k + 0 ≡⟨ +-comm _ 0 ⟩
-          suc (Dividable.factor (div-div2 fj fi fi<fj )) * suc k  ≡⟨ refl ⟩
-          suc k + ((Dividable.factor (div-div2 fj fi fi<fj )) * suc k )  ≡⟨ cong (λ g → suc k + g ) (+-comm 0 _) ⟩
-          suc k + ((Dividable.factor (div-div2 fj fi fi<fj )) * suc k + 0)  ≡⟨ cong (λ g → suc k + g) (Dividable.is-factor (div-div2 fj fi fi<fj) ) ⟩
-          suc k + ((fj * suc k) - (fi * suc k)) ≡⟨ minus+yz {suc k} {fj * suc k} {fi * suc k} (<to≤ (*-monoˡ-< k fi<fj )) ⟩
-           ( (suc k + (fj * suc k)) - (fi * suc k)) ≡⟨ refl ⟩
-          ((suc fj * suc k) - (fi * suc k)) ∎ ) } where
+div-div {i} {j} {k} k>1 di dj = ⟪ div-div1 di dj , div-div1 dj di ⟫ where
+      div-div1 : {i j : ℕ } → Dividable k i →  Dividable k j → Dividable k (i - j)
+      div-div1 {i} {j} di dj = record { factor = fki - fkj  ; is-factor = ( begin 
+          (fki - fkj) * k + 0 ≡⟨ +-comm _ 0 ⟩
+          (fki - fkj) * k  ≡⟨ distr-minus-* {fki} {fkj}  ⟩
+          (fki * k) - (fkj * k)  ≡⟨ cong₂ ( λ i j → i - j ) (+-comm 0 (fki * k)) (+-comm 0 (fkj * k)) ⟩
+          (fki * k + 0) - (fkj * k + 0) ≡⟨ cong₂ ( λ i j → i - j ) (Dividable.is-factor di) (Dividable.is-factor dj) ⟩
+          i - j  ∎ ) } where
              open ≡-Reasoning  
-   div-div0 : { i j : ℕ } →  Dividable (suc k) i →  Dividable (suc k) j → Dividable (suc k) (i - j) ∧ Dividable (suc k) (j - i)
-   div-div0 {i} {j} di dj with <-cmp i j
-   ... | tri< a ¬b ¬c    = ⟪ subst (λ g → Dividable (suc k) g) (sym (minus<=0 {i} {j} (<to≤ a))) div0 , div-div1 di dj a ⟫ 
-   ... | tri≈ ¬a refl ¬c = ⟪ subst (λ g → Dividable (suc k) g) (sym (minus<=0 {i} {i} refl-≤)) div0 ,
-                             subst (λ g → Dividable (suc k) g) (sym (minus<=0 {i} {i} refl-≤)) div0 ⟫
-   ... | tri> ¬a ¬b c    = ⟪ div-div1 dj di c , subst (λ g → Dividable (suc k) g) (sym (minus<=0 {j} {i} (<to≤ c))) div0  ⟫ 
+             fki = Dividable.factor di
+             fkj = Dividable.factor dj
 
 open _∧_
 
@@ -347,9 +319,9 @@
         ... | tri> ¬a ¬b c = record { ni =  i - j ; nj = suc j ; fdec = λ lt →
             subst₂ (λ s t → s < t) (Fsym {suc j} {i - j}) (Fsym {suc j} {suc i}) (fd1 j i (i - j) c refl ) } 
         ind :   ( i j : ℕ ) →
-            Dividable (gcd (Fdec.ni (fedc0 i j)) (Fdec.nj (fedc0 i j))) (Fdec.ni (fedc0 i j))
+              Dividable (gcd (Fdec.ni (fedc0 i j)) (Fdec.nj (fedc0 i j))) (Fdec.ni (fedc0 i j))
             ∧ Dividable (gcd (Fdec.ni (fedc0 i j)) (Fdec.nj (fedc0 i j))) (Fdec.nj (fedc0 i j))
-             → Dividable (gcd i j) i ∧ Dividable (gcd i j) j
+            → Dividable (gcd i j) i ∧ Dividable (gcd i j) j
         ind zero zero prev = ind0 where
            ind0 : Dividable (gcd zero zero) zero ∧ Dividable (gcd zero zero) zero
            ind0 = ⟪ div0 , div0 ⟫
@@ -360,11 +332,11 @@
            ind2 : Dividable (gcd (suc i) zero) (suc i) ∧ Dividable (gcd (suc i) zero) zero
            ind2 = ⟪  subst (λ k → Dividable k (suc i)) (sym (trans refl (gcd20 (suc i)))) div= , div0 ⟫
         ind (suc i) (suc j) prev with <-cmp i j
-        ... | tri< a ¬b ¬c = ⟪ ind3 (suc i) (proj1 prev)   , ind4 (proj2 prev) ⟫ where
-            ind3 : (s : ℕ ) → Dividable (gcd1 (suc i) (suc i) (j - i) (j - i)) s
-                 → Dividable (gcd1 (suc i) (suc i) (suc j) (suc j)) s 
-            ind3 s prev = 
-               subst (λ k → Dividable k s) ( begin
+        ... | tri< a ¬b ¬c = ⟪ ind3 (proj1 prev)   , ind6 (ind4 (proj2 prev)) (ind3 (proj1 prev)) ⟫ where
+            ind3 :  Dividable (gcd (suc i) (j - i)) (suc i)
+                  → Dividable (gcd (suc i) (suc j)) (suc i) 
+            ind3 prev = 
+               subst (λ k → Dividable k (suc i)) ( begin
                  gcd (suc i) (j - i)  ≡⟨ gcdsym {suc i} {j - i} ⟩
                  gcd (j - i ) (suc i)   ≡⟨ sym (gcd+j (j - i) (suc i)) ⟩
                  gcd ((j - i) + suc i) (suc i)  ≡⟨ cong (λ k → gcd k (suc i)) ( begin
@@ -372,13 +344,23 @@
                   suc j ∎ ) ⟩
                  gcd (suc j) (suc i)  ≡⟨ gcdsym {suc j} {suc i} ⟩
                  gcd (suc i) (suc j)  ∎ ) prev where open ≡-Reasoning 
-            ind4 : Dividable (gcd (suc i) (j - i)) (j - i) → Dividable (gcd (suc i) (suc j)) (suc j)
-            ind4 = {!!}
-        ... | tri≈ ¬a b ¬c = {!!}
+            ind7 : (j - i) + suc i ≡ suc j
+            ind7 = begin (suc j - suc i) + suc i ≡⟨ minus+n {suc j} {suc i} (<-trans (s≤s a) a<sa)  ⟩
+                        suc j ∎  where open ≡-Reasoning 
+            ind6 : {k : ℕ } → Dividable k (j - i) → Dividable k (suc i) → Dividable k (suc j)
+            ind6 {k} dj di = subst (λ g → Dividable k g ) ind7 (proj1 (div+div dj di)) 
+            ind4 : Dividable (gcd (suc i) (j - i)) (j - i)
+                 → Dividable (gcd (suc i) (suc j)) (j - i)
+            ind4 prev = subst (λ k → k) ( begin
+                 Dividable (gcd (suc i) (j - i)) (j - i)  ≡⟨ cong  (λ k → Dividable k (j - i)) (gcdsym {suc i}  ) ⟩
+                 Dividable (gcd (j - i ) (suc i) ) (j - i)  ≡⟨ cong  (λ k → Dividable k (j - i)) ( sym (gcd+j  (j - i) (suc i))) ⟩
+                 Dividable (gcd ((j - i) + suc i) (suc i)) (j - i)  ≡⟨ cong  (λ k → Dividable (gcd k (suc i)) (j - i)) ind7 ⟩
+                 Dividable (gcd (suc j) (suc i)) (j - i)    ≡⟨ cong  (λ k → Dividable k (j - i)) (gcdsym {suc j} ) ⟩
+                 Dividable (gcd (suc i) (suc j)) (j - i)   ∎ ) prev where open ≡-Reasoning 
+        ... | tri≈ ¬a refl ¬c = ⟪ ind5 , ind5 ⟫ where
+           ind5 : Dividable (gcd (suc i) (suc i)) (suc i) 
+           ind5 = subst (λ k → Dividable k (suc j)) (sym (gcdmm (suc i) (suc i))) div=  
         ... | tri> ¬a ¬b c = {!!}
-        --ind3 where
-        --   ind3 : Dividable (gcd (suc i) (suc j)) (suc i) ∧ Dividable (gcd (suc i) (suc j)) (suc j)
-        --   ind3 = {!!}
 
         I : Finduction (ℕ ∧ ℕ) _ F
         I = record {