The following lemma should be trivial: Combining the plus sign and a natural is the same that using the plus constructor on this natural.
module sign where
open import Data.Nat
open import Data.Integer using (_◃_; +_)
open import Data.Sign renaming (+ to s+)
open import Relation.Binary.PropositionalEquality
lemma : ∀ y → s+ ◃ y ≡ + y
lemma y = refl
But lemma fails to typecheck with:
s+ ◃ y != + y of type Data.Integer.ℤ
when checking that the expression refl has type s+ ◃ y ≡ + y
I'm using lib-0.7 and according to this link, ◃ is defined as:
_◃_ : Sign → ℕ → ℤ
_ ◃ ℕ.zero = + ℕ.zero
Sign.+ ◃ n = + n
Sign.- ◃ ℕ.suc n = -[1+ n ]
So I expected that s+ ◃ y, following the second pattern rule, evaluate to + y and typechecking to succeed.
What is amiss?
The problem is that the first equation can also be used for s+ ◃ y. Only after you know that y is not zero, the second equation applies.
The solution is simple:
lemma : ∀ y → s+ ◃ y ≡ + y
lemma zero = refl
lemma (suc _) = refl
Collected from the Internet
Please contact [email protected] to delete if infringement.
Comments