X-Git-Url: https://git.linta.de/?p=~helmut%2Fbidiragda.git;a=blobdiff_plain;f=Precond.agda;h=3a487577dfbe7056356ffb100b0fd13c9f52c96e;hp=3e4c21930805bfa3cf0e06abcfa249261f1f1262;hb=6958d1c19cda39564508e0638648eacf32c71509;hpb=fb860d5088732548eeaf914f9533763f8ec63db4 diff --git a/Precond.agda b/Precond.agda index 3e4c219..3a48757 100644 --- a/Precond.agda +++ b/Precond.agda @@ -41,23 +41,18 @@ lemma-maybe-just a (just x) = refl lemma-maybe-just a nothing = refl lemma-union-delete-fromFunc : {m n : ℕ} {A : Set} {is : Vec (Fin n) m} {h : FinMapMaybe n A} {g : Fin n → A} → (toList is) in-domain-of h → ∃ λ v → union h (delete-many is (fromFunc g)) ≡ fromFunc v -lemma-union-delete-fromFunc {is = []} {h = h} {g = g} p = _ , (begin - union h (fromFunc g) - ≡⟨ lemma-tabulate-∘ (λ f → begin +lemma-union-delete-fromFunc {is = []} {h = h} {g = g} p = _ , (lemma-tabulate-∘ (λ f → begin maybe′ just (lookupM f (fromFunc g)) (lookupM f h) ≡⟨ cong (flip (maybe′ just) (lookupM f h)) (lemma-lookupM-fromFunc g f) ⟩ maybe′ just (just (g f)) (lookupM f h) ≡⟨ lemma-maybe-just (g f) (lookupM f h) ⟩ - just (maybe′ id (g f) (lookupM f h)) ∎) ⟩ - tabulate (λ f → just (maybe′ id (g f) (lookup f h))) - ≡⟨ tabulate-∘ just (λ f → maybe′ id (g f) (lookup f h)) ⟩ - map just (tabulate (λ f → maybe′ id (g f) (lookup f h))) ∎) + just (maybe′ id (g f) (lookupM f h)) ∎)) lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} (Data.List.All._∷_ (x , px) ps) = _ , (begin union h (delete i (delete-many is (fromFunc g))) ≡⟨ lemma-tabulate-∘ inner ⟩ union h (delete-many is (fromFunc g)) ≡⟨ proj₂ (lemma-union-delete-fromFunc ps) ⟩ - map just _ ∎) + _ ∎) where inner : (f : Fin n) → maybe′ just (lookupM f (delete i (delete-many is (fromFunc g)))) (lookup f h) ≡ maybe′ just (lookupM f (delete-many is (fromFunc g))) (lookup f h) inner f with f ≟ i inner .i | yes refl = begin