Mercurial > hg > Members > kono > Proof > galois

changeset 198:c93a60686dce

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
insAny
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 30 Nov 2020 08:07:55 +0900
parents 57188c35ea1a
children 6c81c3d535d1
files FLComm.agda FLutil.agda
diffstat 2 files changed, 8 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/FLComm.agda	Mon Nov 30 00:36:01 2020 +0900
+++ b/FLComm.agda	Mon Nov 30 08:07:55 2020 +0900
@@ -59,7 +59,7 @@
    commc :  (L3 L1 : FList n) →  Any (_≡_ (perm→FL [  FL→perm G , FL→perm H ])) L3 
            →  Any (_≡_ (perm→FL [ FL→perm G , FL→perm H ])) (tl3 G L1 L3)
    commc L3 [] any = any
-   commc L3 (cons a L1 _) any = commc (FLinsert (perm→FL [ FL→perm G , FL→perm a ]) L3) L1 {!!} 
+   commc L3 (cons a L1 _) any = commc (FLinsert (perm→FL [ FL→perm G , FL→perm a ]) L3) L1 (insAny _ any)
    comm3 : (L1 : FList n) → Any (H ≡_) L1 → (L3 : FList n) → Any (_≡_ (perm→FL [ g , h ])) (tl3 G L1 L3)
    comm3 (H ∷# []) (here refl) L3 = subst (λ k → Any (_≡_  k) (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3 ) )
        comm6 (x∈FLins ( perm→FL [ FL→perm G , FL→perm H ] ) L3 )
--- a/FLutil.agda	Mon Nov 30 00:36:01 2020 +0900
+++ b/FLutil.agda	Mon Nov 30 08:07:55 2020 +0900
@@ -304,16 +304,15 @@
 nextAny (here x₁) = there (here x₁)
 nextAny (there any) = there (there any)
 
-insAny : {n : ℕ} → {x h : FL n } → (L : FList n)  → Any (_≡_ x) L → Any (_≡_ x) (FLinsert h L)
+insAny : {n : ℕ} → {x h : FL n } → (xs : FList n)  → Any (x ≡_ ) xs → Any (x ≡_ ) (FLinsert h xs)
 insAny {zero} {f0} {f0} (cons a L xr) (here refl) = here refl
 insAny {zero} {f0} {f0} (cons a L xr) (there any) = insAny {zero} {f0} {f0} L any 
-insAny {suc n} {x} {h} (cons a L xr) any with FLcmp h x | FLinsert h (cons a L xr) | inspect (FLinsert h) (cons a L xr) 
-... | tri< a₁ ¬b ¬c | [] | record { eq = eq } = ?
-... | tri< a₁ ¬b ¬c | cons a₂ t x₁ | record { eq = eq } = subst (λ k → Any (_≡_ x) k ) {!!} (there {_} {_} {_} {{!!}} {{!!}} {{!!}} any)
-... | tri≈ ¬a b ¬c | t | record { eq = eq }= subst (λ k → Any (_≡_ x) k ) {!!}  (here refl)
-insAny {suc n} {x} {h} (cons a [] xr) any | tri> ¬a ¬b c | t | record { eq = eq } = {!!}
-insAny {suc n} {x} {h} (cons a (cons a₁ L x₁) xr) (here x₂) | tri> ¬a ¬b c | t | record { eq = eq } = subst (λ k → Any (_≡_ x) k) {!!} (here {!!})
-insAny {suc n} {x} {h} (cons a (cons a₁ L x₁) xr) (there any) | tri> ¬a ¬b c | t | record { eq = eq } = subst (λ k → Any (_≡_ x) k) {!!} (there  {!!})
+insAny {suc n} {x} {h} (cons a L xr) any with FLcmp h a 
+... | tri< x<a ¬b ¬c = there any
+... | tri≈ ¬a b ¬c = any
+insAny {suc n} {a} {h} (cons a [] (Level.lift tt)) (here refl) | tri> ¬a ¬b c = here refl
+insAny {suc n} {x} {h} (cons a (cons a₁ L x₁) xr) (here refl) | tri> ¬a ¬b c = here refl
+insAny {suc n} {x} {h} (cons a (cons a₁ L x₁) xr) (there any) | tri> ¬a ¬b c = there (insAny (cons a₁ L x₁) any)
 
 AnyFList : {n : ℕ }  → (x : FL n ) →  Any (x ≡_ ) (∀Flist fmax)
 AnyFList {zero} f0 = here refl