|
131
|
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 open import Relation.Nullary
|
|
|
23 open import Data.Empty
|
|
|
24 open import Relation.Binary.Core
|
|
|
25 open import Relation.Binary.Definitions
|
|
|
26 open import fin
|
|
|
27 open import Putil
|
|
|
28 open import Gutil
|
|
|
29 open import Solvable
|
|
|
30
|
|
|
31 fmax : { n : ℕ } → FL n
|
|
|
32 fmax {zero} = f0
|
|
|
33 fmax {suc n} = fromℕ< a<sa :: fmax {n}
|
|
|
34
|
|
|
35 fmax< : { n : ℕ } → {x : FL n } → ¬ (fmax f< x )
|
|
|
36 fmax< {suc n} {x :: y} (f<n lt) = nat-≤> (fmax1 x) lt where
|
|
|
37 fmax1 : {n : ℕ } → (x : Fin (suc n)) → toℕ x ≤ toℕ (fromℕ< {n} a<sa)
|
|
|
38 fmax1 {zero} zero = z≤n
|
|
|
39 fmax1 {suc n} zero = z≤n
|
|
|
40 fmax1 {suc n} (suc x) = s≤s (fmax1 x)
|
|
|
41 fmax< {suc n} {x :: y} (f<t lt) = fmax< {n} {y} lt
|
|
|
42
|
|
|
43 fmax¬ : { n : ℕ } → {x : FL n } → ¬ ( x ≡ fmax ) → x f< fmax
|
|
|
44 fmax¬ {zero} {f0} ne = ⊥-elim ( ne refl )
|
|
|
45 fmax¬ {suc n} {x} ne with FLcmp x fmax
|
|
|
46 ... | tri< a ¬b ¬c = a
|
|
|
47 ... | tri≈ ¬a b ¬c = ⊥-elim ( ne b)
|
|
|
48 ... | tri> ¬a ¬b c = ⊥-elim (fmax< c)
|
|
|
49
|
|
|
50 FL0 : {n : ℕ } → FL n
|
|
|
51 FL0 {zero} = f0
|
|
|
52 FL0 {suc n} = zero :: FL0
|
|
|
53
|
|
|
54 open import logic
|
|
|
55
|
|
132
|
56 FL0≤ : {n : ℕ } → FL0 {n} f≤ fmax
|
|
|
57 FL0≤ {zero} = case1 refl
|
|
|
58 FL0≤ {suc zero} = case1 refl
|
|
|
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) )
|
|
131
|
64
|
|
|
65 fsuc : { n : ℕ } → (x : FL n ) → x f< fmax → FL n
|
|
|
66 fsuc {n} (x :: y) (f<n lt) = fromℕ< fsuc1 :: y where
|
|
|
67 fsuc2 : toℕ x < toℕ (fromℕ< a<sa)
|
|
|
68 fsuc2 = lt
|
|
|
69 fsuc1 : suc (toℕ x) < n
|
|
|
70 fsuc1 = ≤-trans (s≤s lt) ( s≤s ( toℕ≤pred[n] (fromℕ< a<sa)) )
|
|
|
71 fsuc (x :: y) (f<t lt) = x :: fsuc y lt
|
|
|
72
|
|
132
|
73 open import Data.List
|
|
|
74
|
|
|
75 flist1 : {n : ℕ } (i : ℕ) → i < suc n → List (FL n) → List (FL n) → List (FL (suc n))
|
|
|
76 flist1 zero i<n [] _ = []
|
|
|
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)
|
|
131
|
84
|
|
|
85 fr22 : fsuc (zero :: zero :: f0) (fmax¬ (λ ())) ≡ (suc zero :: zero :: f0)
|
|
|
86 fr22 = refl
|
|
|
87
|
|
132
|
88 fr4 : List (FL 4)
|
|
|
89 fr4 = Data.List.reverse (flist (fmax {4}) )
|
|
131
|
90
|
|
132
|
91 fr5 : List (List ℕ)
|
|
|
92 fr5 = map plist (map FL→perm (Data.List.reverse (flist (fmax {4}) )))
|
