Mercurial > hg > Members > kono > Proof > automaton

comparison agda/finiteSet.agda @ 132:370b3fc69c1a

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 Nov 2019 11:37:00 +0900
parents 06a42928de38
children 65bea0aad363
comparison
equal deleted inserted replaced
131:06a42928de38 132:370b3fc69c1a
392 fin-< {A} {zero} {m} (s≤s z≤n) fa = record { Q←F = λ () ; F←Q = λ () ; finiso← = λ () ; finiso→ = λ () } 392 fin-< {A} {zero} {m} (s≤s z≤n) fa = record { Q←F = λ () ; F←Q = λ () ; finiso← = λ () ; finiso→ = λ () }
393 fin-< {A} {suc n} {m} (s≤s n<m) fa = iso-fin (fin-∨1 (fin-< {A} {n} {m} (Data.Nat.Properties.<-trans n<m a<sa) fa)) iso where 393 fin-< {A} {suc n} {m} (s≤s n<m) fa = iso-fin (fin-∨1 (fin-< {A} {n} {m} (Data.Nat.Properties.<-trans n<m a<sa) fa)) iso where
394 fin- : FiniteSet (Fin-< (Data.Nat.Properties.<-trans n<m a<sa) fa) 394 fin- : FiniteSet (Fin-< (Data.Nat.Properties.<-trans n<m a<sa) fa)
395 fin- = fin-< {A} {n} {m} (Data.Nat.Properties.<-trans n<m a<sa) fa 395 fin- = fin-< {A} {n} {m} (Data.Nat.Properties.<-trans n<m a<sa) fa
396 iso : ISO (One ∨ Fin-< (Data.Nat.Properties.<-trans n<m a<sa) fa) (Fin-< (s≤s n<m) fa) 396 iso : ISO (One ∨ Fin-< (Data.Nat.Properties.<-trans n<m a<sa) fa) (Fin-< (s≤s n<m) fa)
397 c1 : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa) ))) ≡ n 397 lastf = FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa) ))
398 last1 = FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa))
399 c1 : toℕ lastf ≡ n
398 c1 = subst (λ k → toℕ k ≡ n ) (sym (FiniteSet.finiso← fa _ )) (subst (λ k → k ≡ n) (sym (toℕ-fromℕ≤ _ )) refl ) 400 c1 = subst (λ k → toℕ k ≡ n ) (sym (FiniteSet.finiso← fa _ )) (subst (λ k → k ≡ n) (sym (toℕ-fromℕ≤ _ )) refl )
399 f<n : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa)))) < suc n 401 f<n : toℕ lastf < suc n
400 f<n = subst ( λ k → k < suc n ) (sym c1) a<sa 402 f<n = subst ( λ k → k < suc n ) (sym c1) a<sa
401 ISO.A←B iso x with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm x )) ) n 403 ISO.A←B iso x with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm x )) ) n
402 ISO.A←B iso x | tri< a ¬b ¬c = case2 record { elm = elm x ; elm<n = a } 404 ISO.A←B iso x | tri< a ¬b ¬c = case2 record { elm = elm x ; elm<n = a }
403 ISO.A←B iso x | tri≈ ¬a b ¬c = case1 one 405 ISO.A←B iso x | tri≈ ¬a b ¬c = case1 one
404 ISO.A←B iso x | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c (elm<n x) ) 406 ISO.A←B iso x | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c (elm<n x) )
405 ISO.B←A iso (case1 one) = record { elm = FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa) ); elm<n = f<n } 407 ISO.B←A iso (case1 one) = record { elm = last1 ; elm<n = f<n }
406 ISO.B←A iso (case2 x) = record { elm = elm x ; elm<n = Data.Nat.Properties.<-trans (elm<n x) a<sa } 408 ISO.B←A iso (case2 x) = record { elm = elm x ; elm<n = Data.Nat.Properties.<-trans (elm<n x) a<sa }
407 ISO.iso← iso (case1 one) with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm (ISO.B←A iso (case1 one))))) n 409 ISO.iso← iso (case1 one) with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm (ISO.B←A iso (case1 one))))) n
408 ISO.iso← iso (case1 one) | tri< a ¬b ¬c = ⊥-elim ( ¬b c1 ) 410 ISO.iso← iso (case1 one) | tri< a ¬b ¬c = ⊥-elim ( ¬b c1 )
409 ISO.iso← iso (case1 one) | tri≈ ¬a b ¬c = refl 411 ISO.iso← iso (case1 one) | tri≈ ¬a b ¬c = refl
410 ISO.iso← iso (case1 one) | tri> ¬a ¬b c = ⊥-elim ( ¬b c1 ) 412 ISO.iso← iso (case1 one) | tri> ¬a ¬b c = ⊥-elim ( ¬b c1 )
413 lemma1 : {m n : ℕ } → ( i j : m < n ) → i ≡ j 415 lemma1 : {m n : ℕ } → ( i j : m < n ) → i ≡ j
414 lemma1 {zero} {suc n} (s≤s z≤n) (s≤s z≤n) = refl 416 lemma1 {zero} {suc n} (s≤s z≤n) (s≤s z≤n) = refl
415 lemma1 {suc m} {suc n} (s≤s i) (s≤s j) = cong ( λ k → s≤s k ) ( lemma1 {m} {n} i j ) 417 lemma1 {suc m} {suc n} (s≤s i) (s≤s j) = cong ( λ k → s≤s k ) ( lemma1 {m} {n} i j )
416 ISO.iso← iso (case2 x) | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< b (elm<n x) ) 418 ISO.iso← iso (case2 x) | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< b (elm<n x) )
417 ISO.iso← iso (case2 x) | tri> ¬a ¬b c = ⊥-elim ( nat-<> c (elm<n x) ) 419 ISO.iso← iso (case2 x) | tri> ¬a ¬b c = ⊥-elim ( nat-<> c (elm<n x) )
418 ISO.iso→ iso x with ISO.A←B iso x 420 ISO.iso→ iso x with ISO.A←B iso x
419 ISO.iso→ iso x | case1 one with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm x )) ) n 421 ISO.iso→ iso x | case1 one with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm x )) ) n | inspect (λ x → ISO.B←A iso ( ISO.A←B iso x )) x
420 ISO.iso→ iso x | case1 one | tri< a ¬b ¬c = ⊥-elim ( ¬c lemma3 ) where 422 ... | tri< a ¬b ¬c | record { eq = e } = {!!}
421 lemma2 : n < toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa)))) 423 ... | tri≈ ¬a b ¬c | record { eq = e } = {!!}
422 lemma2 = subst (λ k → n < toℕ k ) (sym (FiniteSet.finiso← fa _ )) {!!} 424 ... | tri> ¬a ¬b c | record { eq = e } = ⊥-elim ( nat-≤> c (elm<n x) )
423 lemma3 : n < toℕ (FiniteSet.F←Q fa (elm x)) 425 ISO.iso→ iso x | case2 x1 = {!!}
424 lemma3 = subst (λ k → n < toℕ k ) {!!} lemma2
425 ISO.iso→ iso x | case1 one | tri≈ ¬a b ¬c = {!!}
426 ISO.iso→ iso x | case1 one | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c (elm<n x) )
427 ISO.iso→ iso x | case2 x1 = {!!} -- with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm x )) ) n
428 -- ISO.iso→ iso x | case2 x1 | tri< a ¬b ¬c = ? 426 -- ISO.iso→ iso x | case2 x1 | tri< a ¬b ¬c = ?
429 -- ISO.iso→ iso x | case2 x1 | tri≈ ¬a b ¬c = {!!} 427 -- ISO.iso→ iso x | case2 x1 | tri≈ ¬a b ¬c = {!!}
430 -- ISO.iso→ iso x | case2 x1 | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c (elm<n x) ) 428 -- ISO.iso→ iso x | case2 x1 | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c (elm<n x) )
431 429
432 fin-× : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A × B) {a * b} 430 fin-× : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A × B) {a * b}