CODEWITHSUNDEEP
agda
ice1000
ice1000

Reputation: 6569

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

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

Upvotes: 4

Views: 233

Answers (1)

gallais
gallais

Reputation: 12103

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.

Upvotes: 2

Related Questions