|
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}) )))
|
|
133
|
93
|
|
|
94 open import Relation.Nary using (⌊_⌋; fromWitness)
|
|
|
95 open import Data.List.Fresh
|
|
134
|
96 open import Data.List.Fresh.Relation.Unary.All
|
|
|
97 open import Data.List.Fresh.Relation.Unary.Any as Any using (Any; here; there)
|
|
|
98
|
|
133
|
99
|
|
|
100 FList : {n : ℕ } → Set
|
|
|
101 FList {n} = List# (FL n) ⌊ _f<?_ ⌋
|
|
|
102
|
|
|
103 fr1 : FList
|
|
|
104 fr1 =
|
|
|
105 ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) ∷#
|
|
|
106 ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) ∷#
|
|
|
107 ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) ∷#
|
|
|
108 ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) ∷#
|
|
|
109 ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷#
|
|
|
110 []
|
|
|
111
|
|
|
112 open import Data.Product
|
|
134
|
113 open import Data.Maybe
|
|
133
|
114
|
|
134
|
115 FLcons : {n : ℕ } → FL n → FList {n} → FList {n}
|
|
|
116 FLcons {zero} f0 y = f0 ∷# []
|
|
|
117 FLcons {suc n} x [] = x ∷# []
|
|
|
118 FLcons {suc n} x (cons a y x₁) with FLcmp x a
|
|
133
|
119 ... | tri≈ ¬a b ¬c = (cons a y x₁)
|
|
134
|
120 ... | tri< a₁ ¬b ¬c = cons x ( cons a y x₁) (FLcons1 x₁) where
|
|
|
121 FLcons1 : a # y → x # (cons a y x₁)
|
|
|
122 FLcons1 ay = ? , ?
|
|
|
123 ... | tri> ¬a ¬b c with FLcons x y
|
|
133
|
124 ... | [] = a ∷# []
|
|
134
|
125 ... | cons a₁ t x₂ = cons a ( cons a₁ t x₂ ) FLcons2 where
|
|
|
126 FLcons2 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ a (cons a₁ t x₂)
|
|
|
127 FLcons2 = {!!} , {!!}
|
|
133
|
128
|
|
134
|
129 fr6 = FLcons ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1
|
|
133
|
130
|
