Mercurial > hg > Members > kono > Proof > galois

changeset 130:bd924ac0e37d

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 Sun, 06 Sep 2020 08:38:06 +0900
parents dae027341d73
children d6ae92b8b5bc
files Putil.agda
diffstat 1 files changed, 39 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Sat Sep 05 10:53:41 2020 +0900
+++ b/Putil.agda	Sun Sep 06 08:38:06 2020 +0900
@@ -430,10 +430,40 @@
    f0 :  FL 0 
    _::_ :  { n : ℕ } → Fin (suc n ) → FL n → FL (suc n)
 
---
--- shrink operation ( reverse of pprep )
---
---     shrink (pprep perm)  refl =p=  perm
+data _f<_  : {n : ℕ } (x : FL n ) (y : FL n)  → Set  where
+   f<n : {m : ℕ } {xn yn : Fin (suc m) } {xt yt : FL m} → xn Data.Fin.< yn →   (xn :: xt) f< ( yn :: yt )
+   f<t : {m : ℕ } {xn : Fin (suc m) } {xt yt : FL m} → xt f< yt →   (xn :: xt) f< ( xn :: yt )
+
+FLeq : {n : ℕ } {xn yn : Fin (suc n)} {x : FL n } {y : FL n}  → xn :: x ≡ yn :: y → ( xn ≡ yn ) ∧ (x ≡ y )
+FLeq refl = record { proj1 = refl ; proj2  = refl }
+
+f<> :  {n : ℕ } {x : FL n } {y : FL n}  → x f< y → y f< x → ⊥
+f<> (f<n x) (f<n x₁) = nat-<> x x₁
+f<> (f<n x) (f<t lt2) = nat-≡< refl x
+f<> (f<t lt) (f<n x) = nat-≡< refl x
+f<> (f<t lt) (f<t lt2) = f<> lt lt2
+
+f-≡< :  {n : ℕ } {x : FL n } {y : FL n}  → x ≡ y → y f< x → ⊥
+f-≡< refl (f<n x) = nat-≡< refl x
+f-≡< refl (f<t lt) = f-≡< refl lt 
+
+FLcmp : {n : ℕ } → Trichotomous {Level.zero} {FL n}  _≡_  _f<_
+FLcmp f0 f0 = tri≈ (λ ()) refl (λ ())
+FLcmp (xn :: xt) (yn :: yt) with <-fcmp xn yn
+... | tri< a ¬b ¬c = tri< (f<n a) (λ eq → nat-≡< (cong toℕ (proj1 (FLeq eq)) ) a) (λ lt  → f<> lt (f<n a) )
+... | tri> ¬a ¬b c = tri> (λ lt  → f<> lt (f<n c) ) (λ eq → nat-≡< (cong toℕ (sym (proj1 (FLeq eq)) )) c) (f<n c)
+... | tri≈ ¬a refl ¬c with FLcmp xt yt
+... | tri< a ¬b ¬c₁ = tri< (f<t a) (λ eq → ¬b (proj2 (FLeq eq) )) (λ lt  → f<> lt (f<t a) )
+... | tri≈ ¬a₁ refl ¬c₁ = tri≈ (λ lt → f-≡< refl lt )  refl (λ lt → f-≡< refl lt )
+... | tri> ¬a₁ ¬b c = tri> (λ lt  → f<> lt (f<t c) ) (λ eq → ¬b (proj2 (FLeq eq) )) (f<t c)
+
+infixr 250 _f<?_
+
+_f<?_ : {n  : ℕ} → (x y : FL n ) → Dec (x f< y )
+x f<? y with FLcmp x y
+... | tri< a ¬b ¬c = yes a
+... | tri≈ ¬a refl ¬c = no ( ¬a )
+... | tri> ¬a ¬b c = no ( ¬a )
 
 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
@@ -442,7 +472,7 @@
           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
@@ -450,7 +480,7 @@
           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
@@ -592,6 +622,9 @@
 perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) ) 
 -- perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (remove (# 0) perm)  
 
+_p<_ : {n : ℕ } ( x y : Permutation n n ) → Set
+x p< y = perm→FL x f<  perm→FL y
+
 pcong-pF : {n : ℕ }  → {x y : Permutation n n}  → x =p= y → perm→FL x ≡ perm→FL y
 pcong-pF {zero} eq = refl
 pcong-pF {suc n} {x} {y} eq = cong₂ (λ j k → j :: k ) ( peq eq (# 0)) (pcong-pF (shrink-cong (presp eq p001 ) (p=0 x) (p=0 y))) where