Agda's `rewrite` fails with an error mentioning variable "w"

Question

I have these definitions (irrelavant ones are removed)

open import Agda.Builtin.Nat renaming (Nat to ℕ)

infix 3 _>0
data _>0 : ℕ → Set where
  intro : ∀ n → suc n >0

infix 4 _*>0_
_*>0_ : ∀ {a b} → a >0 → b >0 → a * b >0
intro n *>0 intro m = intro (m + n * suc m)

infix 5 _÷_⟨_⟩
data ℚ : Set where
  _÷_⟨_⟩ : (a b : ℕ) → b >0 → ℚ

And I wanted to prove this to be true:

open import Agda.Builtin.Equality

div-mul-comm : ∀ a c d → (x : c >0) → (y : d >0) →
               a ÷ c * d ⟨ x *>0 y ⟩ ≡ a ÷ d * c ⟨ y *>0 x ⟩
div-mul-comm a c d x y = ?

But whatever I tried I can't prove this, also, the error message is strange.
This is what I've tried:

postulate nat-multiply-comm : ∀ a b → a * b ≡ b * a

div-mul-comm a c d x y
  rewrite nat-multiply-comm c d = {!!}

Agda says:

c * d != w of type ℕ
when checking that the type
(c d w : ℕ) →
w ≡ d * c →
(a : ℕ) (x : c >0) (y : d >0) →
a ÷ w ⟨ x *>0 y ⟩ ≡ a ÷ d * c ⟨ y *>0 x ⟩
of the generated with function is well-formed

Please provide a Minimal, Complete and Verifiable Example: I had to chase missing import statements and fiddle with fixity levels to get the file to parse. — gallais
I think it's already a minimal one since I just used the standard library... Maybe I should use Agda.Builtin only. Wait — ice1000
It's not complete though. I'm still missing nat-multiply-comm. Using +-comm from the standard library does not yield the error you're reporting. — gallais
I used a postulate. I think there shouldn't be more mistakes. — ice1000

gallais gallais · Accepted Answer · 2017-11-21T12:32:35

The problem here is that when you rewrite c * d to d * c, you also need to patch up the proof x *>0 y that c * d >0 into a proof that d * c >0.

Personally I would introduce two intermediate lemmas:

>0-irrelevant : ∀ a → (p q : a >0) → p ≡ q

which allows you to swap proofs that a >0 around depending on what you need. And

div-subst : ∀ a b c → b ≡ c → (p : b >0) (q : c >0) →
            a ÷ b ⟨ p ⟩ ≡ a ÷ c ⟨ q ⟩

which allows you to replace the second component of a ℚ with an equal value and replace the now obsolete proof p : b >0 by another one q : c >0. >0-irrelevant will be useful to prove this second lemma.

Agda's `rewrite` fails with an error mentioning variable "w"

1 Answers