From 6ce567bf63a61bce4ccf71e3ec402d94d1da2fb1 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Sun, 29 Sep 2019 13:54:46 +0200 Subject: port to agda/2.6.0.1 and agda-stdlib/1.1 * Data.Vec.lookup changed parameter order. * A number of symbols were moved from Data.Maybe to submodules. * In a number of occasions, agda no longer figures implicit arguments and they had to be made explicit. * We can no longer use heterogeneous proofs inside equational reasoning for propositional equality. Use heterogeneous equational reasoning. * Stop importing proof-irrelevance as that would require K. --- Precond.agda | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'Precond.agda') 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 [] -- cgit v1.2.3