drop the injection requirement for gl₁
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Tue, 14 Oct 2014 07:52:00 +0000 (09:52 +0200)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Tue, 14 Oct 2014 07:52:00 +0000 (09:52 +0200)
Turns out, we never use this requirement. The only place where it may
come in relevant is the free theorems. But here non-injectivity turns
out to be reasoning about multiple get functions that are selected by
the additional index each individually satisfying the free theorem and
thus commonly satisfying it as well.

Examples.agda
FreeTheorems.agda
GetTypes.agda

index bda3ae1..ca65835 100644 (file)
@@ -1,14 +1,11 @@
 module Examples where
 
-open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; ⌈_/2⌉ ; pred)
+open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; ⌈_/2⌉)
 open import Data.Nat.Properties using (cancel-+-left)
 import Algebra.Structures
-open Algebra.Structures.IsCommutativeSemiring Data.Nat.Properties.isCommutativeSemiring using (+-isCommutativeMonoid)
-open Algebra.Structures.IsCommutativeMonoid +-isCommutativeMonoid using () renaming (comm to +-comm)
 open import Data.List using (List ; length) renaming ([] to []L ; _∷_ to _∷L_)
 open import Data.Vec using (Vec ; [] ; _∷_ ; reverse ; _++_ ; tail ; take ; drop)
 open import Function using (id)
-open import Function.Injection using () renaming (Injection to _↪_ ; id to id↪)
 open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; cong) renaming (setoid to EqSetoid)
 
 open import Generic using (≡-to-Π)
@@ -20,10 +17,10 @@ open GetTypes.PartialVecVec using (Get)
 open FreeTheorems.PartialVecVec using (assume-get)
 
 reverse' : Get
-reverse' = assume-get id↪ (≡-to-Π id) reverse
+reverse' = assume-get (≡-to-Π id) (≡-to-Π id) reverse
 
 double' : Get
-double' = assume-get id↪ (≡-to-Π g) f
+double' = assume-get (≡-to-Π id) (≡-to-Π g) f
   where g : ℕ → ℕ
         g zero = zero
         g (suc n) = suc (suc (g n))
@@ -32,25 +29,19 @@ double' = assume-get id↪ (≡-to-Π g) f
         f (x ∷ v) = x ∷ x ∷ f v
 
 double'' : Get
-double'' = assume-get id↪ (≡-to-Π _) (λ v → v ++ v)
-
-suc-injection : EqSetoid ℕ ↪ EqSetoid ℕ
-suc-injection = record { to = ≡-to-Π suc; injective = cong pred }
+double'' = assume-get (≡-to-Π id) (≡-to-Π _) (λ v → v ++ v)
 
 tail' : Get
-tail' = assume-get suc-injection (≡-to-Π id) tail
-
-n+-injection : ℕ → EqSetoid ℕ ↪ EqSetoid ℕ
-n+-injection n = record { to = ≡-to-Π (_+_ n); injective = cancel-+-left n }
+tail' = assume-get (≡-to-Π suc) (≡-to-Π id) tail
 
 take' : ℕ → Get
-take' n = assume-get (n+-injection n) (≡-to-Π _) (take n)
+take' n = assume-get (≡-to-Π (_+_ n)) (≡-to-Π _) (take n)
 
 drop' : ℕ → Get
-drop' n = assume-get (n+-injection n) (≡-to-Π _) (drop n)
+drop' n = assume-get (≡-to-Π (_+_ n)) (≡-to-Π _) (drop n)
 
 sieve' : Get
-sieve' = assume-get id↪ (≡-to-Π _) f
+sieve' = assume-get (≡-to-Π id) (≡-to-Π _) f
   where f : {A : Set} {n : ℕ} → Vec A n → Vec A ⌈ n /2⌉
         f []           = []
         f (x ∷ [])     = x ∷ []
@@ -67,7 +58,7 @@ intersperse s (x ∷ [])    = x ∷ []
 intersperse s (x ∷ y ∷ v) = x ∷ s ∷ intersperse s (y ∷ v)
 
 intersperse' : Get
-intersperse' = assume-get suc-injection (≡-to-Π intersperse-len) f
+intersperse' = assume-get (≡-to-Π suc) (≡-to-Π intersperse-len) f
   where f : {A : Set} {n : ℕ} → Vec A (suc n) → Vec A (intersperse-len n)
         f (s ∷ v)        = intersperse s v
 
index d4eb174..08bbe88 100644 (file)
@@ -6,10 +6,8 @@ open import Data.List using (List ; map)
 open import Data.Vec using (Vec) renaming (map to mapV)
 open import Function using (_∘_)
 open import Function.Equality using (_⟶_ ; _⟨$⟩_)
