Mercurial > hg > Members > kono > Proof > galois

comparison FLutil.agda @ 235:d204b7f9b89a

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 Wed, 09 Dec 2020 10:45:41 +0900
parents 9f86424a09b1
children 2b7b343616af
comparison
equal deleted inserted replaced
234:3c3619b196dc 235:d204b7f9b89a
91 fmax¬ {suc n} {x} ne with FLcmp x fmax 91 fmax¬ {suc n} {x} ne with FLcmp x fmax
92 ... | tri< a ¬b ¬c = a 92 ... | tri< a ¬b ¬c = a
93 ... | tri≈ ¬a b ¬c = ⊥-elim ( ne b) 93 ... | tri≈ ¬a b ¬c = ⊥-elim ( ne b)
94 ... | tri> ¬a ¬b c = ⊥-elim (fmax< c) 94 ... | tri> ¬a ¬b c = ⊥-elim (fmax< c)
95 95
96 FL0≤ : {n : ℕ } → FL0 {n} f≤ fmax 96 x≤fmax : {n : ℕ } → {x : FL n} → x f≤ fmax
97 FL0≤ {zero} = case1 refl 97 x≤fmax {n} {x} with FLcmp x fmax
98 FL0≤ {suc zero} = case1 refl 98 ... | tri< a ¬b ¬c = case2 a
99 FL0≤ {suc n} with <-fcmp zero (fromℕ< {n} a<sa) 99 ... | tri≈ ¬a b ¬c = case1 b
100 ... | tri< a ¬b ¬c = case2 (f<n a) 100 ... | tri> ¬a ¬b c = ⊥-elim ( fmax< c )
101 ... | tri≈ ¬a b ¬c with FL0≤ {n}
102 ... | case1 x = case1 (subst₂ (λ j k → (zero :: FL0) ≡ (j :: k ) ) b x refl )
103 ... | case2 x = case2 (subst (λ k → (zero :: FL0) f< (k :: fmax)) b (f<t x) )
104 101
105 open import Data.Nat.Properties using ( ≤-trans ; <-trans ) 102 open import Data.Nat.Properties using ( ≤-trans ; <-trans )
106 fsuc : { n : ℕ } → (x : FL n ) → x f< fmax → FL n 103 fsuc : { n : ℕ } → (x : FL n ) → x f< fmax → FL n
107 fsuc {n} (x :: y) (f<n lt) = fromℕ< fsuc1 :: y where 104 fsuc {n} (x :: y) (f<n lt) = fromℕ< fsuc1 :: y where
108 fsuc1 : suc (toℕ x) < n 105 fsuc1 : suc (toℕ x) < n