Mercurial > hg > Members > kono > Proof > galois
diff FLutil.agda @ 131:d6ae92b8b5bc
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 07 Sep 2020 09:39:50 +0900 (2020-09-07) |
parents | |
children | d84f6d7860f0 |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/FLutil.agda Mon Sep 07 09:39:50 2020 +0900 @@ -0,0 +1,106 @@ +{-# OPTIONS --allow-unsolved-metas #-} +module FLutil where + +open import Level hiding ( suc ; zero ) +open import Algebra +open import Algebra.Structures +open import Data.Fin hiding ( _<_ ; _≤_ ; _-_ ; _+_ ; _≟_) +open import Data.Fin.Properties hiding ( <-trans ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp ) +open import Data.Fin.Permutation +open import Function hiding (id ; flip) +open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) +open import Function.LeftInverse using ( _LeftInverseOf_ ) +open import Function.Equality using (Π) +open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n ) +open import Data.Nat.Properties -- using (<-trans) +open import Relation.Binary.PropositionalEquality +-- open import Data.List using (List; []; _∷_ ; length ; _++_ ; head ; tail ) renaming (reverse to rev ) +open import nat + +open import Symmetric + + +open import Relation.Nullary +open import Data.Empty +open import Relation.Binary.Core +open import Relation.Binary.Definitions +open import fin +open import Putil +open import Gutil +open import Solvable + +open import Relation.Nary using (⌊_⌋; fromWitness) +open import Data.List.Fresh +-- open import Data.List.Fresh.Relation.Unary.All +-- open import Data.List.Fresh.Membership.Setoid +-- open import Data.List.Fresh.Properties + + +FList : {n : ℕ } → Set +FList {n} = List# (FL n) ⌊ _f<?_ ⌋ + +fr1 : FList +fr1 = + ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) ∷# + ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) ∷# + ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) ∷# + ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) ∷# + ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) ∷# + ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷# + [] + +fmax : { n : ℕ } → FL n +fmax {zero} = f0 +fmax {suc n} = fromℕ< a<sa :: fmax {n} + +fmax< : { n : ℕ } → {x : FL n } → ¬ (fmax f< x ) +fmax< {suc n} {x :: y} (f<n lt) = nat-≤> (fmax1 x) lt where + fmax1 : {n : ℕ } → (x : Fin (suc n)) → toℕ x ≤ toℕ (fromℕ< {n} a<sa) + fmax1 {zero} zero = z≤n + fmax1 {suc n} zero = z≤n + fmax1 {suc n} (suc x) = s≤s (fmax1 x) +fmax< {suc n} {x :: y} (f<t lt) = fmax< {n} {y} lt + +fmax¬ : { n : ℕ } → {x : FL n } → ¬ ( x ≡ fmax ) → x f< fmax +fmax¬ {zero} {f0} ne = ⊥-elim ( ne refl ) +fmax¬ {suc n} {x} ne with FLcmp x fmax +... | tri< a ¬b ¬c = a +... | tri≈ ¬a b ¬c = ⊥-elim ( ne b) +... | tri> ¬a ¬b c = ⊥-elim (fmax< c) + +FL0 : {n : ℕ } → FL n +FL0 {zero} = f0 +FL0 {suc n} = zero :: FL0 + +open import logic + +FL0< : {n : ℕ } → FL0 {suc n} f≤ fmax +FL0< {zero} = case1 refl +FL0< {suc (suc zero)} = case1 (cong (λ k → zero :: k) ? ) +FL0< {suc n} = {!!} + +fsuc : { n : ℕ } → (x : FL n ) → x f< fmax → FL n +fsuc {n} (x :: y) (f<n lt) = fromℕ< fsuc1 :: y where + fsuc2 : toℕ x < toℕ (fromℕ< a<sa) + fsuc2 = lt + fsuc1 : suc (toℕ x) < n + fsuc1 = ≤-trans (s≤s lt) ( s≤s ( toℕ≤pred[n] (fromℕ< a<sa)) ) +fsuc (x :: y) (f<t lt) = x :: fsuc y lt + +flist : {n : ℕ } → FList {n} +flist {zero} = [] +flist {suc n} = flist0 FL0 {!!} where + flist0 : (x : FL n) → x f< fmax → FList {suc n} + flist0 = {!!} + +fr22 : fsuc (zero :: zero :: f0) (fmax¬ (λ ())) ≡ (suc zero :: zero :: f0) +fr22 = refl + +fr2 = uncons fr1 + +fr3 : FList +fr3 = + ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷# [] + +-- fr4 : FList +-- fr4 = append-# ? ? fr2 fr3