-open import Function.Injection using (module Injection) renaming (Injection to _↪_)
 open import Relation.Binary.PropositionalEquality using (_≗_ ; cong) renaming (setoid to EqSetoid)
 open import Relation.Binary using (Setoid)
-open Injection using (to)
 
 import GetTypes
 
@@ -38,13 +36,13 @@ module VecVec where
   assume-get {getlen} get = record { getlen = getlen; get = get; free-theorem = free-theorem get }
 
 module PartialVecVec where
-  get-type : {I : Setoid ℓ₀ ℓ₀} → (I ↪ (EqSetoid ℕ)) → (I ⟶ (EqSetoid ℕ)) → Set₁
-  get-type {I} gl₁ gl₂ = {A : Set} {i : Setoid.Carrier I} → Vec A (to gl₁ ⟨$⟩ i) → Vec A (gl₂ ⟨$⟩ i)
+  get-type : {I : Setoid ℓ₀ ℓ₀} → (I ⟶ EqSetoid ℕ) → (I ⟶ EqSetoid ℕ) → Set₁
+  get-type {I} gl₁ gl₂ = {A : Set} {i : Setoid.Carrier I} → Vec A (gl₁ ⟨$⟩ i) → Vec A (gl₂ ⟨$⟩ i)
 
   open GetTypes.PartialVecVec public
 
   postulate
-    free-theorem : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ (EqSetoid ℕ)) → (gl₂ : I ⟶ (EqSetoid ℕ)) (get : get-type gl₁ gl₂)  → {α β : Set} → (f : α → β) → {i : Setoid.Carrier I} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get
+    free-theorem : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ⟶ EqSetoid ℕ) → (gl₂ : I ⟶ EqSetoid ℕ) (get : get-type gl₁ gl₂)  → {α β : Set} → (f : α → β) → {i : Setoid.Carrier I} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get
 
-  assume-get : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ (EqSetoid ℕ)) → (gl₂ : I ⟶ (EqSetoid ℕ)) (get : get-type gl₁ gl₂) → Get
+  assume-get : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ⟶ EqSetoid ℕ) → (gl₂ : I ⟶ EqSetoid ℕ) (get : get-type gl₁ gl₂) → Get
   assume-get {I} gl₁ gl₂ get = record { I = I; gl₁ = gl₁; gl₂ = gl₂; get = get; free-theorem = free-theorem gl₁ gl₂ get }
index f23d154..033257a 100644 (file)
@@ -4,12 +4,10 @@ open import Level using () renaming (zero to ℓ₀)
 open import Data.Nat using (ℕ)
 open import Data.List using (List ; map)
 open import Data.Vec using (Vec) renaming (map to mapV)
-open import Function using (_∘_)
+open import Function using (_∘_ ; id)
 open import Function.Equality using (_⟶_ ; _⟨$⟩_)
-open import Function.Injection using (module Injection) renaming (Injection to _↪_ ; id to id↪)
 open import Relation.Binary.PropositionalEquality using (_≗_) renaming (setoid to EqSetoid)
 open import Relation.Binary using (Setoid)
-open Injection using (to)
 
 open import Generic using (≡-to-Π)
 open import Structures using (Shaped ; module Shaped)
@@ -32,11 +30,11 @@ module PartialVecVec where
   record Get : Set₁ where
     field
       I : Setoid ℓ₀ ℓ₀
-      gl₁ : I  EqSetoid ℕ
+      gl₁ : I  EqSetoid ℕ
       gl₂ : I ⟶ EqSetoid ℕ
 
     |I|   = Setoid.Carrier I
-    |gl₁| = _⟨$⟩_ (to gl₁)
+    |gl₁| = _⟨$⟩_ gl₁
     |gl₂| = _⟨$⟩_ gl₂
 
     field
@@ -46,7 +44,7 @@ module PartialVecVec where
 VecVec-to-PartialVecVec : VecVec.Get → PartialVecVec.Get
 VecVec-to-PartialVecVec G = record
   { I = EqSetoid ℕ
-  ; gl₁ = id↪
+  ; gl₁ = ≡-to-Π id
   ; gl₂ = ≡-to-Π getlen
   ; get = get
   ; free-theorem = free-theorem
@@ -64,11 +62,11 @@ module PartialShapeShape where
       ViewShapeT : Shaped ViewShape ViewContainer
 
       I : Setoid ℓ₀ ℓ₀
-      gl₁ : I  EqSetoid SourceShape
+      gl₁ : I  EqSetoid SourceShape
       gl₂ : I ⟶ EqSetoid ViewShape
 
     |I|   = Setoid.Carrier I
-    |gl₁| = _⟨$⟩_ (to gl₁)
+    |gl₁| = _⟨$⟩_ gl₁
     |gl₂| = _⟨$⟩_ gl₂
 
     open Shaped SourceShapeT using () renaming (fmap to fmapS)