From b1b80567288030782231418407e7244b37227450 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Tue, 14 Oct 2014 09:52:00 +0200
Subject: drop the injection requirement for gl₁
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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 | 27 +++++++++------------------
 1 file changed, 9 insertions(+), 18 deletions(-)

(limited to 'Examples.agda')

diff --git a/Examples.agda b/Examples.agda
index bda3ae1..ca65835 100644
--- a/Examples.agda
+++ b/Examples.agda
@@ -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
 
-- 
cgit v1.2.3