Mercurial > hg > Members > kono > Proof > galois

comparison Putil.agda @ 96:b43c4a7c57d9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
pins done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 30 Aug 2020 08:40:31 +0900
parents 7030fe612746
children f4ff8e352aa7
comparison
equal deleted inserted replaced
95:7030fe612746 96:b43c4a7c57d9
179 p13 = cong (λ k → suc k ) (fromℕ<-toℕ _ (s≤s m≤n) ) 179 p13 = cong (λ k → suc k ) (fromℕ<-toℕ _ (s≤s m≤n) )
180 ... | tri> ¬a ¬b c = p16 (suc x) refl where 180 ... | tri> ¬a ¬b c = p16 (suc x) refl where
181 p16 : (y : Fin (suc (suc n))) → y ≡ suc x → p← y ≡ suc x 181 p16 : (y : Fin (suc (suc n))) → y ≡ suc x → p← y ≡ suc x
182 p16 zero eq = ⊥-elim ( nat-≡< (cong (λ k → suc (toℕ k) ) eq) (s≤s (s≤s (z≤n)))) 182 p16 zero eq = ⊥-elim ( nat-≡< (cong (λ k → suc (toℕ k) ) eq) (s≤s (s≤s (z≤n))))
183 p16 (suc y) eq with <-cmp (toℕ y) (suc m) -- suc (suc m) < toℕ (suc x) 183 p16 (suc y) eq with <-cmp (toℕ y) (suc m) -- suc (suc m) < toℕ (suc x)
184 ... | tri< a ¬b ¬c = p17 where -- x = suc m case 184 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< refl ( ≤-trans c (subst (λ k → k < suc m) p17 a )) ) where
185 p18 : toℕ y ≡ suc (toℕ x) 185 -- x = suc m case, c : suc (suc m) ≤ suc (toℕ x), a : suc (toℕ y) ≤ suc m, suc y ≡ suc x
186 p18 = begin 186 p17 : toℕ y ≡ toℕ x
187 toℕ y 187 p17 with <-cmp (toℕ y) (toℕ x) | cong toℕ eq
188 ≡⟨ {!!} ⟩ 188 ... | tri< a ¬b ¬c | seq = ⊥-elim ( nat-≡< seq (s≤s a) )
189 suc (toℕ y) 189 ... | tri≈ ¬a b ¬c | seq = b
190 ≡⟨⟩ 190 ... | tri> ¬a ¬b c | seq = ⊥-elim ( nat-≡< (sym seq) (s≤s c))
191 toℕ (suc y)
192 ≡⟨ cong toℕ eq ⟩
193 suc (toℕ x)
194 ∎
195 p17 : fromℕ< (≤-trans (fin<n {_} {y}) a≤sa ) ≡ suc x
196 p17 = begin
197 fromℕ< (≤-trans (fin<n {_} {y}) a≤sa )
198 ≡⟨ fromℕ<-irrelevant _ _ p18 _ (s≤s (fin<n {suc n} {x})) ⟩
199 suc (fromℕ< (fin<n {suc n} {x} ))
200 ≡⟨ cong suc (fromℕ<-toℕ x _ ) ⟩
201 suc x
202 ∎
203 ... | tri≈ ¬a b ¬c = eq 191 ... | tri≈ ¬a b ¬c = eq
204 ... | tri> ¬a ¬b c₁ = eq 192 ... | tri> ¬a ¬b c₁ = eq
205 ... | tri< a ¬b ¬c = p10 (fromℕ< (≤-trans (s≤s a) (s≤s (s≤s m≤n) ))) refl where 193 ... | tri< a ¬b ¬c = p10 (fromℕ< (≤-trans (s≤s a) (s≤s (s≤s m≤n) ))) refl where
206 p10 : (y : Fin (suc (suc n)) ) → y ≡ fromℕ< (≤-trans (s≤s a) (s≤s (s≤s m≤n) )) → p← y ≡ suc x 194 p10 : (y : Fin (suc (suc n)) ) → y ≡ fromℕ< (≤-trans (s≤s a) (s≤s (s≤s m≤n) )) → p← y ≡ suc x
207 p10 zero () 195 p10 zero ()