Mercurial > hg > Members > kono > Proof > galois

changeset 26:fb9dcee4ed86

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 Wed, 19 Aug 2020 10:17:12 +0900
parents fab3609ac3f3
children e26c4a3bbea0
files Symmetric.agda
diffstat 1 files changed, 35 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/Symmetric.agda	Wed Aug 19 09:29:06 2020 +0900
+++ b/Symmetric.agda	Wed Aug 19 10:17:12 2020 +0900
@@ -94,15 +94,43 @@
    p→ x | tri≈ ¬a b ¬c = fromℕ≤ a<sa
    p→ x | tri> ¬a ¬b c =  fin+1 (perm ⟨$⟩ʳ (fromℕ≤ (pred<n {_} {x} 0<s  )))
 
-   pincl : ((x  : Fin (suc (suc n))) → Fin (suc (suc n)))
-       ∧ (( p←i : Fin (suc (suc n))  → Fin (suc (suc n))) →  (x y : Fin (suc (suc n)) ) → p→ y ≡ x  → p←i (p→ y)   ≡ y )
-       ∧ (( p←i : Fin (suc (suc n))  → Fin (suc (suc n))) →  (x : Fin (suc (suc n)) )               → p→ (p←i x)   ≡ x )
-   pincl = {!!}
+   record Pincl : Set (Level.suc (Level.zero)) where
+     field
+       p←i    : (x  : Fin (suc (suc n))) → Fin (suc (suc n))
+       piso←i : (x y : Fin (suc (suc n)) ) → p→ y ≡ x  → p←i (p→ y)   ≡ y 
+       piso→i : (x : Fin (suc (suc n)) )               → p→ (p←i x)   ≡ x 
+
+   open Pincl
+
+   pincl : Pincl
+   pincl = record { p←i = p←i0 ; piso←i = p2 ; piso→i = p3 } where
+      p←i0 : (x  : Fin (suc (suc n))) → Fin (suc (suc n))
+      p←i0 x = p0 (suc n) a<sa where
+          p0 : (i : ℕ ) → i < suc (suc n) → Fin (suc (suc n))
+          p0 zero _ = zero
+          p0 (suc i) i<n with fcmp (fromℕ≤ i<n) ( p→ x )
+          p0 (suc i) (s≤s i<n) | tri< a ¬b ¬c = p0 i ( <-trans i<n a<sa )
+          p0 (suc i) i<n | tri≈ ¬a b ¬c = p→ x
+          p0 (suc i) (s≤s i<n) | tri> ¬a ¬b c = p0 i ( <-trans i<n a<sa )
+      p2 :  (x y : Fin (suc (suc n)) ) → p→ y ≡ x  → p←i0 (p→ y)   ≡ y 
+      p2 = {!!}
+      p3 :  (x : Fin (suc (suc n)) )               → p→ (p←i0 x)   ≡ x 
+      p3 x = p30 (suc n) a<sa where
+          p30 : (i : ℕ ) → i < suc (suc n) → p→ (p←i0 x)   ≡ x
+          p30 zero _ = {!!}
+          p30 (suc i) i<n with fcmp (fromℕ≤ i<n) ( p→ x )
+          p30 (suc i) (s≤s i<n) | tri< a ¬b ¬c = p30 i ( <-trans i<n a<sa )
+          p30 (suc i) i<n | tri≈ ¬a b ¬c = begin
+              p→ (p←i0 x)
+           ≡⟨ {!!} ⟩
+              x
+           ∎ where open ≡-Reasoning
+          p30 (suc i) (s≤s i<n) | tri> ¬a ¬b c = p30 i ( <-trans i<n a<sa )
 
    open _∧_
    p← : Fin (suc (suc n)) → Fin (suc (suc n))
-   p← = proj1 pincl
+   p← = p←i pincl
    piso← : (x : Fin (suc (suc n))) → p← ( p→ x ) ≡ x
-   piso← x = proj1 (proj2 pincl) p← (p→ x) x refl
+   piso← x = piso←i pincl (p→ x) x refl
    piso→ : (x : Fin (suc (suc n))) → p→ ( p← x ) ≡ x
-   piso→ = proj2 (proj2 pincl) p←
+   piso→ = piso→i pincl