Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/gcd.agda @ 405:af8f630b7e60

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 24 Sep 2023 18:02:04 +0900
parents b065ba2f68c5
children
comparison
equal deleted inserted replaced
404:dfaf230f7b9a 405:af8f630b7e60
1 {-# OPTIONS --allow-unsolved-metas #-} 1 {-# OPTIONS --cubical-compatible --safe #-}
2
3 -- {-# OPTIONS --allow-unsolved-metas #-}
2 module gcd where 4 module gcd where
3 5
4 open import Data.Nat 6 open import Data.Nat
5 open import Data.Nat.Properties 7 open import Data.Nat.Properties
6 open import Data.Empty 8 open import Data.Empty
14 open Factor 16 open Factor
15 17
16 gcd1 : ( i i0 j j0 : ℕ ) → ℕ 18 gcd1 : ( i i0 j j0 : ℕ ) → ℕ
17 gcd1 zero i0 zero j0 with <-cmp i0 j0 19 gcd1 zero i0 zero j0 with <-cmp i0 j0
18 ... | tri< a ¬b ¬c = i0 20 ... | tri< a ¬b ¬c = i0
19 ... | tri≈ ¬a refl ¬c = i0 21 ... | tri≈ ¬a b ¬c = i0
20 ... | tri> ¬a ¬b c = j0 22 ... | tri> ¬a ¬b c = j0
21 gcd1 zero i0 (suc zero) j0 = 1 23 gcd1 zero i0 (suc zero) j0 = 1
22 gcd1 zero zero (suc (suc j)) j0 = j0 24 gcd1 zero zero (suc (suc j)) j0 = j0
23 gcd1 zero (suc i0) (suc (suc j)) j0 = gcd1 i0 (suc i0) (suc j) (suc (suc j)) 25 gcd1 zero (suc i0) (suc (suc j)) j0 = gcd1 i0 (suc i0) (suc j) (suc (suc j))
24 gcd1 (suc zero) i0 zero j0 = 1 26 gcd1 (suc zero) i0 zero j0 = 1
44 gcd22 (suc i) i0 (suc o) o0 = refl 46 gcd22 (suc i) i0 (suc o) o0 = refl
45 47
46 gcdmm : (n m : ℕ) → gcd1 n m n m ≡ m 48 gcdmm : (n m : ℕ) → gcd1 n m n m ≡ m
47 gcdmm zero m with <-cmp m m 49 gcdmm zero m with <-cmp m m
48 ... | tri< a ¬b ¬c = refl 50 ... | tri< a ¬b ¬c = refl
49 ... | tri≈ ¬a refl ¬c = refl 51 ... | tri≈ ¬a b ¬c = refl
50 ... | tri> ¬a ¬b c = refl 52 ... | tri> ¬a ¬b c = refl
51 gcdmm (suc n) m = subst (λ k → k ≡ m) (sym (gcd22 n m n m )) (gcdmm n m ) 53 gcdmm (suc n) m = subst (λ k → k ≡ m) (sym (gcd22 n m n m )) (gcdmm n m )
52 54
53 gcdsym2 : (i j : ℕ) → gcd1 zero i zero j ≡ gcd1 zero j zero i 55 gcdsym2 : (i j : ℕ) → gcd1 zero i zero j ≡ gcd1 zero j zero i
54 gcdsym2 i j with <-cmp i j | <-cmp j i 56 gcdsym2 i j with <-cmp i j | <-cmp j i
55 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim (nat-<> a a₁) 57 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim (nat-<> a a₁)
56 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (nat-≡< (sym b) a) 58 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (nat-≡< (sym b) a)
57 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl 59 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl
58 ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (nat-≡< (sym b) a) 60 ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (nat-≡< (sym b) a)
59 ... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl 61 ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = b
60 ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (nat-≡< b c) 62 ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (nat-≡< b c)
61 ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl 63 ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl
62 ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (nat-≡< b c) 64 ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (nat-≡< b c)
63 ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (nat-<> c c₁) 65 ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (nat-<> c c₁)
64 gcdsym1 : ( i i0 j j0 : ℕ ) → gcd1 i i0 j j0 ≡ gcd1 j j0 i i0 66 gcdsym1 : ( i i0 j j0 : ℕ ) → gcd1 i i0 j j0 ≡ gcd1 j j0 i i0
315 Fsym {suc i} {suc j} with <-cmp i j | <-cmp j i 317 Fsym {suc i} {suc j} with <-cmp i j | <-cmp j i
316 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim (nat-<> a a₁) 318 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim (nat-<> a a₁)
317 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (¬b (sym b)) 319 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (¬b (sym b))
318 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl 320 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl
319 ... | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = ⊥-elim (¬b refl) 321 ... | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = ⊥-elim (¬b refl)
320 ... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl 322 ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = refl
321 ... | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = ⊥-elim (¬b refl) 323 ... | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = ⊥-elim (¬b refl)
322 ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl 324 ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl
323 ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (¬b (sym b)) 325 ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (¬b (sym b))
324 ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (nat-<> c c₁) 326 ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (nat-<> c c₁)
325 327
692 gcd (m * n + 1 + n) n ≡⟨ gcd+j (m * n + 1) n ⟩ 694 gcd (m * n + 1 + n) n ≡⟨ gcd+j (m * n + 1) n ⟩
693 gcd (m * n + 1) n ≡⟨ gcdmul+1 m n ⟩ 695 gcd (m * n + 1) n ≡⟨ gcdmul+1 m n ⟩
694 1 ∎ where open ≡-Reasoning 696 1 ∎ where open ≡-Reasoning
695 697
696 m*n=m→n : {m n : ℕ } → 0 < m → m * n ≡ m * 1 → n ≡ 1 698 m*n=m→n : {m n : ℕ } → 0 < m → m * n ≡ m * 1 → n ≡ 1
697 m*n=m→n {suc m} {n} (s≤s lt) eq = *-cancelˡ-≡ m eq 699 m*n=m→n {suc m} {n} (s≤s lt) eq = begin
700 n ≡⟨ *-cancelˡ-≡ n 1 (suc m) ( begin
701 suc m * n ≡⟨ eq ⟩
702 suc m * 1 ∎ ) ⟩
703 1 ∎ where open ≡-Reasoning
698 704
699 gcd-is-gratest : { i j k : ℕ } → i > 0 → j > 0 → k > 1 → Dividable k i → Dividable k j → k ≤ gcd i j 705 gcd-is-gratest : { i j k : ℕ } → i > 0 → j > 0 → k > 1 → Dividable k i → Dividable k j → k ≤ gcd i j
700 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 706 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
701 gcd001 : Dividable k ( gcd i j ) 707 gcd001 : Dividable k ( gcd i j )
702 gcd001 = gcd-div _ _ _ k>1 ki kj 708 gcd001 = gcd-div _ _ _ k>1 ki kj
710 id : Dividable d (suc i) 716 id : Dividable d (suc i)
711 id = proj1 (gcd-dividable (suc i) (suc j)) 717 id = proj1 (gcd-dividable (suc i) (suc j))
712 jd : Dividable d (suc j) 718 jd : Dividable d (suc j)
713 jd = proj2 (gcd-dividable (suc i) (suc j)) 719 jd = proj2 (gcd-dividable (suc i) (suc j))
714 cop : gcd (Dividable.factor id) (Dividable.factor jd) ≡ 1 720 cop : gcd (Dividable.factor id) (Dividable.factor jd) ≡ 1
715 cop with (gcd (Dividable.factor id) (Dividable.factor jd)) | inspect (gcd (Dividable.factor id)) (Dividable.factor jd) 721 cop with (gcd (Dividable.factor id) (Dividable.factor jd)) in eq
716 ... | zero | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym eq1) (gcd>0 (Dividable.factor id) (Dividable.factor jd) 722 ... | zero = ⊥-elim ( nat-≡< (sym eq) (gcd>0 (Dividable.factor id) (Dividable.factor jd)
717 (0<factor d>0 (s≤s z≤n) id) (0<factor d>0 (s≤s z≤n) jd) )) 723 (0<factor d>0 (s≤s z≤n) id) (0<factor d>0 (s≤s z≤n) jd) ))
718 ... | suc zero | record { eq = eq1 } = refl 724 ... | suc zero = refl
719 ... | 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 725 ... | suc (suc t) = ⊥-elim ( nat-≤> (gcd-is-gratest {suc i} {(suc j)} (s≤s z≤n) (s≤s z≤n) co1 d1id d1jd ) gcd<d1 ) where
720 -- gcd-is-gratest : { i j k : ℕ } → i > 0 → j > 0 → k > 1 → Dividable k i → Dividable k j → k ≤ gcd i j 726 -- gcd-is-gratest : { i j k : ℕ } → i > 0 → j > 0 → k > 1 → Dividable k i → Dividable k j → k ≤ gcd i j
721 d1 : ℕ 727 d1 : ℕ
722 d1 = gcd (Dividable.factor id) (Dividable.factor jd) 728 d1 = gcd (Dividable.factor id) (Dividable.factor jd)
723 d1>1 : gcd (Dividable.factor id) (Dividable.factor jd) > 1 729 d1>1 : gcd (Dividable.factor id) (Dividable.factor jd) > 1
724 d1>1 = subst (λ k → 1 < k ) (sym eq1) (s≤s (s≤s z≤n)) 730 d1>1 = subst (λ k → 1 < k ) (sym eq) (s≤s (s≤s z≤n))
725 mul1 : {x : ℕ} → 1 * x ≡ x 731 mul1 : {x : ℕ} → 1 * x ≡ x
726 mul1 {zero} = refl 732 mul1 {zero} = refl
727 mul1 {suc x} = begin 733 mul1 {suc x} = begin
728 1 * suc x ≡⟨ cong suc (+-comm x _ ) ⟩ 734 1 * suc x ≡⟨ cong suc (+-comm x _ ) ⟩
729 suc x ∎ where open ≡-Reasoning 735 suc x ∎ where open ≡-Reasoning