Mercurial > hg > Members > kono > Proof > galois

changeset 133:90cd3dd0f09b

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 Tue, 08 Sep 2020 07:16:49 +0900
parents d84f6d7860f0
children 98c54cb6ee4f
files FLutil.agda
diffstat 1 files changed, 34 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/FLutil.agda	Mon Sep 07 20:27:35 2020 +0900
+++ b/FLutil.agda	Tue Sep 08 07:16:49 2020 +0900
@@ -90,3 +90,37 @@
 
 fr5 : List (List ℕ)
 fr5 = map plist (map FL→perm  (Data.List.reverse (flist (fmax {4}) )))
+
+open import Relation.Nary using (⌊_⌋; fromWitness)
+open import Data.List.Fresh
+
+FList : {n : ℕ } → Set
+FList {n} = List# (FL n) ⌊ _f<?_ ⌋
+
+fr1 : FList
+fr1 =
+   ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
+   ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) ∷# 
+   ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
+   ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
+   ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷# 
+   []
+
+open import Data.Product
+
+FLadd : {n : ℕ } → FL n → FList {n}  → FList {n} 
+FLadd {zero} f0 y = f0 ∷# []
+FLadd {suc n} x [] = x ∷# []
+FLadd {suc n} x (cons a y x₁) with FLcmp x a
+... | tri≈ ¬a b ¬c = (cons a y x₁)
+... | tri< a₁ ¬b ¬c = cons x ( cons a y x₁) (FLadd1  x₁) where
+   FLadd1 :  fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y →  fresh (FL (suc n)) ⌊ _f<?_ ⌋ x (cons a y x₁)
+   FLadd1 x₁ = (  {!!} , {!!} )
+... | tri> ¬a ¬b c with FLadd x y
+... | [] = a ∷# []
+... | cons a₁ t x₂ = cons a ( cons a₁ t x₂ ) FLadd2 where
+   FLadd2 :  fresh (FL (suc n)) ⌊ _f<?_ ⌋ a  (cons a₁ t x₂)
+   FLadd2 = (  {!!} , {!!})
+
+fr6 = FLadd ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1 
+