Mercurial > hg > Members > kono > Proof > automaton
changeset 211:28d4fb7b576f
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 20 Jun 2021 23:51:35 +0900 |
| parents | 2aba74f9708d |
| children | cb36711e8b06 |
| files | automaton-in-agda/src/gcd.agda |
| diffstat | 1 files changed, 33 insertions(+), 29 deletions(-) [+] |
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda Sun Jun 20 23:25:01 2021 +0900 +++ b/automaton-in-agda/src/gcd.agda Sun Jun 20 23:51:35 2021 +0900 @@ -259,48 +259,52 @@ Fsym {0} {suc j} = refl Fsym {suc i} {0} = refl Fsym {suc i} {suc j} with <-cmp i j | <-cmp j i - ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = {!!} - ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = {!!} + ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim (nat-<> a a₁) + ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (¬b (sym b)) ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl - ... | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = {!!} + ... | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = ⊥-elim (¬b refl) ... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl - ... | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = {!!} + ... | 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₁ b ¬c = {!!} - ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = {!!} - F< : {i j k : ℕ } → 0 < i → i < j → j < k → F ⟪ i , j ⟫ < F ⟪ i , k ⟫ - F< = {!!} + ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (¬b (sym b)) + ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (nat-<> c c₁) record Fdec ( i j : ℕ ) : Set where field ni : ℕ nj : ℕ fdec : 0 < F ⟪ i , j ⟫ → F ⟪ ni , nj ⟫ < F ⟪ i , j ⟫ + fd1 : ( i j k : ℕ ) → i < j → k ≡ j - i → F ⟪ suc i , k ⟫ < F ⟪ suc i , suc j ⟫ + fd1 i j 0 i<j eq = ⊥-elim ( nat-≡< eq (minus>0 {i} {j} i<j )) + fd1 i j (suc k) i<j eq = fd2 i j k i<j eq where + fd2 : ( i j k : ℕ ) → i < j → suc k ≡ j - i → F ⟪ suc i , suc k ⟫ < F ⟪ suc i , suc j ⟫ + fd2 i j k i<j eq with <-cmp i k | <-cmp i j + ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = fd3 where + fd3 : suc k < suc j -- suc j - suc i < suc j + fd3 = subst (λ g → g < suc j) (sym eq) (y-x<y {suc i} {suc j} (s≤s z≤n) (s≤s z≤n)) + ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (⊥-elim (¬a i<j)) + ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = ⊥-elim (⊥-elim (¬a i<j)) + ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = s≤s z≤n + ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = ⊥-elim (¬a₁ i<j) + ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = s≤s z≤n -- i > j + ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = fd4 where + fd4 : suc i < suc j + fd4 = s≤s a + ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (¬a₁ i<j) + ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (¬a₁ i<j) fedc0 : (i j : ℕ ) → Fdec i j fedc0 0 0 = record { ni = 0 ; nj = 0 ; fdec = λ () } fedc0 (suc i) 0 = record { ni = suc i ; nj = 0 ; fdec = λ () } fedc0 0 (suc j) = record { ni = 0 ; nj = suc j ; fdec = λ () } fedc0 (suc i) (suc j) with <-cmp i j - ... | tri< a ¬b ¬c = record { ni = suc i ; nj = j - i ; fdec = λ lt → fd1 (j - i) refl } where - fd1 : ( k : ℕ ) → k ≡ j - i → F ⟪ suc i , k ⟫ < F ⟪ suc i , suc j ⟫ - fd1 0 eq = {!!} - fd1 (suc k) eq = fd2 i j k a eq where - fd2 : ( i j k : ℕ ) → i < j → suc k ≡ j - i → F ⟪ suc i , suc k ⟫ < F ⟪ suc i , suc j ⟫ - fd2 i j k i<j eq with <-cmp i k | <-cmp i j - ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = fd3 where - fd3 : suc k < suc j - fd3 = {!!} - ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim {!!} -- i ≡ j - ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = ⊥-elim {!!} - ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = s≤s z≤n - ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = ⊥-elim {!!} -- i ≡ j - ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = s≤s z≤n -- i > j - ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = fd4 where - fd4 : suc i < suc j - fd4 = s≤s a - ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim {!!} - ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim {!!} - ... | tri≈ ¬a refl ¬c = record { ni = suc i ; nj = suc j ; fdec = λ eq → {!!} } - ... | tri> ¬a ¬b c = record { ni = i - j ; nj = suc j ; fdec = λ lt → {!!} } where + ... | tri< i<j ¬b ¬c = record { ni = suc i ; nj = j - i ; fdec = λ lt → fd1 i j (j - i) i<j refl } + ... | tri≈ ¬a refl ¬c = record { ni = suc i ; nj = suc j ; fdec = λ lt → ⊥-elim (nat-≡< fd0 lt) } where + fd0 : {i : ℕ } → 0 ≡ F ⟪ suc i , suc i ⟫ + fd0 {i} with <-cmp i i + ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl ) + ... | tri≈ ¬a b ¬c = refl + ... | tri> ¬a ¬b c = ⊥-elim ( ¬b refl ) + ... | tri> ¬a ¬b c = record { ni = i - j ; nj = suc j ; fdec = λ lt → + subst₂ (λ s t → s < t) (Fsym {suc j} {i - j}) (Fsym {suc j} {suc i}) (fd1 j i (i - j) c refl ) } ind : ( i j : ℕ ) → Dividable (gcd (Fdec.ni (fedc0 i j)) (Fdec.nj (fedc0 i j))) (Fdec.ni (fedc0 i j)) ∧ Dividable (gcd (Fdec.ni (fedc0 i j)) (Fdec.nj (fedc0 i j))) (Fdec.nj (fedc0 i j))