Mercurial > hg > Members > kono > Proof > automaton

changeset 224:6077bdd19312

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 22 Jun 2021 15:39:02 +0900
parents 1917df6e3c87
children 9a36ec9b824a
files automaton-in-agda/src/gcd.agda
diffstat 1 files changed, 84 insertions(+), 83 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda	Tue Jun 22 15:36:59 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Tue Jun 22 15:39:02 2021 +0900
@@ -295,84 +295,85 @@
 
 gcd-divable : ( i j  : ℕ )
       → Dividable ( gcd i j ) i ∧ Dividable ( gcd i j ) j
-gcd-divable i j  = n-induction {_} {_} {ℕ ∧ ℕ}
+gcd-divable i j  = f-induction {_} {_} {ℕ ∧ ℕ}
    {λ p  → Dividable ( gcd (proj1 p) (proj2 p) ) (proj1 p) ∧ Dividable ( gcd (proj1 p)  (proj2 p) ) (proj2 p)} F I ⟪ i , j ⟫ where
         F : ℕ ∧ ℕ → ℕ
-        F ⟪ 0 , j ⟫ = 0
+        F ⟪ 0 , 0 ⟫ = 0
+        F ⟪ 0 , suc j ⟫ = 0
         F ⟪ suc i , 0 ⟫ = 0
-        F ⟪ i , j ⟫ with <-cmp i j
-        ... | tri< a ¬b ¬c = j
+        F ⟪ suc i , suc j ⟫ with <-cmp i j
+        ... | tri< a ¬b ¬c = suc j
         ... | tri≈ ¬a b ¬c = 0
-        ... | tri> ¬a ¬b c = i
-        next :  ℕ ∧ ℕ → ℕ ∧ ℕ
-        next ⟪ i , j ⟫ with <-cmp i j
-        ... | tri< a ¬b ¬c = ⟪ i , j - i ⟫
-        ... | tri≈ ¬a b ¬c = ⟪ 0 , 0 ⟫
-        ... | tri> ¬a ¬b c = ⟪ i - j , j  ⟫
+        ... | tri> ¬a ¬b c = suc i
         F0 : { i j : ℕ } → F ⟪ i , j ⟫ ≡ 0 → (i ≡ j) ∨ (i ≡ 0 ) ∨ (j ≡ 0)
         F0 {zero} {zero} p = case1 refl
         F0 {zero} {suc j} p =  case2 (case1 refl)
         F0 {suc i} {zero} p =  case2 (case2 refl)
         F0 {suc i} {suc j} p with <-cmp i j
