From 7391996c5907714d75adba63c8a8063da77a655b Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Thu, 30 Aug 2012 14:18:54 +0200 Subject: give the type of different gets a name --- LiftGet.agda | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/LiftGet.agda b/LiftGet.agda index c5a8880..b2273f0 100644 --- a/LiftGet.agda +++ b/LiftGet.agda @@ -11,20 +11,26 @@ open import Relation.Binary.Core using (_≡_) open import Relation.Binary.PropositionalEquality using (_≗_ ; sym ; cong ; refl) open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) -getVec-to-getList : {getlen : ℕ → ℕ} → ({A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)) → ({B : Set} → List B → List B) +get-type : Set₁ +get-type = {A : Set} → List A → List A + +getV-type : (ℕ → ℕ) → Set₁ +getV-type getlen = {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n) + +getVec-to-getList : {getlen : ℕ → ℕ} → (getV-type getlen) → get-type getVec-to-getList get = toList ∘ get ∘ fromList -getList-to-getlen : ({A : Set} → List A → List A) → ℕ → ℕ +getList-to-getlen : get-type → ℕ → ℕ getList-to-getlen get = length ∘ get ∘ flip replicate tt postulate - free-theorem-list-list : {β γ : Set} → (get : {α : Set} → List α → List α) → (f : β → γ) → get ∘ map f ≗ map f ∘ get + free-theorem-list-list : {β γ : Set} → (get : get-type) → (f : β → γ) → get ∘ map f ≗ map f ∘ get 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) -getList-length : (get : {A : Set} → List A → List A) → {B : Set} → (l : List B) → length (get l) ≡ getList-to-getlen get (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)) ⟩ @@ -41,7 +47,7 @@ length-toList (x ∷V xs) = cong suc (length-toList xs) vec-length : {A : Set} {n m : ℕ} → n ≡ m → Vec A n → Vec A m vec-length refl v = v -getList-to-getVec : ({A : Set} → List A → List A) → ∃ λ (getlen : ℕ → ℕ) → {B : Set} {n : ℕ} → Vec B n → Vec B (getlen n) +getList-to-getVec : get-type → ∃ λ (getlen : ℕ → ℕ) → (getV-type getlen) getList-to-getVec get = getlen , get' where getlen : ℕ → ℕ getlen = getList-to-getlen get @@ -55,7 +61,7 @@ getList-to-getVec get = getlen , get' get' : {C : Set} {m : ℕ} → Vec C m → Vec C (getlen m) get' {_} {m} v = vec-length (length-prop m v) (fromList (get (toList v))) -get-trafo-1 : (get : {A : Set} → List A → List A) → {B : Set} → getVec-to-getList (proj₂ (getList-to-getVec get)) {B} ≗ get {B} +get-trafo-1 : (get : get-type) → {B : Set} → getVec-to-getList (proj₂ (getList-to-getVec get)) {B} ≗ get {B} get-trafo-1 get l = begin getVec-to-getList (proj₂ (getList-to-getVec get)) l ≡⟨ {!!} ⟩ -- cgit v1.2.3