Mercurial > hg > Members > kono > Proof > automaton
changeset 198:4b452c9d7e7b
gcd done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 17 Jun 2021 17:16:36 +0900 |
| parents | daeae196aa50 |
| children | 4a83abf7b822 |
| files | automaton-in-agda/src/gcd.agda automaton-in-agda/src/nat.agda automaton-in-agda/src/root2.agda |
| diffstat | 3 files changed, 46 insertions(+), 75 deletions(-) [+] |
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda Thu Jun 17 16:00:58 2021 +0900 +++ b/automaton-in-agda/src/gcd.agda Thu Jun 17 17:16:36 2021 +0900 @@ -62,41 +62,9 @@ (k + f * suc k) + zero ≡⟨ cong pred fa ⟩ n ∎ ) } where open ≡-Reasoning -decf-eq : {i k : ℕ } → k > 1 → (if : Factor k (suc i)) - → (div : Dividable k (suc i - remain if)) → factor if ≡ Dividable.factor div -decf-eq {i} {suc k} k>1 if div = if1 where - if0 : suc (suc i) > remain if - if0 = begin - suc (remain if) ≤⟨ s≤s (m≤n+m _ (factor if * suc k)) ⟩ - suc (factor if * suc k + remain if) ≡⟨ cong suc ( is-factor if) ⟩ - suc (suc i) ∎ where open ≤-Reasoning - if1 : factor if ≡ Dividable.factor div - if1 = begin - factor if ≡⟨ *-cancelʳ-≡ _ _ {k} ( +-cancelʳ-≡ _ _ ( begin - factor if * suc k + remain if ≡⟨ is-factor if ⟩ - suc i ≡⟨ sym (minus+n {suc i} {remain if} if0) ⟩ - (suc i - remain if) + remain if ≡⟨ cong (λ g → g + remain if) (sym (Dividable.is-factor div )) ⟩ - (Dividable.factor div * suc k + 0) + remain if ≡⟨ cong (λ g → g + remain if) (+-comm _ 0) ⟩ - Dividable.factor div * suc k + remain if ∎ )) ⟩ Dividable.factor div ∎ where open ≡-Reasoning - div0 : {k : ℕ} → Dividable k 0 div0 {k} = record { factor = 0; is-factor = refl } -ifk0 : ( i0 k : ℕ ) → (i0f : Factor k i0 ) → ( i0=0 : remain i0f ≡ 0 ) → factor i0f * k + 0 ≡ i0 -ifk0 i0 k i0f i0=0 = begin - factor i0f * k + 0 ≡⟨ cong (λ m → factor i0f * k + m) (sym i0=0) ⟩ - factor i0f * k + remain i0f ≡⟨ is-factor i0f ⟩ - i0 ∎ - where open ≡-Reasoning - -ifzero : {k : ℕ } → (jf : Factor k zero ) → remain jf ≡ 0 -ifzero {k} record { factor = zero ; remain = zero ; is-factor = is-factor } = refl -ifzero {zero} record { factor = (suc factor₁) ; remain = zero ; is-factor = is-factor } = refl -ifzero {zero} record { factor = (suc f) ; remain = (suc r) ; is-factor = is-factor } = - ⊥-elim (nat-≡< (sym is-factor) (subst (λ k → zero < k ) (+-comm (suc r) _) if1 )) where - if1 : zero < suc r + suc f * zero - if1 = s≤s z≤n - gcd1 : ( i i0 j j0 : ℕ ) → ℕ gcd1 zero i0 zero j0 with <-cmp i0 j0 ... | tri< a ¬b ¬c = i0 @@ -126,30 +94,49 @@ div-div {i} {j} {suc k} k>1 di dj = div-div0 di dj where div-div1 : {i j : ℕ} → Dividable (suc k) i → Dividable (suc k) j → i < j → Dividable (suc k) (j - i) div-div1 {i} {j} record { factor = fi ; is-factor = fai } record { factor = fj ; is-factor = faj } i<j = - subst (λ g → Dividable (suc k) g ) div-div3 ( div-div2 fj fi {!!} ) where + subst (λ g → Dividable (suc k) g ) div-div3 ( div-div2 fj fi fi<fj ) where + fi<fj : fi < fj + fi<fj with <-cmp fi fj + ... | tri< a ¬b ¬c = a + ... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< (cong (λ g → g * suc k + 0) b) (begin + suc (fi * suc k + 0) ≡⟨ cong suc fai ⟩ + suc i ≤⟨ i<j ⟩ + j ≡⟨ sym faj ⟩ + fj * suc k + 0 ∎ )) where open ≤-Reasoning + ... | tri> ¬a ¬b c = ⊥-elim ( nat-<> (*-monoˡ-< k c ) (begin + suc (fi * suc k) ≡⟨ +-comm 0 _ ⟩ + suc (fi * suc k + 0) ≡⟨ cong suc fai ⟩ + suc i ≤⟨ i<j ⟩ + j ≡⟨ sym faj ⟩ + fj * suc k + 0 ≡⟨ +-comm _ 0 ⟩ + fj * suc k ∎ )) where open ≤-Reasoning div-div3 : (fj * suc k) - (fi * suc k) ≡ j - i div-div3 = begin (fj * suc k) - (fi * suc k) ≡⟨ cong₂ (λ g h → g - h) (+-comm 0 (fj * suc k)) (+-comm 0 (fi * suc k)) ⟩ (fj * suc k + 0) - (fi * suc k + 0) ≡⟨ cong₂ (λ g h → g - h) faj fai ⟩ j - i ∎ where open ≡-Reasoning - div-div2 : (fj fi : ℕ) → fi ≤ fj → Dividable (suc k) ((fj * suc k) - (fi * suc k)) - div-div2 zero fi i≤j = subst (λ g → Dividable (suc k) g) (begin + div-div2 : (fj fi : ℕ) → fi < fj → Dividable (suc k) ((fj * suc k) - (fi * suc k)) + div-div2 zero fi i<j = subst (λ g → Dividable (suc k) g) (begin 0 ≡⟨ sym (minus<=0 {0} {fi * suc k} z≤n ) ⟩ 0 - (fi * suc k) ≡⟨ refl ⟩ (zero * suc k) - (fi * suc k) ∎ ) div0 where open ≡-Reasoning - div-div2 (suc fj) zero i≤j = {!!} - div-div2 (suc fj) (suc fi) i≤j = record { factor = suc (Dividable.factor (div-div2 fj (suc fi) fi<fj )) ; is-factor = ( begin - suc (Dividable.factor (div-div2 fj (suc fi) fi<fj )) * suc k + 0 ≡⟨ +-comm _ 0 ⟩ - suc (Dividable.factor (div-div2 fj (suc fi) fi<fj )) * suc k ≡⟨ refl ⟩ - suc k + ((Dividable.factor (div-div2 fj (suc fi) fi<fj )) * suc k ) ≡⟨ cong (λ g → suc k + g ) (+-comm 0 _) ⟩ - suc k + ((Dividable.factor (div-div2 fj (suc fi) fi<fj )) * suc k + 0) - ≡⟨ cong (λ g → suc k + g) (Dividable.is-factor (div-div2 fj (suc fi) fi<fj) ) ⟩ - suc k + ((fj * suc k) - ((suc fi) * suc k)) ≡⟨ minus+yz {suc k} {fj * suc k} {(suc fi) * suc k} {!!} ⟩ - ( (suc k + (fj * suc k)) - ((suc fi) * suc k)) ≡⟨ refl ⟩ - ((suc fj * suc k) - ((suc fi) * suc k)) ∎ ) } where + div-div2 (suc fj) fi i<j with <-cmp fi fj + ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c i<j ) + ... | tri≈ ¬a refl ¬c = record { factor = 1 ; is-factor = (begin + 1 * suc k + 0 ≡⟨ +-comm _ 0 ⟩ + 1 * suc k ≡⟨ cong suc (+-comm _ 0) ⟩ + suc k ≡⟨ sym (minus+y-y {suc k} {fj * suc k}) ⟩ + (suc k + fj * suc k) - (fj * suc k) ≡⟨ refl ⟩ + (suc (k + fj * suc k)) - (fj * suc k) ∎ )} where open ≡-Reasoning + ... | tri< fi<fj ¬b ¬c = record { factor = suc (Dividable.factor (div-div2 fj fi fi<fj )) ; is-factor = ( begin + suc (Dividable.factor (div-div2 fj fi fi<fj )) * suc k + 0 ≡⟨ +-comm _ 0 ⟩ + suc (Dividable.factor (div-div2 fj fi fi<fj )) * suc k ≡⟨ refl ⟩ + suc k + ((Dividable.factor (div-div2 fj fi fi<fj )) * suc k ) ≡⟨ cong (λ g → suc k + g ) (+-comm 0 _) ⟩ + suc k + ((Dividable.factor (div-div2 fj fi fi<fj )) * suc k + 0) ≡⟨ cong (λ g → suc k + g) (Dividable.is-factor (div-div2 fj fi fi<fj) ) ⟩ + suc k + ((fj * suc k) - (fi * suc k)) ≡⟨ minus+yz {suc k} {fj * suc k} {fi * suc k} (<to≤ (*-monoˡ-< k fi<fj )) ⟩ + ( (suc k + (fj * suc k)) - (fi * suc k)) ≡⟨ refl ⟩ + ((suc fj * suc k) - (fi * suc k)) ∎ ) } where open ≡-Reasoning - fi<fj : suc fi ≤ fj - fi<fj = {!!} div-div0 : { i j : ℕ } → Dividable (suc k) i → Dividable (suc k) j → Dividable (suc k) (i - j) ∧ Dividable (suc k) (j - i) div-div0 {i} {j} di dj with <-cmp i j ... | tri< a ¬b ¬c = ⟪ subst (λ g → Dividable (suc k) g) (sym (minus<=0 {i} {j} (<to≤ a))) div0 , div-div1 di dj a ⟫ @@ -241,6 +228,7 @@ gcd205 : (j : ℕ) → gcd1 (suc j) (suc (suc i)) j (suc i) ≡ 1 gcd205 zero = refl gcd205 (suc j) = subst (λ k → k ≡ 1) (gcd22 (suc j) (suc (suc i)) j (suc i)) (gcd205 j) + gcd204 : (i : ℕ) → gcd1 1 1 i i ≡ 1 gcd204 zero = refl gcd204 (suc zero) = refl @@ -274,33 +262,6 @@ gcd1 1 1 (suc j) (suc j) ∎ where open ≡-Reasoning gcd200 (suc (suc i)) i0 (suc j) zero i=i0 () -gcd52 : {i : ℕ } → 1 < suc (suc i) -gcd52 {zero} = a<sa -gcd52 {suc i} = <-trans (gcd52 {i}) a<sa - -gcd50 : (i i0 j j0 : ℕ) → 1 < i0 → i ≤ i0 → j ≤ j0 → gcd1 i i0 j j0 ≤ i0 -gcd50 zero i0 zero j0 0<i i<i0 j<j0 with <-cmp i0 j0 -... | tri< a ¬b ¬c = ≤-refl -... | tri≈ ¬a refl ¬c = ≤-refl -... | tri> ¬a ¬b c = ≤-trans refl-≤s c -gcd50 zero (suc i0) (suc zero) j0 0<i i<i0 j<j0 = gcd51 0<i where - gcd51 : 1 < suc i0 → gcd1 zero (suc i0) 1 j0 ≤ suc i0 - gcd51 1<i = <to≤ 1<i -gcd50 zero (suc i0) (suc (suc j)) j0 0<i i<i0 j<j0 = gcd50 i0 (suc i0) (suc j) (suc (suc j)) 0<i refl-≤s refl-≤s -gcd50 (suc zero) i0 zero j0 0<i i<i0 j<j0 = <to≤ 0<i -gcd50 (suc (suc i)) i0 zero zero 0<i i<i0 j<j0 = ≤-refl -gcd50 (suc (suc i)) i0 zero (suc j0) 0<i i<i0 j<j0 = ≤-trans (gcd50 (suc i) (suc (suc i)) j0 (suc j0) gcd52 refl-≤s refl-≤s) i<i0 -gcd50 (suc i) i0 (suc j) j0 0<i i<i0 j<j0 = subst (λ k → k ≤ i0 ) (sym (gcd22 i i0 j j0)) - (gcd50 i i0 j j0 0<i (≤-trans refl-≤s i<i0) (≤-trans refl-≤s j<j0)) - -gcd5 : ( n k : ℕ ) → 1 < n → gcd n k ≤ n -gcd5 n k 0<n = gcd50 n n k k 0<n ≤-refl ≤-refl - -gcd6 : ( n k : ℕ ) → 1 < n → gcd k n ≤ n -gcd6 n k 1<n = subst (λ m → m ≤ n) (gcdsym {n} {k}) (gcd5 n k 1<n) - -gcd4 : ( n k : ℕ ) → 1 < n → gcd n k ≡ k → k ≤ n -gcd4 n k 1<n eq = subst (λ m → m ≤ n ) eq (gcd5 n k 1<n) gcdmul+1 : ( m n : ℕ ) → gcd (m * n + 1) n ≡ 1 gcdmul+1 zero n = gcd204 n
--- a/automaton-in-agda/src/nat.agda Thu Jun 17 16:00:58 2021 +0900 +++ b/automaton-in-agda/src/nat.agda Thu Jun 17 17:16:36 2021 +0900 @@ -144,6 +144,9 @@ x≤x+y {zero} {y} = z≤n x≤x+y {suc z} {y} = s≤s (x≤x+y {z} {y}) +x≤y+x : {z y : ℕ } → z ≤ y + z +x≤y+x {z} {y} = subst (λ k → z ≤ k ) (+-comm _ y ) x≤x+y + <-plus : {x y z : ℕ } → x < y → x + z < y + z <-plus {zero} {suc y} {z} (s≤s z≤n) = s≤s (subst (λ k → z ≤ k ) (+-comm z _ ) x≤x+y ) <-plus {suc x} {suc y} {z} (s≤s lt) = s≤s (<-plus {x} {y} {z} lt) @@ -218,6 +221,13 @@ minus>0 {zero} {suc _} (s≤s z≤n) = s≤s z≤n minus>0 {suc x} {suc y} (s≤s lt) = minus>0 {x} {y} lt +minus+y-y : {x y : ℕ } → (x + y) - y ≡ x +minus+y-y {zero} {y} = minus<=0 {zero + y} {y} ≤-refl +minus+y-y {suc x} {y} = begin + (suc x + y) - y ≡⟨ sym (minus+1 {_} {y} x≤y+x) ⟩ + suc ((x + y) - y) ≡⟨ cong suc (minus+y-y {x} {y}) ⟩ + suc x ∎ where open ≡-Reasoning + open import Relation.Binary.Definitions distr-minus-* : {x y z : ℕ } → (minus x y) * z ≡ minus (x * z) (y * z)
--- a/automaton-in-agda/src/root2.agda Thu Jun 17 16:00:58 2021 +0900 +++ b/automaton-in-agda/src/root2.agda Thu Jun 17 17:16:36 2021 +0900 @@ -58,7 +58,7 @@ -- → Dividable k ( gcd i j ) root2-irrational : ( n m : ℕ ) → n > 1 → m > 1 → 2 * n * n ≡ m * m → ¬ (gcd n m ≡ 1) -root2-irrational n m n>1 m>1 2nm = rot13 ( gcd-div n m 2 (s≤s (s≤s z≤n)) f2 fm (f3 n rot7) refl ) where +root2-irrational n m n>1 m>1 2nm = rot13 ( gcd-div n m 2 (s≤s (s≤s z≤n)) {!!} {!!} ) where rot13 : {m : ℕ } → Dividable 2 m → m ≡ 1 → ⊥ rot13 d refl with Dividable.factor d | Dividable.is-factor d ... | zero | ()