-        ... | tri< a ¬b ¬c = ⊥-elim ( F11 p )  where
-             F11 : F ⟪ suc i , suc j  ⟫ ≡ 0 → ⊥
-             F11 eq with <-cmp (suc i) (suc j)
-             ... | tri≈ ¬a b ¬c = nat-≡< b (s≤s a)
-        ... | tri≈ ¬a refl ¬c = case1 refl
-        ... | tri> ¬a ¬b c =  ⊥-elim  (F11 p) where 
-             F11 : F ⟪ suc i , suc j  ⟫ ≡ 0 → ⊥
-             F11 eq with <-cmp (suc i) (suc j)
-             ... | tri≈ ¬a b ¬c = nat-≡< (sym b) (s≤s c)
-        Fcase1 : { i j : ℕ } → i ≡ j → Dividable (gcd i j) i ∧ Dividable (gcd i j) j
-        Fcase1 {i} {i} refl = ⟪  subst (λ k → Dividable k i) (sym (gcdmm i i)) div= , subst (λ k → Dividable k i) (sym (gcdmm i i)) div= ⟫
-        Fcase21 : { i j : ℕ } → i ≡ 0 → Dividable (gcd i j) i ∧ Dividable (gcd i j) j
-        Fcase21 {0} {j} refl = ⟪  subst (λ k → Dividable k 0) (sym (trans (gcdsym {0} {j} ) (gcd20 j)))div0
-                                , subst (λ k → Dividable k j) (sym (trans (gcdsym {0} {j}) (gcd20 j))) div= ⟫
-        Fcase22 : { i j : ℕ } → j ≡ 0 → Dividable (gcd i j) i ∧ Dividable (gcd i j) j
-        Fcase22 {i} {0} refl = ⟪  subst (λ k → Dividable k i) (sym (gcd20 i)) div=
-                                , subst (λ k → Dividable k 0) (sym (gcd20 i)) div0 ⟫
-        Fn0 : {i  : ℕ} → (F (next  ⟪ i , 0 ⟫) ≡ 0 ) ∧ (F (next  ⟪ 0 , i ⟫) ≡ 0 )
-        Fn0 {zero} = ⟪ refl , refl ⟫
-        Fn0 {suc i} = ⟪ refl , refl ⟫
-        Fn= : {i j : ℕ} → i ≡ j → F (next  ⟪ i , j ⟫) ≡ 0 
-        Fn= {0} refl = refl
-        Fn= {suc i} refl with <-cmp (suc i) (suc i)
-        ... | tri< a ¬b ¬c = subst (λ k → F ⟪ suc i , k ⟫ ≡ 0 ) (sym (minus<=0 {suc i} {suc i} ≤-refl )) refl
-        ... | tri≈ ¬a b ¬c = refl
-        ... | tri> ¬a ¬b c = subst (λ k → F ⟪ k , suc i  ⟫ ≡ 0 ) (sym (minus<=0 {suc i} {suc i} ≤-refl )) refl
-        F01 : {i j : ℕ} → F ⟪ i , j - i ⟫ ≡ 0 → F (next ⟪ i , j - i ⟫) ≡ 0
-        F01 {zero} {zero} eq = refl
-        F01 {zero} {suc j} eq = refl
-        F01 {suc i} {zero} eq = refl
-        F01 {suc i} {suc j} eq with F0 {suc i} {j - i} eq
-        ... | case1 x = Fn= {suc i} {j - i } x -- suc i ≡ suc j - suc i
-        ... | case2 (case2 x) = subst (λ k → F (next ⟪ suc i , k ⟫) ≡ 0 ) (sym x) (proj1 (Fn0 {suc i})) -- j - i ≡ 0
-        F00 :  {p : ℕ ∧ ℕ} → F (next p) ≡ zero → Dividable (gcd (proj1 p) (proj2 p)) (proj1 p) ∧ Dividable (gcd (proj1 p) (proj2 p)) (proj2 p)
-        F00 {⟪ 0 , j ⟫} eq = Fcase21 refl
-        F00 {⟪ i , 0 ⟫} eq = Fcase22 refl
-        F00 {⟪ suc i , suc j ⟫} eq with <-cmp (suc i) (suc j)
-        ... | tri< a ¬b ¬c with F0 {suc i} {j - i} eq
-        ... | case2 (case2 j-i=0 ) = Fcase1 (sym (i-j=0→i=j (<to≤ a) j-i=0 ))
-        ... | case1 (si=j-i)  = {!!}
-        F00 {⟪ suc i , suc j ⟫} eq | tri≈ ¬a b ¬c = Fcase1 b -- case1 b
-        F00 {⟪ suc i , suc j ⟫} eq | tri> ¬a ¬b c with  F0 {i - j} {suc j} eq
-        ... | case1 x = {!!}
-        ... | case2 (case1 x) = Fcase1 (i-j=0→i=j (<to≤ c) x )
+        ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< (sym p) (s≤s z≤n ))
+        ... | tri≈ ¬a refl ¬c =  case1 refl
+        ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym p) (s≤s z≤n ))
+        F00 :  {p : ℕ ∧ ℕ} → F p ≡ zero → Dividable (gcd (proj1 p) (proj2 p)) (proj1 p) ∧ Dividable (gcd (proj1 p) (proj2 p)) (proj2 p)
+        F00 {⟪ i , j ⟫} eq with F0 {i} {j} eq
+        ... | case1 refl = ⟪  subst (λ k → Dividable k i) (sym (gcdmm i i)) div= , subst (λ k → Dividable k i) (sym (gcdmm i i)) div= ⟫
+        ... | case2 (case1 refl) = ⟪  subst (λ k → Dividable k i) (sym (trans (gcdsym {0} {j} ) (gcd20 j)))div0
+                                    , subst (λ k → Dividable k j) (sym (trans (gcdsym {0} {j}) (gcd20 j))) div= ⟫
+        ... | case2 (case2 refl) = ⟪  subst (λ k → Dividable k i) (sym (gcd20 i)) div=
+                                    , subst (λ k → Dividable k j) (sym (gcd20 i)) div0 ⟫
+        Fsym :  {i j : ℕ } → F ⟪ i , j ⟫ ≡ F ⟪ j , i ⟫
+        Fsym {0} {0} = refl
+        Fsym {0} {suc j} = refl
+        Fsym {suc i} {0} = refl
+        Fsym {suc i} {suc j} with <-cmp i j | <-cmp j i
+        ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim (nat-<> a a₁)
+        ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (¬b (sym b))
+        ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl
+        ... | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = ⊥-elim (¬b refl)
+        ... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl
+        ... | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = ⊥-elim (¬b refl)
+        ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl
+        ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (¬b (sym b))
+        ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (nat-<> c c₁)
+
+        record Fdec ( i j : ℕ ) : Set where
+           field
+               ni : ℕ 
+               nj : ℕ 
+               fdec :  0 < F ⟪ i , j ⟫  → F ⟪ ni , nj ⟫  < F ⟪ i , j ⟫
 
