Mercurial > hg > Members > kono > Proof > automaton
changeset 321:b065ba2f68c5
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 14 Jan 2022 19:11:12 +0900 |
| parents | 4a00e5f2b793 |
| children | 596913103389 |
| files | automaton-in-agda/src/gcd.agda automaton-in-agda/src/nat.agda automaton-in-agda/src/root2.agda |
| diffstat | 3 files changed, 147 insertions(+), 73 deletions(-) [+] |
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda Fri Jan 14 14:39:36 2022 +0900 +++ b/automaton-in-agda/src/gcd.agda Fri Jan 14 19:11:12 2022 +0900 @@ -700,3 +700,75 @@ gcd-is-gratest {i} {j} {k} i>0 j>0 k>1 ki kj = div→k≤m k>1 (gcd>0 i j i>0 j>0 ) gcd001 where gcd001 : Dividable k ( gcd i j ) gcd001 = gcd-div _ _ _ k>1 ki kj + +gcd-div-1 : {i j : ℕ } → i > 0 → j > 0 → gcd (Dividable.factor (proj1 (gcd-dividable i j))) (Dividable.factor (proj2 (gcd-dividable i j))) ≡ 1 +gcd-div-1 {suc i} {suc j} i>0 j>0 = cop where + d : ℕ + d = gcd (suc i) (suc j) + d>0 : gcd (suc i) (suc j) > 0 + d>0 = gcd>0 (suc i) (suc j) (s≤s z≤n ) (s≤s z≤n ) + id : Dividable d (suc i) + id = proj1 (gcd-dividable (suc i) (suc j)) + jd : Dividable d (suc j) + jd = proj2 (gcd-dividable (suc i) (suc j)) + cop : gcd (Dividable.factor id) (Dividable.factor jd) ≡ 1 + cop with (gcd (Dividable.factor id) (Dividable.factor jd)) | inspect (gcd (Dividable.factor id)) (Dividable.factor jd) + ... | zero | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym eq1) (gcd>0 (Dividable.factor id) (Dividable.factor jd) + (0<factor d>0 (s≤s z≤n) id) (0<factor d>0 (s≤s z≤n) jd) )) + ... | suc zero | record { eq = eq1 } = refl + ... | suc (suc t) | record { eq = eq1 } = ⊥-elim ( nat-≤> (gcd-is-gratest {suc i} {(suc j)} (s≤s z≤n) (s≤s z≤n) co1 d1id d1jd ) gcd<d1 ) where + -- gcd-is-gratest : { i j k : ℕ } → i > 0 → j > 0 → k > 1 → Dividable k i → Dividable k j → k ≤ gcd i j + d1 : ℕ + d1 = gcd (Dividable.factor id) (Dividable.factor jd) + d1>1 : gcd (Dividable.factor id) (Dividable.factor jd) > 1 + d1>1 = subst (λ k → 1 < k ) (sym eq1) (s≤s (s≤s z≤n)) + mul1 : {x : ℕ} → 1 * x ≡ x + mul1 {zero} = refl + mul1 {suc x} = begin + 1 * suc x ≡⟨ cong suc (+-comm x _ ) ⟩ + suc x ∎ where open ≡-Reasoning + co1 : gcd (suc i) (suc j) * d1 > 1 + co1 = begin + 2 ≤⟨ d1>1 ⟩ + d1 ≡⟨ sym mul1 ⟩ + 1 * d1 ≤⟨ *≤ {1} {gcd (suc i) (suc j) } {d1} d>0 ⟩ + gcd (suc i) (suc j) * d1 ∎ where open ≤-Reasoning + gcdd1 = gcd-dividable (Dividable.factor id) (Dividable.factor jd) + gcdf1 = Dividable.factor (proj1 gcdd1) + gcdf2 = Dividable.factor (proj2 gcdd1) + d1id : Dividable (gcd (suc i) (suc j) * d1) (suc i) + d1id = record { factor = gcdf1 ; is-factor = begin + gcdf1 * (d * d1) + 0 ≡⟨ +-comm _ 0 ⟩ + gcdf1 * (d * d1) ≡⟨ cong (λ k1 → gcdf1 * k1) (*-comm d d1) ⟩ + gcdf1 * (d1 * d) ≡⟨ sym (*-assoc gcdf1 d1 d) ⟩ + gcdf1 * d1 * d ≡⟨ sym ( +-comm _ 0) ⟩ + (gcdf1 * d1) * d + 0 ≡⟨ cong (λ k1 → k1 * d + 0 ) (sym (+-comm (gcdf1 * d1) 0)) ⟩ + (gcdf1 * d1 + 0 ) * d + 0 ≡⟨ cong (λ k1 → k1 * d + 0 ) ( Dividable.is-factor (proj1 gcdd1) ) ⟩ + Dividable.factor id * d + 0 ≡⟨ Dividable.is-factor id ⟩ + suc i ∎ } where open ≡-Reasoning + d1jd : Dividable (gcd (suc i) (suc j) * d1) (suc j) + d1jd = record { factor = gcdf2 ; is-factor = begin + gcdf2 * (d * d1) + 0 ≡⟨ +-comm _ 0 ⟩ + gcdf2 * (d * d1) ≡⟨ cong (λ k1 → gcdf2 * k1) (*-comm d d1) ⟩ + gcdf2 * (d1 * d) ≡⟨ sym (*-assoc gcdf2 d1 d) ⟩ + gcdf2 * d1 * d ≡⟨ sym ( +-comm _ 0) ⟩ + (gcdf2 * d1) * d + 0 ≡⟨ cong (λ k1 → k1 * d + 0 ) (sym (+-comm (gcdf2 * d1) 0)) ⟩ + (gcdf2 * d1 + 0 ) * d + 0 ≡⟨ cong (λ k1 → k1 * d + 0 ) ( Dividable.is-factor (proj2 gcdd1) ) ⟩ + Dividable.factor jd * d + 0 ≡⟨ Dividable.is-factor jd ⟩ + (suc j) ∎ } where open ≡-Reasoning + mul2 : {g d1 : ℕ } → g > 0 → d1 > 1 → g < g * d1 + mul2 {suc g} {suc zero} g>0 (s≤s ()) + mul2 {suc g} {suc (suc d2)} g>0 d1>1 = begin + suc (suc g) ≡⟨ cong suc (+-comm 0 _ ) ⟩ + suc (suc g + 0) ≤⟨ s≤s (≤-plus-0 z≤n) ⟩ + suc (suc g + (g + d2 * suc g)) ≡⟨ cong suc (sym (+-assoc 1 g _) ) ⟩ + suc ((1 + g) + (g + d2 * suc g)) ≡⟨ cong (λ k → suc (k + (g + d2 * suc g) )) (+-comm 1 g) ⟩ + suc ((g + 1) + (g + d2 * suc g)) ≡⟨ cong suc (+-assoc g 1 _ ) ⟩ + suc (g + (1 + (g + d2 * suc g))) ≡⟨⟩ + suc (g + suc (g + d2 * suc g)) ≡⟨⟩ + suc (suc d2) * suc g ≡⟨ *-comm (suc (suc d2)) _ ⟩ + suc g * suc (suc d2) ∎ where open ≤-Reasoning + gcd<d1 : gcd (suc i) (suc j) < gcd (suc i ) (suc j) * d1 + gcd<d1 = mul2 (gcd>0 (suc i) (suc j) (s≤s z≤n) (s≤s z≤n) ) d1>1 + +
--- a/automaton-in-agda/src/nat.agda Fri Jan 14 14:39:36 2022 +0900 +++ b/automaton-in-agda/src/nat.agda Fri Jan 14 19:11:12 2022 +0900 @@ -182,6 +182,9 @@ *< {zero} {suc y} lt = s≤s z≤n *< {suc x} {suc y} (s≤s lt) = <-plus-0 (*< lt) +*-cancel-left : {x y z : ℕ } → x > 0 → x * y ≡ x * z → y ≡ z +*-cancel-left {suc x} {y} {z} x>0 eq = *-cancelˡ-≡ x eq + <to<s : {x y : ℕ } → x < y → x < suc y <to<s {zero} {suc y} (s≤s lt) = s≤s z≤n <to<s {suc x} {suc y} (s≤s lt) = s≤s (<to<s {x} {y} lt)
--- a/automaton-in-agda/src/root2.agda Fri Jan 14 14:39:36 2022 +0900 +++ b/automaton-in-agda/src/root2.agda Fri Jan 14 19:11:12 2022 +0900 @@ -98,90 +98,89 @@ mkRational : ( i j : ℕ ) → 0 < j → Rational mkRational zero j 0<j = record { i = 0 ; j = 1 ; coprime = refl ; 0<j = s≤s z≤n } -mkRational (suc i) j (s≤s 0<j) = record { i = Dividable.factor id ; j = Dividable.factor jd ; coprime = cop ; 0<j = 0<fj } where +mkRational (suc i) (suc j) (s≤s 0<j) = record { i = Dividable.factor id ; j = Dividable.factor jd ; coprime = cop ; 0<j = 0<fj } where d : ℕ - d = gcd (suc i) j - d>0 : gcd (suc i) j > 0 - d>0 = GCD.gcd>0 (suc i) j (s≤s z≤n) (s≤s z≤n ) + d = gcd (suc i) (suc j) + d>0 : gcd (suc i) (suc j) > 0 + d>0 = GCD.gcd>0 (suc i) (suc j) (s≤s z≤n) (s≤s z≤n ) + id : Dividable d (suc i) + id = proj1 (GCD.gcd-dividable (suc i) (suc j)) + jd : Dividable d (suc j) + jd = proj2 (GCD.gcd-dividable (suc i) (suc j)) 0<fj : Dividable.factor jd > 0 0<fj = 0<factor d>0 (s≤s z≤n ) jd - id : Dividable d (suc i) - id = proj1 (GCD.gcd-dividable (suc i) j) - jd : Dividable d j - jd = proj2 (GCD.gcd-dividable (suc i) j) cop : gcd (Dividable.factor id) (Dividable.factor jd) ≡ 1 - cop with (gcd (Dividable.factor id) (Dividable.factor jd)) | inspect (gcd (Dividable.factor id)) (Dividable.factor jd) - ... | zero | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym eq1) (GCD.gcd>0 (Dividable.factor id) (Dividable.factor jd) - (0<factor d>0 (s≤s z≤n) id) (0<factor d>0 (s≤s z≤n) jd) )) - ... | suc zero | record { eq = eq1 } = refl - ... | suc (suc t) | record { eq = eq1 } = ⊥-elim ( nat-≤> (GCD.gcd-is-gratest {suc i} {j} (s≤s z≤n) (s≤s z≤n) co1 d1id d1jd ) gcd<d1 ) where - -- gcd-is-gratest : { i j k : ℕ } → i > 0 → j > 0 → k > 1 → Dividable k i → Dividable k j → k ≤ gcd i j - d1 : ℕ - d1 = gcd (Dividable.factor id) (Dividable.factor jd) - d1>1 : gcd (Dividable.factor id) (Dividable.factor jd) > 1 - d1>1 = subst (λ k → 1 < k ) (sym eq1) (s≤s (s≤s z≤n)) - mul1 : {x : ℕ} → 1 * x ≡ x - mul1 {zero} = refl - mul1 {suc x} = begin - 1 * suc x ≡⟨ cong suc (+-comm x _ ) ⟩ - suc x ∎ where open ≡-Reasoning - co1 : gcd (suc i) j * d1 > 1 - co1 = begin - 2 ≤⟨ d1>1 ⟩ - d1 ≡⟨ sym mul1 ⟩ - 1 * d1 ≤⟨ *≤ {1} {gcd (suc i) j } {d1} d>0 ⟩ - gcd (suc i) j * d1 ∎ where open ≤-Reasoning - gcdd1 = GCD.gcd-dividable (Dividable.factor id) (Dividable.factor jd) - gcdf1 = Dividable.factor (proj1 gcdd1) - gcdf2 = Dividable.factor (proj2 gcdd1) - d1id : Dividable (gcd (suc i) j * d1) (suc i) - d1id = record { factor = gcdf1 ; is-factor = begin - gcdf1 * (d * d1) + 0 ≡⟨ +-comm _ 0 ⟩ - gcdf1 * (d * d1) ≡⟨ cong (λ k1 → gcdf1 * k1) (*-comm d d1) ⟩ - gcdf1 * (d1 * d) ≡⟨ sym (*-assoc gcdf1 d1 d) ⟩ - gcdf1 * d1 * d ≡⟨ sym ( +-comm _ 0) ⟩ - (gcdf1 * d1) * d + 0 ≡⟨ cong (λ k1 → k1 * d + 0 ) (sym (+-comm (gcdf1 * d1) 0)) ⟩ - (gcdf1 * d1 + 0 ) * d + 0 ≡⟨ cong (λ k1 → k1 * d + 0 ) ( Dividable.is-factor (proj1 gcdd1) ) ⟩ - Dividable.factor id * d + 0 ≡⟨ Dividable.is-factor id ⟩ - suc i ∎ } where open ≡-Reasoning - d1jd : Dividable (gcd (suc i) j * d1) j - d1jd = record { factor = gcdf2 ; is-factor = begin - gcdf2 * (d * d1) + 0 ≡⟨ +-comm _ 0 ⟩ - gcdf2 * (d * d1) ≡⟨ cong (λ k1 → gcdf2 * k1) (*-comm d d1) ⟩ - gcdf2 * (d1 * d) ≡⟨ sym (*-assoc gcdf2 d1 d) ⟩ - gcdf2 * d1 * d ≡⟨ sym ( +-comm _ 0) ⟩ - (gcdf2 * d1) * d + 0 ≡⟨ cong (λ k1 → k1 * d + 0 ) (sym (+-comm (gcdf2 * d1) 0)) ⟩ - (gcdf2 * d1 + 0 ) * d + 0 ≡⟨ cong (λ k1 → k1 * d + 0 ) ( Dividable.is-factor (proj2 gcdd1) ) ⟩ - Dividable.factor jd * d + 0 ≡⟨ Dividable.is-factor jd ⟩ - j ∎ } where open ≡-Reasoning - mul2 : {g d1 : ℕ } → g > 0 → d1 > 1 → g < g * d1 - mul2 {suc g} {suc zero} g>0 (s≤s ()) - mul2 {suc g} {suc (suc d2)} g>0 d1>1 = begin - suc (suc g) ≡⟨ cong suc (+-comm 0 _ ) ⟩ - suc (suc g + 0) ≤⟨ s≤s (≤-plus-0 z≤n) ⟩ - suc (suc g + (g + d2 * suc g)) ≡⟨ cong suc (sym (+-assoc 1 g _) ) ⟩ - suc ((1 + g) + (g + d2 * suc g)) ≡⟨ cong (λ k → suc (k + (g + d2 * suc g) )) (+-comm 1 g) ⟩ - suc ((g + 1) + (g + d2 * suc g)) ≡⟨ cong suc (+-assoc g 1 _ ) ⟩ - suc (g + (1 + (g + d2 * suc g))) ≡⟨⟩ - suc (g + suc (g + d2 * suc g)) ≡⟨⟩ - suc (suc d2) * suc g ≡⟨ *-comm (suc (suc d2)) _ ⟩ - suc g * suc (suc d2) ∎ where open ≤-Reasoning - gcd<d1 : gcd (suc i) j < gcd (suc i ) j * d1 - gcd<d1 = mul2 (GCD.gcd>0 (suc i) j (s≤s z≤n) (s≤s z≤n) ) d1>1 + cop = GCD.gcd-div-1 {suc i} {suc j} (s≤s z≤n) (s≤s z≤n ) - -Rational* : (r s : Rational) → Rational -Rational* r s = mkRational (Rational.i r * Rational.i s) (Rational.j r * Rational.j s) (r1 (Rational.0<j r) (Rational.0<j s) ) where - r1 : {x y : ℕ} → x > 0 → y > 0 → x * y > 0 - r1 {x} {y} x>0 y>0 = begin +r1 : {x y : ℕ} → x > 0 → y > 0 → x * y > 0 +r1 {x} {y} x>0 y>0 = begin 1 * 1 ≤⟨ *≤ {1} {x} {1} x>0 ⟩ x * 1 ≡⟨ *-comm x 1 ⟩ 1 * x ≤⟨ *≤ {1} {y} {x} y>0 ⟩ y * x ≡⟨ *-comm y x ⟩ x * y ∎ where open ≤-Reasoning +Rational* : (r s : Rational) → Rational +Rational* r s = mkRational (Rational.i r * Rational.i s) (Rational.j r * Rational.j s) (r1 (Rational.0<j r) (Rational.0<j s) ) + _r=_ : Rational → ℕ → Set -r r= n = (Rational.i r ≡ n) ∧ (Rational.j r ≡ 1) +r r= p = p * Rational.j r ≡ Rational.i r + +r3 : ( p : ℕ ) → p > 0 → ( r : Rational ) → Rational* r r r= p → p * Rational.j r * Rational.j r ≡ Rational.i r * Rational.i r +r3 p p>0 r rr = r4 where + i : ℕ + i = Rational.i r * Rational.i r + j : ℕ + j = Rational.j r * Rational.j r + 0<j : 0 < j + 0<j = r1 (Rational.0<j r) (Rational.0<j r) + d1 = Dividable.factor (proj1 (GCD.gcd-dividable i j)) + d2 = Dividable.factor (proj2 (GCD.gcd-dividable i j)) + ri=id : ( i j : ℕ) → (0<i : 0 < i ) → (0<j : 0 < j) + → Rational.i (mkRational i j 0<j) ≡ Dividable.factor (proj1 (GCD.gcd-dividable i j)) + ri=id (suc i₁) (suc j₁) 0<i (s≤s 0<j₁) = refl + ri=jd : ( i j : ℕ) → (0<i : 0 < i ) → (0<j : 0 < j) + → Rational.j (mkRational i j 0<j) ≡ Dividable.factor (proj2 (GCD.gcd-dividable i j)) + ri=jd (suc i₁) (suc j₁) 0<i (s≤s 0<j₁) = refl + d : ℕ + d = gcd i j + r7 : i > 0 → d > 0 + r7 0<i = GCD.gcd>0 _ _ 0<i 0<j + r6 : i > 0 → d2 > 0 + r6 0<i = 0<factor (r7 0<i ) 0<j (proj2 (GCD.gcd-dividable i j)) + r8 : 0 < i → d2 * p ≡ d1 + r8 0<i = begin + d2 * p ≡⟨ *-comm d2 p ⟩ + p * d2 ≡⟨ cong (λ k → p * k ) (sym (ri=jd i j 0<i 0<j )) ⟩ + p * Rational.j (mkRational i j _ ) ≡⟨ rr ⟩ + Rational.i (Rational* r r) ≡⟨ ri=id i j 0<i 0<j ⟩ + d1 ∎ where open ≡-Reasoning + r4 : p * Rational.j r * Rational.j r ≡ Rational.i r * Rational.i r + r4 with <-cmp (Rational.i r * Rational.i r) 0 + ... | tri≈ ¬a b ¬c = {!!} + ... | tri> ¬a ¬b c = begin + p * Rational.j r * Rational.j r ≡⟨ *-cancel-left (r6 c) ( begin + d2 * (p * Rational.j r * Rational.j r) ≡⟨ {!!} ⟩ + (d2 * p) * Rational.j r * Rational.j r ≡⟨ cong (λ k → k * Rational.j r * Rational.j r) (r8 c) ⟩ + d1 * Rational.j r * Rational.j r ≡⟨ *-cancel-left (r7 c) ( begin + d * (d1 * Rational.j r * Rational.j r) ≡⟨ {!!} ⟩ + d * d1 * Rational.j r * Rational.j r ≡⟨ {!!} ⟩ + (d1 * d + 0) * j ≡⟨ cong (λ k → k * j ) (Dividable.is-factor (proj1 (GCD.gcd-dividable i j)) ) ⟩ + i * j ≡⟨ *-comm i j ⟩ + j * i ≡⟨ cong (λ k → k * i ) (sym (Dividable.is-factor (proj2 (GCD.gcd-dividable i j))) ) ⟩ + (d2 * GCD.gcd i j + 0) * i ≡⟨ {!!} ⟩ + d * (d2 * (Rational.i r * Rational.i r)) ∎ ) ⟩ + d2 * (Rational.i r * Rational.i r) ∎ ) ⟩ + Rational.i r * Rational.i r ∎ where open ≡-Reasoning + + root-prime-irrational1 : ( p : ℕ ) → Prime p → ( r : Rational ) → ¬ ( Rational* r r r= p ) -root-prime-irrational1 p pr r div = root-prime-irrational (Rational.i r) (Rational.j r) {!!} {!!} pr {!!} {!!} (Rational.coprime r) +root-prime-irrational1 p pr r div with <-cmp (Rational.j r) 1 +... | tri< a ¬b ¬c = ⊥-elim (nat-≤> (Rational.0<j r) a ) +... | tri≈ ¬a b ¬c = {!!} +... | tri> ¬a ¬b c with <-cmp (Rational.i r) 1 +... | tri< a ¬b₁ ¬c = {!!} +... | tri≈ ¬a₁ b ¬c = {!!} +... | tri> ¬a₁ ¬b₁ c₁ = root-prime-irrational (Rational.j r) (Rational.i r) p c pr c₁ (r3 p (<-trans a<sa (Prime.p>1 pr ) ) r div) + (trans (GCD.gcdsym {Rational.j r} {_} ) (Rational.coprime r) )