From c835e655a05c73f7dd2dc46c652be3d43e91a4b7 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Sun, 25 Nov 2018 10:35:23 +0100 Subject: 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. --- LiftGet.agda | 81 ++++++++++++++++++++++++++++++------------------------------ 1 file changed, 40 insertions(+), 41 deletions(-) (limited to 'LiftGet.agda') 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 -- cgit v1.2.3