Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/nat.agda @ 403:c298981108c1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix for std-lib 2.0
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 24 Sep 2023 11:32:01 +0900
parents 5b985fea126e
children
comparison
equal deleted inserted replaced
402:093e386c10a2 403:c298981108c1
1 {-# OPTIONS --allow-unsolved-metas #-} 1 {-# OPTIONS --cubical-compatible --safe #-}
2
2 module nat where 3 module nat where
3 4
4 open import Data.Nat 5 open import Data.Nat
5 open import Data.Nat.Properties 6 open import Data.Nat.Properties
6 open import Data.Empty 7 open import Data.Empty
102 div2-rev ⟪ x , false ⟫ = x + x 103 div2-rev ⟪ x , false ⟫ = x + x
103 104
104 div2-eq : (x : ℕ ) → div2-rev ( div2 x ) ≡ x 105 div2-eq : (x : ℕ ) → div2-rev ( div2 x ) ≡ x
105 div2-eq zero = refl 106 div2-eq zero = refl
106 div2-eq (suc zero) = refl 107 div2-eq (suc zero) = refl
107 div2-eq (suc (suc x)) with div2 x | inspect div2 x 108 div2-eq (suc (suc x)) with div2 x in eq1
108 ... | ⟪ x1 , true ⟫ | record { eq = eq1 } = begin -- eq1 : div2 x ≡ ⟪ x1 , true ⟫ 109 ... | ⟪ x1 , true ⟫ = begin -- eq1 : div2 x ≡ ⟪ x1 , true ⟫
109 div2-rev ⟪ suc x1 , true ⟫ ≡⟨⟩ 110 div2-rev ⟪ suc x1 , true ⟫ ≡⟨⟩
110 suc (suc (x1 + suc x1)) ≡⟨ cong (λ k → suc (suc k )) (+-comm x1 _ ) ⟩ 111 suc (suc (x1 + suc x1)) ≡⟨ cong (λ k → suc (suc k )) (+-comm x1 _ ) ⟩
111 suc (suc (suc (x1 + x1))) ≡⟨⟩ 112 suc (suc (suc (x1 + x1))) ≡⟨⟩
112 suc (suc (div2-rev ⟪ x1 , true ⟫)) ≡⟨ cong (λ k → suc (suc (div2-rev k ))) (sym eq1) ⟩ 113 suc (suc (div2-rev ⟪ x1 , true ⟫)) ≡⟨ cong (λ k → suc (suc (div2-rev k ))) (sym eq1) ⟩
113 suc (suc (div2-rev (div2 x))) ≡⟨ cong (λ k → suc (suc k)) (div2-eq x) ⟩ 114 suc (suc (div2-rev (div2 x))) ≡⟨ cong (λ k → suc (suc k)) (div2-eq x) ⟩
114 suc (suc x) ∎ where open ≡-Reasoning 115 suc (suc x) ∎ where open ≡-Reasoning
115 ... | ⟪ x1 , false ⟫ | record { eq = eq1 } = begin 116 ... | ⟪ x1 , false ⟫ = begin
116 div2-rev ⟪ suc x1 , false ⟫ ≡⟨⟩ 117 div2-rev ⟪ suc x1 , false ⟫ ≡⟨⟩
117 suc (x1 + suc x1) ≡⟨ cong (λ k → (suc k )) (+-comm x1 _ ) ⟩ 118 suc (x1 + suc x1) ≡⟨ cong (λ k → (suc k )) (+-comm x1 _ ) ⟩
118 suc (suc (x1 + x1)) ≡⟨⟩ 119 suc (suc (x1 + x1)) ≡⟨⟩
119 suc (suc (div2-rev ⟪ x1 , false ⟫)) ≡⟨ cong (λ k → suc (suc (div2-rev k ))) (sym eq1) ⟩ 120 suc (suc (div2-rev ⟪ x1 , false ⟫)) ≡⟨ cong (λ k → suc (suc (div2-rev k ))) (sym eq1) ⟩
120 suc (suc (div2-rev (div2 x))) ≡⟨ cong (λ k → suc (suc k)) (div2-eq x) ⟩ 121 suc (suc (div2-rev (div2 x))) ≡⟨ cong (λ k → suc (suc k)) (div2-eq x) ⟩
135 minus a zero = a 136 minus a zero = a
136 minus zero (suc b) = zero 137 minus zero (suc b) = zero
137 minus (suc a) (suc b) = minus a b 138 minus (suc a) (suc b) = minus a b
138 139
139 _-_ = minus 140 _-_ = minus
141
142 sn-m=sn-m : {m n : ℕ } → m ≤ n → suc n - m ≡ suc ( n - m )
143 sn-m=sn-m {0} {n} z≤n = refl
144 sn-m=sn-m {suc m} {suc n} (s≤s m<n) = sn-m=sn-m m<n
145
146 si-sn=i-n : {i n : ℕ } → n < i → suc (i - suc n) ≡ (i - n)
147 si-sn=i-n {i} {n} n<i = begin
148 suc (i - suc n) ≡⟨ sym (sn-m=sn-m n<i ) ⟩
149 suc i - suc n ≡⟨⟩
150 i - n
151 ∎ where
152 open ≡-Reasoning
153
154 refl-≤s : {x : ℕ } → x ≤ suc x
155 refl-≤s {zero} = z≤n
156 refl-≤s {suc x} = s≤s (refl-≤s {x})
157
158 a≤sa = refl-≤s
159
160 n-m<n : (n m : ℕ ) → n - m ≤ n
161 n-m<n zero zero = z≤n
162 n-m<n (suc n) zero = s≤s (n-m<n n zero)
163 n-m<n zero (suc m) = z≤n
164 n-m<n (suc n) (suc m) = ≤-trans (n-m<n n m ) refl-≤s
165
166 n-n-m=m : {m n : ℕ } → m ≤ n → m ≡ (n - (n - m))
167 n-n-m=m {0} {zero} z≤n = refl
168 n-n-m=m {0} {suc n} z≤n = n-n-m=m {0} {n} z≤n
169 n-n-m=m {suc m} {suc n} (s≤s m≤n) = sym ( begin
170 suc n - ( n - m ) ≡⟨ sn-m=sn-m (n-m<n n m) ⟩
171 suc (n - ( n - m )) ≡⟨ cong (λ k → suc k ) (sym (n-n-m=m m≤n)) ⟩
172 suc m
173 ∎ ) where
174 open ≡-Reasoning
140 175
141 m+= : {i j m : ℕ } → m + i ≡ m + j → i ≡ j 176 m+= : {i j m : ℕ } → m + i ≡ m + j → i ≡ j
142 m+= {i} {j} {zero} refl = refl 177 m+= {i} {j} {zero} refl = refl
143 m+= {i} {j} {suc m} eq = m+= {i} {j} {m} ( cong (λ k → pred k ) eq ) 178 m+= {i} {j} {suc m} eq = m+= {i} {j} {m} ( cong (λ k → pred k ) eq )
144 179
235 <∨≤ : ( x y : ℕ ) → (x < y ) ∨ (y ≤ x) 270 <∨≤ : ( x y : ℕ ) → (x < y ) ∨ (y ≤ x)
236 <∨≤ x y with <-cmp x y 271 <∨≤ x y with <-cmp x y
237 ... | tri< a ¬b ¬c = case1 a 272 ... | tri< a ¬b ¬c = case1 a
238 ... | tri≈ ¬a refl ¬c = case2 ≤-refl 273 ... | tri≈ ¬a refl ¬c = case2 ≤-refl
239 ... | tri> ¬a ¬b c = case2 (<to≤ c) 274 ... | tri> ¬a ¬b c = case2 (<to≤ c)
240
241 refl-≤s : {x : ℕ } → x ≤ suc x
242 refl-≤s {zero} = z≤n
243 refl-≤s {suc x} = s≤s (refl-≤s {x})
244
245 a≤sa = refl-≤s
246 275
247 refl-≤ : {x : ℕ } → x ≤ x 276 refl-≤ : {x : ℕ } → x ≤ x
248 refl-≤ {zero} = z≤n 277 refl-≤ {zero} = z≤n
249 refl-≤ {suc x} = s≤s (refl-≤ {x}) 278 refl-≤ {suc x} = s≤s (refl-≤ {x})
250 279
694 k + (f * k + 0) ≡⟨ sym (+-assoc k _ _) ⟩ 723 k + (f * k + 0) ≡⟨ sym (+-assoc k _ _) ⟩
695 k + f * k + 0 ≡⟨ eq ⟩ 724 k + f * k + 0 ≡⟨ eq ⟩
696 m ∎ where open ≤-Reasoning 725 m ∎ where open ≤-Reasoning
697 726
698 0<factor : { m k : ℕ } → k > 0 → m > 0 → (d : Dividable k m ) → Dividable.factor d > 0 727 0<factor : { m k : ℕ } → k > 0 → m > 0 → (d : Dividable k m ) → Dividable.factor d > 0
699 0<factor {m} {k} k>0 m>0 d with Dividable.factor d | inspect Dividable.factor d 728 0<factor {m} {k} k>0 m>0 d with Dividable.factor d in eq1
700 ... | zero | record { eq = eq1 } = ⊥-elim ( nat-≡< ff1 m>0 ) where 729 ... | zero = ⊥-elim ( nat-≡< ff1 m>0 ) where
701 ff1 : 0 ≡ m 730 ff1 : 0 ≡ m
702 ff1 = begin 731 ff1 = begin
703 0 ≡⟨⟩ 732 0 ≡⟨⟩
704 0 * k + 0 ≡⟨ cong (λ j → j * k + 0) (sym eq1) ⟩ 733 0 * k + 0 ≡⟨ cong (λ j → j * k + 0) (sym eq1) ⟩
705 Dividable.factor d * k + 0 ≡⟨ Dividable.is-factor d ⟩ 734 Dividable.factor d * k + 0 ≡⟨ Dividable.is-factor d ⟩
706 m ∎ where open ≡-Reasoning 735 m ∎ where open ≡-Reasoning
707 ... | suc t | _ = s≤s z≤n 736 ... | suc t = s≤s z≤n
708 737
709 div→k≤m : { m k : ℕ } → k > 1 → m > 0 → Dividable k m → m ≥ k 738 div→k≤m : { m k : ℕ } → k > 1 → m > 0 → Dividable k m → m ≥ k
710 div→k≤m {m} {k} k>1 m>0 d with <-cmp m k 739 div→k≤m {m} {k} k>1 m>0 d with <-cmp m k
711 ... | tri< a ¬b ¬c = ⊥-elim ( div<k k>1 m>0 a d ) 740 ... | tri< a ¬b ¬c = ⊥-elim ( div<k k>1 m>0 a d )
712 ... | tri≈ ¬a refl ¬c = ≤-refl 741 ... | tri≈ ¬a refl ¬c = ≤-refl