Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/finiteSetUtil.agda @ 363:21aa222b11c9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
finiteSet from fin injection done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 19 Jul 2023 07:58:18 +0900
parents 6d5344d3be9c
children 708570e55a91
comparison
equal deleted inserted replaced
362:6d5344d3be9c 363:21aa222b11c9
702 702
703 lem06 : (i j : ℕ) → (i<fa : i < finite fa) (j<fa : j < finite fa) 703 lem06 : (i j : ℕ) → (i<fa : i < finite fa) (j<fa : j < finite fa)
704 → Is B A f (Q←F fa (fromℕ< i<fa)) → Is B A f (Q←F fa (fromℕ< j<fa)) → count-B i ≡ count-B j → i ≡ j 704 → Is B A f (Q←F fa (fromℕ< i<fa)) → Is B A f (Q←F fa (fromℕ< j<fa)) → count-B i ≡ count-B j → i ≡ j
705 lem06 i j i<fa j<fa bi bj eq = lem08 where 705 lem06 i j i<fa j<fa bi bj eq = lem08 where
706 lem20 : (i j : ℕ) → i < j → (i<fa : i < finite fa) (j<fa : j < finite fa) 706 lem20 : (i j : ℕ) → i < j → (i<fa : i < finite fa) (j<fa : j < finite fa)
707 → Is B A f (Q←F fa (fromℕ< i<fa)) → Is B A f (Q←F fa (fromℕ< j<fa)) → count-B j ≡ count-B i → ⊥ 707 → Is B A f (Q←F fa (fromℕ< i<fa)) → Is B A f (Q←F fa (fromℕ< j<fa)) → count-B i < count-B j
708 lem20 zero (suc j) i<j i<fa j<fa bi bj le with <-cmp (finite fa) (suc j) 708 lem20 zero (suc j) i<j i<fa j<fa bi bj with <-cmp (finite fa) (suc j)
709 ... | tri< a ¬b ¬c = ⊥-elim (¬c j<fa) 709 ... | tri< a ¬b ¬c = ⊥-elim (¬c j<fa)
710 ... | tri≈ ¬a b ¬c = ⊥-elim (¬c j<fa) 710 ... | tri≈ ¬a b ¬c = ⊥-elim (¬c j<fa)
711 ... | tri> ¬a ¬b c with is-B (Q←F fa ( fromℕ< 0<fa )) | inspect count-B 0 | is-B (Q←F fa (fromℕ< c)) | inspect count-B (suc j) 711 ... | tri> ¬a ¬b c with is-B (Q←F fa ( fromℕ< 0<fa )) | inspect count-B 0 | is-B (Q←F fa (fromℕ< c)) | inspect count-B (suc j)
712 ... | no nisc | _ | _ | _ = ⊥-elim (nisc record { a = Is.a bi ; fa=c = lem26 } ) where 712 ... | no nisc | _ | _ | _ = ⊥-elim (nisc record { a = Is.a bi ; fa=c = lem26 } ) where
713 lem26 : f (Is.a bi) ≡ Q←F fa (fromℕ< 0<fa) 713 lem26 : f (Is.a bi) ≡ Q←F fa (fromℕ< 0<fa)
714 lem26 = trans (Is.fa=c bi) (cong (Q←F fa) (fromℕ<-cong _ _ refl i<fa 0<fa) ) 714 lem26 = trans (Is.fa=c bi) (cong (Q←F fa) (fromℕ<-cong _ _ refl i<fa 0<fa) )
715 ... | yes _ | _ | no nisc | _ = ⊥-elim (nisc record { a = Is.a bj ; fa=c = lem26 } ) where 715 ... | yes _ | _ | no nisc | _ = ⊥-elim (nisc record { a = Is.a bj ; fa=c = lem26 } ) where
716 lem26 : f (Is.a bj) ≡ Q←F fa (fromℕ< c) 716 lem26 : f (Is.a bj) ≡ Q←F fa (fromℕ< c)
717 lem26 = trans (Is.fa=c bj) (cong (Q←F fa) (fromℕ<-cong _ _ refl j<fa c) ) 717 lem26 = trans (Is.fa=c bj) (cong (Q←F fa) (fromℕ<-cong _ _ refl j<fa c) )
718 ... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = ⊥-elim ( nat-≤> lem25 a<sa) where 718 ... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = lem25 where
719 lem24 : count-B j ≡ 0 719 lem25 : 2 ≤ suc (count-B j)
720 lem24 = cong pred le
721 lem25 : 1 ≤ 0
722 lem25 = begin 720 lem25 = begin
723 1 ≡⟨ sym eq1 ⟩ 721 2 ≡⟨ cong suc (sym eq1) ⟩
724 count-B 0 ≤⟨ count-B-mono {0} {j} z≤n ⟩ 722 suc (count-B 0) ≤⟨ s≤s (count-B-mono {0} {j} z≤n) ⟩
725 count-B j ≡⟨ lem24 ⟩ 723 suc (count-B j) ∎ where open ≤-Reasoning
726 0 ∎ where open ≤-Reasoning 724 lem20 (suc i) zero () i<fa j<fa bi bj
727 lem20 (suc i) zero () bi bj le 725 lem20 (suc i) (suc j) (s≤s i<j) i<fa j<fa bi bj = lem21 where
728 lem20 (suc i) (suc j) (s≤s i<j) bi bj le = ? 726 --
727 -- i < suc i ≤ j
728 -- cb i < suc (cb i) < cb (suc i) ≤ cb j
729 --
730 lem23 : suc (count-B j) ≡ count-B (suc j)
731 lem23 with <-cmp (finite fa) (suc j)
732 ... | tri< a ¬b ¬c = ⊥-elim (¬c j<fa)
733 ... | tri≈ ¬a b ¬c = ⊥-elim (¬c j<fa)
734 ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c)) | inspect count-B (suc j)
735 ... | yes _ | record { eq = eq1 } = refl
736 ... | no nisa | _ = ⊥-elim ( nisa record { a = Is.a bj ; fa=c = lem26 } ) where
737 lem26 : f (Is.a bj) ≡ Q←F fa (fromℕ< c)
738 lem26 = trans (Is.fa=c bj) (cong (Q←F fa) (fromℕ<-cong _ _ refl j<fa c) )
739 lem21 : count-B (suc i) < count-B (suc j)
740 lem21 = sx≤py→x≤y ( begin
741 suc (suc (count-B (suc i))) ≤⟨ s≤s ( s≤s ( count-B-mono i<j )) ⟩
742 suc (suc (count-B j)) ≡⟨ cong suc lem23 ⟩
743 suc (count-B (suc j)) ∎ ) where
744 open ≤-Reasoning
729 745
730 lem08 : i ≡ j 746 lem08 : i ≡ j
731 lem08 with <-cmp i j 747 lem08 with <-cmp i j
732 ... | tri< a ¬b ¬c = ⊥-elim ? -- ( lem20 i j a i<fa j<fa bi bj (sym eq) ) 748 ... | tri< a ¬b ¬c = ⊥-elim (nat-≡< eq ( lem20 i j a i<fa j<fa bi bj ))
733 ... | tri≈ ¬a b ¬c = b 749 ... | tri≈ ¬a b ¬c = b
734 ... | tri> ¬a ¬b c₁ = ⊥-elim ? -- ( lem20 j i c₁ j<fa i<fa bj bi eq ) 750 ... | tri> ¬a ¬b c₁ = ⊥-elim (nat-≡< (sym eq) ( lem20 j i c₁ j<fa i<fa bj bi ))
735 751
736 lem09 : (i j : ℕ) → suc n ≤ j → j ≡ count-B i → CountB n 752 lem09 : (i j : ℕ) → suc n ≤ j → j ≡ count-B i → CountB n
737 lem09 0 (suc j) (s≤s le) eq with is-B (Q←F fa (fromℕ< {0} 0<fa )) | inspect count-B 0 753 lem09 0 (suc j) (s≤s le) eq with is-B (Q←F fa (fromℕ< {0} 0<fa )) | inspect count-B 0
738 ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) ) 754 ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) )
739 ... | yes isb | record { eq = eq1 } with ≤-∨ (s≤s le) 755 ... | yes isb | record { eq = eq1 } with ≤-∨ (s≤s le)