Mercurial > hg > Members > kono > Proof > galois
changeset 320:8fb16f9a882a
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 19 Sep 2023 11:11:38 +0900 |
| parents | fff18d4a063b |
| children | 7c6f665e687f |
| files | Galois.agda-lib src/Putil.agda src/fin.agda |
| diffstat | 3 files changed, 126 insertions(+), 88 deletions(-) [+] |
line wrap: on
line diff
--- a/Galois.agda-lib Mon Sep 18 13:19:37 2023 +0900 +++ b/Galois.agda-lib Tue Sep 19 11:11:38 2023 +0900 @@ -1,5 +1,5 @@ name: Galois -depend: standard-library-2.0 +depend: standard-library include: src flags: --warning=noUnsupportedIndexedMatch
--- a/src/Putil.agda Mon Sep 18 13:19:37 2023 +0900 +++ b/src/Putil.agda Tue Sep 19 11:11:38 2023 +0900 @@ -5,7 +5,7 @@ open import Algebra open import Algebra.Structures open import Data.Fin hiding ( _<_ ; _≤_ ; _-_ ; _+_ ; _≟_) -open import Data.Fin.Properties hiding ( <-trans ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp ) +open import Data.Fin.Properties as DFP hiding ( <-trans ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp ) open import Data.Fin.Permutation open import Function hiding (id ; flip) open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) @@ -123,7 +123,7 @@ -- pins1 (suc i) (suc j) (s≤s si≤n) = psawpim {suc (suc (suc n))} {j} (s≤s (s≤s si≤n)) ∘ₚ pins1 i j (≤-trans si≤n a≤sa ) -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) -open ≡-Reasoning +-- open ≡-Reasoning pins : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n) pins {_} {zero} _ = pid @@ -157,7 +157,7 @@ toℕ (fromℕ< (≤-trans (fin<n {_} {suc x} ) (s≤s a≤sa))) ≡⟨ toℕ-fromℕ< ( s≤s ( ≤-trans fin<n a≤sa ) ) ⟩ suc (toℕ x) - ∎ + ∎ where open ≡-Reasoning piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x piso→ zero with <-cmp (toℕ (fromℕ< (≤-trans (s≤s z≤n) (s≤s (s≤s m≤n) )))) (suc m) @@ -190,18 +190,18 @@ toℕ (fromℕ< (≤-trans a (s≤s m≤n))) ≡⟨ toℕ-fromℕ< {suc (toℕ x)} {suc n} (≤-trans a (s≤s m≤n)) ⟩ suc (toℕ x) - ∎ + ∎ where open ≡-Reasoning p15 : p← (suc y) ≡ suc x p15 with <-cmp (toℕ y) (suc m) -- eq : suc y ≡ suc (suc (fromℕ< (≤-pred (≤-trans a (s≤s m≤n))))) , a : suc x < suc m ... | tri< a₁ ¬b ¬c = p11 where p11 : fromℕ< (≤-trans (fin<n {_} {y}) a≤sa ) ≡ suc x p11 = begin fromℕ< (≤-trans (fin<n {_} {y}) a≤sa ) - ≡⟨ ? ⟩ -- lemma10 {suc (suc n)} {_} {_} p12 {≤-trans (fin<n {_} {y}) a≤sa} {s≤s (fin<n {suc n} {x} )} ⟩ + ≡⟨ lemma10 {suc (suc n)} {_} {_} p12 {≤-trans (fin<n {_} {y}) a≤sa} {s≤s (fin<n {suc n} {x} )} ⟩ suc (fromℕ< (fin<n {suc n} {x} )) ≡⟨ cong suc (fromℕ<-toℕ x _ ) ⟩ suc x - ∎ + ∎ where open ≡-Reasoning ... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< b (subst (λ k → k < suc m) (sym p12) a )) -- suc x < suc m -> y = suc x → toℕ y < suc m ... | tri> ¬a ¬b c = ⊥-elim ( nat-<> c (subst (λ k → k < suc m) (sym p12) a )) @@ -232,13 +232,13 @@ fromℕ< (≤-trans (s≤s a₁) (s≤s (s≤s m≤n) )) ≡⟨⟩ fromℕ< (s≤s (≤-trans a₁ (s≤s m≤n))) - ≡⟨ ? ⟩ -- lemma10 {suc (suc n)} (p3 x) {p6} {p2} ⟩ + ≡⟨ lemma10 {suc (suc n)} (p3 x) {p6} {p2} ⟩ fromℕ< ( s≤s (fin<n {suc n} {x}) ) ≡⟨⟩ suc (fromℕ< (fin<n {suc n} {x} )) ≡⟨ cong suc (fromℕ<-toℕ x _ ) ⟩ suc x - ∎ + ∎ where open ≡-Reasoning t7 = plist (pins {3} (n≤ 3)) ∷ plist (flip ( pins {3} (n≤ 3) )) ∷ plist ( pins {3} (n≤ 3) ∘ₚ flip ( pins {3} (n≤ 3))) ∷ [] -- t8 = {!!} @@ -278,13 +278,13 @@ p004 = p003 (fromℕ< (s≤s (s≤s m≤n))) ( begin fromℕ< (s≤s (s≤s m≤n)) - ≡⟨ ? ⟩ -- lemma10 {suc (suc n)} (cong suc meq) {s≤s (s≤s m≤n)} {subst (λ k → suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) } ⟩ + ≡⟨ lemma10 {suc (suc n)} (cong suc meq) {s≤s (s≤s m≤n)} {subst (λ k → suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) } ⟩ fromℕ< (subst (λ k → suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) ) ≡⟨ fromℕ<-toℕ {suc (suc n)} (suc t) (subst (λ k → suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) ) ⟩ suc t ≡⟨ sym e ⟩ (perm ⟨$⟩ʳ (# 0)) - ∎ ) + ∎ ) where open ≡-Reasoning ---- -- other elements are preserved in pins @@ -350,7 +350,7 @@ y ⟨$⟩ʳ zero ≡⟨ cong ( λ k → y ⟨$⟩ʳ k ) (sym (toℕ-injective b )) ⟩ y ⟨$⟩ʳ q - ∎ + ∎ where open ≡-Reasoning pleq1 (suc i) (s≤s i<sn) eq q q<i with <-cmp (toℕ q) (suc i) ... | tri< a ¬b ¬c = pleq1 i (<-trans i<sn a<sa ) (taileq eq) q a ... | tri> ¬a ¬b c = ⊥-elim (nat-≤> c q<i ) @@ -363,6 +363,7 @@ ≡⟨ cong (λ k → y ⟨$⟩ʳ k) (sym (pleq3 b)) ⟩ y ⟨$⟩ʳ q ∎ where + open ≡-Reasoning pleq3 : toℕ q ≡ suc i → q ≡ suc (fromℕ< i<sn) pleq3 tq=si = toℕ-injective ( begin toℕ q @@ -409,7 +410,8 @@ suc ( y ⟨$⟩ʳ q ) ≡⟨⟩ pprep y ⟨$⟩ʳ suc q - ∎ + ∎ where + open ≡-Reasoning pprep-dist : {n : ℕ} → {x y : Permutation n n } → pprep (x ∘ₚ y) =p= (pprep x ∘ₚ pprep y) pprep-dist {n} {x} {y} = record { peq = pprep-dist1 } where @@ -430,7 +432,8 @@ suc (suc (y ⟨$⟩ʳ q)) ≡⟨⟩ pswap y ⟨$⟩ʳ suc (suc q) - ∎ + ∎ where + open ≡-Reasoning pswap-dist : {n : ℕ} → {x y : Permutation n n } → pprep (pprep (x ∘ₚ y)) =p= (pswap x ∘ₚ pswap y) pswap-dist {n} {x} {y} = record { peq = pswap-dist1 } where @@ -446,7 +449,8 @@ perm ⟨$⟩ʳ zero ≡⟨ cong (λ k → perm ⟨$⟩ʳ k ) (sym p0=0) ⟩ perm ⟨$⟩ʳ ( perm ⟨$⟩ˡ zero) ≡⟨ inverseʳ perm ⟩ zero - ∎ + ∎ where + open ≡-Reasoning shlem← : {n : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → (x : Fin (suc n)) → perm ⟨$⟩ʳ x ≡ zero → x ≡ zero shlem← perm p0=0 x px=0 = begin @@ -454,7 +458,8 @@ perm ⟨$⟩ˡ ( perm ⟨$⟩ʳ x ) ≡⟨ cong (λ k → perm ⟨$⟩ˡ k ) px=0 ⟩ perm ⟨$⟩ˡ zero ≡⟨ p0=0 ⟩ zero - ∎ + ∎ where + open ≡-Reasoning sh2 : {n : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → {x : Fin n} → ¬ perm ⟨$⟩ˡ (suc x) ≡ zero sh2 perm p0=0 {x} eq with shlem→ perm p0=0 (suc x) eq @@ -469,62 +474,85 @@ shrink : {n : ℕ} → (perm : Permutation (suc n) (suc n) ) → perm ⟨$⟩ˡ (# 0) ≡ # 0 → Permutation n n shrink {n} perm p0=0 = permutation p→ p← piso← piso→ where + p00 : (x : Fin n) → (c : 0 < toℕ (perm ⟨$⟩ʳ (suc x) ) ) → Data.Nat.pred (toℕ (Inverse.to perm (suc x))) < n + p00 x c = sx≤py→x≤y ( begin + suc (suc (Data.Nat.pred (toℕ (Inverse.to perm (suc x))))) ≡⟨ cong suc (sucprd c) ⟩ + suc (toℕ (Inverse.to perm (suc x))) ≤⟨ fin<n ⟩ + suc n ∎ ) where + open Data.Nat.Properties.≤-Reasoning + + p01 : (x : Fin n) → (c : 0 < toℕ (perm ⟨$⟩ˡ (suc x) ) ) → Data.Nat.pred (toℕ (Inverse.from perm (suc x))) < n + p01 x c = sx≤py→x≤y ( begin + suc (suc (Data.Nat.pred (toℕ (Inverse.from perm (suc x))))) ≡⟨ cong suc (sucprd c) ⟩ + suc (toℕ (Inverse.from perm (suc x))) ≤⟨ fin<n ⟩ + suc n ∎ ) where + open Data.Nat.Properties.≤-Reasoning + p→ : Fin n → Fin n - p→ x with perm ⟨$⟩ʳ (suc x) | inspect (_⟨$⟩ʳ_ perm ) (suc x) - p→ x | zero | record { eq = e } = ⊥-elim ( sh1 perm p0=0 {x} e ) - p→ x | suc t | _ = t + p→ x with <-fcmp (perm ⟨$⟩ʳ (suc x) ) (# 0) + p→ x | tri≈ ¬a b ¬c = ⊥-elim (sh1 perm p0=0 b) + p→ x | tri> ¬a ¬b c = fromℕ< {Data.Nat.pred (toℕ (Inverse.to perm (suc x)))} (p00 x c) p← : Fin n → Fin n - p← x with perm ⟨$⟩ˡ (suc x) | inspect (_⟨$⟩ˡ_ perm ) (suc x) - p← x | zero | record { eq = e } = ⊥-elim ( sh2 perm p0=0 {x} e ) - p← x | suc t | _ = t + p← x with <-fcmp (perm ⟨$⟩ˡ (suc x)) (# 0) + p← x | tri≈ ¬a b ¬c = ⊥-elim (sh2 perm p0=0 b) + p← x | tri> ¬a ¬b c = fromℕ< {Data.Nat.pred (toℕ (Inverse.from perm (suc x)))} (p01 x c) + -- using "with" something binded in ≡ is prohibited piso← : (x : Fin n ) → p→ ( p← x ) ≡ x - piso← x with perm ⟨$⟩ˡ (suc x) | inspect (_⟨$⟩ˡ_ perm ) (suc x) - piso← x | zero | record { eq = e } = ⊥-elim ( sh2 perm p0=0 {x} e ) - piso← x | suc t | _ with perm ⟨$⟩ʳ (suc t) | inspect (_⟨$⟩ʳ_ perm ) (suc t) - piso← x | suc t | _ | zero | record { eq = e } = ⊥-elim ( sh1 perm p0=0 e ) - piso← x | suc t | record { eq = e0 } | suc t1 | record { eq = e1 } = begin - t1 - ≡⟨ plem0 plem1 ⟩ - x - ∎ where - open ≡-Reasoning - plem0 : suc t1 ≡ suc x → t1 ≡ x - plem0 refl = refl - plem1 : suc t1 ≡ suc x - plem1 = begin - suc t1 - ≡⟨ sym e1 ⟩ - Inverse.to perm _ - ≡⟨ cong (λ k → Inverse.to perm k ) (sym e0) ⟩ - Inverse.to perm ( Inverse.from perm _ ) - ≡⟨ inverseʳ perm ⟩ - suc x - ∎ + piso← x = p02 _ _ refl refl where + p02 : (y z : Fin n) → p← x ≡ y → p→ y ≡ z → z ≡ x + p02 y z px=y py=z with <-fcmp (perm ⟨$⟩ˡ (suc x)) (# 0) + ... | tri≈ ¬a b ¬c = ⊥-elim (sh2 perm p0=0 b) + ... | tri> ¬a ¬b c with <-fcmp (perm ⟨$⟩ʳ (suc y)) (# 0) + ... | tri≈ ¬a₁ b ¬c = ⊥-elim (sh1 perm p0=0 b) + ... | tri> ¬a₁ ¬b₁ c₁ = ? where + open ≡-Reasoning + p03 : toℕ (Inverse.to perm (suc x)) ≡ suc (toℕ y) + p03 = ? + -- with perm ⟨$⟩ˡ (suc x) in eq + -- ... | t = ? +-- ... | zero = ⊥-elim ( sh2 perm p0=0 {y} eq ) +-- ... | suc s with perm ⟨$⟩ˡ (suc x) in eq1 +-- ... | zero = ⊥-elim ( sh1 perm p0=0 eq1 ) +-- ... | suc t1 = begin +-- ? ≡⟨ ? ⟩ +-- ? ∎ where +-- open ≡-Reasoning +-- plem0 : suc t1 ≡ suc x → t1 ≡ x +-- plem0 refl = refl +-- plem1 : suc t1 ≡ suc x +-- plem1 = begin +-- suc t1 ≡⟨ sym eq1 ⟩ +-- Inverse.to perm _ ≡⟨ cong (λ k → Inverse.to perm k ) (sym ?) ⟩ +-- Inverse.to perm ( Inverse.from perm _ ) ≡⟨ inverseʳ perm ⟩ +-- suc x +-- ∎ +-- piso→ : (x : Fin n ) → p← ( p→ x ) ≡ x - piso→ x with perm ⟨$⟩ʳ (suc x) | inspect (_⟨$⟩ʳ_ perm ) (suc x) - piso→ x | zero | record { eq = e } = ⊥-elim ( sh1 perm p0=0 {x} e ) - piso→ x | suc t | _ with perm ⟨$⟩ˡ (suc t) | inspect (_⟨$⟩ˡ_ perm ) (suc t) - piso→ x | suc t | _ | zero | record { eq = e } = ⊥-elim ( sh2 perm p0=0 e ) - piso→ x | suc t | record { eq = e0 } | suc t1 | record { eq = e1 } = begin - t1 - ≡⟨ plem2 plem3 ⟩ - x - ∎ where - plem2 : suc t1 ≡ suc x → t1 ≡ x - plem2 refl = refl - plem3 : suc t1 ≡ suc x - plem3 = begin - suc t1 ≡⟨ sym e1 ⟩ - Inverse.from perm (suc t) ≡⟨ cong (λ k → Inverse.from perm k ) (sym e0 ) ⟩ - Inverse.from perm ((Inverse.to perm (suc x)) ) ≡⟨ cong (λ k → Inverse.from perm (Inverse.to perm (suc x)) ) (sym e0 ) ⟩ - Inverse.from perm ( Inverse.to perm _ ) ≡⟨ inverseˡ perm ⟩ - suc x ∎ - + piso→ x = ? +-- with perm ⟨$⟩ʳ (suc x) | inspect (_⟨$⟩ʳ_ perm ) (suc x) +-- piso→ x | zero | record { eq = e } = ⊥-elim ( sh1 perm p0=0 {x} e ) +-- piso→ x | suc t | _ with perm ⟨$⟩ˡ (suc t) | inspect (_⟨$⟩ˡ_ perm ) (suc t) +-- piso→ x | suc t | _ | zero | record { eq = e } = ⊥-elim ( sh2 perm p0=0 e ) +-- piso→ x | suc t | record { eq = e0 } | suc t1 | record { eq = e1 } = begin +-- t1 +-- ≡⟨ plem2 plem3 ⟩ +-- x +-- ∎ where +-- plem2 : suc t1 ≡ suc x → t1 ≡ x +-- plem2 refl = refl +-- plem3 : suc t1 ≡ suc x +-- plem3 = begin +-- suc t1 ≡⟨ sym e1 ⟩ +-- Inverse.from perm (suc t) ≡⟨ cong (λ k → Inverse.from perm k ) (sym e0 ) ⟩ +-- Inverse.from perm ((Inverse.to perm (suc x)) ) ≡⟨ cong (λ k → Inverse.from perm (Inverse.to perm (suc x)) ) (sym e0 ) ⟩ +-- Inverse.from perm ( Inverse.to perm _ ) ≡⟨ inverseˡ perm ⟩ +-- suc x ∎ +-- shrink-iso : { n : ℕ } → {perm : Permutation n n} → shrink (pprep perm) refl =p= perm -shrink-iso {n} {perm} = record { peq = λ q → refl } +shrink-iso {n} {perm} = record { peq = λ q → ? } shrink-iso2 : { n : ℕ } → {perm : Permutation (suc n) (suc n)} → (p=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0) → pprep (shrink perm p=0) =p= perm @@ -536,10 +564,12 @@ perm ⟨$⟩ʳ ( perm ⟨$⟩ˡ zero ) ≡⟨ cong (λ k → perm ⟨$⟩ʳ k ) p=0 ⟩ perm ⟨$⟩ʳ zero - ∎ - s001 (suc q) with perm ⟨$⟩ʳ (suc q) | inspect (_⟨$⟩ʳ_ perm ) (suc q) - ... | zero | record {eq = e} = ⊥-elim (sh1 perm p=0 {q} e) - ... | suc t | e = refl + ∎ where + open ≡-Reasoning + s001 = ? + -- s001 (suc q) with perm ⟨$⟩ʳ (suc q) | inspect (_⟨$⟩ʳ_ perm ) (suc q) + -- ... | zero | record {eq = e} = ⊥-elim (sh1 perm p=0 {q} e) + -- ... | suc t | e = refl shrink-cong : { n : ℕ } → {x y : Permutation (suc n) (suc n)} @@ -547,22 +577,23 @@ → (x=0 : x ⟨$⟩ˡ (# 0) ≡ # 0 ) → (y=0 : y ⟨$⟩ˡ (# 0) ≡ # 0 ) → shrink x x=0 =p= shrink y y=0 shrink-cong {n} {x} {y} x=y x=0 y=0 = record { peq = p002 } where p002 : (q : Fin n) → (shrink x x=0 ⟨$⟩ʳ q) ≡ (shrink y y=0 ⟨$⟩ʳ q) - p002 q with x ⟨$⟩ʳ (suc q) | inspect (_⟨$⟩ʳ_ x ) (suc q) | y ⟨$⟩ʳ (suc q) | inspect (_⟨$⟩ʳ_ y ) (suc q) - p002 q | zero | record { eq = ex } | zero | ey = ⊥-elim ( sh1 x x=0 ex ) - p002 q | zero | record { eq = ex } | suc py | ey = ⊥-elim ( sh1 x x=0 ex ) - p002 q | suc px | ex | zero | record { eq = ey } = ⊥-elim ( sh1 y y=0 ey ) - p002 q | suc px | record { eq = ex } | suc py | record { eq = ey } = p003 ( begin - suc px - ≡⟨ sym ex ⟩ - x ⟨$⟩ʳ (suc q) - ≡⟨ peq x=y (suc q) ⟩ - y ⟨$⟩ʳ (suc q) - ≡⟨ ey ⟩ - suc py - ∎ ) where - p003 : suc px ≡ suc py → px ≡ py - p003 refl = refl - + p002 q = ? +-- p002 q with x ⟨$⟩ʳ (suc q) | inspect (_⟨$⟩ʳ_ x ) (suc q) | y ⟨$⟩ʳ (suc q) | inspect (_⟨$⟩ʳ_ y ) (suc q) +-- p002 q | zero | record { eq = ex } | zero | ey = ⊥-elim ( sh1 x x=0 ex ) +-- p002 q | zero | record { eq = ex } | suc py | ey = ⊥-elim ( sh1 x x=0 ex ) +-- p002 q | suc px | ex | zero | record { eq = ey } = ⊥-elim ( sh1 y y=0 ey ) +-- p002 q | suc px | record { eq = ex } | suc py | record { eq = ey } = p003 ( begin +-- suc px +-- ≡⟨ sym ex ⟩ +-- x ⟨$⟩ʳ (suc q) +-- ≡⟨ peq x=y (suc q) ⟩ +-- y ⟨$⟩ʳ (suc q) +-- ≡⟨ ey ⟩ +-- suc py +-- ∎ ) where +-- p003 : suc px ≡ suc py → px ≡ py +-- p003 refl = refl +-- open import FLutil FL→perm : {n : ℕ } → FL n → Permutation n n @@ -643,7 +674,8 @@ pins ( toℕ≤pred[n] x ) ⟨$⟩ʳ (# 0) ≡⟨ px=x x ⟩ x - ∎ + ∎ where + open ≡-Reasoning x=0 : (perm ∘ₚ flip (pins (toℕ≤pred[n] x))) ⟨$⟩ˡ (# 0) ≡ # 0 x=0 = subst ( λ k → (perm ∘ₚ flip (pins (toℕ≤pred[n] k))) ⟨$⟩ˡ (# 0) ≡ # 0 ) f001 (p=0 perm) x=0' : (pprep (FL→perm fl) ∘ₚ pid) ⟨$⟩ˡ (# 0) ≡ # 0 @@ -671,7 +703,8 @@ perm→FL ( FL→perm fl ) ≡⟨ FL→iso fl ⟩ fl - ∎ + ∎ where + open ≡-Reasoning pcong-Fp : {n : ℕ } → {x y : FL n} → x ≡ y → FL→perm x =p= FL→perm y pcong-Fp {n} {x} {x} refl = prefl @@ -691,6 +724,7 @@ ≡⟨⟩ perm ⟨$⟩ʳ q ∎ ) } + where open ≡-Reasoning FL-inject : {n : ℕ } → {g h : Permutation n n } → perm→FL g ≡ perm→FL h → g =p= h FL-inject {n} {g} {h} g=h = record { peq = λ q → ( begin @@ -702,6 +736,7 @@ ≡⟨ peq (FL←iso h) q ⟩ h ⟨$⟩ʳ q ∎ ) } + where open ≡-Reasoning FLpid : {n : ℕ} → (x : Permutation n n) → perm→FL x ≡ FL0 → FL→perm FL0 =p= pid → x =p= pid FLpid x eq p0id = ptrans pf2 (ptrans pf0 p0id ) where @@ -712,4 +747,4 @@ pFL0 : {n : ℕ } → FL0 {n} ≡ perm→FL pid pFL0 {zero} = refl -pFL0 {suc n} = cong (λ k → zero :: k ) pFL0 +pFL0 {suc n} = cong (λ k → zero :: k ) ? -- pFL0
--- a/src/fin.agda Mon Sep 18 13:19:37 2023 +0900 +++ b/src/fin.agda Tue Sep 19 11:11:38 2023 +0900 @@ -104,6 +104,10 @@ -- lemma10 : {n i j : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → fromℕ< i<n ≡ fromℕ< j<n -- lemma10 {n} refl = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8 refl )) +lemma10 : {n i j : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → fromℕ< i<n ≡ fromℕ< j<n +lemma10 {.(suc _)} {zero} {zero} refl {s≤s z≤n} {s≤s z≤n} = refl +lemma10 {suc n} {suc i} {suc i} refl {s≤s i<n} {s≤s j<n} = cong suc (lemma10 {n} {i} {i} refl {i<n} {j<n}) + -- lemma31 : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c -- lemma31 {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8 refl) @@ -134,7 +138,6 @@ open import Data.List open import Relation.Binary.Definitions - ----- -- -- find duplicate element in a List (Fin n)