# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1624184806 -32400
# Node ID 1c537e2b8f69394976100f273192ca01a1957164
# Parent  984630d2fb0c88842fc924eceebf0340644c211e
... f-induction

diff -r 984630d2fb0c -r 1c537e2b8f69 automaton-in-agda/src/gcd.agda
--- a/automaton-in-agda/src/gcd.agda	Sun Jun 20 10:09:40 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Sun Jun 20 19:26:46 2021 +0900
@@ -65,6 +65,11 @@
 div0 :  {k : ℕ} → Dividable k 0
 div0 {k} = record { factor = 0; is-factor = refl }
 
+div= :  {k : ℕ} → Dividable k k
+div= {k} = record { factor = 1; is-factor = ( begin
+        k + 0 * k + 0  ≡⟨ trans ( +-comm _ 0) ( +-comm _ 0) ⟩
+        k ∎ ) }  where open ≡-Reasoning
+
 gcd1 : ( i i0 j j0 : ℕ ) → ℕ
 gcd1 zero i0 zero j0 with <-cmp i0 j0
 ... | tri< a ¬b ¬c = i0
@@ -81,6 +86,58 @@
 gcd : ( i j : ℕ ) → ℕ
 gcd i j = gcd1 i i j j 
 
+gcd20 : (i : ℕ) → gcd i 0 ≡ i
+gcd20 zero = refl
+gcd20 (suc i) = gcd201 (suc i) where
+    gcd201 : (i : ℕ ) → gcd1 i i zero zero ≡ i
+    gcd201 zero = refl
+    gcd201 (suc zero) = refl
+    gcd201 (suc (suc i)) = refl
+
+gcd22 : ( i i0 o o0 : ℕ ) → gcd1 (suc i) i0 (suc o) o0 ≡ gcd1 i i0 o o0
+gcd22 zero i0 zero o0 = refl
+gcd22 zero i0 (suc o) o0 = refl
+gcd22 (suc i) i0 zero o0 = refl
+gcd22 (suc i) i0 (suc o) o0 = refl 
+
+gcdmm : (n m : ℕ) → gcd1 n m n m ≡ m
+gcdmm zero m with <-cmp m m
+... | tri< a ¬b ¬c = refl
+... | tri≈ ¬a refl ¬c = refl
+... | tri> ¬a ¬b c = refl
+gcdmm (suc n) m  = subst (λ k → k ≡ m) (sym (gcd22 n m n m )) (gcdmm n m )
+
+gcdsym2 : (i j : ℕ) → gcd1 zero i zero j ≡ gcd1 zero j zero i
+gcdsym2 i 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 (nat-≡< (sym b) a) 
+... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl
+... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (nat-≡< (sym b) a) 
+... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl
+... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (nat-≡< b c) 
+... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl
+... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (nat-≡< b c) 
+... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (nat-<> c c₁) 
+gcdsym1 : ( i i0 j j0 : ℕ ) → gcd1 i i0 j j0 ≡ gcd1 j j0 i i0
+gcdsym1 zero zero zero zero = refl
+gcdsym1 zero zero zero (suc j0) = refl
+gcdsym1 zero (suc i0) zero zero = refl
+gcdsym1 zero (suc i0) zero (suc j0) = gcdsym2 (suc i0) (suc j0)
+gcdsym1 zero zero (suc zero) j0 = refl
+gcdsym1 zero zero (suc (suc j)) j0 = refl
+gcdsym1 zero (suc i0) (suc zero) j0 = refl
+gcdsym1 zero (suc i0) (suc (suc j)) j0 = gcdsym1 i0 (suc i0) (suc j) (suc (suc j))
+gcdsym1 (suc zero) i0 zero j0 = refl
+gcdsym1 (suc (suc i)) i0 zero zero = refl
+gcdsym1 (suc (suc i)) i0 zero (suc j0) = gcdsym1 (suc i) (suc (suc i))j0 (suc j0) 
+gcdsym1 (suc i) i0 (suc j) j0 = subst₂ (λ j k → j ≡ k ) (sym (gcd22 i _ _ _)) (sym (gcd22 j _ _ _)) (gcdsym1 i i0 j j0 )
+
+gcdsym : { n m : ℕ} → gcd n m ≡ gcd m n
+gcdsym {n} {m} = gcdsym1 n n m m 
+
+gcd11 : ( i  : ℕ ) → gcd i i ≡ i
+gcd11 i = gcdmm i i 
+
 div1 : { k : ℕ } → k > 1 →  ¬  Dividable k 1
 div1 {k} k>1 record { factor = (suc f) ; is-factor = fa } = ⊥-elim ( nat-≡< (sym fa) ( begin
     2 ≤⟨ k>1 ⟩
@@ -170,13 +227,6 @@
    → Dividable k ( gcd i  j ) 
 gcd-div i j k k>1 if jf = gcd-gt i i j j k k>1 (DtoF if) if (DtoF jf) jf (div-div k>1 if jf)
 
--- open import Data.Sum.Base
--- factor-0 : (i j : ℕ) → j ≤ i → Factor (i - j) 0 → i ≡ j
--- factor-0 i j lt eq with m*n≡0⇒m≡0∨n≡0 (factor eq) ( m+n≡0⇒m≡0 (factor eq * (i - j)) (is-factor eq ) )
--- ... | inj₁ x = {!!}
--- ... | inj₂ y =  i-j=0→i=j lt y
---     factor eq * (i - j) + remain eq ≡⟨ is-factor eq ⟩ 
-
 gg1 : {i0 : ℕ } → 1 * i0 + 0 ≡ i0
 gg1 {i0} = begin  1 * i0 + 0 ≡⟨ +-comm _ 0 ⟩
     i0 + 0 ≡⟨ +-comm _ 0 ⟩
@@ -187,6 +237,84 @@
 
 open import Data.Sum.Base
 
+gcd-divable1 : ( i j  : ℕ )
+      → Dividable ( gcd i j ) i ∧ Dividable ( gcd i  j ) j
+gcd-divable1 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 ⟪ i , 0 ⟫ = 0
+        F ⟪ suc i , suc j ⟫ with <-cmp i j
+        ... | tri< a ¬b ¬c = j - i 
+        ... | tri≈ ¬a b ¬c = 0
+        ... | tri> ¬a ¬b c = i - j
+        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 = case1 ( sym (cong suc ( i-j=0→i=j {j} {i} (<to≤ a)  p )) )
+        ... | tri≈ ¬a refl ¬c = case1 refl
+        ... | tri> ¬a ¬b c = case1 (cong suc ( i-j=0→i=j {i} {j} (<to≤ c) p ))
+        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 ⟫
+        record Fdec ( i j : ℕ ) : Set where
+           field
+               ni : ℕ 
+               nj : ℕ 
+               fdec :  0 < F ⟪ i , j ⟫  → F ⟪ ni , nj ⟫  < F ⟪ i , j ⟫
+        F<i : {i j : ℕ} → 0 < i  → 0 < j →  F ⟪ i , j  ⟫  <  j
+        F<i {suc i} {suc j} 0<i 0<j with <-cmp i j
+        ... | tri< a ¬b ¬c = fd3 where
+           fd3 : suc j - suc i < suc j
+           fd3 = {!!} 
+        ... | tri≈ ¬a refl ¬c = fd4 where
+           fd4 : 0 < suc j
+           fd4 = {!!} 
+        ... | tri> ¬a ¬b c = fd5 where
+           fd5 : suc i - suc j < suc j
+           fd5 = {!!} 
+        i-j≤F : {i j : ℕ} → 0 < i  → 0 < j → j < i  →  i - j ≤ F ⟪ i , j  ⟫  
+        i-j≤F = {!!}
+        F-sym : {i j : ℕ} → F ⟪ i , j  ⟫  ≡  F ⟪ j , i  ⟫ 
+        F-sym {zero} {zero} = refl
+        F-sym {zero} {suc j} = refl
+        F-sym {suc i} {zero} = refl
+        F-sym {suc i} {suc j} with <-cmp  i j | <-cmp j i
+        ... | tri< a ¬b ¬c | tri> a' ¬b' ¬c' = refl
+        ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim (¬c₁ a)
+        ... | tri< a ¬b ¬c | tri≈ ¬a refl ¬c₁ = ⊥-elim (¬b refl)
+        ... | tri≈ ¬a refl ¬c |  tri≈ ¬a' refl ¬c'  = refl
+        ... | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = ⊥-elim (¬a a)
+        ... | 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₁ refl ¬c = ⊥-elim (¬b refl)
+        ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (¬a c₁)
+        fedc0 : (i j : ℕ ) → Fdec i j
+        fedc0 0 j = record { ni = 0 ; nj = j ; fdec =  λ lt → ⊥-elim  {!!} }
+        fedc0 i 0 = record { ni = i ; nj = 0 ; fdec =  λ lt → ⊥-elim  {!!} }
+        fedc0 (suc i) (suc j) with <-cmp i j
+        ... | tri< a ¬b ¬c = record { ni =  suc i ; nj = suc j - suc i ; fdec = λ lt → fd1 } where
+            fd1 :  F ⟪ suc i , suc j - suc i ⟫ < F ⟪ suc i , suc j ⟫
+            fd1 = begin
+              suc (F ⟪ suc i , suc j - suc i ⟫) ≤⟨ F<i {suc i} {suc j - suc i} (s≤s z≤n)  {!!}  ⟩
+              suc j - suc i  ≤⟨ i-j≤F {!!} {!!} {!!} ⟩
+              F ⟪ suc i , suc j ⟫ ∎   where open ≤-Reasoning  
+        ... | tri≈ ¬a b ¬c = record { ni =  suc i ; nj = suc j     ; fdec = λ lt → ⊥-elim (nat-≡< {!!} {!!} ) }
+        ... | tri> ¬a ¬b c = record { ni =  suc i - suc j ; nj = suc j ; fdec = {!!} }
+        I : Finduction (ℕ ∧ ℕ) _ F
+        I = record {
+              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 = {!!}
+          } 
+
 gcd-divable : ( i i0 j j0 : ℕ )
       → (if : Factor i0 j0) (jf : Factor j0 i0)   -- factor eq * i0 + (j0 - i0) = j0
       → ((i0 ≤ j0) ∧ (remain if ≡ j - i))  ∨ ((j0 ≤ i0) ∧ (remain jf ≡ i - j))
@@ -236,6 +364,10 @@
       factor jf * suc (suc j) + (i0 - suc j) ≡⟨ {!!}  ⟩
       factor jf * j0 + remain jf ≡⟨ is-factor jf  ⟩
       suc i0  ∎   where open ≡-Reasoning
+    gg11 : ((suc i0 ≤ j0) ∧ (remain if ≡ (suc (suc j) - zero))) ∨ ((j0 ≤ suc i0) ∧ (remain jf ≡ (zero - suc (suc j))))
+       → ((suc i0 ≤ suc (suc j)) ∧ ((suc j - i0) ≡ (suc j - i0))) ∨ ((suc (suc j) ≤ suc i0) ∧ ((i0 - suc j) ≡ (i0 - suc j)))
+    gg11 (case1 x) = case1 ⟪ {!!} , refl ⟫
+    gg11 (case2 x) = case2 ⟪ {!!} , refl ⟫
     gg7 : Dividable gg8 (suc i0) ∧ Dividable gg8 (suc (suc j))
     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 }
@@ -295,58 +427,6 @@
       factor jf * j0 + remain jf  ≡⟨ is-factor jf   ⟩
       i0 ∎   where open ≡-Reasoning  
 
-gcd22 : ( i i0 o o0 : ℕ ) → gcd1 (suc i) i0 (suc o) o0 ≡ gcd1 i i0 o o0
-gcd22 zero i0 zero o0 = refl
-gcd22 zero i0 (suc o) o0 = refl
-gcd22 (suc i) i0 zero o0 = refl
-gcd22 (suc i) i0 (suc o) o0 = refl 
-
-gcd20 : (i : ℕ) → gcd i 0 ≡ i
-gcd20 zero = refl
-gcd20 (suc i) = gcd201 (suc i) where
-    gcd201 : (i : ℕ ) → gcd1 i i zero zero ≡ i
-    gcd201 zero = refl
-    gcd201 (suc zero) = refl
-    gcd201 (suc (suc i)) = refl
-
-gcdmm : (n m : ℕ) → gcd1 n m n m ≡ m
-gcdmm zero m with <-cmp m m
-... | tri< a ¬b ¬c = refl
-... | tri≈ ¬a refl ¬c = refl
-... | tri> ¬a ¬b c = refl
-gcdmm (suc n) m  = subst (λ k → k ≡ m) (sym (gcd22 n m n m )) (gcdmm n m )
-
-gcdsym2 : (i j : ℕ) → gcd1 zero i zero j ≡ gcd1 zero j zero i
-gcdsym2 i 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 (nat-≡< (sym b) a) 
-... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl
-... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (nat-≡< (sym b) a) 
-... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl
-... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (nat-≡< b c) 
-... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl
-... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (nat-≡< b c) 
-... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (nat-<> c c₁) 
-gcdsym1 : ( i i0 j j0 : ℕ ) → gcd1 i i0 j j0 ≡ gcd1 j j0 i i0
-gcdsym1 zero zero zero zero = refl
-gcdsym1 zero zero zero (suc j0) = refl
-gcdsym1 zero (suc i0) zero zero = refl
-gcdsym1 zero (suc i0) zero (suc j0) = gcdsym2 (suc i0) (suc j0)
-gcdsym1 zero zero (suc zero) j0 = refl
-gcdsym1 zero zero (suc (suc j)) j0 = refl
-gcdsym1 zero (suc i0) (suc zero) j0 = refl
-gcdsym1 zero (suc i0) (suc (suc j)) j0 = gcdsym1 i0 (suc i0) (suc j) (suc (suc j))
-gcdsym1 (suc zero) i0 zero j0 = refl
-gcdsym1 (suc (suc i)) i0 zero zero = refl
-gcdsym1 (suc (suc i)) i0 zero (suc j0) = gcdsym1 (suc i) (suc (suc i))j0 (suc j0) 
-gcdsym1 (suc i) i0 (suc j) j0 = subst₂ (λ j k → j ≡ k ) (sym (gcd22 i _ _ _)) (sym (gcd22 j _ _ _)) (gcdsym1 i i0 j j0 )
-
-gcdsym : { n m : ℕ} → gcd n m ≡ gcd m n
-gcdsym {n} {m} = gcdsym1 n n m m 
-
-gcd11 : ( i  : ℕ ) → gcd i i ≡ i
-gcd11 i = gcdmm i i 
-
 gcd203 : (i : ℕ) → gcd1 (suc i) (suc i) i i ≡ 1
 gcd203 zero = refl
 gcd203 (suc i) = gcd205 (suc i) where
diff -r 984630d2fb0c -r 1c537e2b8f69 automaton-in-agda/src/nat.agda
--- a/automaton-in-agda/src/nat.agda	Sun Jun 20 10:09:40 2021 +0900
+++ b/automaton-in-agda/src/nat.agda	Sun Jun 20 19:26:46 2021 +0900
@@ -234,6 +234,16 @@
          suc ((x + y) - y) ≡⟨ cong suc (minus+y-y {x} {y}) ⟩
          suc x ∎  where open ≡-Reasoning
 
+y-x<y : {x y : ℕ } → 0 < x → 0 < y  → y - x  <  y
+y-x<y {x} {y} 0<x 0<y with <-cmp x (suc y)
+... | tri< a ¬b ¬c = +-cancelʳ-< {x} (y - x) y ( begin
+         suc ((y - x) + x) ≡⟨ cong suc (minus+n {y} {x} a ) ⟩
+         suc y  ≡⟨ +-comm 1 _ ⟩
+         y + suc 0  ≤⟨ +-mono-≤ ≤-refl 0<x ⟩
+         y + x ∎ )  where open ≤-Reasoning
+... | tri≈ ¬a refl ¬c = subst ( λ k → k < y ) (sym (minus<=0 {y} {x} refl-≤s )) 0<y
+... | tri> ¬a ¬b c = subst ( λ k → k < y ) (sym (minus<=0 {y} {x} (≤-trans (≤-trans refl-≤s refl-≤s) c))) 0<y -- suc (suc y) ≤ x → y ≤ x
+
 open import Relation.Binary.Definitions
 
 distr-minus-* : {x y z : ℕ } → (minus x y) * z ≡ minus (x * z) (y * z) 
@@ -365,7 +375,7 @@
   field
     fzero   : {p : P} → f p ≡ zero → Q p
     pnext : (p : P ) → P
-    decline : {p : P} → f (pnext p) < f p
+    decline : {p : P} → 0 < f p  → f (pnext p) < f p
     ind : {p : P} → Q (pnext p) → Q p
 
 y<sx→y≤x : {x y : ℕ} → y < suc x → y ≤ x
@@ -375,7 +385,10 @@
   → (f : P → ℕ) 
   → Finduction P Q f
   → (p : P ) → Q p
-f-induction {n} {m} {P} {Q} f I p = f-induction0 p (f p)  (<to≤ (Finduction.decline I {p})) where 
+f-induction {n} {m} {P} {Q} f I p with <-cmp 0 (f p)
+... | tri> ¬a ¬b ()
+... | tri≈ ¬a b ¬c = Finduction.fzero I (sym b) 
+... | tri< lt _ _ = f-induction0 p (f p) (<to≤ (Finduction.decline I lt)) where 
    f-induction0 : (p : P) → (x : ℕ) → (f (Finduction.pnext I p)) ≤ x → Q p
    f-induction0 p zero le = Finduction.ind I (Finduction.fzero I (fi0 _ le)) where
       fi0 : (x : ℕ) → x ≤ zero → x ≡ zero
@@ -384,7 +397,8 @@
    ... | tri< (s≤s a) ¬b ¬c = f-induction0 p x a 
    ... | tri≈ ¬a b ¬c = Finduction.ind I (f-induction0 (Finduction.pnext I p) x (y<sx→y≤x f1)) where
        f1 : f (Finduction.pnext I (Finduction.pnext I p)) < suc x
-       f1 = subst (λ k → f (Finduction.pnext I (Finduction.pnext I p)) < k ) b ( Finduction.decline I {Finduction.pnext I p} )
+       f1 = subst (λ k → f (Finduction.pnext I (Finduction.pnext I p)) < k ) b ( Finduction.decline I {Finduction.pnext I p}
+         (subst (λ k → 0 < k ) (sym b) (s≤s z≤n ) ))
    ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> le c )