Mercurial > hg > Members > kono > Proof > automaton
diff automaton-in-agda/src/finiteSetUtil.agda @ 403:c298981108c1
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 | 708570e55a91 |
| children | dfaf230f7b9a |
line wrap: on
line diff
--- a/automaton-in-agda/src/finiteSetUtil.agda Thu Aug 10 09:59:47 2023 +0900 +++ b/automaton-in-agda/src/finiteSetUtil.agda Sun Sep 24 11:32:01 2023 +0900 @@ -1,4 +1,4 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} module finiteSetUtil where @@ -14,7 +14,6 @@ open import finiteSet open import fin open import Data.Nat.Properties as NP hiding ( _≟_ ) -open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) record Found ( Q : Set ) (p : Q → Bool ) : Set where field @@ -25,13 +24,12 @@ open import Axiom.Extensionality.Propositional open import Level hiding (suc ; zero) -postulate f-extensionality : { n : Level} → Axiom.Extensionality.Propositional.Extensionality n n -- (Level.suc n) module _ {Q : Set } (F : FiniteSet Q) where open FiniteSet F equal?-refl : { x : Q } → equal? x x ≡ true equal?-refl {x} with F←Q x ≟ F←Q x - ... | yes refl = refl + ... | yes eq = refl ... | no ne = ⊥-elim (ne refl) equal→refl : { x y : Q } → equal? x y ≡ true → x ≡ y equal→refl {q0} {q1} eq with F←Q q0 ≟ F←Q q1 @@ -89,9 +87,9 @@ found← : { p : Q → Bool } → exists p ≡ true → Found Q p found← {p} exst = found2 finite NP.≤-refl (first-end p ) where found2 : (m : ℕ ) (m<n : m Data.Nat.≤ finite ) → End m p → Found Q p - found2 0 m<n end = ⊥-elim ( ¬-bool (not-found (λ q → end (F←Q q) z≤n ) ) (subst (λ k → exists k ≡ true) (sym lemma) exst ) ) where - lemma : (λ z → p (Q←F (F←Q z))) ≡ p - lemma = f-extensionality ( λ q → subst (λ k → p k ≡ p q ) (sym (finiso→ q)) refl ) + found2 0 m<n end = ⊥-elim ( ¬-bool f01 exst ) where + f01 : exists p ≡ false + f01 = not-found (λ q → subst ( λ k → p k ≡ false ) (finiso→ _) (end (F←Q q) z≤n )) found2 (suc m) m<n end with bool-≡-? (p (Q←F (fromℕ< m<n))) true found2 (suc m) m<n end | yes eq = record { found-q = Q←F (fromℕ< m<n) ; found-p = eq } found2 (suc m) m<n end | no np = @@ -289,7 +287,7 @@ open ≡-Reasoning open Data.Product -cast-iso : {n m : ℕ } → (eq : n ≡ m ) → (f : Fin m ) → cast eq ( cast (sym eq ) f) ≡ f +cast-iso : {n m : ℕ } → (eq : n ≡ m ) → (f : Fin m ) → Data.Fin.cast eq ( Data.Fin.cast (sym eq ) f) ≡ f cast-iso refl zero = refl cast-iso refl (suc f) = cong ( λ k → suc k ) ( cast-iso refl f ) @@ -338,8 +336,6 @@ ... | no _ = List2Func {Q} fin (NP.<-trans n<m a<sa ) t q open import Level renaming ( suc to Suc ; zero to Zero) -open import Axiom.Extensionality.Propositional --- postulate f-extensionality : { n : Level} → Axiom.Extensionality.Propositional.Extensionality n n F2L-iso : { Q : Set } → (fin : FiniteSet Q ) → (x : Vec Bool (FiniteSet.finite fin) ) → F2L fin a<sa (λ q _ → List2Func fin a<sa x q ) ≡ x F2L-iso {Q} fin x = f2l m a<sa x where @@ -363,9 +359,7 @@ lemma3f : F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q ) ≡ t lemma3f = begin F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q ) - ≡⟨ cong (λ k → F2L fin (NP.<-trans n<m a<sa) ( λ q q<n → k q q<n )) - (f-extensionality ( λ q → - (f-extensionality ( λ q<n → lemma4 q q<n )))) ⟩ + ≡⟨ cong (λ k → F2L fin (NP.<-trans n<m a<sa) ?) ? ⟩ F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (NP.<-trans n<m a<sa) t q ) ≡⟨ f2l n (NP.<-trans n<m a<sa ) t ⟩ t @@ -410,9 +404,9 @@ fun← iso x = F2L fin a<sa ( λ q _ → x q ) fun→ iso x = List2Func fin a<sa x fiso← iso x = F2L-iso fin x - fiso→ iso x = lemma where - lemma : List2Func fin a<sa (F2L fin a<sa (λ q _ → x q)) ≡ x - lemma = f-extensionality ( λ q → L2F-iso fin x q ) + fiso→ iso f = lemma where + lemma : List2Func fin a<sa (F2L fin a<sa (λ q _ → f q)) ≡ f + lemma = ? Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n) @@ -427,21 +421,10 @@ get-< : { n : ℕ } { A : Set } {fa : FiniteSet A } {n<m : n < FiniteSet.finite fa }→ (f : fin-less fa n<m ) → toℕ (FiniteSet.F←Q fa (get-elm f )) < n get-< (elm1 _ b ) = b -fin-less-cong : { n : ℕ } { A : Set } (fa : FiniteSet A ) (n<m : n < FiniteSet.finite fa ) - → (x y : fin-less fa n<m ) → get-elm {n} {A} {fa} x ≡ get-elm {n} {A} {fa} y → get-< x ≅ get-< y → x ≡ y -fin-less-cong fa n<m (elm1 elm x) (elm1 elm x) refl HE.refl = refl - fin-< : {A : Set} → { n : ℕ } → (fa : FiniteSet A ) → (n<m : n < FiniteSet.finite fa ) → FiniteSet (fin-less fa n<m ) fin-< {A} {n} fa n<m = iso-fin (Fin2Finite n) iso where m = FiniteSet.finite fa iso : Bijection (Fin n) (fin-less fa n<m ) - lemma8f : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n - lemma8f {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl - lemma8f {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8f {i} {i} refl ) - lemma10f : {n i j : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → fromℕ< i<n ≡ fromℕ< j<n - lemma10f refl = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8f refl )) - lemma3f : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NP.<-trans a<b b<c ≡ a<c - lemma3f {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8f refl) lemma11f : {n : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NP.<-trans (toℕ<n x) n<m)) ≡ toℕ x lemma11f {n} {x} n<m = begin toℕ (fromℕ< (NP.<-trans (toℕ<n x) n<m)) @@ -475,7 +458,7 @@ open ≡-Reasoning lemma6 : toℕ (fromℕ< (NP.<-trans (toℕ<n x) n<m)) < n lemma6 = subst ( λ k → k < n ) (sym (toℕ-fromℕ< (NP.<-trans (toℕ<n x) n<m))) (toℕ<n x ) - fiso→ iso (elm1 elm x) = fin-less-cong fa n<m _ _ lemma (lemma8 (cong (λ k → toℕ (FiniteSet.F←Q fa k) ) lemma ) ) where + fiso→ iso (elm1 elm x) = ? where -- fin-less-cong fa n<m _ _ lemma (lemma8 (cong (λ k → toℕ (FiniteSet.F←Q fa k) ) lemma ) ) where lemma13 : toℕ (fromℕ< x) ≡ toℕ (FiniteSet.F←Q fa elm) lemma13 = begin toℕ (fromℕ< x) @@ -489,7 +472,7 @@ FiniteSet.Q←F fa (fromℕ< ( NP.<-trans (toℕ<n ( fromℕ< x ) ) n<m)) ≡⟨ cong (λ k → FiniteSet.Q←F fa k) (lemma10 lemma13 ) ⟩ FiniteSet.Q←F fa (fromℕ< ( NP.<-trans x n<m)) - ≡⟨ cong (λ k → FiniteSet.Q←F fa (fromℕ< k )) (HE.≅-to-≡ (lemma8 refl)) ⟩ + ≡⟨ cong (λ k → FiniteSet.Q←F fa (fromℕ< k )) ? ⟩ FiniteSet.Q←F fa (fromℕ< ( toℕ<n (FiniteSet.F←Q fa elm))) ≡⟨ cong (λ k → FiniteSet.Q←F fa k ) ( fromℕ<-toℕ _ _ ) ⟩ FiniteSet.Q←F fa (FiniteSet.F←Q fa elm ) @@ -545,22 +528,22 @@ dup-in-list+fin {Q} finq q qs p = i-phase1 qs p where i-phase2 : (qs : List Q) → fin-phase2 (F←Q finq q) (map (F←Q finq) qs) ≡ true → phase2 finq q qs ≡ true - i-phase2 (x ∷ qs) p with equal? finq q x | inspect (equal? finq q ) x | <-fcmp (F←Q finq q) (F←Q finq x) - ... | true | _ | t = refl - ... | false | _ | tri< a ¬b ¬c = i-phase2 qs p - ... | false | record { eq = eq } | tri≈ ¬a b ¬c = ⊥-elim (¬-bool eq + i-phase2 (x ∷ qs) p with equal? finq q x in eq | <-fcmp (F←Q finq q) (F←Q finq x) + ... | true | t = refl + ... | false | tri< a ¬b ¬c = i-phase2 qs p + ... | false | tri≈ ¬a b ¬c = ⊥-elim (¬-bool eq (subst₂ (λ j k → equal? finq j k ≡ true) (finiso→ finq q) (subst (λ k → Q←F finq k ≡ x) (sym b) (finiso→ finq x)) ( equal?-refl finq ))) - ... | false | _ | tri> ¬a ¬b c = i-phase2 qs p + ... | false | tri> ¬a ¬b c = i-phase2 qs p i-phase1 : (qs : List Q) → fin-phase1 (F←Q finq q) (map (F←Q finq) qs) ≡ true → phase1 finq q qs ≡ true - i-phase1 (x ∷ qs) p with equal? finq q x | inspect (equal? finq q ) x | <-fcmp (F←Q finq q) (F←Q finq x) - ... | true | record { eq = eq } | tri< a ¬b ¬c = ⊥-elim ( nat-≡< (cong (λ x → toℕ (F←Q finq x)) ( equal→refl finq eq )) a ) - ... | true | _ | tri≈ ¬a b ¬c = i-phase2 qs p - ... | true | record { eq = eq} | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (cong (λ x → toℕ (F←Q finq x)) (sym ( equal→refl finq eq ))) c ) - ... | false | _ | tri< a ¬b ¬c = i-phase1 qs p - ... | false | record {eq = eq} | tri≈ ¬a b ¬c = ⊥-elim (¬-bool eq + i-phase1 (x ∷ qs) p with equal? finq q x in eq | <-fcmp (F←Q finq q) (F←Q finq x) + ... | true | tri< a ¬b ¬c = ⊥-elim ( nat-≡< (cong (λ x → toℕ (F←Q finq x)) ( equal→refl finq eq )) a ) + ... | true | tri≈ ¬a b ¬c = i-phase2 qs p + ... | true | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (cong (λ x → toℕ (F←Q finq x)) (sym ( equal→refl finq eq ))) c ) + ... | false | tri< a ¬b ¬c = i-phase1 qs p + ... | false | tri≈ ¬a b ¬c = ⊥-elim (¬-bool eq (subst₂ (λ j k → equal? finq j k ≡ true) (finiso→ finq q) (subst (λ k → Q←F finq k ≡ x) (sym b) (finiso→ finq x)) ( equal?-refl finq ))) - ... | false | _ | tri> ¬a ¬b c = i-phase1 qs p + ... | false | tri> ¬a ¬b c = i-phase1 qs p record Dup-in-list {Q : Set } (finq : FiniteSet Q) (qs : List Q) : Set where field @@ -587,8 +570,8 @@ → (fi : InjectiveF B A) → (is-B : (a : A ) → Dec (Is B A (InjectiveF.f fi) a) ) → FiniteSet B -inject-fin {A} {B} fa fi is-B with finite fa | inspect finite fa -... | zero | record { eq = eq1 } = record { +inject-fin {A} {B} fa fi is-B with finite fa in eq1 +... | zero = record { finite = 0 ; Q←F = λ () ; F←Q = λ b → ⊥-elim ( lem00 b) @@ -598,7 +581,7 @@ lem00 : ( b : B) → ⊥ lem00 b with subst (λ k → Fin k ) eq1 (F←Q fa (InjectiveF.f fi b)) ... | () -... | suc pfa | record { eq = eq1 } = record { +... | suc pfa = record { finite = maxb ; Q←F = λ fb → CountB.b (cb00 _ (fin<n {_} fb)) ; F←Q = λ b → fromℕ< (cb<mb b) @@ -643,28 +626,32 @@ lem01 zero with <-cmp (finite fa) 1 lem01 zero | tri< a ¬b ¬c = ≤-refl lem01 zero | tri≈ ¬a b ¬c = ≤-refl - lem01 zero | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c)) | is-B (Q←F fa ( fromℕ< {0} 0<fa )) | inspect count-B 0 - ... | yes isb1 | yes isb0 | record { eq = eq0 } = s≤s z≤n - ... | yes isb1 | no nisb0 | record { eq = eq0 } = z≤n - ... | no nisb1 | yes isb0 | record { eq = eq0 } = refl-≤≡ (sym eq0) - ... | no nisb1 | no nisb0 | record { eq = eq0 } = z≤n - lem01 (suc i) with <-cmp (finite fa) (suc i) | <-cmp (finite fa) (suc (suc i)) | inspect count-B (suc i) | inspect count-B (suc (suc i)) - ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ | record { eq = eq0 } | record { eq = eq1 } = refl-≤≡ (sym eq0) - ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ | _ | _ = ⊥-elim (nat-≡< b (<-trans a a<sa)) - ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c | _ | _ = ⊥-elim (nat-<> a (<-trans a<sa c) ) - ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | record { eq = eq0 } | _ = refl-≤≡ (sym eq0) - ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | _ | _ = ⊥-elim (nat-≡< (sym b) (subst (λ k → _ < k ) (sym b₁) a<sa) ) - ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c | _ | _ = ⊥-elim (nat-≡< (sym b) (<-trans a<sa c)) - ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c | _ | _ = ⊥-elim (nat-≤> a (<-transʳ c a<sa ) ) - ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c | record { eq = eq0 } | record { eq = eq1 } with is-B (Q←F fa (fromℕ< c)) - ... | yes isb = refl-≤≡ (sym eq0) - ... | no nisb = refl-≤≡ (sym eq0) - lem01 (suc i) | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ | record { eq = eq0 } | record { eq = eq1 } + lem01 zero | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c)) | is-B (Q←F fa ( fromℕ< {0} 0<fa )) + ... | yes isb1 | yes isb0 = s≤s z≤n + ... | yes isb1 | no nisb0 = z≤n + ... | no nisb1 | yes isb0 = refl-≤≡ (sym lem14 ) where + lem14 : count-B 0 ≡ 1 + lem14 with is-B (Q←F fa ( fromℕ< {0} 0<fa )) + ... | yes isb = refl + ... | no ne = ⊥-elim (ne isb0) + ... | no nisb1 | no nisb0 = z≤n + lem01 (suc i) with <-cmp (finite fa) (suc i) | <-cmp (finite fa) (suc (suc i)) + ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = refl-≤≡ (sym ? ) + ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (nat-≡< b (<-trans a a<sa)) + ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = ⊥-elim (nat-<> a (<-trans a<sa c) ) + ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = refl-≤≡ (sym ?) + ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = ⊥-elim (nat-≡< (sym b) (subst (λ k → _ < k ) (sym b₁) a<sa) ) + ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (nat-≡< (sym b) (<-trans a<sa c)) + ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = ⊥-elim (nat-≤> a (<-transʳ c a<sa ) ) + ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c with is-B (Q←F fa (fromℕ< c)) + ... | yes isb = refl-≤≡ (sym ?) + ... | no nisb = refl-≤≡ (sym ?) + lem01 (suc i) | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ with is-B (Q←F fa (fromℕ< c)) | is-B (Q←F fa (fromℕ< c₁)) - ... | yes isb0 | yes isb1 = ≤-trans (refl-≤≡ (sym eq0)) a≤sa - ... | yes isb0 | no nisb1 = refl-≤≡ (sym eq0) - ... | no nisb0 | yes isb1 = ≤-trans (refl-≤≡ (sym eq0)) a≤sa - ... | no nisb0 | no nisb1 = refl-≤≡ (sym eq0) + ... | yes isb0 | yes isb1 = ≤-trans (refl-≤≡ (sym ?)) a≤sa + ... | yes isb0 | no nisb1 = refl-≤≡ (sym ?) + ... | no nisb0 | yes isb1 = ≤-trans (refl-≤≡ (sym ?)) a≤sa + ... | no nisb0 | no nisb1 = refl-≤≡ (sym ?) lem31 : (b : B) → 0 < count-B (toℕ (F←Q fa (f b))) lem31 b = lem32 (toℕ (F←Q fa (f b))) refl where @@ -679,10 +666,10 @@ Q←F fa ( fromℕ< (fin<n _) ) ≡⟨ cong (λ k → Q←F fa k) (fromℕ<-cong _ _ eq (fin<n _) 0<fa) ⟩ Q←F fa ( fromℕ< {0} 0<fa ) ∎ where open ≡-Reasoning - lem32 (suc i) eq with <-cmp (finite fa) (suc i) | inspect count-B (suc i) - ... | tri< a ¬b ¬c | _ = ⊥-elim ( nat-≡< eq (<-trans (fin<n _) a) ) - ... | tri≈ ¬a eq1 ¬c | _ = ⊥-elim ( nat-≡< eq (subst (λ k → toℕ (F←Q fa (f b)) < k ) eq1 (fin<n _))) - ... | tri> ¬a ¬b c | record { eq = eq1 } with is-B (Q←F fa (fromℕ< c)) + lem32 (suc i) eq with <-cmp (finite fa) (suc i) + ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< eq (<-trans (fin<n _) a) ) + ... | tri≈ ¬a eq1 ¬c = ⊥-elim ( nat-≡< eq (subst (λ k → toℕ (F←Q fa (f b)) < k ) eq1 (fin<n _))) + ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c)) ... | yes isb = s≤s z≤n ... | no nisb = ⊥-elim ( nisb record { a = b ; fa=c = lem33 } ) where lem33 : f b ≡ Q←F fa ( fromℕ< c) @@ -713,17 +700,17 @@ lem20 zero (suc j) i<j i<fa j<fa bi bj with <-cmp (finite fa) (suc j) ... | tri< a ¬b ¬c = ⊥-elim (¬c j<fa) ... | tri≈ ¬a b ¬c = ⊥-elim (¬c j<fa) - ... | 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) - ... | no nisc | _ | _ | _ = ⊥-elim (nisc record { a = Is.a bi ; fa=c = lem26 } ) where + ... | tri> ¬a ¬b c with is-B (Q←F fa ( fromℕ< 0<fa )) | is-B (Q←F fa (fromℕ< c)) + ... | no nisc | _ = ⊥-elim (nisc record { a = Is.a bi ; fa=c = lem26 } ) where lem26 : f (Is.a bi) ≡ Q←F fa (fromℕ< 0<fa) lem26 = trans (Is.fa=c bi) (cong (Q←F fa) (fromℕ<-cong _ _ refl i<fa 0<fa) ) - ... | yes _ | _ | no nisc | _ = ⊥-elim (nisc record { a = Is.a bj ; fa=c = lem26 } ) where + ... | yes _ | no nisc = ⊥-elim (nisc record { a = Is.a bj ; fa=c = lem26 } ) where lem26 : f (Is.a bj) ≡ Q←F fa (fromℕ< c) lem26 = trans (Is.fa=c bj) (cong (Q←F fa) (fromℕ<-cong _ _ refl j<fa c) ) - ... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = lem25 where + ... | yes _ | yes _ = lem25 where lem25 : 2 ≤ suc (count-B j) lem25 = begin - 2 ≡⟨ cong suc (sym eq1) ⟩ + 2 ≡⟨ cong suc (sym ?) ⟩ suc (count-B 0) ≤⟨ s≤s (count-B-mono {0} {j} z≤n) ⟩ suc (count-B j) ∎ where open ≤-Reasoning lem20 (suc i) zero () i<fa j<fa bi bj @@ -736,9 +723,9 @@ lem23 with <-cmp (finite fa) (suc j) ... | tri< a ¬b ¬c = ⊥-elim (¬c j<fa) ... | tri≈ ¬a b ¬c = ⊥-elim (¬c j<fa) - ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c)) | inspect count-B (suc j) - ... | yes _ | record { eq = eq1 } = refl - ... | no nisa | _ = ⊥-elim ( nisa record { a = Is.a bj ; fa=c = lem26 } ) where + ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c)) + ... | yes _ = refl + ... | no nisa = ⊥-elim ( nisa record { a = Is.a bj ; fa=c = lem26 } ) where lem26 : f (Is.a bj) ≡ Q←F fa (fromℕ< c) lem26 = trans (Is.fa=c bj) (cong (Q←F fa) (fromℕ<-cong _ _ refl j<fa c) ) lem21 : count-B (suc i) < count-B (suc j) @@ -755,10 +742,10 @@ ... | tri> ¬a ¬b c₁ = ⊥-elim (nat-≡< (sym eq) ( lem20 j i c₁ j<fa i<fa bj bi )) lem09 : (i j : ℕ) → suc n ≤ j → j ≡ count-B i → CountB n - lem09 0 (suc j) (s≤s le) eq with is-B (Q←F fa (fromℕ< {0} 0<fa )) | inspect count-B 0 - ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) ) - ... | yes isb | record { eq = eq1 } with ≤-∨ (s≤s le) - ... | case1 eq2 = record { b = Is.a isb ; cb = 0 ; b=cn = lem10 ; cb=n = trans eq1 (sym (trans eq2 eq)) + lem09 0 (suc j) (s≤s le) eq with is-B (Q←F fa (fromℕ< {0} 0<fa )) + ... | no nisb = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) ) + ... | yes isb with ≤-∨ (s≤s le) + ... | case1 eq2 = record { b = Is.a isb ; cb = 0 ; b=cn = lem10 ; cb=n = trans ? (sym (trans eq2 eq)) ; cb-inject = λ cb1 c1<fa b1 eq → lem06 0 cb1 0<fa c1<fa isb b1 eq } where lem10 : 0 ≡ toℕ (F←Q fa (f (Is.a isb))) lem10 = begin @@ -767,13 +754,13 @@ toℕ (F←Q fa (Q←F fa (fromℕ< {0} 0<fa ))) ≡⟨ cong (λ k → toℕ ((F←Q fa k))) (sym (Is.fa=c isb)) ⟩ toℕ (F←Q fa (f (Is.a isb))) ∎ where open ≡-Reasoning ... | case2 (s≤s lt) = ⊥-elim ( nat-≡< (sym eq) (s≤s (<-transʳ z≤n lt) )) - lem09 (suc i) (suc j) (s≤s le) eq with <-cmp (finite fa) (suc i) | inspect count-B (suc i) - ... | tri< a ¬b ¬c | _ = lem09 i (suc j) (s≤s le) eq - ... | tri≈ ¬a b ¬c | _ = lem09 i (suc j) (s≤s le) eq - ... | tri> ¬a ¬b c | record { eq = eq1 } with is-B (Q←F fa (fromℕ< c)) + lem09 (suc i) (suc j) (s≤s le) eq with <-cmp (finite fa) (suc i) + ... | tri< a ¬b ¬c = lem09 i (suc j) (s≤s le) eq + ... | tri≈ ¬a b ¬c = lem09 i (suc j) (s≤s le) eq + ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c)) ... | no nisb = lem09 i (suc j) (s≤s le) eq ... | yes isb with ≤-∨ (s≤s le) - ... | case1 eq2 = record { b = Is.a isb ; cb = suc i ; b=cn = lem11 ; cb=n = trans eq1 (sym (trans eq2 eq )) + ... | case1 eq2 = record { b = Is.a isb ; cb = suc i ; b=cn = lem11 ; cb=n = trans ? (sym (trans eq2 eq )) ; cb-inject = λ cb1 c1<fa b1 eq → lem06 (suc i) cb1 c c1<fa isb b1 eq } where lem11 : suc i ≡ toℕ (F←Q fa (f (Is.a isb))) lem11 = begin