Mercurial > hg > Members > kono > Proof > automaton

changeset 208:984630d2fb0c

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 Sun, 20 Jun 2021 10:09:40 +0900
parents 764bc577b1e9
children 1c537e2b8f69
files automaton-in-agda/src/gcd.agda
diffstat 1 files changed, 39 insertions(+), 32 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda	Sat Jun 19 11:52:45 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Sun Jun 20 10:09:40 2021 +0900
@@ -189,24 +189,26 @@
 
 gcd-divable : ( i i0 j j0 : ℕ )
       → (if : Factor i0 j0) (jf : Factor j0 i0)   -- factor eq * i0 + (j0 - i0) = j0
-      → remain if ≡ j - i  → remain jf ≡ i - j
+      → ((i0 ≤ j0) ∧ (remain if ≡ j - i))  ∨ ((j0 ≤ i0) ∧ (remain jf ≡ i - j))
       → Dividable ( gcd1 i i0 j j0 ) i0 ∧ Dividable ( gcd1 i i0 j j0 ) j0
-gcd-divable zero i0 zero j0 if jf if=0 jf=0 with <-cmp i0 j0
-... | tri< a ¬b ¬c = ⟪ record { factor = 1 ; is-factor = gg1 } ,  record { factor = factor if ; is-factor = gg2 } ⟫ where
-    gg2 : factor if *  i0 + 0 ≡ j0
-    gg2 = begin
-      factor if * i0 + 0 ≡⟨ cong (λ k → factor if * i0 + k) (sym if=0) ⟩
+gcd-divable zero i0 zero j0 if jf if=0∨jf=0 with <-cmp i0 j0
+... | tri< a ¬b ¬c = ⟪ record { factor = 1 ; is-factor = gg1 } ,  record { factor = factor if ; is-factor = (gg2 if=0∨jf=0) } ⟫ where
+    gg2 : (if=0∨jf=0 : ((i0 ≤ j0) ∧ (remain if ≡ 0)) ∨ ((j0 ≤ i0) ∧ (remain jf ≡ 0))) →  factor if *  i0 + 0 ≡ j0
+    gg2 (case1 x) = begin
+      factor if * i0 + 0 ≡⟨ cong (λ k → factor if * i0 + k) (sym (proj2 x)) ⟩
       factor if * i0 + remain if ≡⟨ is-factor if ⟩
       j0 ∎   where open ≡-Reasoning  
+    gg2 (case2 x) = ⊥-elim ( nat-≤> (proj1 x) a)
 ... | tri≈ ¬a refl ¬c = ⟪ record { factor = 1 ; is-factor = gg1 } ,  record { factor = 1 ; is-factor = gg1 } ⟫
-... | tri> ¬a ¬b c = ⟪ record { factor = factor jf ; is-factor = gg2 } ,  record { factor = 1 ; is-factor = gg1 } ⟫ where
-    gg2 : factor jf *  j0 + 0 ≡ i0
-    gg2 = begin
-      factor jf * j0 + 0 ≡⟨ cong (λ k → factor jf * j0 + k) (sym jf=0)  ⟩
+... | tri> ¬a ¬b c = ⟪ record { factor = factor jf ; is-factor = gg2 if=0∨jf=0  } ,  record { factor = 1 ; is-factor = gg1 } ⟫ where
+    gg2 : (if=0∨jf=0 : ((i0 ≤ j0) ∧ (remain if ≡ 0)) ∨ ((j0 ≤ i0) ∧ (remain jf ≡ 0))) → factor jf *  j0 + 0 ≡ i0
+    gg2 (case1 x) = ⊥-elim ( nat-≤> (proj1 x) c)
+    gg2 (case2 x) = begin
+      factor jf * j0 + 0 ≡⟨ cong (λ k → factor jf * j0 + k) (sym (proj2 x)) ⟩
       factor jf * j0 + remain jf ≡⟨ is-factor jf ⟩
       i0 ∎   where open ≡-Reasoning  
-gcd-divable zero i0 (suc zero) j0 if jf if=0 jf=0 =  ⟪ record { factor = i0 ; is-factor = gg3 } ,  record { factor = j0 ; is-factor = gg3 } ⟫ 
-gcd-divable zero zero (suc (suc j)) j0 if jf if=0 jf=0 = ⟪ record { factor = factor jf ; is-factor = gg4 } ,  record { factor = 1 ; is-factor = gg1 } ⟫
+gcd-divable zero i0 (suc zero) j0 if jf if=0∨jf=0 =  ⟪ record { factor = i0 ; is-factor = gg3 } ,  record { factor = j0 ; is-factor = gg3 } ⟫ 
+gcd-divable zero zero (suc (suc j)) j0 if jf if=0∨jf=0 = ⟪ record { factor = factor jf ; is-factor = gg4 } ,  record { factor = 1 ; is-factor = gg1 } ⟫
    where
     gg4 :  factor jf * j0  + 0 ≡ zero
     gg4 with  m*n≡0⇒m≡0∨n≡0 (factor jf) (  m+n≡0⇒m≡0 (factor jf * j0) (is-factor jf))
