diff options
Diffstat (limited to 'Precond.agda')
| -rw-r--r-- | Precond.agda | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/Precond.agda b/Precond.agda index 9b4a66c..9d21022 100644 --- a/Precond.agda +++ b/Precond.agda @@ -42,28 +42,28 @@ lemma-maybe-just : {A : Set} → (a : A) → (ma : Maybe A) → maybe′ Maybe.j lemma-maybe-just a (just x) = P.refl lemma-maybe-just a nothing = P.refl -lemma-union-delete-fromFunc : {m n : ℕ} {A : Set} {is : Vec (Fin n) m} {h : FinMapMaybe n A} {g : Fin n → A} → 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 = _ , (tabulate-cong (λ f → begin +lemma-union-delete-fromFunc : {m n : ℕ} {A : Set} {is : Vec (Fin n) m} (h : FinMapMaybe n A) {g : Fin n → A} → is in-domain-of h → ∃ λ v → union h (delete-many is (fromFunc g)) ≡ fromFunc v +lemma-union-delete-fromFunc {is = []} h {g = g} p = _ , (tabulate-cong (λ f → begin maybe′ just (lookupM f (fromFunc g)) (lookupM f h) ≡⟨ P.cong (flip (maybe′ just) (lookupM f h)) (lookup∘tabulate (just ∘ 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)) ∎)) -lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} (Data.List.All._∷_ (x , px) ps) = _ , (begin +lemma-union-delete-fromFunc {n = n} {is = i ∷ is} h {g = g} (Data.List.All._∷_ (x , px) ps) = _ , (begin union h (delete i (delete-many is (fromFunc g))) ≡⟨ tabulate-cong inner ⟩ union h (delete-many is (fromFunc g)) - ≡⟨ proj₂ (lemma-union-delete-fromFunc ps) ⟩ + ≡⟨ proj₂ (lemma-union-delete-fromFunc h ps) ⟩ _ ∎) - 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) + where inner : (f : Fin n) → maybe′ just (lookupM f (delete i (delete-many is (fromFunc g)))) (lookup h f) ≡ maybe′ just (lookupM f (delete-many is (fromFunc g))) (lookup h f) inner f with f ≟ i inner .i | yes P.refl = begin - maybe′ just (lookupM i (delete i (delete-many is (fromFunc g)))) (lookup i h) + maybe′ just (lookupM i (delete i (delete-many is (fromFunc g)))) (lookup h i) ≡⟨ P.cong (maybe′ just _) px ⟩ just x ≡⟨ P.cong (maybe′ just _) (P.sym px) ⟩ - maybe′ just (lookupM i (delete-many is (fromFunc g))) (lookup i h) ∎ - inner f | no f≢i = P.cong (flip (maybe′ just) (lookup f h)) (lookup∘update′ f≢i (delete-many is (fromFunc g)) nothing) + maybe′ just (lookupM i (delete-many is (fromFunc g))) (lookup h i) ∎ + inner f | no f≢i = P.cong (flip (maybe′ just) (lookup h f)) (lookup∘update′ f≢i (delete-many is (fromFunc g)) nothing) module _ (G : Get) where open Get G @@ -96,7 +96,7 @@ module _ (G : Get) where g = fromFunc (denumerate SourceShapeT s) g′ = delete-many (contentV (get s′)) g t = enumerate SourceShapeT (gl₁ i) - wp = lemma-union-delete-fromFunc (lemma-assoc-domain (contentV (get t)) (contentV v) p) + wp = lemma-union-delete-fromFunc h (lemma-assoc-domain (contentV (get t)) (contentV v) p) data All-different {A : Set} : List A → Set where different-[] : All-different [] |