Mercurial > hg > Members > kono > Proof > automaton

changeset 146:6663205ed308

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 Wed, 30 Dec 2020 12:07:07 +0900
parents cdfdc8bfb3db
children 0d8a834c9c50
files agda/root2.agda
diffstat 1 files changed, 45 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/agda/root2.agda	Tue Dec 29 17:53:40 2020 +0900
+++ b/agda/root2.agda	Wed Dec 30 12:07:07 2020 +0900
@@ -31,7 +31,10 @@
 even*n {n} {m} en = subst even (*-comm m n) (n*even {m} {n} en)
 
 gcd1 : ( i i0 j j0 : ℕ ) → ℕ
-gcd1 zero i0 zero j0 = i0
+gcd1 zero i0 zero j0 with <-cmp i0 j0
+... | tri< a ¬b ¬c = j0
+... | tri≈ ¬a refl ¬c = i0
+... | tri> ¬a ¬b c = i0
 gcd1 zero i0 (suc zero) j0 = 1
 gcd1 zero zero (suc (suc j)) j0 = j0
 gcd1 zero (suc i0) (suc (suc j)) j0 = gcd1 i0 (suc i0) (suc j) (suc (suc j))
@@ -59,25 +62,58 @@
 -- gcd25 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd m n
 -- gcd27 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n k ≡ k → k ≤ n
 
+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 
+
+gcdsym : { n m : ℕ} → gcd n m ≡ gcd m n
+gcdsym {n} {m} = gcdsym1 n n m m where
+   gcdsym0 : (i : ℕ) → gcd1 zero i zero i ≡ gcd1 zero i zero i
+   gcdsym0 i = refl
+   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 )
+
 gcd24 : { n m k : ℕ} → n > 1 → m > 1 → k > 1 → gcd n k ≡ k → gcd m k ≡ k → ¬ ( gcd n m ≡ 1 )
 gcd24 {n} {m} {k} 1<n 1<m 1<k gn gm gnm = gcd21 n n m m k k 1<n 1<m 1<k gn gm gnm where
-   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 
    gcd23 : { j j0 : ℕ } → 1 < j → 1 < j0 → ¬ (gcd1 zero zero j j0 ≡ 1)
-   gcd23 {zero} {suc j0} 1<j 1<j0 ()
+   gcd23 {zero} {suc j0} 1<j 1<j0 _ = {!!}
    gcd23 {suc zero} {suc j0} 1<j 1<j0 gn = nat-<≡ 1<j
    gcd23 {suc (suc j)} {suc .0} 1<j 1<j0 refl = nat-<≡ 1<j0
    1<ss : {j : ℕ} → 1 < suc (suc j)
    1<ss = s≤s (s≤s z≤n)
    gcd21 : ( i i0 j j0 o o0 : ℕ ) → 1 < i0 → 1 < j0 → 1 < o0 →  gcd1 i i0 o o0 ≡ k → gcd1 j j0 o o0 ≡ k → gcd1 i i0 j j0 ≡ 1 → ⊥
-   gcd21 zero i0 zero j0 o o0 1<i 1<j 1<o refl gm gnm = nat-≡< (sym gnm) 1<i
+   gcd21 zero i0 zero j0 o o0 1<i 1<j 1<o refl gm gnm = nat-≡< (sym gnm) {!!}
    --- gcd1 zero i0 o o0 ≡ k    o = suc zero → k ≡ 1 
    ---                          i0 = zero , o = suc (suc o) → o0 = k -> gcd1 zero zero (suc j) j0 ≡ 1
    --                           i0 = suc i0, o = suc (suc o) → gn = gcd1 i0 (suc i0) (suc o) (suc (suc o))
-   gcd21 zero i0 (suc j) j0 o o0 1<i 1<j 1<o gn gm gnm = {!!}
+   gcd21 zero i0 (suc j) j0 zero o0 1<i 1<j 1<o refl gm gnm = {!!}
+   gcd21 zero i0 (suc j) j0 (suc zero) o0 1<i 1<j 1<o refl gm gnm = nat-<≡ 1<k
+   gcd21 zero (suc i0) (suc j) j0 (suc (suc o)) o0 1<i 1<j 1<o gn gm gnm = 
+      gcd21 i0 {!!} (suc j) j0 (suc o) (suc (suc o)) 1<i 1<j {!!} gn {!!} {!!}
    gcd21 (suc i) i0 zero j0 o o0 1<i 1<j 1<o gn gm gnm = {!!}
    -- ?
    gcd21 (suc i) i0 (suc j) j0 zero o0 1<i 1<j 1<o gn gm gnm = {!!}