Mercurial > hg > Members > kono > Proof > automaton
changeset 232:9011d76a67fb
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 25 Jun 2021 09:20:32 +0900 |
parents | 54977cc189e6 |
children | 327094b57ee2 |
files | automaton-in-agda/src/gcd.agda |
diffstat | 1 files changed, 23 insertions(+), 19 deletions(-) [+] |
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda Fri Jun 25 08:49:12 2021 +0900 +++ b/automaton-in-agda/src/gcd.agda Fri Jun 25 09:20:32 2021 +0900 @@ -466,25 +466,29 @@ ; ind = λ {p} prev → ind (proj1 p ) ( proj2 p ) prev } --- gcd-equlid : ( i i0 j j0 b0 : ℕ ) --- Dividable i0 (j0 + i - j ) ∨ Dividable j0 (i0 + j - i) --- (x0 < j0 → gcd x0 j0 ≡ 1) → gcd (i0 * b0) j0 ≡ j0 → gcd1 i i0 j j0 ≡ 1 → gcd b0 j0 ≡ j0 --- gcd-equlid zero i0 zero j0 a a0 b b0 ab ab0 x0 x0<j0 gxj=1 a*b gabj ga1 with <-cmp i0 j0 --- ... | tri< a' ¬b ¬c = {!!} --- ... | tri≈ ¬a refl ¬c = {!!} --- ... | tri> ¬a ¬b c = {!!} --- gcd-equlid zero i0 (suc zero) j0 a a0 b b0 ab ab0 x0 x0<j0 gxj=1 a*b gabj ga1 = {!!} --- gcd-equlid zero zero (suc (suc j)) j0 a a0 b b0 ab ab0 x0 x0<j0 gxj=1 a*b gabj ga1 = {!!} --- gcd-equlid zero (suc i0) (suc (suc j)) j0 a a0 b b0 ab ab0 x0 x0<j0 gxj=1 a*b gabj ga1 = {!!} --- gcd-equlid i0 (suc i0) (suc j) (suc (suc j)) {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} --- gcd-equlid (suc zero) i0 zero j0 = {!!} --- gcd-equlid (suc (suc i)) i0 zero zero a a0 b b0 ab ab0 x0 x0<j0 gxj=1 a*b gabj ga1 = {!!} --- gcd-equlid (suc (suc i)) i0 zero (suc j0) a a0 b b0 ab ab0 x0 x0<j0 gxj=1 a*b gabj ga1 = --- gcd-equlid (suc i) (suc (suc i)) j0 (suc j0) {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} --- gcd-equlid (suc zero) i0 (suc j) j0 a a0 b b0 ab ab0 x0 x0<j0 gxj=1 a*b gabj ga1 = --- gcd-equlid zero i0 j j0 {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} --- gcd-equlid (suc (suc i)) i0 (suc j) j0 a a0 b b0 ab ab0 x0 x0<j0 gxj=1 a*b gabj ga1 = --- gcd-equlid (suc i) i0 j j0 {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} +-- record Equlid (i j gcd : ℕ ) : Set where +-- field +-- eqa : ℕ +-- eqb : ℕ +-- gcd-equ : ((eqa * i) - (eqb * j) ≡ gcd ) ∨ ((eqb * j) - (eqa * i) ≡ gcd ) +-- +-- gcd-equlid1 : ( i i0 j j0 : ℕ ) → Equlid i0 j0 (gcd1 i i0 j j0) +-- gcd-equlid1 zero i0 zero j0 with <-cmp i0 j0 +-- ... | tri< a' ¬b ¬c = record { eqa = 1 ; eqb = 0 ; gcd-equ = case1 {!!} } +-- ... | tri≈ ¬a refl ¬c = record { eqa = 1 ; eqb = 0 ; gcd-equ = case1 {!!} } +-- ... | tri> ¬a ¬b c = record { eqa = 0 ; eqb = 1 ; gcd-equ = case2 {!!} } +-- gcd-equlid1 zero i0 (suc zero) j0 = record { eqa = 1 ; eqb = 1 ; gcd-equ = case1 {!!} } +-- gcd-equlid1 zero zero (suc (suc j)) j0 = record { eqa = 0 ; eqb = 1 ; gcd-equ = case2 {!!} } +-- gcd-equlid1 zero (suc i0) (suc (suc j)) j0 with gcd-equlid1 i0 (suc i0) (suc j) (suc (suc j)) +-- ... | e = record { eqa = Equlid.eqb e ; eqb = Equlid.eqa e ; gcd-equ = {!!} } +-- gcd-equlid1 (suc zero) i0 zero j0 = {!!} +-- gcd-equlid1 (suc (suc i)) i0 zero zero = {!!} +-- gcd-equlid1 (suc (suc i)) i0 zero (suc j0) with gcd-equlid1 (suc i) (suc (suc i)) j0 (suc j0) +-- ... | e = {!!} +-- gcd-equlid1 (suc zero) i0 (suc j) j0 = +-- gcd-equlid1 zero i0 j j0 +-- gcd-equlid1 (suc (suc i)) i0 (suc j) j0 = +-- gcd-equlid1 (suc i) i0 j j0 gcdmul+1 : ( m n : ℕ ) → gcd (m * n + 1) n ≡ 1