diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2018-11-25 10:35:23 +0100 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2018-11-25 10:35:23 +0100 |
| commit | c835e655a05c73f7dd2dc46c652be3d43e91a4b7 (patch) | |
| tree | 3089ac9a52dfd62e931926cb5900d9b266f0f298 | |
| parent | 04e312472d4737815cf6c37258b547673faa0b91 (diff) | |
| download | bidiragda-c835e655a05c73f7dd2dc46c652be3d43e91a4b7.tar.gz | |
reorganize equality imports
Since we are working with multiple setoids now, it makes more sense to
qualify their members. Follow the "as P" pattern from the standard
library. Also stop importing those symbols from Relation.Binary.Core as
later agda-stdlib versions will move them away. Rather than EqSetoid or
PropEq, use P.setoid consistently.
| -rw-r--r-- | BFFPlug.agda | 22 | ||||
| -rw-r--r-- | Bidir.agda | 119 | ||||
| -rw-r--r-- | CheckInsert.agda | 39 | ||||
| -rw-r--r-- | Examples.agda | 18 | ||||
| -rw-r--r-- | FinMap.agda | 60 | ||||
| -rw-r--r-- | Generic.agda | 47 | ||||
| -rw-r--r-- | LiftGet.agda | 81 | ||||
| -rw-r--r-- | Precond.agda | 47 | ||||
| -rw-r--r-- | Structures.agda | 4 |
9 files changed, 217 insertions, 220 deletions
diff --git a/BFFPlug.agda b/BFFPlug.agda index 0d69723..4992a3e 100644 --- a/BFFPlug.agda +++ b/BFFPlug.agda @@ -8,7 +8,7 @@ open import Data.Maybe using (Maybe ; just ; nothing) open import Data.Vec using (Vec) open import Data.Product using (∃ ; _,_) open import Relation.Binary using (module DecSetoid) -open import Relation.Binary.PropositionalEquality using (refl ; cong ; subst ; sym ; module ≡-Reasoning) renaming (setoid to PropEq) +open import Relation.Binary.PropositionalEquality as P using (module ≡-Reasoning) open import Relation.Nullary using (yes ; no) open import Function using (flip ; id ; _∘_) open import Function.LeftInverse using (_RightInverseOf_) @@ -32,39 +32,39 @@ bffplug G sput {i} {m} s v with sput i m ... | nothing = nothing ... | just j with Get.gl₂ G j ≟ m ... | no gl₂j≢m = nothing -bffplug G sput {i} s v | just j | yes refl with bff G j s v -... | nothing = nothing -... | just s′ = just (j , s′) +bffplug G sput {i} s v | just j | yes P.refl with bff G j s v +... | nothing = nothing +... | just s′ = just (j , s′) _SimpleRightInvOf_ : {A B : Set} → (A → B) → (B → A) → Set f SimpleRightInvOf g = ≡-to-Π f RightInverseOf ≡-to-Π g bffinv : (G : Get) → (nelteg : ℕ → Get.I G) → nelteg SimpleRightInvOf Get.gl₂ G → {i : Get.I G} → {m : ℕ} → Vec Carrier (Get.gl₁ G i) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (Get.gl₁ G (nelteg m))) -bffinv G nelteg inv {m = m} s v = bff G (nelteg m) s (subst (Vec Carrier) (sym (inv m)) v) +bffinv G nelteg inv {m = m} s v = bff G (nelteg m) s (P.subst (Vec Carrier) (P.sym (inv m)) v) module InvExamples where open Examples using (reverse' ; drop' ; sieve' ; tail' ; take') reverse-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier m) - reverse-put s v = bffinv reverse' id (λ _ → refl) s v >>= sequenceV + reverse-put s v = bffinv reverse' id (λ _ → P.refl) s v >>= sequenceV drop-put : (k : ℕ) → {n m : ℕ} → Vec Carrier (k + n) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (k + m)) - drop-put k = bffinv (drop' k) id (λ _ → refl) + drop-put k = bffinv (drop' k) id (λ _ → P.refl) double : ℕ → ℕ double zero = zero double (suc n) = suc (suc (double n)) sieve-inv-len : double SimpleRightInvOf ⌈_/2⌉ - sieve-inv-len zero = refl - sieve-inv-len (suc zero) = refl - sieve-inv-len (suc (suc x)) = cong (suc ∘ suc) (sieve-inv-len x) + sieve-inv-len zero = P.refl + sieve-inv-len (suc zero) = P.refl + sieve-inv-len (suc (suc x)) = P.cong (suc ∘ suc) (sieve-inv-len x) sieve-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec (Maybe Carrier) (double m)) sieve-put = bffinv sieve' double sieve-inv-len tail-put : {n m : ℕ} → Vec Carrier (suc n) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (suc m)) - tail-put = bffinv tail' id (λ _ → refl) + tail-put = bffinv tail' id (λ _ → P.refl) take-put : (k : ℕ) → {n : ℕ} → Vec Carrier (k + n) → Vec Carrier k → Maybe (Vec Carrier (k + n)) take-put k = bffsameshape (take' k) @@ -18,9 +18,8 @@ open import Data.Vec.Equality using () renaming (module Equality to VecEq) open import Data.Vec.Properties using (lookup∘tabulate ; lookup∘update ; map-cong ; map-∘ ; map-lookup-allFin) open import Data.Product using (∃ ; _×_ ; _,_ ; proj₁ ; proj₂) open import Function using (id ; _∘_ ; flip) -open import Relation.Binary.Core using (refl ; _≡_) open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid) -open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans ; cong₂ ; decSetoid ; module ≡-Reasoning) renaming (setoid to EqSetoid) +open import Relation.Binary.PropositionalEquality as P using (_≡_ ; inspect ; [_] ; module ≡-Reasoning) open import Relation.Binary using (Setoid ; module Setoid ; module DecSetoid) import Relation.Binary.EqReasoning as EqR @@ -38,10 +37,10 @@ open Setoid using () renaming (_≈_ to _∋_≈_) open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq) lemma-1 : {m n : ℕ} → (f : Fin n → Carrier) → (is : Vec (Fin n) m) → assoc is (map f is) ≡ just (restrict f is) -lemma-1 f [] = refl +lemma-1 f [] = P.refl lemma-1 f (i ∷ is′) = begin (assoc is′ (map f is′) >>= checkInsert i (f i)) - ≡⟨ cong (λ m → m >>= checkInsert i (f i)) (lemma-1 f is′) ⟩ + ≡⟨ P.cong (λ m → m >>= checkInsert i (f i)) (lemma-1 f is′) ⟩ checkInsert i (f i) (restrict f is′) ≡⟨ lemma-checkInsert-restrict f i is′ ⟩ just (restrict f (i ∷ is′)) ∎ @@ -49,15 +48,15 @@ lemma-1 f (i ∷ is′) = begin lemma-lookupM-checkInserted : {n : ℕ} → (i : Fin n) → (x : Carrier) → (h : FinMapMaybe n Carrier) → {h' : FinMapMaybe n Carrier} → checkInsert i x h ≡ just h' → MaybeSetoid A.setoid ∋ lookupM i h' ≈ just x lemma-lookupM-checkInserted i x h p with checkInsert i x h | insertionresult i x h -lemma-lookupM-checkInserted i x h refl | ._ | same x' x≈x' pl = begin +lemma-lookupM-checkInserted i x h P.refl | ._ | same x' x≈x' pl = begin lookupM i h ≡⟨ pl ⟩ just x' ≈⟨ MaybeEq.just (Setoid.sym A.setoid x≈x') ⟩ just x ∎ where open EqR (MaybeSetoid A.setoid) -lemma-lookupM-checkInserted i x h refl | ._ | new _ = Setoid.reflexive (MaybeSetoid A.setoid) (lookup∘update i h (just x)) -lemma-lookupM-checkInserted i x h () | ._ | wrong _ _ _ +lemma-lookupM-checkInserted i x h P.refl | ._ | new _ = Setoid.reflexive (MaybeSetoid A.setoid) (lookup∘update i h (just x)) +lemma-lookupM-checkInserted i x h () | ._ | wrong _ _ _ _in-domain-of_ : {m n : ℕ} {A : Set} → (is : Vec (Fin m) n) → (FinMapMaybe m A) → Set _in-domain-of_ is h = All (λ i → ∃ λ x → lookupM i h ≡ just x) (toList is) @@ -67,8 +66,8 @@ lemma-assoc-domain [] [] ph = Data.List.All.[] lemma-assoc-domain (i' ∷ is') (x' ∷ xs') ph with assoc is' xs' | inspect (assoc is') xs' lemma-assoc-domain (i' ∷ is') (x' ∷ xs') () | nothing | [ ph' ] lemma-assoc-domain (i' ∷ is') (x' ∷ xs') ph | just h' | [ ph' ] with checkInsert i' x' h' | inspect (checkInsert i' x') h' | insertionresult i' x' h' -lemma-assoc-domain (i' ∷ is') (x' ∷ xs') refl | just h | [ ph' ] | ._ | _ | same x _ pl = All._∷_ (x , pl) (lemma-assoc-domain is' xs' ph') -lemma-assoc-domain (i' ∷ is') (x' ∷ xs') refl | just h' | [ ph' ] | ._ | [ cI≡ ] | new _ = All._∷_ +lemma-assoc-domain (i' ∷ is') (x' ∷ xs') P.refl | just h | [ ph' ] | ._ | _ | same x _ pl = All._∷_ (x , pl) (lemma-assoc-domain is' xs' ph') +lemma-assoc-domain (i' ∷ is') (x' ∷ xs') P.refl | just h' | [ ph' ] | ._ | [ cI≡ ] | new _ = All._∷_ (x' , lookup∘update i' h' (just x')) (Data.List.All.map (λ {i} p → proj₁ p , lemma-lookupM-checkInsert i i' h' (proj₂ p) x' cI≡) @@ -76,9 +75,9 @@ lemma-assoc-domain (i' ∷ is') (x' ∷ xs') refl | just h' | [ ph' ] | ._ | [ c lemma-assoc-domain (i' ∷ is') (x' ∷ xs') () | just h' | [ ph' ] | ._ | _ | wrong _ _ _ lemma-map-lookupM-assoc : {m : ℕ} → (i : Fin m) → (x : Carrier) → (h : FinMapMaybe m Carrier) → {h' : FinMapMaybe m Carrier} → checkInsert i x h ≡ just h' → {n : ℕ} → (js : Vec (Fin m) n) → js in-domain-of h → map (flip lookupM h') js ≡ map (flip lookupM h) js -lemma-map-lookupM-assoc i x h ph [] pj = refl -lemma-map-lookupM-assoc i x h ph (j ∷ js) (Data.List.All._∷_ (x' , pl) pj) = cong₂ _∷_ - (trans (lemma-lookupM-checkInsert j i h pl x ph) (sym pl)) +lemma-map-lookupM-assoc i x h ph [] pj = P.refl +lemma-map-lookupM-assoc i x h ph (j ∷ js) (Data.List.All._∷_ (x' , pl) pj) = P.cong₂ _∷_ + (P.trans (lemma-lookupM-checkInsert j i h pl x ph) (P.sym pl)) (lemma-map-lookupM-assoc i x h ph js pj) lemma-2 : {m n : ℕ} → (is : Vec (Fin n) m) → (v : Vec Carrier m) → (h : FinMapMaybe n Carrier) → assoc is v ≡ just h → VecISetoid (MaybeSetoid A.setoid) at _ ∋ map (flip lookupM h) is ≈ map just v @@ -89,7 +88,7 @@ lemma-2 (i ∷ is) (x ∷ xs) h p | just h' | [ ir ] = begin lookupM i h ∷ map (flip lookupM h) is ≈⟨ VecEq._∷-cong_ (lemma-lookupM-checkInserted i x h' p) (ISetoid.refl (VecISetoid (MaybeSetoid A.setoid))) ⟩ just x ∷ map (flip lookupM h) is - ≡⟨ cong (_∷_ (just x)) (lemma-map-lookupM-assoc i x h' p is (lemma-assoc-domain is xs ir)) ⟩ + ≡⟨ P.cong (_∷_ (just x)) (lemma-map-lookupM-assoc i x h' p is (lemma-assoc-domain is xs ir)) ⟩ just x ∷ map (flip lookupM h') is ≈⟨ VecEq._∷-cong_ (Setoid.refl (MaybeSetoid A.setoid)) (lemma-2 is xs h' ir) ⟩ just x ∷ map just xs ∎ @@ -100,7 +99,7 @@ lemma-fmap-denumerate-enumerate {S} {C} ShapeT {s = s} c = begin fmap (denumerate ShapeT c) (fill s (allFin (arity s))) ≡⟨ fill-fmap (denumerate ShapeT c) s (allFin (arity s)) ⟩ fill s (map (flip lookupVec (content c)) (allFin (arity s))) - ≡⟨ cong (fill s) (map-lookup-allFin (content c)) ⟩ + ≡⟨ P.cong (fill s) (map-lookup-allFin (content c)) ⟩ fill s (content c) ≡⟨ content-fill c ⟩ c ∎ @@ -111,29 +110,29 @@ lemma-fmap-denumerate-enumerate {S} {C} ShapeT {s = s} c = begin theorem-1 : (G : Get) → {i : Get.I G} → (s : Get.SourceContainer G Carrier (Get.gl₁ G i)) → bff G i s (Get.get G s) ≡ just (Get.fmapS G just s) theorem-1 G {i} s = begin bff G i s (get s) - ≡⟨ cong (bff G i s ∘ get) (sym (lemma-fmap-denumerate-enumerate SourceShapeT s)) ⟩ + ≡⟨ P.cong (bff G i s ∘ get) (P.sym (lemma-fmap-denumerate-enumerate SourceShapeT s)) ⟩ bff G i s (get (fmapS f t)) - ≡⟨ cong (bff G i s) (free-theorem f t) ⟩ + ≡⟨ P.cong (bff G i s) (free-theorem f t) ⟩ bff G i s (fmapV f (get t)) - ≡⟨ refl ⟩ + ≡⟨ P.refl ⟩ h′↦r <$> (h↦h′ <$> (assoc (Shaped.content ViewShapeT (get t)) (Shaped.content ViewShapeT (fmapV f (get t))))) - ≡⟨ cong (_<$>_ h′↦r ∘ _<$>_ h↦h′ ∘ assoc (Shaped.content ViewShapeT (get t))) (Shaped.fmap-content ViewShapeT f (get t)) ⟩ + ≡⟨ P.cong (_<$>_ h′↦r ∘ _<$>_ h↦h′ ∘ assoc (Shaped.content ViewShapeT (get t))) (Shaped.fmap-content ViewShapeT f (get t)) ⟩ h′↦r <$> (h↦h′ <$> (assoc (Shaped.content ViewShapeT (get t)) (map f (Shaped.content ViewShapeT (get t))))) - ≡⟨ cong (_<$>_ h′↦r ∘ _<$>_ h↦h′) (lemma-1 f (Shaped.content ViewShapeT (get t))) ⟩ + ≡⟨ P.cong (_<$>_ h′↦r ∘ _<$>_ h↦h′) (lemma-1 f (Shaped.content ViewShapeT (get t))) ⟩ (Maybe.just ∘ h′↦r ∘ h↦h′) (restrict f (Shaped.content ViewShapeT (get t))) - ≡⟨ cong just (begin + ≡⟨ P.cong just (begin h′↦r (union (restrict f (Shaped.content ViewShapeT (get t))) (reshape g′ (Shaped.arity SourceShapeT (gl₁ i)))) - ≡⟨ cong (h′↦r ∘ union (restrict f (Shaped.content ViewShapeT (get t)))) (lemma-reshape-id g′) ⟩ + ≡⟨ P.cong (h′↦r ∘ union (restrict f (Shaped.content ViewShapeT (get t)))) (lemma-reshape-id g′) ⟩ h′↦r (union (restrict f (Shaped.content ViewShapeT (get t))) g′) - ≡⟨ cong h′↦r (lemma-disjoint-union f (Shaped.content ViewShapeT (get t))) ⟩ + ≡⟨ P.cong h′↦r (lemma-disjoint-union f (Shaped.content ViewShapeT (get t))) ⟩ h′↦r (fromFunc f) - ≡⟨ refl ⟩ + ≡⟨ P.refl ⟩ fmapS (flip lookupM (fromFunc f)) t ≡⟨ IsFunctor.cong (Shaped.isFunctor SourceShapeT (gl₁ i)) (lemma-lookupM-fromFunc f) t ⟩ fmapS (Maybe.just ∘ f) t ≡⟨ IsFunctor.composition (Shaped.isFunctor SourceShapeT (gl₁ i)) just f t ⟩ fmapS just (fmapS f t) - ≡⟨ cong (fmapS just) (lemma-fmap-denumerate-enumerate SourceShapeT s) ⟩ + ≡⟨ P.cong (fmapS just) (lemma-fmap-denumerate-enumerate SourceShapeT s) ⟩ fmapS just s ∎) ⟩ _ ∎ where open ≡-Reasoning open Get G @@ -145,7 +144,7 @@ theorem-1 G {i} s = begin lemma-<$>-just : {A B : Set} {f : A → B} {b : B} (ma : Maybe A) → (f <$> ma) ≡ just b → ∃ λ a → ma ≡ just a -lemma-<$>-just (just x) f<$>ma≡just-b = x , refl +lemma-<$>-just (just x) f<$>ma≡just-b = x , P.refl lemma-<$>-just nothing () lemma-union-not-used : {n : ℕ} → {A : Set} → (h h′ : FinMapMaybe n A) → (i : Fin n) → ∃ (λ x → lookupM i h ≡ just x) → lookupM i (union h h′) ≡ lookupM i h @@ -153,60 +152,60 @@ lemma-union-not-used h h′ i (x , px) = begin lookupM i (union h h′) ≡⟨ lookup∘tabulate (λ j → maybe′ just (lookupM j h′) (lookupM j h)) i ⟩ maybe′ just (lookupM i h′) (lookupM i h) - ≡⟨ cong (maybe′ just (lookupM i h′)) px ⟩ + ≡⟨ P.cong (maybe′ just (lookupM i h′)) px ⟩ maybe′ just (lookupM i h′) (just x) - ≡⟨ sym px ⟩ + ≡⟨ P.sym px ⟩ lookupM i h ∎ where open ≡-Reasoning lemma->>=-just : {A B : Set} (ma : Maybe A) {f : A → Maybe B} {b : B} → (ma >>= f) ≡ just b → ∃ λ a → ma ≡ just a -lemma->>=-just (just a) p = a , refl +lemma->>=-just (just a) p = a , P.refl lemma->>=-just nothing () lemma-just-sequenceV : {A : Set} {n : ℕ} → (v : Vec A n) → sequenceV (map just v) ≡ just v -lemma-just-sequenceV [] = refl -lemma-just-sequenceV (x ∷ xs) = cong (_<$>_ (_∷_ x)) (lemma-just-sequenceV xs) +lemma-just-sequenceV [] = P.refl +lemma-just-sequenceV (x ∷ xs) = P.cong (_<$>_ (_∷_ x)) (lemma-just-sequenceV xs) lemma-just-sequence : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → {A : Set} {s : S} → (c : C A s) → Shaped.sequence ShapeT (Shaped.fmap ShapeT just c) ≡ just c lemma-just-sequence ShapeT {s = s} c = begin fill s <$> sequenceV (content (fmap just c)) - ≡⟨ cong (_<$>_ (fill s) ∘ sequenceV) (fmap-content just c) ⟩ + ≡⟨ P.cong (_<$>_ (fill s) ∘ sequenceV) (fmap-content just c) ⟩ fill s <$> sequenceV (map just (content c)) - ≡⟨ cong (_<$>_ (fill s)) (lemma-just-sequenceV (content c)) ⟩ + ≡⟨ P.cong (_<$>_ (fill s)) (lemma-just-sequenceV (content c)) ⟩ fill s <$> just (content c) - ≡⟨ cong just (content-fill c) ⟩ + ≡⟨ P.cong just (content-fill c) ⟩ just c ∎ where open ≡-Reasoning open Shaped ShapeT lemma-sequenceV-successful : {A : Set} {n : ℕ} → (v : Vec (Maybe A) n) → {r : Vec A n} → sequenceV v ≡ just r → v ≡ map just r -lemma-sequenceV-successful [] {r = []} p = refl +lemma-sequenceV-successful [] {r = []} p = P.refl lemma-sequenceV-successful (just x ∷ xs) p with sequenceV xs | inspect sequenceV xs lemma-sequenceV-successful (just x ∷ xs) () | nothing | _ -lemma-sequenceV-successful (just x ∷ xs) {r = .x ∷ .ys} refl | just ys | [ p′ ] = cong (_∷_ (just x)) (lemma-sequenceV-successful xs p′) +lemma-sequenceV-successful (just x ∷ xs) {r = .x ∷ .ys} P.refl | just ys | [ p′ ] = P.cong (_∷_ (just x)) (lemma-sequenceV-successful xs p′) lemma-sequenceV-successful (nothing ∷ xs) () lemma-sequence-successful : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → {A : Set} {s : S} → (c : C (Maybe A) s) → {r : C A s} → Shaped.sequence ShapeT c ≡ just r → c ≡ Shaped.fmap ShapeT just r -lemma-sequence-successful ShapeT {s = s} c {r} p = just-injective (sym (begin +lemma-sequence-successful ShapeT {s = s} c {r} p = just-injective (P.sym (begin fill s <$> (map just <$> (content <$> just r)) - ≡⟨ cong (_<$>_ (fill s) ∘ _<$>_ (map just)) (begin + ≡⟨ P.cong (_<$>_ (fill s) ∘ _<$>_ (map just)) (begin content <$> just r - ≡⟨ cong (_<$>_ content) (sym p) ⟩ + ≡⟨ P.cong (_<$>_ content) (P.sym p) ⟩ content <$> (fill s <$> sequenceV (content c)) - ≡⟨ sym (Functor.composition MaybeFunctor content (fill s) (sequenceV (content c))) ⟩ + ≡⟨ P.sym (Functor.composition MaybeFunctor content (fill s) (sequenceV (content c))) ⟩ content ∘ fill s <$> sequenceV (content c) ≡⟨ Functor.cong MaybeFunctor (fill-content s) (sequenceV (content c)) ⟩ id <$> sequenceV (content c) ≡⟨ Functor.identity MaybeFunctor (sequenceV (content c)) ⟩ sequenceV (content c) - ≡⟨ cong sequenceV (lemma-sequenceV-successful (content c) (proj₂ wp)) ⟩ + ≡⟨ P.cong sequenceV (lemma-sequenceV-successful (content c) (proj₂ wp)) ⟩ sequenceV (map just (proj₁ wp)) ≡⟨ lemma-just-sequenceV (proj₁ wp) ⟩ just (proj₁ (lemma-<$>-just (sequenceV (content c)) p)) ∎) ⟩ fill s <$> (map just <$> just (proj₁ (lemma-<$>-just (sequenceV (content c)) p))) - ≡⟨ cong (_<$>_ (fill s) ∘ just) (sym (lemma-sequenceV-successful (content c) (proj₂ wp))) ⟩ + ≡⟨ P.cong (_<$>_ (fill s) ∘ just) (P.sym (lemma-sequenceV-successful (content c) (proj₂ wp))) ⟩ fill s <$> just (content c) - ≡⟨ cong just (content-fill c) ⟩ + ≡⟨ P.cong just (content-fill c) ⟩ just c ∎)) where open ≡-Reasoning open Shaped ShapeT @@ -221,15 +220,15 @@ module _ (G : Get) where lemma-get-sequence : {A : Set} → {i : I} {v : SourceContainer (Maybe A) (gl₁ i)} {r : SourceContainer A (gl₁ i)} → sequenceSource v ≡ just r → (get <$> sequenceSource v) ≡ sequenceView (get v) lemma-get-sequence {v = v} {r = r} p = begin get <$> sequenceSource v - ≡⟨ cong (_<$>_ get ∘ sequenceSource) (lemma-sequence-successful SourceShapeT v p) ⟩ + ≡⟨ P.cong (_<$>_ get ∘ sequenceSource) (lemma-sequence-successful SourceShapeT v p) ⟩ get <$> sequenceSource (fmapS just r) - ≡⟨ cong (_<$>_ get) (lemma-just-sequence SourceShapeT r) ⟩ + ≡⟨ P.cong (_<$>_ get) (lemma-just-sequence SourceShapeT r) ⟩ get <$> just r - ≡⟨ sym (lemma-just-sequence ViewShapeT (get r)) ⟩ + ≡⟨ P.sym (lemma-just-sequence ViewShapeT (get r)) ⟩ sequenceView (fmapV just (get r)) - ≡⟨ cong sequenceView (sym (free-theorem just r)) ⟩ + ≡⟨ P.cong sequenceView (P.sym (free-theorem just r)) ⟩ sequenceView (get (fmapS just r)) - ≡⟨ cong (sequenceView ∘ get) (sym (lemma-sequence-successful SourceShapeT v p)) ⟩ + ≡⟨ P.cong (sequenceView ∘ get) (P.sym (lemma-sequence-successful SourceShapeT v p)) ⟩ sequenceView (get v) ∎ sequenceV-cong : {S : Setoid ℓ₀ ℓ₀} {n : ℕ} {m₁ m₂ : Setoid.Carrier (VecISetoid (MaybeSetoid S) at n)} → VecISetoid (MaybeSetoid S) at _ ∋ m₁ ≈ m₂ → MaybeSetoid (VecISetoid S at n) ∋ sequenceV m₁ ≈ sequenceV m₂ @@ -241,15 +240,15 @@ sequenceV-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-con sequenceV-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | nothing | nothing | nothing = Setoid.refl (MaybeSetoid (VecISetoid S at _)) sequenceV-cong {S} (VecEq._∷-cong_ nothing xs≈ys) = Setoid.refl (MaybeSetoid (VecISetoid S at _)) -sequence-cong : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → (α : Setoid ℓ₀ ℓ₀) → {s : S} {x y : C (Maybe (Setoid.Carrier α)) s} → ShapedISetoid (EqSetoid S) ShapeT (MaybeSetoid α) at _ ∋ x ≈ y → MaybeSetoid (ShapedISetoid (EqSetoid S) ShapeT α at _) ∋ Shaped.sequence ShapeT x ≈ Shaped.sequence ShapeT y +sequence-cong : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → (α : Setoid ℓ₀ ℓ₀) → {s : S} {x y : C (Maybe (Setoid.Carrier α)) s} → ShapedISetoid (P.setoid S) ShapeT (MaybeSetoid α) at _ ∋ x ≈ y → MaybeSetoid (ShapedISetoid (P.setoid S) ShapeT α at _) ∋ Shaped.sequence ShapeT x ≈ Shaped.sequence ShapeT y sequence-cong ShapeT α {x = x} {y = y} (shape≈ , content≈) with sequenceV (Shaped.content ShapeT x) | sequenceV (Shaped.content ShapeT y) | sequenceV-cong content≈ -sequence-cong ShapeT α {s} (shape≈ , content≈) | .(just x) | .(just y) | just {x} {y} x≈y = just (refl , (begin +sequence-cong ShapeT α {s} (shape≈ , content≈) | .(just x) | .(just y) | just {x} {y} x≈y = just (P.refl , (begin content (fill s x) ≡⟨ fill-content s x ⟩ x ≈⟨ x≈y ⟩ y - ≡⟨ sym (fill-content s y) ⟩ + ≡⟨ P.sym (fill-content s y) ⟩ content (fill s y) ∎)) where open EqR (VecISetoid α at _) open Shaped ShapeT @@ -260,17 +259,17 @@ module _ (G : Get) where open Shaped SourceShapeT using () renaming (arity to arityS) open Shaped ViewShapeT using () renaming (content to contentV) - theorem-2 : {i : I} → (j : I) → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ j)) → (u : SourceContainer (Maybe Carrier) (gl₁ j)) → bff G j s v ≡ just u → ShapedISetoid (EqSetoid _) ViewShapeT (MaybeSetoid A.setoid) at _ ∋ get u ≈ Get.fmapV G just v + theorem-2 : {i : I} → (j : I) → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ j)) → (u : SourceContainer (Maybe Carrier) (gl₁ j)) → bff G j s v ≡ just u → ShapedISetoid (P.setoid _) ViewShapeT (MaybeSetoid A.setoid) at _ ∋ get u ≈ Get.fmapV G just v theorem-2 {i} j s v u p with lemma-<$>-just ((flip union (reshape (delete-many (contentV (get (enumerate SourceShapeT (gl₁ i)))) (fromFunc (denumerate SourceShapeT s))) (arityS (gl₁ j)))) <$> assoc (contentV (get (enumerate SourceShapeT (gl₁ j)))) (contentV v)) p theorem-2 {i} j s v u p | h′ , ph′ with lemma-<$>-just (assoc (contentV (get (enumerate SourceShapeT (gl₁ j)))) (contentV v)) ph′ - theorem-2 {i} j s v u p | h′ , ph′ | h , ph = refl , (begin + theorem-2 {i} j s v u p | h′ , ph′ | h , ph = P.refl , (begin contentV (get u) - ≡⟨ cong contentV (just-injective (trans (cong (_<$>_ get) (sym p)) - (cong (_<$>_ get ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) ph))) ⟩ + ≡⟨ P.cong contentV (just-injective (P.trans (P.cong (_<$>_ get) (P.sym p)) + (P.cong (_<$>_ get ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) ph))) ⟩ contentV (get (h′↦r (h↦h′ h))) - ≡⟨ refl ⟩ + ≡⟨ P.refl ⟩ contentV (get (fmapS (flip lookupM (h↦h′ h)) t)) - ≡⟨ cong contentV (free-theorem (flip lookupM (h↦h′ h)) t) ⟩ + ≡⟨ P.cong contentV (free-theorem (flip lookupM (h↦h′ h)) t) ⟩ contentV (fmapV (flip lookupM (h↦h′ h)) (get t)) ≡⟨ Shaped.fmap-content ViewShapeT (flip lookupM (h↦h′ h)) (get t) ⟩ map (flip lookupM (h↦h′ h)) (contentV (get t)) @@ -278,7 +277,7 @@ module _ (G : Get) where map (flip lookupM h) (contentV (get t)) ≈⟨ lemma-2 (contentV (get t)) (contentV v) h ph ⟩ map just (contentV v) - ≡⟨ sym (Shaped.fmap-content ViewShapeT just v) ⟩ + ≡⟨ P.sym (Shaped.fmap-content ViewShapeT just v) ⟩ contentV (fmapV just v) ∎) where open EqR (VecISetoid (MaybeSetoid A.setoid) at _) s′ = enumerate SourceShapeT (gl₁ i) @@ -291,10 +290,10 @@ module _ (G : Get) where module _ (G : Get) where open Get G - theorem-2′ : {i : I} → (j : I) → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ j)) → (u : SourceContainer Carrier (gl₁ j)) → bff G j s v ≡ just (Get.fmapS G just u) → ShapedISetoid (EqSetoid _) ViewShapeT A.setoid at _ ∋ get u ≈ v + theorem-2′ : {i : I} → (j : I) → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ j)) → (u : SourceContainer Carrier (gl₁ j)) → bff G j s v ≡ just (Get.fmapS G just u) → ShapedISetoid (P.setoid _) ViewShapeT A.setoid at _ ∋ get u ≈ v theorem-2′ j s v u p = drop-just (begin get <$> just u - ≡⟨ cong (_<$>_ get) (sym (lemma-just-sequence SourceShapeT u)) ⟩ + ≡⟨ P.cong (_<$>_ get) (P.sym (lemma-just-sequence SourceShapeT u)) ⟩ get <$> Shaped.sequence SourceShapeT (fmapS just u) ≡⟨ lemma-get-sequence G (lemma-just-sequence SourceShapeT u) ⟩ Shaped.sequence ViewShapeT (get (fmapS just u)) @@ -302,4 +301,4 @@ module _ (G : Get) where Shaped.sequence ViewShapeT (fmapV just v) ≡⟨ lemma-just-sequence ViewShapeT v ⟩ just v ∎) - where open EqR (MaybeSetoid (ShapedISetoid (EqSetoid _) ViewShapeT A.setoid at _)) + where open EqR (MaybeSetoid (ShapedISetoid (P.setoid _) ViewShapeT A.setoid at _)) diff --git a/CheckInsert.agda b/CheckInsert.agda index 316d8b1..6a1300b 100644 --- a/CheckInsert.agda +++ b/CheckInsert.agda @@ -13,9 +13,8 @@ open import Data.Vec.Properties using (lookup∘update′) open import Relation.Nullary using (Dec ; yes ; no ; ¬_) open import Relation.Nullary.Negation using (contradiction) open import Relation.Binary using (Setoid ; module DecSetoid) -open import Relation.Binary.Core using (refl ; _≡_ ; _≢_) import Relation.Binary.EqReasoning as EqR -open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans) +open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≢_ ; inspect ; [_] ; module ≡-Reasoning) open import FinMap @@ -43,44 +42,44 @@ insertionresult i x h | nothing | [ il ] = new il lemma-checkInsert-same : {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → lookupM i m ≡ just x → checkInsert i x m ≡ just m lemma-checkInsert-same i x m p with lookupM i m -lemma-checkInsert-same i x m refl | .(just x) with deq x x -lemma-checkInsert-same i x m refl | .(just x) | yes x≈x = refl -lemma-checkInsert-same i x m refl | .(just x) | no x≉x = contradiction A.refl x≉x +lemma-checkInsert-same i x m P.refl | .(just x) with deq x x +lemma-checkInsert-same i x m P.refl | .(just x) | yes x≈x = P.refl +lemma-checkInsert-same i x m P.refl | .(just x) | no x≉x = contradiction A.refl x≉x lemma-checkInsert-new : {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → lookupM i m ≡ nothing → checkInsert i x m ≡ just (insert i x m) lemma-checkInsert-new i x m p with lookupM i m -lemma-checkInsert-new i x m refl | .nothing = refl +lemma-checkInsert-new i x m P.refl | .nothing = P.refl lemma-checkInsert-wrong : {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → (x' : Carrier) → ¬ (x ≈ x') → lookupM i m ≡ just x' → checkInsert i x m ≡ nothing lemma-checkInsert-wrong i x m x' d p with lookupM i m -lemma-checkInsert-wrong i x m x' d refl | .(just x') with deq x x' -lemma-checkInsert-wrong i x m x' d refl | .(just x') | yes q = contradiction q d -lemma-checkInsert-wrong i x m x' d refl | .(just x') | no ¬q = refl +lemma-checkInsert-wrong i x m x' d P.refl | .(just x') with deq x x' +lemma-checkInsert-wrong i x m x' d P.refl | .(just x') | yes q = contradiction q d +lemma-checkInsert-wrong i x m x' d P.refl | .(just x') | no ¬q = P.refl lemma-checkInsert-restrict : {n m : ℕ} → (f : Fin n → Carrier) → (i : Fin n) → (is : Vec (Fin n) m) → checkInsert i (f i) (restrict f is) ≡ just (restrict f (i ∷V is)) lemma-checkInsert-restrict f i is with checkInsert i (f i) (restrict f is) | insertionresult i (f i) (restrict f is) -lemma-checkInsert-restrict f i is | ._ | same x fi≈x p = cong just (lemma-insert-same _ i (trans p (cong just (sym (lemma-lookupM-restrict i f is p))))) -lemma-checkInsert-restrict f i is | ._ | new _ = refl +lemma-checkInsert-restrict f i is | ._ | same x fi≈x p = P.cong just (lemma-insert-same _ i (P.trans p (P.cong just (P.sym (lemma-lookupM-restrict i f is p))))) +lemma-checkInsert-restrict f i is | ._ | new _ = P.refl lemma-checkInsert-restrict f i is | ._ | wrong x fi≉x p = contradiction (Setoid.reflexive A.setoid (lemma-lookupM-restrict i f is p)) fi≉x lemma-lookupM-checkInsert : {n : ℕ} → (i j : Fin n) → (h : FinMapMaybe n Carrier) → {x : Carrier} → lookupM i h ≡ just x → (y : Carrier) → {h' : FinMapMaybe n Carrier} → checkInsert j y h ≡ just h' → lookupM i h' ≡ just x lemma-lookupM-checkInsert i j h pl y ph' with checkInsert j y h | insertionresult j y h -lemma-lookupM-checkInsert i j h pl y refl | ._ | same _ _ _ = pl -lemma-lookupM-checkInsert i j h pl y ph' | ._ | new _ with i ≟ j -lemma-lookupM-checkInsert i .i h pl y ph' | ._ | new pl' | yes refl = contradiction (trans (sym pl) pl') (λ ()) -lemma-lookupM-checkInsert i j h {x} pl y refl | ._ | new _ | no i≢j = begin +lemma-lookupM-checkInsert i j h pl y P.refl | ._ | same _ _ _ = pl +lemma-lookupM-checkInsert i j h pl y ph' | ._ | new _ with i ≟ j +lemma-lookupM-checkInsert i .i h pl y ph' | ._ | new pl' | yes P.refl = contradiction (P.trans (P.sym pl) pl') (λ ()) +lemma-lookupM-checkInsert i j h {x} pl y P.refl | ._ | new _ | no i≢j = begin lookupM i (insert j y h) ≡⟨ lookup∘update′ i≢j h (just y) ⟩ lookupM i h ≡⟨ pl ⟩ just x ∎ - where open Relation.Binary.PropositionalEquality.≡-Reasoning + where open ≡-Reasoning lemma-lookupM-checkInsert i j h pl y () | ._ | wrong _ _ _ lemma-lookupM-checkInsert-other : {n : ℕ} → (i j : Fin n) → i ≢ j → (x : Carrier) → (h : FinMapMaybe n Carrier) → {h' : FinMapMaybe n Carrier} → checkInsert j x h ≡ just h' → lookupM i h' ≡ lookupM i h lemma-lookupM-checkInsert-other i j i≢j x h ph' with lookupM j h -lemma-lookupM-checkInsert-other i j i≢j x h ph' | just y with deq x y -lemma-lookupM-checkInsert-other i j i≢j x h refl | just y | yes x≈y = refl -lemma-lookupM-checkInsert-other i j i≢j x h () | just y | no x≉y -lemma-lookupM-checkInsert-other i j i≢j x h refl | nothing = lookup∘update′ i≢j h (just x) +lemma-lookupM-checkInsert-other i j i≢j x h ph' | just y with deq x y +lemma-lookupM-checkInsert-other i j i≢j x h P.refl | just y | yes x≈y = P.refl +lemma-lookupM-checkInsert-other i j i≢j x h () | just y | no x≉y +lemma-lookupM-checkInsert-other i j i≢j x h P.refl | nothing = lookup∘update′ i≢j h (just x) diff --git a/Examples.agda b/Examples.agda index bedad5a..a36ba3a 100644 --- a/Examples.agda +++ b/Examples.agda @@ -8,7 +8,7 @@ open import Data.List using (List ; length) renaming ([] to []L ; _∷_ to _∷L open import Data.Vec using (Vec ; [] ; _∷_ ; reverse ; _++_ ; tail ; take ; drop ; map) open import Function using (id) import Relation.Binary -open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; cong) +open import Relation.Binary.PropositionalEquality as P using (_≡_) open import Structures using (Shaped) import GetTypes @@ -40,7 +40,7 @@ tail' : Get tail' = assume-get suc id tail tail-example : bff ℕ-decSetoid tail' 2 (8 ∷ 5 ∷ []) (3 ∷ 1 ∷ []) ≡ just (just 8 ∷ just 3 ∷ just 1 ∷ []) -tail-example = refl +tail-example = P.refl take' : ℕ → Get take' n = assume-get (_+_ n) _ (take n) @@ -56,7 +56,7 @@ sieve' = assume-get id _ f f (x ∷ _ ∷ xs) = x ∷ f xs sieve-example : bff ℕ-decSetoid sieve' 4 (0 ∷ 2 ∷ []) (1 ∷ 3 ∷ []) ≡ just (just 1 ∷ just 2 ∷ just 3 ∷ nothing ∷ []) -sieve-example = refl +sieve-example = P.refl intersperse-len : ℕ → ℕ intersperse-len zero = zero @@ -74,10 +74,10 @@ intersperse' = assume-get suc intersperse-len f f (s ∷ v) = intersperse s v intersperse-neg-example : bff ℕ-decSetoid intersperse' 3 (0 ∷ []) (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ []) ≡ nothing -intersperse-neg-example = refl +intersperse-neg-example = P.refl intersperse-pos-example : bff ℕ-decSetoid intersperse' 3 (0 ∷ []) (1 ∷ 2 ∷ 3 ∷ 2 ∷ 5 ∷ []) ≡ just (map just (2 ∷ 1 ∷ 3 ∷ 5 ∷ [])) -intersperse-pos-example = refl +intersperse-pos-example = P.refl data PairVec (α : Set) (β : Set) : List α → Set where []P : PairVec α β []L @@ -101,9 +101,9 @@ PairVecFirstShaped α = record fill (a ∷L s) (b ∷ v) = a , b ∷P fill s v content-fill : {β : Set} {s : List α} → (p : PairVec α β s) → fill s (content p) ≡ p - content-fill []P = refl - content-fill (a , b ∷P p) = cong (_,_∷P_ a b) (content-fill p) + content-fill []P = P.refl + content-fill (a , b ∷P p) = P.cong (_,_∷P_ a b) (content-fill p) fill-content : {β : Set} → (s : List α) → (v : Vec β (length s)) → content (fill s v) ≡ v - fill-content []L [] = refl - fill-content (a ∷L s) (b ∷ v) = cong (_∷_ b) (fill-content s v) + fill-content []L [] = P.refl + fill-content (a ∷L s) (b ∷ v) = P.cong (_∷_ b) (fill-content s v) diff --git a/FinMap.agda b/FinMap.agda index 8322b79..57d3ecf 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -18,8 +18,8 @@ open import Function.Equality using (module Π) open import Function.Surjection using (module Surjection) open import Relation.Nullary using (yes ; no) open import Relation.Nullary.Negation using (contradiction) -open import Relation.Binary.Core using (_≡_ ; refl ; _≢_ ; Decidable) -open import Relation.Binary.PropositionalEquality as P using (cong ; sym ; _≗_ ; trans ; cong₂) +open import Relation.Binary.Core using (Decidable) +open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≢_ ; _≗_) open P.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) open import Generic using (just-injective) @@ -77,79 +77,79 @@ delete-many = flip (foldr (const _) delete) lemma-insert-same : {n : ℕ} {A : Set} → (m : FinMapMaybe n A) → (f : Fin n) → {a : A} → lookupM f m ≡ just a → m ≡ insert f a m lemma-insert-same [] () p -lemma-insert-same {suc n} (x ∷ xs) zero p = cong (flip _∷_ xs) p -lemma-insert-same (x ∷ xs) (suc i) p = cong (_∷_ x) (lemma-insert-same xs i p) +lemma-insert-same {suc n} (x ∷ xs) zero p = P.cong (flip _∷_ xs) p +lemma-insert-same (x ∷ xs) (suc i) p = P.cong (_∷_ x) (lemma-insert-same xs i p) lemma-lookupM-empty : {A : Set} {n : ℕ} → (i : Fin n) → lookupM {A} i empty ≡ nothing -lemma-lookupM-empty zero = refl +lemma-lookupM-empty zero = P.refl lemma-lookupM-empty (suc i) = lemma-lookupM-empty i lemma-lookupM-restrict : {A : Set} {n m : ℕ} → (i : Fin n) → (f : Fin n → A) → (is : Vec (Fin n) m) → {a : A} → lookupM i (restrict f is) ≡ just a → f i ≡ a -lemma-lookupM-restrict i f [] p = contradiction (trans (sym p) (lemma-lookupM-empty i)) (λ ()) +lemma-lookupM-restrict i f [] p = contradiction (P.trans (P.sym p) (lemma-lookupM-empty i)) (λ ()) lemma-lookupM-restrict i f (i' ∷ is) p with i ≟ i' -lemma-lookupM-restrict i f (.i ∷ is) {a} p | yes refl = just-injective (begin +lemma-lookupM-restrict i f (.i ∷ is) {a} p | yes P.refl = just-injective (begin just (f i) - ≡⟨ sym (lookup∘update i (restrict f is) (just (f i))) ⟩ + ≡⟨ P.sym (lookup∘update i (restrict f is) (just (f i))) ⟩ lookupM i (insert i (f i) (restrict f is)) ≡⟨ p ⟩ just a ∎) lemma-lookupM-restrict i f (i' ∷ is) {a} p | no i≢i' = lemma-lookupM-restrict i f is (begin lookupM i (restrict f is) - ≡⟨ sym (lookup∘update′ i≢i' (restrict f is) (just (f i'))) ⟩ + ≡⟨ P.sym (lookup∘update′ i≢i' (restrict f is) (just (f i'))) ⟩ lookupM i (insert i' (f i') (restrict f is)) ≡⟨ p ⟩ just a ∎) lemma-lookupM-restrict-∈ : {A : Set} {n m : ℕ} → (i : Fin n) → (f : Fin n → A) → (js : Vec (Fin n) m) → i ∈ js → lookupM i (restrict f js) ≡ just (f i) lemma-lookupM-restrict-∈ i f [] () lemma-lookupM-restrict-∈ i f (j ∷ js) p with i ≟ j -lemma-lookupM-restrict-∈ i f (.i ∷ js) p | yes refl = lookup∘update i (restrict f js) (just (f i)) +lemma-lookupM-restrict-∈ i f (.i ∷ js) p | yes P.refl = lookup∘update i (restrict f js) (just (f i)) lemma-lookupM-restrict-∈ i f (j ∷ js) (Any.here i≡j) | no i≢j = contradiction i≡j i≢j lemma-lookupM-restrict-∈ i f (j ∷ js) (Any.there p) | no i≢j = - trans (lookup∘update′ i≢j (restrict f js) (just (f j))) - (lemma-lookupM-restrict-∈ i f js p) + P.trans (lookup∘update′ i≢j (restrict f js) (just (f j))) + (lemma-lookupM-restrict-∈ i f js p) lemma-lookupM-restrict-∉ : {A : Set} {n m : ℕ} → (i : Fin n) → (f : Fin n → A) → (js : Vec (Fin n) m) → i ∉ js → lookupM i (restrict f js) ≡ nothing lemma-lookupM-restrict-∉ i f [] i∉[] = lemma-lookupM-empty i lemma-lookupM-restrict-∉ i f (j ∷ js) i∉jjs = - trans (lookup∘update′ (All.head i∉jjs) (restrict f js) (just (f j))) - (lemma-lookupM-restrict-∉ i f js (All.tail i∉jjs)) + P.trans (lookup∘update′ (All.head i∉jjs) (restrict f js) (just (f j))) + (lemma-lookupM-restrict-∉ i f js (All.tail i∉jjs)) lemma-tabulate-∘ : {n : ℕ} {A : Set} → {f g : Fin n → A} → f ≗ g → tabulate f ≡ tabulate g -lemma-tabulate-∘ {zero} {_} {f} {g} f≗g = refl -lemma-tabulate-∘ {suc n} {_} {f} {g} f≗g = cong₂ _∷_ (f≗g zero) (lemma-tabulate-∘ (f≗g ∘ suc)) +lemma-tabulate-∘ {zero} {_} {f} {g} f≗g = P.refl +lemma-tabulate-∘ {suc n} {_} {f} {g} f≗g = P.cong₂ _∷_ (f≗g zero) (lemma-tabulate-∘ (f≗g ∘ suc)) lemma-lookupM-fromFunc : {n : ℕ} {A : Set} → (f : Fin n → A) → flip lookupM (fromFunc f) ≗ Maybe.just ∘ f -lemma-lookupM-fromFunc f zero = refl +lemma-lookupM-fromFunc f zero = P.refl lemma-lookupM-fromFunc f (suc i) = lemma-lookupM-fromFunc (f ∘ suc) i lemma-lookupM-delete : {n : ℕ} {A : Set} {i j : Fin n} → (f : FinMapMaybe n A) → i ≢ j → lookupM i (delete j f) ≡ lookupM i f -lemma-lookupM-delete {i = zero} {j = zero} (_ ∷ _) p = contradiction refl p -lemma-lookupM-delete {i = zero} {j = suc j} (_ ∷ _) p = refl -lemma-lookupM-delete {i = suc i} {j = zero} (x ∷ xs) p = refl -lemma-lookupM-delete {i = suc i} {j = suc j} (x ∷ xs) p = lemma-lookupM-delete xs (p ∘ cong suc) +lemma-lookupM-delete {i = zero} {j = zero} (_ ∷ _) p = contradiction P.refl p +lemma-lookupM-delete {i = zero} {j = suc j} (_ ∷ _) p = P.refl +lemma-lookupM-delete {i = suc i} {j = zero} (x ∷ xs) p = P.refl +lemma-lookupM-delete {i = suc i} {j = suc j} (x ∷ xs) p = lemma-lookupM-delete xs (p ∘ P.cong suc) lemma-lookupM-delete-many : {n m : ℕ} {A : Set} (h : FinMapMaybe n A) → (i : Fin n) → (js : Vec (Fin n) m) → i ∉ js → lookupM i (delete-many js h) ≡ lookupM i h -lemma-lookupM-delete-many {n} h i [] i∉[] = refl +lemma-lookupM-delete-many {n} h i [] i∉[] = P.refl lemma-lookupM-delete-many {n} h i (j ∷ js) i∉jjs = - trans (lemma-lookupM-delete (delete-many js h) (All.head i∉jjs)) - (lemma-lookupM-delete-many h i js (All.tail i∉jjs)) + P.trans (lemma-lookupM-delete (delete-many js h) (All.head i∉jjs)) + (lemma-lookupM-delete-many h i js (All.tail i∉jjs)) lemma-reshape-id : {n : ℕ} {A : Set} → (m : FinMapMaybe n A) → reshape m n ≡ m -lemma-reshape-id [] = refl -lemma-reshape-id (x ∷ xs) = cong (_∷_ x) (lemma-reshape-id xs) +lemma-reshape-id [] = P.refl +lemma-reshape-id (x ∷ xs) = P.cong (_∷_ x) (lemma-reshape-id xs) lemma-disjoint-union : {n m : ℕ} {A : Set} → (f : Fin n → A) → (t : Vec (Fin n) m) → union (restrict f t) (delete-many t (fromFunc f)) ≡ fromFunc f lemma-disjoint-union {n} f t = lemma-tabulate-∘ inner where inner : (x : Fin n) → maybe′ just (lookupM x (delete-many t (fromFunc f))) (lookupM x (restrict f t)) ≡ just (f x) inner x with is-∈ _≟_ x t - inner x | yes-∈ x∈t = cong (maybe′ just (lookupM x (delete-many t (fromFunc f)))) (lemma-lookupM-restrict-∈ x f t x∈t) + inner x | yes-∈ x∈t = P.cong (maybe′ just (lookupM x (delete-many t (fromFunc f)))) (lemma-lookupM-restrict-∈ x f t x∈t) inner x | no-∉ x∉t = begin maybe′ just (lookupM x (delete-many t (fromFunc f))) (lookupM x (restrict f t)) - ≡⟨ cong₂ (maybe′ just) (lemma-lookupM-delete-many (fromFunc f) x t x∉t) (lemma-lookupM-restrict-∉ x f t x∉t) ⟩ + ≡⟨ P.cong₂ (maybe′ just) (lemma-lookupM-delete-many (fromFunc f) x t x∉t) (lemma-lookupM-restrict-∉ x f t x∉t) ⟩ maybe′ just (lookupM x (fromFunc f)) nothing ≡⟨ lemma-lookupM-fromFunc f x ⟩ just (f x) ∎ lemma-exchange-maps : {n m : ℕ} → {A : Set} → {h h′ : FinMapMaybe n A} → {P : Fin n → Set} → (∀ j → P j → lookupM j h ≡ lookupM j h′) → {is : Vec (Fin n) m} → All P (toList is) → mapV (flip lookupM h) is ≡ mapV (flip lookupM h′) is -lemma-exchange-maps h≈h′ {[]} All.[] = refl -lemma-exchange-maps h≈h′ {i ∷ is} (pi All.∷ pis) = cong₂ _∷_ (h≈h′ i pi) (lemma-exchange-maps h≈h′ pis) +lemma-exchange-maps h≈h′ {[]} All.[] = P.refl +lemma-exchange-maps h≈h′ {i ∷ is} (pi All.∷ pis) = P.cong₂ _∷_ (h≈h′ i pi) (lemma-exchange-maps h≈h′ pis) diff --git a/Generic.agda b/Generic.agda index 9046ebb..90f5816 100644 --- a/Generic.agda +++ b/Generic.agda @@ -13,19 +13,18 @@ open import Function using (_∘_ ; id ; flip) open import Function.Equality using (_⟶_) open import Level using () renaming (zero to ℓ₀) open import Relation.Binary using (Setoid ; module Setoid) -open import Relation.Binary.Core using (_≡_ ; refl) open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid) -open import Relation.Binary.PropositionalEquality using (_≗_ ; cong ; subst ; trans ; cong₂) renaming (setoid to EqSetoid) +open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≗_) open Setoid using () renaming (_≈_ to _∋_≈_) open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_) open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_) -≡-to-Π : {A B : Set} → (A → B) → EqSetoid A ⟶ EqSetoid B -≡-to-Π f = record { _⟨$⟩_ = f; cong = cong f } +≡-to-Π : {A B : Set} → (A → B) → P.setoid A ⟶ P.setoid B +≡-to-Π f = record { _⟨$⟩_ = f; cong = P.cong f } just-injective : {A : Set} → {x y : A} → Maybe.just x ≡ Maybe.just y → x ≡ y -just-injective refl = refl +just-injective P.refl = P.refl sequenceV : {A : Set} {n : ℕ} → Vec (Maybe A) n → Maybe (Vec A n) sequenceV []V = just []V @@ -35,39 +34,39 @@ mapMV : {A B : Set} {n : ℕ} → (A → Maybe B) → Vec A n → Maybe (Vec B n mapMV f = sequenceV ∘ map f mapMV-cong : {A B : Set} {f g : A → Maybe B} → f ≗ g → {n : ℕ} → mapMV {n = n} f ≗ mapMV g -mapMV-cong f≗g v = cong sequenceV (map-cong f≗g v) +mapMV-cong f≗g v = P.cong sequenceV (map-cong f≗g v) mapMV-purity : {A B : Set} {n : ℕ} → (f : A → B) → (v : Vec A n) → mapMV (Maybe.just ∘ f) v ≡ just (map f v) -mapMV-purity f []V = refl -mapMV-purity f (x ∷V xs) = cong (_<$>_ (_∷V_ (f x))) (mapMV-purity f xs) +mapMV-purity f []V = P.refl +mapMV-purity f (x ∷V xs) = P.cong (_<$>_ (_∷V_ (f x))) (mapMV-purity f xs) -maybeEq-from-≡ : {A : Set} {a b : Maybe A} → a ≡ b → MaybeEq (EqSetoid A) ∋ a ≈ b -maybeEq-from-≡ {a = just x} {b = .(just x)} refl = just refl -maybeEq-from-≡ {a = nothing} {b = .nothing} refl = nothing +maybeEq-from-≡ : {A : Set} {a b : Maybe A} → a ≡ b → MaybeEq (P.setoid A) ∋ a ≈ b +maybeEq-from-≡ {a = just x} {b = .(just x)} P.refl = just P.refl +maybeEq-from-≡ {a = nothing} {b = .nothing} P.refl = nothing -maybeEq-to-≡ : {A : Set} {a b : Maybe A} → MaybeEq (EqSetoid A) ∋ a ≈ b → a ≡ b -maybeEq-to-≡ (just refl) = refl -maybeEq-to-≡ nothing = refl +maybeEq-to-≡ : {A : Set} {a b : Maybe A} → MaybeEq (P.setoid A) ∋ a ≈ b → a ≡ b +maybeEq-to-≡ (just P.refl) = P.refl +maybeEq-to-≡ nothing = P.refl subst-cong : {A : Set} → (T : A → Set) → {g : A → A} → {a b : A} → (f : {c : A} → T c → T (g c)) → (p : a ≡ b) → - f ∘ subst T p ≗ subst T (cong g p) ∘ f -subst-cong T f refl _ = refl + f ∘ P.subst T p ≗ P.subst T (P.cong g p) ∘ f +subst-cong T f P.refl _ = P.refl subst-fromList : {A : Set} {x y : List A} → (p : y ≡ x) → - subst (Vec A) (cong length p) (fromList y) ≡ fromList x -subst-fromList refl = refl + P.subst (Vec A) (P.cong length p) (fromList y) ≡ fromList x +subst-fromList P.refl = P.refl subst-subst : {A : Set} (T : A → Set) {a b c : A} → (p : a ≡ b) → (p′ : b ≡ c) → (x : T a) → - subst T p′ (subst T p x) ≡ subst T (trans p p′) x -subst-subst T refl p′ x = refl + P.subst T p′ (P.subst T p x) ≡ P.subst T (P.trans p p′) x +subst-subst T P.refl p′ x = P.refl toList-fromList : {A : Set} → (l : List A) → toList (fromList l) ≡ l -toList-fromList []L = refl -toList-fromList (x ∷L xs) = cong (_∷L_ x) (toList-fromList xs) +toList-fromList []L = P.refl +toList-fromList (x ∷L xs) = P.cong (_∷L_ x) (toList-fromList xs) toList-subst : {A : Set} → {n m : ℕ} (v : Vec A n) → (p : n ≡ m) → - toList (subst (Vec A) p v) ≡ toList v -toList-subst v refl = refl + toList (P.subst (Vec A) p v) ≡ toList v +toList-subst v P.refl = P.refl VecISetoid : Setoid ℓ₀ ℓ₀ → ISetoid ℕ ℓ₀ ℓ₀ VecISetoid S = record diff --git a/LiftGet.agda b/LiftGet.agda index 35bafb1..9e2a805 100644 --- a/LiftGet.agda +++ b/LiftGet.agda @@ -7,9 +7,8 @@ open import Data.List using (List ; [] ; _∷_ ; length ; replicate ; map) open import Data.List.Properties using (length-map ; length-replicate) open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂) open import Function using (_∘_ ; flip ; const) -open import Relation.Binary.Core using (_≡_) -open import Relation.Binary.PropositionalEquality using (_≗_ ; sym ; cong ; refl ; subst ; trans ; proof-irrelevance ; module ≡-Reasoning) -open import Relation.Binary.HeterogeneousEquality as H using (module ≅-Reasoning ; _≅_ ; ≅-to-≡ ; ≡-to-≅ ; ≡-subst-removable) renaming (refl to het-refl ; sym to het-sym ; cong to het-cong ; reflexive to het-reflexive) +open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≗_ ; proof-irrelevance ; module ≡-Reasoning) +open import Relation.Binary.HeterogeneousEquality as H using (module ≅-Reasoning ; _≅_ ; ≅-to-≡ ; ≡-to-≅ ; ≡-subst-removable) import FreeTheorems open import Generic using (toList-fromList ; toList-subst) @@ -20,12 +19,12 @@ getVec-to-getList : {getlen : ℕ → ℕ} → (getV-type getlen) → get-type getVec-to-getList get = toList ∘ get ∘ fromList fromList∘map : {α β : Set} → (f : α → β) → (l : List α) → fromList (map f l) ≅ mapV f (fromList l) -fromList∘map f [] = het-refl +fromList∘map f [] = H.refl fromList∘map f (x ∷ xs) = H.cong₂ (λ n → _∷V_ {n = n} (f x)) (H.reflexive (length-map f xs)) (fromList∘map f xs) toList∘map : {α β : Set} {n : ℕ} → (f : α → β) → (v : Vec α n) → toList (mapV f v) ≡ map f (toList v) -toList∘map f []V = refl -toList∘map f (x ∷V xs) = cong (_∷_ (f x)) (toList∘map f xs) +toList∘map f []V = P.refl +toList∘map f (x ∷V xs) = P.cong (_∷_ (f x)) (toList∘map f xs) GetV-to-GetL : GetV → GetL GetV-to-GetL getrecord = record { get = toList ∘ get ∘ fromList; free-theorem = ft } @@ -34,9 +33,9 @@ GetV-to-GetL getrecord = record { get = toList ∘ get ∘ fromList; free-theore ft : {α β : Set} → (f : α → β) → (xs : List α) → toList (get (fromList (map f xs))) ≡ map f (toList (get (fromList xs))) ft f xs = begin toList (get (fromList (map f xs))) - ≅⟨ H.cong₂ {B = Vec _} (λ n → toList ∘ get) (het-reflexive (length-map f xs)) (fromList∘map f xs) ⟩ + ≅⟨ H.cong₂ {B = Vec _} (λ n → toList ∘ get) (H.reflexive (length-map f xs)) (fromList∘map f xs) ⟩ toList (get (mapV f (fromList xs))) - ≡⟨ cong toList (free-theorem f (fromList xs)) ⟩ + ≡⟨ P.cong toList (free-theorem f (fromList xs)) ⟩ toList (mapV f (get (fromList xs))) ≡⟨ toList∘map f (get (fromList xs)) ⟩ map f (toList (get (fromList xs))) ∎ @@ -45,30 +44,30 @@ getList-to-getlen : get-type → ℕ → ℕ getList-to-getlen get = length ∘ get ∘ flip replicate tt replicate-length : {A : Set} → (l : List A) → map (const tt) l ≡ replicate (length l) tt -replicate-length [] = refl -replicate-length (_ ∷ l) = cong (_∷_ tt) (replicate-length l) +replicate-length [] = P.refl +replicate-length (_ ∷ l) = P.cong (_∷_ tt) (replicate-length l) getList-length : (get : get-type) → {B : Set} → (l : List B) → length (get l) ≡ getList-to-getlen get (length l) getList-length get l = begin length (get l) - ≡⟨ sym (length-map (const tt) (get l)) ⟩ + ≡⟨ P.sym (length-map (const tt) (get l)) ⟩ length (map (const tt) (get l)) - ≡⟨ cong length (sym (free-theoremL get (const tt) l)) ⟩ + ≡⟨ P.cong length (P.sym (free-theoremL get (const tt) l)) ⟩ length (get (map (const tt) l)) - ≡⟨ cong (length ∘ get) (replicate-length l) ⟩ + ≡⟨ P.cong (length ∘ get) (replicate-length l) ⟩ length (get (replicate (length l) tt)) ∎ where open ≡-Reasoning length-toList : {A : Set} {n : ℕ} → (v : Vec A n) → length (toList v) ≡ n -length-toList []V = refl -length-toList (x ∷V xs) = cong suc (length-toList xs) +length-toList []V = P.refl +length-toList (x ∷V xs) = P.cong suc (length-toList xs) getList-to-getVec-length-property : (get : get-type) → {C : Set} → {m : ℕ} → (v : Vec C m) → length (get (toList v)) ≡ length (get (replicate m tt)) getList-to-getVec-length-property get {_} {m} v = begin length (get (toList v)) ≡⟨ getList-length get (toList v) ⟩ length (get (replicate (length (toList v)) tt)) - ≡⟨ cong (length ∘ get ∘ flip replicate tt) (length-toList v) ⟩ + ≡⟨ P.cong (length ∘ get ∘ flip replicate tt) (length-toList v) ⟩ length (get (replicate m tt)) ∎ where open ≡-Reasoning @@ -77,7 +76,7 @@ getList-to-getVec get = getlen , get' where getlen : ℕ → ℕ getlen = getList-to-getlen get get' : {C : Set} {m : ℕ} → Vec C m → Vec C (getlen m) - get' {C} v = subst (Vec C) (getList-to-getVec-length-property get v) (fromList (get (toList v))) + get' {C} v = P.subst (Vec C) (getList-to-getVec-length-property get v) (fromList (get (toList v))) private module GetV-Implementation (getrecord : GetL) where @@ -91,21 +90,21 @@ private length-property = getList-to-getVec-length-property get getV : {C : Set} {m : ℕ} → Vec C m → Vec C (getlen m) - getV s = subst (Vec _) (length-property s) (fromList (get (toList s))) + getV s = P.subst (Vec _) (length-property s) (fromList (get (toList s))) ft : {α β : Set} (f : α → β) {n : ℕ} (v : Vec α n) → getV (mapV f v) ≡ mapV f (getV v) ft f v = ≅-to-≡ (begin - subst (Vec _) (length-property (mapV f v)) (fromList (get (toList (mapV f v)))) + P.subst (Vec _) (length-property (mapV f v)) (fromList (get (toList (mapV f v)))) ≅⟨ ≡-subst-removable (Vec _) (length-property (mapV f v)) (fromList (get (toList (mapV f v)))) ⟩ fromList (get (toList (mapV f v))) - ≅⟨ het-cong (fromList ∘ get) (het-reflexive (toList∘map f v)) ⟩ + ≅⟨ H.cong (fromList ∘ get) (H.reflexive (toList∘map f v)) ⟩ fromList (get (map f (toList v))) - ≅⟨ het-cong fromList (het-reflexive (free-theorem f (toList v))) ⟩ + ≅⟨ H.cong fromList (H.reflexive (free-theorem f (toList v))) ⟩ fromList (map f (get (toList v))) ≅⟨ fromList∘map f (get (toList v)) ⟩ mapV f (fromList (get (toList v))) ≅⟨ H.cong₂ (λ n → mapV {n = n} f) (H.reflexive (length-property v)) (H.sym (≡-subst-removable (Vec _) (length-property v) (fromList (get (toList v))))) ⟩ - mapV f (subst (Vec _) (length-property v) (fromList (get (toList v)))) ∎) + mapV f (P.subst (Vec _) (length-property v) (fromList (get (toList v)))) ∎) where open ≅-Reasoning GetL-to-GetV : GetL → GetV @@ -115,33 +114,33 @@ GetL-to-GetV getrecord = record { getlen = getlen; get = getV; free-theorem = ft get-commut-1-≅ : (get : get-type) {A : Set} → (l : List A) → fromList (get l) ≅ proj₂ (getList-to-getVec get) (fromList l) get-commut-1-≅ get l = begin fromList (get l) - ≅⟨ het-cong (fromList ∘ get) (≡-to-≅ (sym (toList-fromList l))) ⟩ + ≅⟨ H.cong (fromList ∘ get) (≡-to-≅ (P.sym (toList-fromList l))) ⟩ fromList (get (toList (fromList l))) - ≅⟨ het-sym (≡-subst-removable (Vec _) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l))))) ⟩ - subst (Vec _) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l)))) ∎ + ≅⟨ H.sym (≡-subst-removable (Vec _) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l))))) ⟩ + P.subst (Vec _) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l)))) ∎ where open ≅-Reasoning -get-commut-1 : (get : get-type) {A : Set} → (l : List A) → fromList (get l) ≡ subst (Vec A) (sym (getList-length get l)) (proj₂ (getList-to-getVec get) (fromList l)) +get-commut-1 : (get : get-type) {A : Set} → (l : List A) → fromList (get l) ≡ P.subst (Vec A) (P.sym (getList-length get l)) (proj₂ (getList-to-getVec get) (fromList l)) get-commut-1 get {A} l = ≅-to-≡ (begin fromList (get l) ≅⟨ get-commut-1-≅ get l ⟩ proj₂ (getList-to-getVec get) (fromList l) - ≅⟨ het-sym (≡-subst-removable (Vec _) (sym (getList-length get l)) (proj₂ (getList-to-getVec get) (fromList l))) ⟩ - subst (Vec _) (sym (getList-length get l)) (proj₂ (getList-to-getVec get) (fromList l)) ∎) + ≅⟨ H.sym (≡-subst-removable (Vec _) (P.sym (getList-length get l)) (proj₂ (getList-to-getVec get) (fromList l))) ⟩ + P.subst (Vec _) (P.sym (getList-length get l)) (proj₂ (getList-to-getVec get) (fromList l)) ∎) where open ≅-Reasoning get-trafo-1 : (get : get-type) → {B : Set} → getVec-to-getList (proj₂ (getList-to-getVec get)) {B} ≗ get {B} get-trafo-1 get {B} l = begin getVec-to-getList (proj₂ (getList-to-getVec get)) l - ≡⟨ refl ⟩ + ≡⟨ P.refl ⟩ toList (proj₂ (getList-to-getVec get) (fromList l)) - ≡⟨ refl ⟩ - toList (subst (Vec B) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l))))) + ≡⟨ P.refl ⟩ + toList (P.subst (Vec B) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l))))) ≡⟨ toList-subst (fromList (get (toList (fromList l)))) (getList-to-getVec-length-property get (fromList l)) ⟩ toList (fromList (get (toList (fromList l)))) ≡⟨ toList-fromList (get (toList (fromList l))) ⟩ get (toList (fromList l)) - ≡⟨ cong get (toList-fromList l) ⟩ + ≡⟨ P.cong get (toList-fromList l) ⟩ get l ∎ where open ≡-Reasoning @@ -152,26 +151,26 @@ vec-len : {A : Set} {n : ℕ} → Vec A n → ℕ vec-len {_} {n} _ = n fromList-toList : {A : Set} {n : ℕ} → (v : Vec A n) → fromList (toList v) ≅ v -fromList-toList []V = het-refl -fromList-toList (x ∷V xs) = H.cong₂ (λ n → _∷V_ {n = n} x) (het-reflexive (length-toList xs)) (fromList-toList xs) +fromList-toList []V = H.refl +fromList-toList (x ∷V xs) = H.cong₂ (λ n → _∷V_ {n = n} x) (H.reflexive (length-toList xs)) (fromList-toList xs) get-commut-2 : {getlen : ℕ → ℕ} → (get : getV-type getlen) → {B : Set} {n : ℕ} → (toList ∘ get {B} {n}) ≗ (getVec-to-getList get) ∘ toList -get-commut-2 get {B} v = sym (≅-to-≡ (H.cong₂ (λ n → toList ∘ get {n = n}) (H.reflexive (length-toList v)) (fromList-toList v))) +get-commut-2 get {B} v = P.sym (≅-to-≡ (H.cong₂ (λ n → toList ∘ get {n = n}) (H.reflexive (length-toList v)) (fromList-toList v))) get-trafo-2-getlen : {getlen : ℕ → ℕ} → (get : getV-type getlen) → proj₁ (getList-to-getVec (getVec-to-getList get)) ≗ getlen get-trafo-2-getlen {getlen} get n = begin proj₁ (getList-to-getVec (getVec-to-getList get)) n - ≡⟨ refl ⟩ + ≡⟨ P.refl ⟩ length (toList (get (fromList (replicate n tt)))) ≡⟨ length-toList (get (fromList (replicate n tt))) ⟩ vec-len (get (fromList (replicate n tt))) - ≡⟨ cong getlen (length-replicate n) ⟩ + ≡⟨ P.cong getlen (length-replicate n) ⟩ getlen n ∎ where open ≡-Reasoning get-trafo-2-get-≅ : {getlen : ℕ → ℕ} → (get : getV-type getlen) → {B : Set} {n : ℕ} → (v : Vec B n) → proj₂ (getList-to-getVec (getVec-to-getList get)) v ≅ get v get-trafo-2-get-≅ {getlen} get v = begin - subst (Vec _) (getList-to-getVec-length-property (getVec-to-getList get) v) (fromList (toList (get (fromList (toList v))))) + P.subst (Vec _) (getList-to-getVec-length-property (getVec-to-getList get) v) (fromList (toList (get (fromList (toList v))))) ≅⟨ ≡-subst-removable (Vec _) (getList-to-getVec-length-property (getVec-to-getList get) v) (fromList (toList (get (fromList (toList v))))) ⟩ fromList (toList (get (fromList (toList v)))) ≅⟨ fromList-toList (get (fromList (toList v))) ⟩ @@ -180,11 +179,11 @@ get-trafo-2-get-≅ {getlen} get v = begin get v ∎ where open ≅-Reasoning -get-trafo-2-get : {getlen : ℕ → ℕ} → (get : getV-type getlen) → {B : Set} {n : ℕ} → proj₂ (getList-to-getVec (getVec-to-getList get)) ≗ subst (Vec B) (sym (get-trafo-2-getlen get n)) ∘ get +get-trafo-2-get : {getlen : ℕ → ℕ} → (get : getV-type getlen) → {B : Set} {n : ℕ} → proj₂ (getList-to-getVec (getVec-to-getList get)) ≗ P.subst (Vec B) (P.sym (get-trafo-2-getlen get n)) ∘ get get-trafo-2-get get v = ≅-to-≡ (begin proj₂ (getList-to-getVec (getVec-to-getList get)) v ≅⟨ get-trafo-2-get-≅ get v ⟩ get v - ≅⟨ het-sym (≡-subst-removable (Vec _) (sym (get-trafo-2-getlen get (vec-len v))) (get v)) ⟩ - subst (Vec _) (sym (get-trafo-2-getlen get (vec-len v))) (get v) ∎) + ≅⟨ H.sym (≡-subst-removable (Vec _) (P.sym (get-trafo-2-getlen get (vec-len v))) (get v)) ⟩ + P.subst (Vec _) (P.sym (get-trafo-2-getlen get (vec-len v))) (get v) ∎) where open ≅-Reasoning diff --git a/Precond.agda b/Precond.agda index cc81db4..07775ac 100644 --- a/Precond.agda +++ b/Precond.agda @@ -1,4 +1,5 @@ -open import Relation.Binary.Core using (Decidable ; _≡_) +open import Relation.Binary.Core using (Decidable) +open import Relation.Binary.PropositionalEquality using (_≡_) module Precond (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where @@ -21,29 +22,29 @@ open import Data.Maybe using (just) open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂) open import Function using (flip ; _∘_ ; id) open import Relation.Binary using (Setoid) -open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym ; decSetoid) -open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) +open import Relation.Binary.PropositionalEquality as P using (inspect ; [_]) +open P.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) open import Relation.Nullary using (yes ; no) open import Structures using (IsFunctor ; module Shaped ; Shaped) open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty ; delete-many ; lemma-tabulate-∘ ; delete ; lemma-lookupM-delete ; lemma-lookupM-fromFunc ; reshape ; lemma-reshape-id) import CheckInsert -open CheckInsert (decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other) +open CheckInsert (P.decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other) import BFF import Bidir -open Bidir (decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain) +open Bidir (P.decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain) import GetTypes open GetTypes.PartialShapeShape using (Get ; module Get) -open BFF.PartialShapeBFF (decSetoid deq) using (assoc ; enumerate ; denumerate ; bff) +open BFF.PartialShapeBFF (P.decSetoid deq) using (assoc ; enumerate ; denumerate ; bff) lemma-maybe-just : {A : Set} → (a : A) → (ma : Maybe A) → maybe′ Maybe.just (just a) ma ≡ Maybe.just (maybe′ id a ma) -lemma-maybe-just a (just x) = refl -lemma-maybe-just a nothing = refl +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 = _ , (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) ⟩ + ≡⟨ P.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)) ∎)) @@ -55,20 +56,20 @@ lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} (Data.List.A _ ∎) 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 + inner .i | yes P.refl = begin maybe′ just (lookupM i (delete i (delete-many is (fromFunc g)))) (lookup i h) - ≡⟨ cong (maybe′ just _) px ⟩ + ≡⟨ P.cong (maybe′ just _) px ⟩ just x - ≡⟨ cong (maybe′ just _) (sym px) ⟩ + ≡⟨ P.cong (maybe′ just _) (P.sym px) ⟩ maybe′ just (lookupM i (delete-many is (fromFunc g))) (lookup i h) ∎ - inner f | no f≢i = cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-delete (delete-many is (fromFunc g)) f≢i) + inner f | no f≢i = P.cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-delete (delete-many is (fromFunc g)) f≢i) module _ (G : Get) where open Get G open Shaped ViewShapeT using () renaming (content to contentV) assoc-enough : {i : I} → (j : I) → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ j)) → ∃ (λ h → assoc (contentV (get (enumerate SourceShapeT (gl₁ j)))) (contentV v) ≡ just h) → ∃ λ u → bff G j s v ≡ just u - assoc-enough {i} j s v (h , p) = _ , cong (_<$>_ ((λ f → fmapS f t) ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ (Shaped.arity SourceShapeT (gl₁ j))))) p + assoc-enough {i} j s v (h , p) = _ , P.cong (_<$>_ ((λ f → fmapS f t) ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ (Shaped.arity SourceShapeT (gl₁ j))))) p where g′ = delete-many (contentV (get (enumerate SourceShapeT (gl₁ i)))) (fromFunc (denumerate SourceShapeT s)) t = enumerate SourceShapeT (gl₁ j) @@ -81,10 +82,10 @@ module _ (G : Get) where bff G i s v ≡⟨ proj₂ (assoc-enough G i s v (h , p)) ⟩ just (fmapS (flip lookupM (union h (reshape g′ (Shaped.arity SourceShapeT (gl₁ i))))) t) - ≡⟨ cong just (begin _ - ≡⟨ cong ((λ f → fmapS f t) ∘ flip lookupM ∘ union h) (lemma-reshape-id g′) ⟩ + ≡⟨ P.cong just (begin _ + ≡⟨ P.cong ((λ f → fmapS f t) ∘ flip lookupM ∘ union h) (lemma-reshape-id g′) ⟩ fmapS (flip lookupM (union h g′)) t - ≡⟨ cong ((λ f → fmapS f t) ∘ flip lookupM) (proj₂ wp) ⟩ + ≡⟨ P.cong ((λ f → fmapS f t) ∘ flip lookupM) (proj₂ wp) ⟩ fmapS (flip lookupM (fromFunc (proj₁ wp))) t ≡⟨ IsFunctor.cong (Shaped.isFunctor SourceShapeT (gl₁ i)) (lemma-lookupM-fromFunc (proj₁ wp)) t ⟩ fmapS (Maybe.just ∘ proj₁ wp) t @@ -101,9 +102,9 @@ data All-different {A : Set} : List A → Set where different-∷ : {x : A} {xs : List A} → x ∉ xs → All-different xs → All-different (x ∷ xs) lemma-∉-lookupM-assoc : {m n : ℕ} → (i : Fin n) → (is : Vec (Fin n) m) → (xs : Vec Carrier m) → {h : FinMapMaybe n Carrier} → assoc is xs ≡ just h → (i ∉ toList is) → lookupM i h ≡ nothing -lemma-∉-lookupM-assoc i [] [] refl i∉is = lemma-lookupM-empty i -lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') ph i∉is with assoc is' xs' | inspect (assoc is') xs' -lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') () i∉is | nothing | [ ph' ] +lemma-∉-lookupM-assoc i [] [] P.refl i∉is = lemma-lookupM-empty i +lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') ph i∉is with assoc is' xs' | inspect (assoc is') xs' +lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') () i∉is | nothing | [ ph' ] lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') {h} ph i∉is | just h' | [ ph' ] = begin lookupM i h ≡⟨ lemma-lookupM-checkInsert-other i i' (i∉is ∘ here) x' h' ph ⟩ @@ -112,13 +113,13 @@ lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') {h} ph i∉is | just h' | [ nothing ∎ different-assoc : {m n : ℕ} → (u : Vec (Fin n) m) → (v : Vec Carrier m) → All-different (toList u) → ∃ λ h → assoc u v ≡ just h -different-assoc [] [] p = empty , refl +different-assoc [] [] p = empty , P.refl different-assoc (u ∷ us) (v ∷ vs) (different-∷ u∉us diff-us) with different-assoc us vs diff-us different-assoc (u ∷ us) (v ∷ vs) (different-∷ u∉us diff-us) | h , p' = insert u v h , (begin assoc (u ∷ us) (v ∷ vs) - ≡⟨ refl ⟩ + ≡⟨ P.refl ⟩ (assoc us vs >>= checkInsert u v) - ≡⟨ cong (flip _>>=_ (checkInsert u v)) p' ⟩ + ≡⟨ P.cong (flip _>>=_ (checkInsert u v)) p' ⟩ checkInsert u v h ≡⟨ lemma-checkInsert-new u v h (lemma-∉-lookupM-assoc u us vs p' u∉us) ⟩ just (insert u v h) ∎) diff --git a/Structures.agda b/Structures.agda index 10abd42..1a8fd64 100644 --- a/Structures.agda +++ b/Structures.agda @@ -9,7 +9,7 @@ import Data.Vec.Properties as VP open import Function using (_∘_ ; flip ; id) open import Function.Equality using (_⟶_ ; _⇨_ ; _⟨$⟩_) open import Relation.Binary using (_Preserves_⟶_) -open import Relation.Binary.PropositionalEquality as P using (_≗_ ; _≡_ ; refl ; module ≡-Reasoning) +open import Relation.Binary.PropositionalEquality as P using (_≗_ ; _≡_ ; module ≡-Reasoning) open import Generic using (sequenceV) @@ -26,7 +26,7 @@ record IsFunctor (F : Set → Set) (f : {α β : Set} → (α → β) → F α { _⟨$⟩_ = f (_⟨$⟩_ g) ; cong = P.cong (f (_⟨$⟩_ g)) } - ; cong = λ {g} {h} g≗h {x} x≡y → P.subst (λ z → f (_⟨$⟩_ g) x ≡ f (_⟨$⟩_ h) z) x≡y (cong (λ _ → g≗h refl) x) + ; cong = λ {g} {h} g≗h {x} x≡y → P.subst (λ z → f (_⟨$⟩_ g) x ≡ f (_⟨$⟩_ h) z) x≡y (cong (λ _ → g≗h P.refl) x) } record Functor (f : Set → Set) : Set₁ where |