Members/kono/Proof/galois: Putil.agda comparison

comparison Putil.agda @ 91:482ef04890f8

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Sat, 29 Aug 2020 07:48:45 +0900
parents	bb8c5b366219
children	2e5d0b142eca

comparison

equal deleted inserted replaced

-:bb8c5b366219
+:482ef04890f8
 pins {suc _} {suc zero} _ = pswap pid
 pins {suc (suc n)} {suc m} (s≤s m<n) =  pins1 (suc m) (suc (suc n)) lem0 where
 pins1 : (i j : ℕ ) → j ≤ suc (suc n)  → Permutation (suc (suc (suc n ))) (suc (suc (suc n)))
 pins1 _ zero _ = pid
 pins1 zero _ _ = pid
-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 refl-≤s )
+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
 pins'  : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n)
 pins' {_} {zero} _ = pid
 pins' {suc n} {suc m} (s≤s  m≤n) = permutation p← p→  record { left-inverse-of = piso← ; right-inverse-of = piso→ } where
 next : Fin (suc (suc n)) → Fin (suc (suc n))
 next zero = suc zero
-next (suc x) = fromℕ< (≤-trans (fin<n {_} {x} ) refl-≤s )
+next (suc x) = fromℕ< (≤-trans (fin<n {_} {x} ) a≤sa )
 p→ : Fin (suc (suc n)) → Fin (suc (suc n))
 p→ x with <-cmp (toℕ x) (suc m)
 ... | tri< a ¬b ¬c = fromℕ< (≤-trans (s≤s  a) (s≤s (s≤s  m≤n) ))
 ... | tri≈ ¬a b ¬c = zero
 ... | tri> ¬a ¬b c = x
 p← : Fin (suc (suc n)) → Fin (suc (suc n))
 p← zero = fromℕ< (s≤s (s≤s m≤n))
 p← (suc x) with <-cmp (toℕ x) (suc m)
-... | tri< a ¬b ¬c = fromℕ< (≤-trans (fin<n {_} {x}) refl-≤s )
+... | tri< a ¬b ¬c = fromℕ< (≤-trans (fin<n {_} {x}) a≤sa )
 ... | tri≈ ¬a b ¬c = suc x
 ... | tri> ¬a ¬b c = suc x
 mm : toℕ (fromℕ< {suc m} {suc (suc n)} (s≤s (s≤s m≤n))) ≡ suc m
 mm = toℕ-fromℕ< (s≤s (s≤s  m≤n))
-mma : (x : Fin (suc n) ) → suc (toℕ x) ≤ suc m → toℕ ( fromℕ< (≤-trans (fin<n {_} {x}) refl-≤s ) ) ≤ m
+mma : (x : Fin (suc n) ) → suc (toℕ x) ≤ suc m → toℕ ( fromℕ< (≤-trans (fin<n {_} {x}) a≤sa ) ) ≤ m
-mma x (s≤s x<sm) = subst (λ k → k ≤ m) (sym (toℕ-fromℕ< (≤-trans fin<n refl-≤s ) )) x<sm
+mma x (s≤s x<sm) = subst (λ k → k ≤ m) (sym (toℕ-fromℕ< (≤-trans fin<n a≤sa ) )) x<sm
+p3 : (x : Fin (suc n) ) →  toℕ (fromℕ< (≤-trans (fin<n {_} {suc x} ) (s≤s a≤sa))) ≡ suc (toℕ x)
+p3 x = begin
+toℕ (fromℕ< (≤-trans (fin<n {_} {suc x} ) (s≤s a≤sa)))
+≡⟨ toℕ-fromℕ< ( s≤s ( ≤-trans fin<n  a≤sa ) ) ⟩
+suc (toℕ x)
+∎
 piso← : (x : Fin (suc (suc n)) ) → p→ ( p← x ) ≡ x
 piso← zero with <-cmp (toℕ (fromℕ< (s≤s (s≤s m≤n)))) (suc m) | mm
 ... | tri< a ¬b ¬c | t = ⊥-elim ( ¬b t )
 ... | tri≈ ¬a b ¬c | t = refl
 ... | tri> ¬a ¬b c | t = ⊥-elim ( ¬b t )
 piso← (suc x) with <-cmp (toℕ x) (suc m)
