Mercurial > hg > Members > kono > Proof > automaton

changeset 223:1917df6e3c87

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
... give up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 22 Jun 2021 15:36:59 +0900
parents a1bb9fb21928
children 6077bdd19312
files automaton-in-agda/src/gcd.agda
diffstat 1 files changed, 15 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda	Tue Jun 22 14:48:46 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Tue Jun 22 15:36:59 2021 +0900
@@ -334,30 +334,30 @@
         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 <-cmp i j --  F ⟪ i - (j - i) , j - i ⟫ ∨ F ⟪ (j - i) -i , j - i -i ⟫
-        ... | tri< a ¬b ¬c =  {!!}
-        ... | tri≈ ¬a refl ¬c = subst (λ k → F (next ⟪ suc i , k ⟫) ≡ 0) F011 (proj1 (Fn0 {suc i})  ) where
-             F011 : 0 ≡ i - i 
-             F011 = sym (minus<=0 {i} ≤-refl )
-        ... | tri> ¬a ¬b c = subst (λ k → F (next ⟪ suc i , k ⟫) ≡ 0) F011 (proj1 (Fn0 {suc i})  ) where
-             F011 : 0 ≡ j - i 
-             F011 = sym (minus<=0 {j} {i} (<to≤ c) )
+        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)  = {!!}
-        ... | case2 (case2 j-i=0 ) = {!!}
-        F00 {⟪ suc i , suc j ⟫} eq | tri≈ ¬a b ¬c = {!!} -- case1 b
-        F00 {⟪ suc i , suc j ⟫} eq | tri> ¬a ¬b c with <-cmp (i - j) (suc j)
-        ... | tri< a ¬b₁ ¬c = Fcase22 {!!}
-        ... | tri≈ ¬a₁ b ¬c = {!!} -- i -j = j
-        ... | tri> ¬a₁ ¬b₁ c₁ = Fcase1 ( i-j=0→i=j (<to≤ c) {!!} )
+        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 )
 
         Fdecl :  ( p : ℕ ∧ ℕ ) → 0 < F p  →  F (next p) < F p
         Fdecl ⟪ 0 , j ⟫ ()
@@ -418,7 +418,7 @@
            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 {!!}  , ind6 a (ind4 a {!!}) (ind3 a {!!} ) ⟫ where
+        ... | tri< a ¬b ¬c = ⟪ ind3 a (suc i)  , ind6 a (ind4 a {!!}) (ind3 a {!!} ) ⟫ 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=