@@ -219,16 +221,15 @@
       factor jf * j0  ≡⟨ cong (λ k → factor jf * k) y  ⟩
       factor jf * 0  ≡⟨ *-comm (factor jf) 0  ⟩
       0 ∎   where open ≡-Reasoning
-gcd-divable zero (suc i0) (suc (suc j)) j0 if jf if=0 jf=0  =
+gcd-divable zero (suc i0) (suc (suc j)) j0 if jf if=0∨jf=0  =
     ⟪ record { factor = gg8 ; is-factor = {!!} } , record { factor = gg8 ; is-factor = {!!} } ⟫ where
     gg8 : ℕ
     gg8 = gcd1 i0 (suc i0) (suc j) (suc (suc j))
-    gg9 : factor if * suc i0 + (suc j - i0) ≡ suc (suc j) 
+    gg9 : 1 * suc i0 + (suc j - i0) ≡ suc (suc j)
     gg9 = begin
-      factor if * suc i0 + (suc j - i0)  ≡⟨ {!!}  ⟩
-      factor if * suc i0 + (suc (suc j) - zero)  ≡⟨ {!!} ⟩
-      factor if * suc i0 + remain if ≡⟨ is-factor if ⟩
-      j0  ≡⟨ {!!}  ⟩
+      1 * suc i0 + (suc j - i0)   ≡⟨ +-comm (1 * suc i0) _ ⟩
+      (suc (suc j) - suc i0 ) + 1 * suc i0    ≡⟨ cong (λ k →  (suc (suc j) - suc i0 ) + suc k ) (+-comm i0 0) ⟩
+      (suc (suc j) - suc i0 ) + suc i0    ≡⟨ minus+n (s≤s (s≤s {!!})) ⟩
       suc (suc j)  ∎   where open ≡-Reasoning
     gg10 : factor jf * suc (suc j) + (i0 - suc j) ≡ suc i0
     gg10 = begin
@@ -236,17 +237,19 @@
       factor jf * j0 + remain jf ≡⟨ is-factor jf  ⟩
       suc i0  ∎   where open ≡-Reasoning
     gg7 : Dividable gg8 (suc i0) ∧ Dividable gg8 (suc (suc j))
-    gg7 = gcd-divable i0 (suc i0) (suc j) (suc (suc j))
-        record { factor = factor if ; is-factor = gg9 ; remain = suc j - i0 }
-        record { factor = factor jf ; is-factor = gg10 ; remain = i0 - suc j } refl refl 
+    gg7 = gcd-divable i0 (suc i0) (suc j) (suc (suc j)) -- Factor (suc i0) (suc (suc j)),  Factor (suc (suc j)) (suc i0)
+        record { factor = 1 ; is-factor = {!!} ; remain = suc j - i0 }
+        record { factor = factor jf ; is-factor = {!!} ; remain = i0 - suc j } {!!} 
+--
+--   gcd i (i + j ) = gcd i j
 --if   : Factor (suc i0) j0    --  factor if * (suc i0) + (suc (suc j) - zero  ≡ j0
 --jf   : Factor j0 (suc i0)    --  factor jf * j0 + (zero - suc (suc j))) ≡ suc i0
 --if=0 : remain if ≡ (suc (suc j) - zero)
 --jf=0 : remain jf ≡ (zero - suc (suc j))
 --    factor if * suc i0 + (suc j - i0) ≡ suc (suc j)
 --    factor jf * suc (suc j) + (i0 - suc j) ≡ suc i
-gcd-divable (suc zero) i0 zero j0 if jf if=0 jf=0 = ⟪ record { factor = i0 ; is-factor = gg3 } ,  record { factor = j0 ; is-factor = gg3 } ⟫
-gcd-divable (suc (suc i)) i0 zero zero if jf if=0 jf=0 = ⟪ record { factor = 1 ; is-factor = gg1 } ,  record { factor = factor if ; is-factor = gg4 } ⟫
+gcd-divable (suc zero) i0 zero j0 if jf if=0∨jf=0 = ⟪ record { factor = i0 ; is-factor = gg3 } ,  record { factor = j0 ; is-factor = gg3 } ⟫
+gcd-divable (suc (suc i)) i0 zero zero if jf if=0∨jf=0 = ⟪ record { factor = 1 ; is-factor = gg1 } ,  record { factor = factor if ; is-factor = gg4 } ⟫
    where
     gg4 :  factor if * i0  + 0 ≡ zero
     gg4 with  m*n≡0⇒m≡0∨n≡0 (factor if) (  m+n≡0⇒m≡0 (factor if * i0) (is-factor if))
