Mercurial > hg > Members > kono > Proof > galois

comparison FLutil.agda @ 132:d84f6d7860f0

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 20:27:35 +0900
parents d6ae92b8b5bc
children 90cd3dd0f09b
comparison
equal deleted inserted replaced
131:d6ae92b8b5bc 132:d84f6d7860f0
17 -- open import Data.List using (List; []; _∷_ ; length ; _++_ ; head ; tail ) renaming (reverse to rev ) 17 -- open import Data.List using (List; []; _∷_ ; length ; _++_ ; head ; tail ) renaming (reverse to rev )
18 open import nat 18 open import nat
19 19
20 open import Symmetric 20 open import Symmetric
21 21
22
23 open import Relation.Nullary 22 open import Relation.Nullary
24 open import Data.Empty 23 open import Data.Empty
25 open import Relation.Binary.Core 24 open import Relation.Binary.Core
26 open import Relation.Binary.Definitions 25 open import Relation.Binary.Definitions
27 open import fin 26 open import fin
28 open import Putil 27 open import Putil
29 open import Gutil 28 open import Gutil
30 open import Solvable 29 open import Solvable
31
32 open import Relation.Nary using (⌊_⌋; fromWitness)
33 open import Data.List.Fresh
34 -- open import Data.List.Fresh.Relation.Unary.All
35 -- open import Data.List.Fresh.Membership.Setoid
36 -- open import Data.List.Fresh.Properties
37
38
39 FList : {n : ℕ } → Set
40 FList {n} = List# (FL n) ⌊ _f<?_ ⌋
41
42 fr1 : FList
43 fr1 =
44 ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) ∷#
45 ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) ∷#
46 ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) ∷#
47 ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) ∷#
48 ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) ∷#
49 ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷#
50 []
51 30
52 fmax : { n : ℕ } → FL n 31 fmax : { n : ℕ } → FL n
53 fmax {zero} = f0 32 fmax {zero} = f0
54 fmax {suc n} = fromℕ< a<sa :: fmax {n} 33 fmax {suc n} = fromℕ< a<sa :: fmax {n}
55 34
72 FL0 {zero} = f0 51 FL0 {zero} = f0
73 FL0 {suc n} = zero :: FL0 52 FL0 {suc n} = zero :: FL0
74 53
75 open import logic 54 open import logic
76 55
77 FL0< : {n : ℕ } → FL0 {suc n} f≤ fmax 56 FL0≤ : {n : ℕ } → FL0 {n} f≤ fmax
78 FL0< {zero} = case1 refl 57 FL0≤ {zero} = case1 refl
79 FL0< {suc (suc zero)} = case1 (cong (λ k → zero :: k) ? ) 58 FL0≤ {suc zero} = case1 refl
80 FL0< {suc n} = {!!} 59 FL0≤ {suc n} with <-fcmp zero (fromℕ< {n} a<sa)
60 ... | tri< a ¬b ¬c = case2 (f<n a)
61 ... | tri≈ ¬a b ¬c with FL0≤ {n}
62 ... | case1 x = case1 (subst₂ (λ j k → (zero :: FL0) ≡ (j :: k ) ) b x refl )
63 ... | case2 x = case2 (subst (λ k → (zero :: FL0) f< (k :: fmax)) b (f<t x) )
81 64
82 fsuc : { n : ℕ } → (x : FL n ) → x f< fmax → FL n 65 fsuc : { n : ℕ } → (x : FL n ) → x f< fmax → FL n
83 fsuc {n} (x :: y) (f<n lt) = fromℕ< fsuc1 :: y where 66 fsuc {n} (x :: y) (f<n lt) = fromℕ< fsuc1 :: y where
84 fsuc2 : toℕ x < toℕ (fromℕ< a<sa) 67 fsuc2 : toℕ x < toℕ (fromℕ< a<sa)
85 fsuc2 = lt 68 fsuc2 = lt
86 fsuc1 : suc (toℕ x) < n 69 fsuc1 : suc (toℕ x) < n
87 fsuc1 = ≤-trans (s≤s lt) ( s≤s ( toℕ≤pred[n] (fromℕ< a<sa)) ) 70 fsuc1 = ≤-trans (s≤s lt) ( s≤s ( toℕ≤pred[n] (fromℕ< a<sa)) )
88 fsuc (x :: y) (f<t lt) = x :: fsuc y lt 71 fsuc (x :: y) (f<t lt) = x :: fsuc y lt
89 72
90 flist : {n : ℕ } → FList {n} 73 open import Data.List
91 flist {zero} = [] 74
92 flist {suc n} = flist0 FL0 {!!} where 75 flist1 : {n : ℕ } (i : ℕ) → i < suc n → List (FL n) → List (FL n) → List (FL (suc n))
93 flist0 : (x : FL n) → x f< fmax → FList {suc n} 76 flist1 zero i<n [] _ = []
94 flist0 = {!!} 77 flist1 zero i<n (a ∷ x ) z = ( zero :: a ) ∷ flist1 zero i<n x z
78 flist1 (suc i) (s≤s i<n) [] z = flist1 i (<-trans i<n a<sa) z z
79 flist1 (suc i) i<n (a ∷ x ) z = ((fromℕ< i<n ) :: a ) ∷ flist1 (suc i) i<n x z
80
81 flist : {n : ℕ } → FL n → List (FL n)
82 flist {zero} f0 = f0 ∷ []
83 flist {suc n} (x :: y) = flist1 n a<sa (flist y) (flist y)
95 84
96 fr22 : fsuc (zero :: zero :: f0) (fmax¬ (λ ())) ≡ (suc zero :: zero :: f0) 85 fr22 : fsuc (zero :: zero :: f0) (fmax¬ (λ ())) ≡ (suc zero :: zero :: f0)
97 fr22 = refl 86 fr22 = refl
98 87
99 fr2 = uncons fr1 88 fr4 : List (FL 4)
89 fr4 = Data.List.reverse (flist (fmax {4}) )
100 90
101 fr3 : FList 91 fr5 : List (List ℕ)
102 fr3 = 92 fr5 = map plist (map FL→perm (Data.List.reverse (flist (fmax {4}) )))
103 ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷# []
104
105 -- fr4 : FList
106 -- fr4 = append-# ? ? fr2 fr3