diff options
Diffstat (limited to 'LiftGet.agda')
| -rw-r--r-- | LiftGet.agda | 81 |
1 files changed, 40 insertions, 41 deletions
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 |