@@ -259,32 +262,36 @@
       factor if * i0  ≡⟨ cong (λ k → factor if * k) y  ⟩
       factor if * 0  ≡⟨ *-comm (factor if) 0  ⟩
       0 ∎   where open ≡-Reasoning
-gcd-divable (suc (suc i)) i0 zero (suc j0) if jf if=0 jf=0 with gcd-divable (suc i) (suc (suc i)) j0 (suc j0) {!!} {!!} refl refl
+gcd-divable (suc (suc i)) i0 zero (suc j0) if jf if=0∨jf=0 with gcd-divable (suc i) (suc (suc i)) j0 (suc j0) {!!} {!!} {!!}
 ... | t = ⟪ {!!} , {!!} ⟫
-gcd-divable (suc zero) i0 (suc j) j0 if jf if=0 jf=0 =  
+gcd-divable (suc zero) i0 (suc j) j0 if jf if=0∨jf=0 =  
      gcd-divable zero i0 j j0 record {  factor = factor if ; is-factor = gg4 ; remain = j - zero }
-                              record {  factor = factor jf ; is-factor = gg5 ; remain = zero - j  } refl refl where
+                              record {  factor = factor jf ; is-factor = gg5 ; remain = zero - j  } {!!} where
     gg4 : factor if * i0 + (j - zero) ≡ j0
     gg4 = begin
-      factor if * i0 + (j - zero)  ≡⟨  cong ( λ k → factor if * i0 + k) (sym if=0) ⟩
+      factor if * i0 + (j - zero)  ≡⟨  cong ( λ k → factor if * i0 + k) (sym {!!}) ⟩
       factor if * i0 + remain if ≡⟨ is-factor if   ⟩
       j0 ∎   where open ≡-Reasoning  
     gg5 : factor jf * j0 + (zero - j) ≡ i0
     gg5 = begin
-      factor jf * j0 + (zero - j)  ≡⟨  cong ( λ k → factor jf * j0 + k) (sym jf=0) ⟩
+      factor jf * j0 + (zero - j)  ≡⟨  cong ( λ k → factor jf * j0 + k) (sym {!!}) ⟩
       factor jf * j0 + remain jf ≡⟨ is-factor jf   ⟩
       i0 ∎   where open ≡-Reasoning  
-gcd-divable (suc (suc i)) i0 (suc j) j0 if jf if=0 jf=0 = 
+gcd-divable (suc (suc i)) i0 (suc j) j0 if jf if=0∨jf=0 = 
      gcd-divable (suc i) i0 j j0 record {  factor = factor if ; is-factor = gg4 ; remain = j - suc i }
-                              record {  factor = factor jf ; is-factor = gg5 ; remain = suc i - j } refl refl where
+                              record {  factor = factor jf ; is-factor = gg5 ; remain = suc i - j } (gg6 if=0∨jf=0) where
+    gg6 : ((i0 ≤ j0) ∧ (remain if ≡ (suc j - suc (suc i)))) ∨ ((j0 ≤ i0) ∧ (remain jf ≡ (suc (suc i) - suc j)))
+        → ((i0 ≤ j0) ∧ ((j - suc i) ≡ (j - suc i))) ∨ ((j0 ≤ i0) ∧ ((suc i - j) ≡ (suc i - j)))
+    gg6 (case1 x) = case1 ⟪ proj1 x , refl ⟫ 
+    gg6 (case2 x) = case2 ⟪ proj1 x , refl ⟫ 
     gg4 : factor if * i0 + (j - suc i ) ≡ j0
     gg4 = begin
-      factor if * i0 + ( j - suc i ) ≡⟨ cong ( λ k → factor if * i0 + k ) (sym if=0) ⟩ 
+      factor if * i0 + ( j - suc i ) ≡⟨ cong ( λ k → factor if * i0 + k ) (sym {!!}) ⟩ 
       factor if * i0 + remain if  ≡⟨ is-factor if   ⟩
       j0 ∎   where open ≡-Reasoning  
     gg5 : factor jf * j0 + (suc i - j) ≡ i0
     gg5 = begin
-      factor jf * j0 + ( suc i - j ) ≡⟨ cong ( λ k → factor jf * j0 + k ) (sym jf=0) ⟩  
+      factor jf * j0 + ( suc i - j ) ≡⟨ cong ( λ k → factor jf * j0 + k ) (sym {!!}) ⟩  
       factor jf * j0 + remain jf  ≡⟨ is-factor jf   ⟩
       i0 ∎   where open ≡-Reasoning