Mercurial > hg > Members > kono > Proof > galois

changeset 27:e26c4a3bbea0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dead end
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 19 Aug 2020 11:23:15 +0900
parents fb9dcee4ed86
children
files Symmetric.agda
diffstat 1 files changed, 17 insertions(+), 22 deletions(-) [+]
line wrap: on
line diff
--- a/Symmetric.agda	Wed Aug 19 10:17:12 2020 +0900
+++ b/Symmetric.agda	Wed Aug 19 11:23:15 2020 +0900
@@ -101,31 +101,26 @@
        piso→i : (x : Fin (suc (suc n)) )               → p→ (p←i x)   ≡ x 
 
    open Pincl
+   open _∧_
 
    pincl : Pincl
-   pincl = record { p←i = p←i0 ; piso←i = p2 ; piso→i = p3 } where
+   pincl = record { p←i = λ x → proj1 (p←i0 x)
+         ; piso←i = λ x y p=x → proj1 (proj2 (p←i0 x) ) x y _ p=x
+         ; piso→i = λ x → proj2 (proj2 (p←i0 x) ) x (proj1 (p←i0 x)) } 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 )
+          ∧ ( (x y p : Fin (suc (suc n))) → p→ y ≡ x → p ≡ y  )
+          ∧ ( (x p : Fin (suc (suc n))) → p→ p   ≡ x )
+      p←i0 = p0 (suc n) a<sa where
+          p0 : (i : ℕ ) → i < suc (suc n) →  (x  : Fin (suc (suc n))) → ( Fin (suc (suc n))
+              ∧ ( (x y p : Fin (suc (suc n))) → p→ y ≡ x → p ≡ y  )
+              ∧ ( (x p : Fin (suc (suc n))) → p→ p ≡ x ))
+          p0 zero _ x = {!!}
+          p0 (suc i) i<n x with fcmp (fromℕ≤ i<n) ( p→ x )
+          p0 (suc i) (s≤s i<n) x | tri< a ¬b ¬c = p0 i ( <-trans i<n a<sa ) x
+          p0 (suc i) (s≤s i<n) x | tri> ¬a ¬b c = p0 i ( <-trans i<n a<sa ) x
+          p0 (suc i) (s≤s i<n) x | tri≈ ¬a b ¬c = ⟪  p→ x , ⟪ {!!} , (λ x1 p → {!!} ) ⟫ ⟫ where
+              lemma-p0 : (i<n : suc i ≤ suc n ) → (p x1 : Fin (suc (suc n)))  → fromℕ≤ (s≤s i<n) ≡  p→ x  → p→ x ≡ x1
+              lemma-p0 = {!!}
 
    open _∧_
    p← : Fin (suc (suc n)) → Fin (suc (suc n))