diff options
| -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 |