Mercurial > hg > Members > kono > Proof > automaton

changeset 147:0d8a834c9c50

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 Thu, 31 Dec 2020 03:21:05 +0900
parents 6663205ed308
children 8207b69c500b
files agda/root2.agda
diffstat 1 files changed, 55 insertions(+), 38 deletions(-) [+]
line wrap: on
line diff
--- a/agda/root2.agda	Wed Dec 30 12:07:07 2020 +0900
+++ b/agda/root2.agda	Thu Dec 31 03:21:05 2020 +0900
@@ -68,54 +68,71 @@
 gcd22 (suc i) i0 zero o0 = refl
 gcd22 (suc i) i0 (suc o) o0 = refl 
 
+gcd27 : ( i i0 : ℕ ) → gcd1 i i0 0 1 ≤ 1
+gcd27 zero zero = ≤-refl
+gcd27 zero (suc i0) = {!!}
+gcd27 (suc i) zero = {!!}
+gcd27 (suc i) (suc i0) = {!!}
+
+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 )
+
 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 )
+gcdsym {n} {m} = gcdsym1 n n m m 
 
 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
-   gcd23 : { j j0 : ℕ } → 1 < j → 1 < j0 → ¬ (gcd1 zero zero j j0 ≡ 1)
-   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
+   gcd23 : {i0 j0 : ℕ } → 1 < i0  → 1 < j0 → 1 < gcd1 zero i0 zero j0
+   gcd23 {i0} {j0} 1<i 1<j with <-cmp i0 j0
+   ... | tri< a ¬b ¬c = 1<j
+   ... | tri≈ ¬a refl ¬c = 1<i
+   ... | tri> ¬a ¬b c = 1<i
    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) {!!}
-   --- 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 zero o0 1<i 1<j 1<o refl gm gnm = {!!}
+   gcd21 zero i0 zero j0 o o0 1<i 1<j 1<o refl gm gnm = nat-≡< (sym gnm) (gcd23 1<i 1<j)
+   gcd21 zero i0 (suc j) j0 zero o0 1<i 1<j 1<o refl gm gnm = gcd25 i0 o0 j j0 1<o 1<i 1<k gm (subst (λ k → k ≡ 1) (gcdsym1 zero _ (suc j) _) gnm)  where
+      gcd25 : (i0 o0 j j0 : ℕ) → 1 < o0 → 1 < i0
+            → 1 < gcd1 zero i0 zero o0 
+            → ( gm : gcd1 (suc j) j0 zero o0 ≡ gcd1 zero i0 zero o0 ) → (gnm : gcd1 (suc j) j0 zero i0 ≡ 1) → ⊥
+      gcd25 i0 o0 zero j0 1<o 1<i 1<k gm refl with <-cmp i0 o0
+      ... | tri< a ¬b ¬c    = ⊥-elim ( nat-≡< gm 1<o )
+      ... | tri≈ ¬a refl ¬c = ⊥-elim ( nat-≡< gm 1<o )
+      ... | tri> ¬a ¬b c    = ⊥-elim ( nat-≡< gm 1<i )
+      -- gm       : gcd1 (suc j) (suc (suc j)) (suc o0) (suc (suc o0)) ≡ (gcd1 zero (suc i0) zero (suc (suc o0))
+      --            gcd1 j       (suc (suc j))       o0 (suc (suc o0)) 
+      -- gnm      : gcd1 (suc j) (suc (suc j)) i0 (suc i0) ≡ 1
+      gcd25 i0       (suc zero)     (suc j) j0 1<o 1<i 1<k gm gnm = ⊥-elim ( nat-≤> (subst (λ k → k ≤ 1 ) gm (gcd27 (suc j) (suc (suc j)))) 1<k )
+      gcd25 (suc zero) (suc (suc o0)) (suc j) j0 1<o 1<i 1<k gm gnm = {!!}
+      gcd25 (suc (suc i0)) (suc (suc o0)) (suc j) j0 1<o 1<i 1<k 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 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 = {!!}
    gcd21 (suc i) i0 (suc j) j0 (suc o) o0 1<i 1<j 1<o gn gm gnm = 
        gcd21 i i0 j j0 o o0 1<i 1<j 1<o (subst (λ m → m ≡ k) (gcd22 i i0 _ _ ) gn)