-        Fdecl :  ( p : ℕ ∧ ℕ ) → 0 < F p  →  F (next p) < F p
-        Fdecl ⟪ 0 , j ⟫ ()
-        Fdecl ⟪ suc i , 0 ⟫ ()
-        Fdecl ⟪ suc i , suc j ⟫ 0<F with <-cmp (suc i) (suc j)
-        ... | tri< a ¬b ¬c = fd1 where
-             fd1 : F ⟪ suc i , j - i ⟫ < suc j
-             fd1 with <-cmp i ( j - i )
-             ... | tri< a ¬b ¬c = {!!}  -- j - i < j
-             ... | tri≈ ¬a b ¬c = {!!} -- 0 < j
-             ... | tri> ¬a ¬b c = {!!} -- i < j
-        ... | tri≈ ¬a refl ¬c  = ⊥-elim ( nat-≡< refl 0<F )
-        ... | tri> ¬a ¬b c = fd2 where
-             fd2 : F ⟪ i  - j , suc j  ⟫ < suc i
-             fd2 = {!!}
+        fd1 : ( i j k : ℕ ) → i < j  → k ≡ j - i →  F ⟪ suc i , k ⟫ < F ⟪ suc i , suc j ⟫
+        fd1 i j 0 i<j eq = ⊥-elim ( nat-≡< eq (minus>0 {i} {j} i<j )) 
+        fd1 i j (suc k) i<j eq = fd2 i j k i<j eq where
+               fd2 : ( i j k : ℕ ) → i < j → suc k ≡ j - i  →  F ⟪ suc i , suc k ⟫ < F ⟪ suc i , suc j ⟫
+               fd2 i j k i<j eq with <-cmp i k | <-cmp i j
+               ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = fd3 where
+                    fd3 : suc k < suc j  -- suc j - suc i < suc j
+                    fd3 = subst (λ g → g < suc j) (sym eq) (y-x<y {suc i} {suc j} (s≤s z≤n) (s≤s z≤n))
+               ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (⊥-elim (¬a i<j))
+               ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = ⊥-elim (⊥-elim (¬a i<j))
+               ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = s≤s z≤n
+               ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = ⊥-elim (¬a₁ i<j)
+               ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c =  s≤s z≤n -- i > j
+               ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = fd4 where
+                    fd4 : suc i < suc j
+                    fd4 = s≤s a
+               ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c =  ⊥-elim (¬a₁ i<j)
+               ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ =  ⊥-elim (¬a₁ i<j)
+
+        fedc0 : (i j : ℕ ) → Fdec i j
+        fedc0 0 0 = record { ni =  0 ; nj = 0 ; fdec = λ ()  } 
+        fedc0 (suc i) 0 = record { ni =  suc i ; nj = 0 ; fdec = λ ()  } 
+        fedc0 0 (suc j)  = record { ni =  0 ; nj = suc j ; fdec = λ ()  } 
+        fedc0 (suc i) (suc j) with <-cmp i j
+        ... | tri< i<j ¬b ¬c = record { ni =  suc i ; nj = j - i ; fdec = λ lt → fd1 i j (j - i) i<j refl  } 
+        ... | tri≈ ¬a refl ¬c = record { ni =  suc i ; nj = suc j     ; fdec = λ lt → ⊥-elim (nat-≡< fd0 lt) } where
+              fd0 : {i : ℕ } → 0 ≡ F ⟪ suc i , suc i ⟫
+              fd0 {i} with <-cmp i i
+              ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
+              ... | tri≈ ¬a b ¬c = refl
+              ... | tri> ¬a ¬b c =  ⊥-elim ( ¬b refl )
+        ... | 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 ) } 
 
         ind3 : {i j : ℕ } → i < j 
                → Dividable (gcd (suc i) (j - i)) (suc i) 
