Mercurial > hg > Members > kono > Proof > galois

comparison FLutil.agda @ 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
children d84f6d7860f0
comparison
equal deleted inserted replaced
130:bd924ac0e37d 131:d6ae92b8b5bc
1 {-# OPTIONS --allow-unsolved-metas #-}
2 module FLutil where
3
4 open import Level hiding ( suc ; zero )
5 open import Algebra
6 open import Algebra.Structures
7 open import Data.Fin hiding ( _<_ ; _≤_ ; _-_ ; _+_ ; _≟_)
8 open import Data.Fin.Properties hiding ( <-trans ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp )
9 open import Data.Fin.Permutation
10 open import Function hiding (id ; flip)
11 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
12 open import Function.LeftInverse using ( _LeftInverseOf_ )
13 open import Function.Equality using (Π)
14 open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
15 open import Data.Nat.Properties -- using (<-trans)
16 open import Relation.Binary.PropositionalEquality
17 -- open import Data.List using (List; []; _∷_ ; length ; _++_ ; head ; tail ) renaming (reverse to rev )
18 open import nat
19
20 open import Symmetric
21
22
23 open import Relation.Nullary
24 open import Data.Empty
25 open import Relation.Binary.Core
26 open import Relation.Binary.Definitions
27 open import fin
28 open import Putil
29 open import Gutil
30 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
52 fmax : { n : ℕ } → FL n
53 fmax {zero} = f0
54 fmax {suc n} = fromℕ< a<sa :: fmax {n}
55
56 fmax< : { n : ℕ } → {x : FL n } → ¬ (fmax f< x )
57 fmax< {suc n} {x :: y} (f<n lt) = nat-≤> (fmax1 x) lt where
58 fmax1 : {n : ℕ } → (x : Fin (suc n)) → toℕ x ≤ toℕ (fromℕ< {n} a<sa)
59 fmax1 {zero} zero = z≤n
60 fmax1 {suc n} zero = z≤n
61 fmax1 {suc n} (suc x) = s≤s (fmax1 x)
62 fmax< {suc n} {x :: y} (f<t lt) = fmax< {n} {y} lt
63
64 fmax¬ : { n : ℕ } → {x : FL n } → ¬ ( x ≡ fmax ) → x f< fmax
65 fmax¬ {zero} {f0} ne = ⊥-elim ( ne refl )
66 fmax¬ {suc n} {x} ne with FLcmp x fmax
67 ... | tri< a ¬b ¬c = a
68 ... | tri≈ ¬a b ¬c = ⊥-elim ( ne b)
69 ... | tri> ¬a ¬b c = ⊥-elim (fmax< c)
70
71 FL0 : {n : ℕ } → FL n
72 FL0 {zero} = f0
73 FL0 {suc n} = zero :: FL0
74
75 open import logic
76
77 FL0< : {n : ℕ } → FL0 {suc n} f≤ fmax
78 FL0< {zero} = case1 refl
79 FL0< {suc (suc zero)} = case1 (cong (λ k → zero :: k) ? )
80 FL0< {suc n} = {!!}
81
82 fsuc : { n : ℕ } → (x : FL n ) → x f< fmax → FL n
83 fsuc {n} (x :: y) (f<n lt) = fromℕ< fsuc1 :: y where
84 fsuc2 : toℕ x < toℕ (fromℕ< a<sa)
85 fsuc2 = lt
86 fsuc1 : suc (toℕ x) < n
87 fsuc1 = ≤-trans (s≤s lt) ( s≤s ( toℕ≤pred[n] (fromℕ< a<sa)) )
88 fsuc (x :: y) (f<t lt) = x :: fsuc y lt
89
90 flist : {n : ℕ } → FList {n}
91 flist {zero} = []
92 flist {suc n} = flist0 FL0 {!!} where
93 flist0 : (x : FL n) → x f< fmax → FList {suc n}
94 flist0 = {!!}
95
96 fr22 : fsuc (zero :: zero :: f0) (fmax¬ (λ ())) ≡ (suc zero :: zero :: f0)
97 fr22 = refl
98
99 fr2 = uncons fr1
100
101 fr3 : FList
102 fr3 =
103 ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷# []
104
105 -- fr4 : FList
106 -- fr4 = append-# ? ? fr2 fr3