-... | tri≈ ¬a b ¬c = ?
+... | tri> ¬a ¬b c with <-cmp (toℕ (suc x)) (suc m)
-... | tri> ¬a ¬b c = {!!}
+... | tri< a ¬b₁ ¬c = ⊥-elim ( nat-<> a (<-trans c a<sa ) )
-... | tri< a ¬b ¬c with <-cmp (toℕ ( fromℕ< (≤-trans (fin<n {_} {x}) refl-≤s ) )) (suc m)
+... | tri≈ ¬a₁ b ¬c = ⊥-elim (  nat-≡< (sym b) (<-trans c a<sa ))
+... | tri> ¬a₁ ¬b₁ c₁ = refl
+piso← (suc x) | tri≈ ¬a b ¬c with <-cmp (toℕ (suc x)) (suc m)
+... | tri< a ¬b ¬c₁ = ⊥-elim (  nat-≡< b (<-trans a<sa a) )
+... | tri≈ ¬a₁ refl ¬c₁ = ⊥-elim ( nat-≡< b a<sa )
+... | tri> ¬a₁ ¬b c = refl
+piso← (suc x) | tri< a ¬b ¬c with <-cmp (toℕ ( fromℕ< (≤-trans (fin<n {_} {x}) a≤sa ) )) (suc m)
 ... | tri≈ ¬a b ¬c₁ = ⊥-elim ( ¬a (s≤s (mma x a)))
 ... | tri> ¬a ¬b₁ c = ⊥-elim ( ¬a (s≤s (mma x a)))
 ... | tri< a₁ ¬b₁ ¬c₁ = p0 where
 p2 : suc (suc (toℕ x)) ≤ suc (suc n)
 p2 = s≤s (fin<n {suc n} {x})
-p6 : suc (toℕ (fromℕ< (≤-trans (fin<n {_} {suc x}) (s≤s refl-≤s)))) ≤ suc (suc n)
+p6 : suc (toℕ (fromℕ< (≤-trans (fin<n {_} {suc x}) (s≤s a≤sa)))) ≤ suc (suc n)
 p6 = s≤s (≤-trans a₁ (s≤s m≤n))
-p3 :   toℕ (fromℕ< (≤-trans (fin<n {_} {suc x} ) (s≤s refl-≤s))) ≡ suc (toℕ x)
-p3 = begin
-toℕ (fromℕ< (≤-trans (fin<n {_} {suc x} ) (s≤s refl-≤s)))
-≡⟨ toℕ-fromℕ< ( s≤s ( ≤-trans fin<n  refl-≤s ) ) ⟩
-suc (toℕ x)
-∎ where open ≡-Reasoning
 p0 : fromℕ< (≤-trans (s≤s  a₁) (s≤s (s≤s  m≤n) ))  ≡ suc x
 p0 = begin
 fromℕ< (≤-trans (s≤s  a₁) (s≤s (s≤s  m≤n) ))
 ≡⟨⟩
 fromℕ< (s≤s (≤-trans a₁ (s≤s m≤n)))
-≡⟨ lemma10 p3 {p6} {p2} ⟩
+≡⟨ lemma10 (p3 x) {p6} {p2} ⟩
 fromℕ< ( s≤s (fin<n {suc n} {x}) )
-≡⟨ lemma3 {toℕ x} {suc n} (fin<n {suc (n)} {x})  ⟩
+≡⟨⟩
 suc (fromℕ< (fin<n {suc n} {x} ))
-≡⟨ cong suc (fromℕ<-toℕ x (fin<n {suc n} {x}) ) ⟩
+≡⟨ cong suc (fromℕ<-toℕ x _ ) ⟩
 suc x
-∎ where open ≡-Reasoning
+∎
 piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x
 piso→ = {!!}
 x ⟨$⟩ʳ zero
 ≡⟨ toℕ-injective (headeq eq) ⟩
 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 )
 ... | tri≈ ¬a b ¬c = begin
 x ⟨$⟩ʳ q
 ≡⟨ toℕ-injective pleq2  ⟩
 y ⟨$⟩ʳ (suc (fromℕ< i<sn))
 ≡⟨ 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
 ≡⟨ b ⟩
 suc i
 ≡⟨ sym (toℕ-fromℕ< (s≤s i<sn)) ⟩
 toℕ (fromℕ< (s≤s i<sn))
 ≡⟨⟩
 toℕ (suc (fromℕ< i<sn))
