Mercurial > hg > Members > kono > Proof > automaton
changeset 185:f9473f83f6e7
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 14 Jun 2021 00:25:04 +0900 |
| parents | a810ae49187c |
| children | 08f4ec41ea93 |
| files | automaton-in-agda/src/gcd.agda automaton-in-agda/src/nat.agda automaton-in-agda/src/root2.agda |
| diffstat | 3 files changed, 39 insertions(+), 13 deletions(-) [+] |
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda Sun Jun 13 22:14:04 2021 +0900 +++ b/automaton-in-agda/src/gcd.agda Mon Jun 14 00:25:04 2021 +0900 @@ -27,9 +27,13 @@ open ≡-Reasoning decf : { n k : ℕ } → ( x : Factor k (suc n) ) → Factor k n -decf {n} {k} x with remain x -... | zero = record { factor = factor x ; remain = k ; is-factor = {!!} } -... | suc r = record { factor = factor x ; remain = r ; is-factor = {!!} } +decf {n} {k} x with remain x | inspect remain x +... | zero | record { eq = e } = record { factor = factor x ; remain = k ; is-factor = {!!} } where + d0 : factor x * k + remain x ≡ suc n + d0 = is-factor x + d1 : factor x * k + k ≡ n + d1 = {!!} +... | suc r | record { eq = e } = record { factor = factor x ; remain = r ; is-factor = {!!} } ifk0 : ( i0 k : ℕ ) → (i0f : Factor k i0 ) → ( i0=0 : remain i0f ≡ 0 ) → factor i0f * k + 0 ≡ i0 ifk0 i0 k i0f i0=0 = begin @@ -38,7 +42,12 @@ i0 ∎ ifzero : {k : ℕ } → (jf : Factor k zero ) → remain jf ≡ 0 -ifzero = {!!} +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 @@ -183,9 +192,9 @@ ... | 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 + 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 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))
--- a/automaton-in-agda/src/nat.agda Sun Jun 13 22:14:04 2021 +0900 +++ b/automaton-in-agda/src/nat.agda Mon Jun 14 00:25:04 2021 +0900 @@ -319,6 +319,9 @@ decline : {p : P} → f (pnext p) < f p ind : {p : P} → Q (pnext p) → Q p +y<sx→y≤x : {x y : ℕ} → y < suc x → y ≤ x +y<sx→y≤x (s≤s lt) = lt + f-induction : {n m : Level} {P : Set n } → {Q : P → Set m } → (f : P → ℕ) → Finduction P Q f @@ -330,11 +333,9 @@ fi0 .0 z≤n = refl f-induction0 p (suc x) le with <-cmp (f (Finduction.pnext I p)) (suc x) ... | tri< (s≤s a) ¬b ¬c = f-induction0 p x a - ... | tri≈ ¬a b ¬c = Finduction.ind I (f-induction0 (Finduction.pnext I p) x (f2 f1)) where + ... | tri≈ ¬a b ¬c = Finduction.ind I (f-induction0 (Finduction.pnext I p) x (y<sx→y≤x f1)) where f1 : f (Finduction.pnext I (Finduction.pnext I p)) < suc x f1 = subst (λ k → f (Finduction.pnext I (Finduction.pnext I p)) < k ) b ( Finduction.decline I {Finduction.pnext I p} ) - f2 : {x y : ℕ} → y < suc x → y ≤ x - f2 (s≤s lt) = lt ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> le c )
--- a/automaton-in-agda/src/root2.agda Sun Jun 13 22:14:04 2021 +0900 +++ b/automaton-in-agda/src/root2.agda Mon Jun 14 00:25:04 2021 +0900 @@ -53,10 +53,11 @@ open Factor 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-gt n n m m 2 f2 f2 f2 fm {!!} {!!} {!!} {!!}) where +root2-irrational n m n>1 m>1 2nm = rot13 ( gcd-gt n n m m 2 f2 f2 f2 fm (f3 n rot7) refl f4 f4) where rot13 : {m : ℕ } → Dividable 2 m → m ≡ 1 → ⊥ - rot13 d refl with Dividable.is-factor d - ... | t = {!!} + rot13 d refl with Dividable.factor d | Dividable.is-factor d + ... | zero | () + ... | suc n | () rot11 : {m : ℕ } → even m → Factor 2 m rot11 {zero} em = record { factor = 0 ; remain = 0 ; is-factor = refl } rot11 {suc zero} () @@ -95,6 +96,21 @@ rot7 = even^2 {n} (subst (λ k → even k) (sym rot3) ((n*even {Even.j E} {m} ( even^2 {m} ( rot1 ))))) f2 : Factor 2 n f2 = rot11 rot7 + f3 : ( n : ℕ) → (e : even n ) → remain (rot11 {n} e) ≡ 0 + f3 zero e = refl + f3 (suc (suc n)) e = f3 n e + f4 : {m : ℕ} → remain f2 + m ≡ m + f4 {m} = begin + remain f2 + m ≡⟨ cong (λ k → k + m) (f3 n rot7) ⟩ + 0 + m ≡⟨ refl ⟩ + m ∎ where open ≡-Reasoning fm : Factor 2 m - fm = record { factor = Even.j E ; remain = 0 ; is-factor = {!!} } + fm = record { factor = Even.j E ; remain = 0 ; is-factor = fm1 } where + fm1 : Even.j E * 2 + 0 ≡ m + fm1 = begin + Even.j E * 2 + 0 ≡⟨ +-comm _ 0 ⟩ + Even.j E * 2 ≡⟨ *-comm (Even.j E) 2 ⟩ + 2 * Even.j E ≡⟨ sym ( Even.is-twice E ) ⟩ + m ∎ where open ≡-Reasoning +