@@ -404,25 +405,25 @@
                  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 
 
-        ind :  (p : ℕ ∧  ℕ ) → (
-                 Dividable (gcd (proj1 (next p)) (proj2 (next p))) (proj1 (next p))
-                       ∧ Dividable (gcd (proj1 (next p)) (proj2 (next p))) (proj2 (next p)) )
-            → Dividable (gcd (proj1 p) (proj2 p)) (proj1 p) ∧ Dividable (gcd (proj1 p) (proj2 p)) (proj2 p)
-        ind ⟪ zero , zero ⟫ prev = ind0 where
+        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.nj (fedc0 i 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 ⟫
-        ind ⟪ zero , (suc j) ⟫ prev = ind1 where
+        ind zero (suc j) prev = ind1 where
            ind1 : Dividable (gcd zero (suc j)) zero ∧ Dividable (gcd zero (suc j)) (suc j)
            ind1 = ⟪ div0 , subst (λ k → Dividable k (suc j)) (sym (trans (gcdsym {zero} {suc j}) (gcd20 (suc j)))) div=  ⟫
-        ind ⟪ (suc i) , zero ⟫ prev = ind2 where
+        ind (suc i) zero prev = ind2 where
            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 a (suc i)  , ind6 a (ind4 a {!!}) (ind3 a {!!} ) ⟫ where
+        ind (suc i) (suc j) prev with <-cmp i j
+        ... | tri< a ¬b ¬c = ⟪ ind3 a (proj1 prev)  , ind6 a (ind4 a (proj2 prev)) (ind3 a (proj1 prev) ) ⟫ where
         ... | 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 = ⟪ ind8 c {!!} {!!} , ind10 c  {!!} ⟫ where
+        ... | tri> ¬a ¬b c = ⟪ ind8 c (proj1 prev) (proj2 prev) , ind10 c  (proj2 prev) ⟫ where
            ind9 : {i j : ℕ} → i < j → gcd (j - i) (suc i) ≡ gcd (suc j) (suc i)
            ind9 {i} {j} i<j = begin
                  gcd (j - i ) (suc i)    ≡⟨ sym (gcd+j (j - i ) (suc i)  ) ⟩
@@ -441,12 +442,12 @@
              gcd (i - j + suc j) (suc j)  ≡⟨ cong (λ k → gcd k (suc j)) (ind7 j<i ) ⟩
              gcd (suc i) (suc j) ∎ ) dji where open ≡-Reasoning 
 
-        I : Ninduction (ℕ ∧ ℕ) _ F
+        I : Finduction (ℕ ∧ ℕ) _ F
         I = record {
-              pnext = λ p → next p
-            ; fzero = F00 
-            ; decline = λ {p} lt → Fdecl p lt
-            ; ind = λ {p} prev → ind p prev
+              fzero = F00 
+            ; pnext = λ p → ⟪ Fdec.ni (fedc0 (proj1 p) (proj2 p)) ,  Fdec.nj (fedc0 (proj1 p) (proj2 p)) ⟫ 
+            ; decline = λ {p} lt → Fdec.fdec (fedc0 (proj1 p) (proj2 p))  lt
+            ; ind = λ {p} prev → ind (proj1 p ) ( proj2 p ) prev
           }