-∎ ) where open ≡-Reasoning
+∎ )
 pleq2 : toℕ ( x ⟨$⟩ʳ (suc (fromℕ< i<sn)) ) ≡ toℕ ( y ⟨$⟩ʳ (suc (fromℕ< i<sn)) )
 pleq2 = headeq eq
 pprep-cong : {n  : ℕ} → {x y : Permutation n n } → x =p= y → pprep x =p= pprep y
 pprep-cong {n} {x} {y} x=y = record { peq = pprep-cong1 } where
 suc ( x ⟨$⟩ʳ q )
 ≡⟨ cong ( λ k → suc k ) ( peq x=y q ) ⟩
 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
 pprep-dist1 : (q : Fin (suc n)) → (pprep (x ∘ₚ y) ⟨$⟩ʳ q) ≡ ((pprep x ∘ₚ pprep y) ⟨$⟩ʳ q)
 pprep-dist1 zero = refl
 suc (suc (x ⟨$⟩ʳ q))
 ≡⟨ cong ( λ k → suc (suc k) ) ( peq x=y q ) ⟩
 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
 pswap-dist1 : (q : Fin (suc (suc n))) → ((pprep (pprep (x ∘ₚ y))) ⟨$⟩ʳ q) ≡ ((pswap x ∘ₚ pswap y) ⟨$⟩ʳ q)
 pswap-dist1 zero = refl
 FL←iso : {n : ℕ }  → (perm : Permutation n n )  → FL→perm ( perm→FL perm  ) =p= perm
 -- FL←iso {0} perm = record { peq = λ () }
 -- FL←iso {suc n} perm = {!!}
 lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n
-lem2 i≤n = ≤-trans i≤n ( refl-≤s )
+lem2 i≤n = ≤-trans i≤n ( a≤sa )
 ∀-FL : (n : ℕ ) → List (FL (suc n))
 ∀-FL  x  = fls6 x  where
 fls4 :  ( i n : ℕ ) → (i<n : i ≤ n ) → FL  n → List (FL  (suc n))  → List (FL  (suc n))
 fls4 zero n i≤n perm x = (zero :: perm ) ∷ x
-fls4 (suc i) n i≤n  perm x = fls4 i n (≤-trans refl-≤s i≤n ) perm ((fromℕ< (s≤s i≤n) :: perm ) ∷ x)
+fls4 (suc i) n i≤n  perm x = fls4 i n (≤-trans a≤sa i≤n ) perm ((fromℕ< (s≤s i≤n) :: perm ) ∷ x)
 fls5 :  ( n : ℕ ) → List (FL n) → List (FL  (suc n))  → List (FL (suc n))
 fls5 n [] x = x
 fls5 n (h ∷ x) y = fls5  n x (fls4 n n lem0 h y)
 fls6 :  ( n : ℕ ) → List (FL  (suc n))
 fls6 zero = (zero :: f0) ∷ []
 lem1 : {i n : ℕ } → i ≤ n → i < suc n
 lem1 z≤n = s≤s z≤n
 lem1 (s≤s lt) = s≤s (lem1 lt)
 pls4 :  ( i n : ℕ ) → (i<n : i ≤ n ) → Permutation n n → List (Permutation (suc n) (suc n))  → List (Permutation (suc n) (suc n))
 pls4 zero n i≤n perm x = (pprep perm ∘ₚ pins i≤n ) ∷ x
-pls4 (suc i) n i≤n  perm x = pls4 i n (≤-trans refl-≤s i≤n ) perm (pprep perm ∘ₚ pins {n} {suc i} i≤n  ∷ x)
+pls4 (suc i) n i≤n  perm x = pls4 i n (≤-trans a≤sa i≤n ) perm (pprep perm ∘ₚ pins {n} {suc i} i≤n  ∷ x)
 pls5 :  ( n : ℕ ) → List (Permutation n n) → List (Permutation (suc n) (suc n))  → List (Permutation (suc n) (suc n))
 pls5 n [] x = x
 pls5 n (h ∷ x) y = pls5  n x (pls4 n n lem0 h y)
 pls6 :  ( n : ℕ ) → List (Permutation (suc n) (suc n))
 pls6 zero = pid ∷ []

Mercurial > hg > Members > kono > Proof > galois

comparison Putil.agda @ 91:482ef04890f8