Mercurial > hg > Members > kono > Proof > galois

changeset 131:d6ae92b8b5bc

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 Mon, 07 Sep 2020 09:39:50 +0900
parents bd924ac0e37d
children d84f6d7860f0
files FLutil.agda Putil.agda fin.agda
diffstat 3 files changed, 113 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/FLutil.agda	Mon Sep 07 09:39:50 2020 +0900
@@ -0,0 +1,106 @@
+{-# OPTIONS --allow-unsolved-metas #-} 
+module FLutil where
+
+open import Level hiding ( suc ; zero )
+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.Permutation
+open import Function hiding (id ; flip)
+open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
+open import Function.LeftInverse  using ( _LeftInverseOf_ )
+open import Function.Equality using (Π)
+open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
+open import Data.Nat.Properties -- using (<-trans)
+open import Relation.Binary.PropositionalEquality 
+-- open import Data.List using (List; []; _∷_ ; length ; _++_ ; head ; tail ) renaming (reverse to rev )
+open import nat
+
+open import Symmetric
+
+
+open import Relation.Nullary
+open import Data.Empty
+open import  Relation.Binary.Core
+open import  Relation.Binary.Definitions
+open import fin
+open import Putil
+open import Gutil
+open import Solvable
+
+open import Relation.Nary using (⌊_⌋; fromWitness)
+open import Data.List.Fresh
+-- open import Data.List.Fresh.Relation.Unary.All
+-- open import Data.List.Fresh.Membership.Setoid
+-- open import Data.List.Fresh.Properties
+
+
+FList : {n : ℕ } → Set
+FList {n} = List# (FL n) ⌊ _f<?_ ⌋
+
+fr1 : FList
+fr1 =
+   ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
+   ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) ∷# 
+   ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
+   ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) ∷# 
+   ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
+   ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷# 
+   []
+
+fmax : { n : ℕ } →  FL n
+fmax {zero} = f0
+fmax {suc n} = fromℕ< a<sa :: fmax {n}
+
+fmax< : { n : ℕ } → {x : FL n } → ¬ (fmax f< x )
+fmax< {suc n} {x :: y} (f<n lt) = nat-≤> (fmax1 x) lt where
+    fmax1 : {n : ℕ } → (x : Fin (suc n)) → toℕ x ≤ toℕ (fromℕ< {n} a<sa)
+    fmax1 {zero} zero = z≤n
+    fmax1 {suc n} zero = z≤n
+    fmax1 {suc n} (suc x) = s≤s (fmax1 x) 
+fmax< {suc n} {x :: y} (f<t lt) = fmax< {n} {y} lt
+
+fmax¬ : { n : ℕ } → {x : FL n } → ¬ ( x ≡ fmax ) → x f< fmax
+fmax¬ {zero} {f0} ne = ⊥-elim ( ne refl ) 
+fmax¬ {suc n} {x} ne with FLcmp x fmax
+... | tri< a ¬b ¬c = a
+... | tri≈ ¬a b ¬c = ⊥-elim ( ne b)
+... | tri> ¬a ¬b c = ⊥-elim (fmax< c)
+
+FL0 : {n : ℕ } → FL n
+FL0 {zero} = f0
+FL0 {suc n} = zero :: FL0
+
+open import logic
+
+FL0< : {n : ℕ } → FL0 {suc n} f≤ fmax
+FL0< {zero} = case1 refl
+FL0< {suc (suc zero)} = case1 (cong (λ k → zero :: k) ? )
+FL0< {suc n} = {!!}
+
+fsuc : { n : ℕ } → (x : FL n ) → x f< fmax → FL n 
+fsuc {n} (x :: y) (f<n lt) = fromℕ< fsuc1 :: y where
+    fsuc2 : toℕ x < toℕ (fromℕ< a<sa) 
+    fsuc2 = lt
+    fsuc1 : suc (toℕ x) < n
+    fsuc1 =  ≤-trans (s≤s lt) ( s≤s ( toℕ≤pred[n] (fromℕ< a<sa)) )
+fsuc (x :: y) (f<t lt) = x :: fsuc y lt
+
+flist : {n : ℕ } → FList {n}
+flist {zero} = []
+flist {suc n} = flist0 FL0 {!!} where
+   flist0 : (x : FL n) → x f< fmax → FList {suc n}
+   flist0 = {!!}
+
+fr22 : fsuc (zero :: zero :: f0) (fmax¬ (λ ())) ≡ (suc zero :: zero :: f0)
+fr22 = refl
+
+fr2 = uncons fr1
+
+fr3 : FList
+fr3 =
+   ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷#  []
+
+-- fr4 : FList
+-- fr4 = append-# ? ? fr2 fr3
--- a/Putil.agda	Sun Sep 06 08:38:06 2020 +0900
+++ b/Putil.agda	Mon Sep 07 09:39:50 2020 +0900
@@ -434,6 +434,9 @@
    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 )
 
+_f≤_ : {n : ℕ } (x : FL n ) (y : FL n)  → Set
+_f≤_ x y = (x ≡ y ) ∨  (x f< y )
+
 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 }
 
--- a/fin.agda	Sun Sep 06 08:38:06 2020 +0900
+++ b/fin.agda	Mon Sep 07 09:39:50 2020 +0900
@@ -3,6 +3,7 @@
 module fin where
 
 open import Data.Fin hiding (_<_ ; _≤_ )
+open import Data.Fin.Properties hiding ( <-trans )
 open import Data.Nat
 open import logic
 open import nat
@@ -32,6 +33,9 @@
 pred<n {suc n} {zero} (s≤s z≤n) = s≤s z≤n
 pred<n {suc n} {suc f} (s≤s z≤n) = fin<n
 
+fin<asa : {n : ℕ} → toℕ (fromℕ< {n} a<sa) ≡ n
+fin<asa = toℕ-fromℕ< nat.a<sa
+
 -- fromℕ<-toℕ
 toℕ→from : {n : ℕ} {x : Fin (suc n)} → toℕ x ≡ n → fromℕ n ≡ x
 toℕ→from {0} {zero} refl = refl