Mercurial > hg > Members > kono > Proof > galois

changeset 210:2eb62a2a34f2

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 Sat, 05 Dec 2020 09:41:16 +0900
parents 40695d752dd0
children 08166685ed2c
files FLComm.agda fin.agda nat.agda
diffstat 3 files changed, 37 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/FLComm.agda	Sat Dec 05 07:32:31 2020 +0900
+++ b/FLComm.agda	Sat Dec 05 09:41:16 2020 +0900
@@ -50,23 +50,35 @@
      anyList : FList n
      anyP : (x : FL n) → p f≤ x →  Any ( _≡ x ) anyList 
 
+open import fin
 open AnyFL
 anyFL : (n : ℕ ) → AnyFL n FL0
 anyFL zero = record { anyList =  f0 ∷# []  ; anyP = any00 } where
    any00 : (p : FL zero) →  FL0 f≤ p → Any (_≡ p) (f0 ∷# [])
    any00 f0 (case1 refl) = here refl
-anyFL (suc n) = any01 n (anyList (anyFL n)) (anyP (anyFL n) FL0 (case1 refl) ) fmax {!!} where
+anyFL (suc n) = any01 n (anyList (anyFL n)) (anyP (anyFL n) FL0 (case1 refl) ) {!!} where
+   -- any03 : AnyFL (suc n) (fromℕ< a<sa :: fmax) → AnyFL (suc n) FL0
+   -- loop on i 
    any02 : (i : ℕ ) → (i<n : i < suc n ) → (a : FL n) → AnyFL (suc n) (fromℕ< i<n  :: a) → AnyFL (suc n) (zero :: a)
    any02 zero (s≤s z≤n) a any = any
-   any02 (suc i) i<n a any = {!!}
-   any01 : (i : ℕ ) → (L : FList n) → Any (_≡ FL0) L → (x : FL (suc n)) → AnyFL (suc n) x → AnyFL (suc n) FL0 
-   any01 zero [] _ x any = {!!}
-   any01 (suc i) [] _ x any = {!!}
-   any01 zero (cons a L x)    _ y any = any03 {!!} where
-      any03 : AnyFL (suc n) (fromℕ< a<sa :: fmax) → AnyFL (suc n) FL0
-      any03 any = any02 n a<sa FL0 {!!}
-   any01 (suc i) (cons .FL0 L x) (here refl) y any = any01 i L {!!} {!!} {!!} -- can't happen
-   any01 (suc i) (cons a L x) (there b) y any = {!!} -- any01 i L b any 
+   any02 (suc i) i<n a any = any02 i {!!} a {!!}
+   -- loop on a 
+   any03 :  (L : FList n) → (a : FL n) →  fresh (FL n) ⌊ _f<?_ ⌋ a L  →  AnyFL (suc n) (fromℕ< a<sa :: a ) → AnyFL (suc n) FL0
+   any03 [] a ar any = {!!} -- any02 n a<sa a any
+   any03 (cons b L br) a (a<b Data.Product., _) any = any03 L b br record { anyList = anyList any04 ; anyP = any05 } where
+      any06 : {n : ℕ} → zero Data.Fin.< fromℕ< {n} a<sa
+      any06 = {!!}
+      any04 : AnyFL (suc n) (zero :: a)
+      any04 = any02 n a<sa a any
+      any05 : (x : FL (suc n)) → (fromℕ< a<sa :: b) f≤ x → Any (_≡ x) (anyList any04) -- 0<fmax : zero Data.Fin.< fromℕ< a<sa
+      any05 .(fromℕ< a<sa :: b) (case1 refl) = anyP any04 (fromℕ< a<sa :: b) (case2 (f<n any06 )) -- (fromℕ< a<sa :: b) f< x → (zero :: a) f≤ x
+      any05 x (case2 mb<x ) = anyP any04 x (case2 (f<-trans (f<n any06) mb<x ))
+   any01 : (i : ℕ ) → (L : FList n) → Any (_≡ FL0) L → AnyFL (suc n) fmax → AnyFL (suc n) FL0 
+   any01 zero [] ()
+   any01 (suc i) [] ()
+   any01 zero (cons a L x)    _ any = {!!}
+   any01 (suc i) (cons .FL0 L x) (here refl) any = any01 i L {!!} {!!} -- can't happen
+   any01 (suc i) (cons a L ar) (there b) any = any03 L a ar {!!}
 
 -- all comm cobmbibation in P and Q
 record AnyComm (P Q : FList n) : Set where
--- a/fin.agda	Sat Dec 05 07:32:31 2020 +0900
+++ b/fin.agda	Sat Dec 05 09:41:16 2020 +0900
@@ -10,15 +10,6 @@
 open import Relation.Binary.PropositionalEquality
 
 
-n≤n : (n : ℕ) →  n Data.Nat.≤ n
-n≤n zero = z≤n
-n≤n (suc n) = s≤s (n≤n n)
-
-<→m≤n : {m n : ℕ} → m  < n →  m Data.Nat.≤ n
-<→m≤n {zero} lt = z≤n
-<→m≤n {suc m} {zero} ()
-<→m≤n {suc m} {suc n} (s≤s lt) = s≤s (<→m≤n lt)
-
 -- toℕ<n
 fin<n : {n : ℕ} {f : Fin n} → toℕ f < n
 fin<n {_} {zero} = s≤s z≤n
@@ -41,6 +32,12 @@
 toℕ→from {0} {zero} refl = refl
 toℕ→from {suc n} {suc x} eq = cong (λ k → suc k ) ( toℕ→from {n} {x} (cong (λ k → Data.Nat.pred k ) eq ))
 
+0≤fmax : {n : ℕ } → (# 0) Data.Fin.≤ fromℕ< {n} a<sa
+0≤fmax  = subst (λ k → 0 ≤ k ) (sym (toℕ-fromℕ< a<sa)) z≤n
+
+0<fmax : {n : ℕ } → (# 0) Data.Fin.< fromℕ< {suc n} a<sa
+0<fmax = subst (λ k → 0 < k ) (sym (toℕ-fromℕ< a<sa)) (s≤s z≤n)
+
 -- toℕ-injective
 i=j : {n : ℕ} (i j : Fin n) → toℕ i ≡ toℕ j → i ≡ j
 i=j {suc n} zero zero refl = refl
--- a/nat.agda	Sat Dec 05 07:32:31 2020 +0900
+++ b/nat.agda	Sat Dec 05 09:41:16 2020 +0900
@@ -53,6 +53,15 @@
 <-∨ {suc x} {suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → suc k ) eq)
 <-∨ {suc x} {suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)
 
+n≤n : (n : ℕ) →  n Data.Nat.≤ n
+n≤n zero = z≤n
+n≤n (suc n) = s≤s (n≤n n)
+
+<→m≤n : {m n : ℕ} → m  < n →  m Data.Nat.≤ n
+<→m≤n {zero} lt = z≤n
+<→m≤n {suc m} {zero} ()
+<→m≤n {suc m} {suc n} (s≤s lt) = s≤s (<→m≤n lt)
+
 max : (x y : ℕ) → ℕ
 max zero zero = zero
 max zero (suc x) = (suc x)