CODEWITHSUNDEEP
agdatype-constraintsequational-reasoning
dbanas
dbanas

Reputation: 1888

Why is chain of equational reasoning failing to meet trivially solvable constraints?

The following Agda code:

module test where

open import Data.Float

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)

postulate
  distrib : {m a b : Float} → m * (a + b) ≡ (m * a) + (m * b)

dbg : (m a b : Float) → m * (a + b) ≡ (m * a) + (m * b)
dbg m a b =
  begin
    m * (a + b)
  ≡⟨ distrib ⟩  -- (Line "22")
    (m * a) + (m * b)
  ∎

yields:

_m_18 : Float  [ at /Users/dbanas/Documents/Agda/agda_misc/test.agda:22,6-13 ]
_a_19 : Float  [ at /Users/dbanas/Documents/Agda/agda_misc/test.agda:22,6-13 ]
_b_20 : Float  [ at /Users/dbanas/Documents/Agda/agda_misc/test.agda:22,6-13 ]

———— Errors ————————————————————————————————————————————————
Failed to solve the following constraints:
  (_m_18 * _a_19) + (_m_18 * _b_20) = (m * a) + (m * b) : Float
  _m_18 * (_a_19 + _b_20) = m * (a + b) : Float

after I type C-c C-l.
(Note: "22,6-13" identifies the second occurrence of the word "distrib".)

I don't understand why the constraints can't be met. They seem trivially solvable:

_m_18 = m
_a_19 = a
_b_20 = b

Upvotes: 3

Views: 130

Answers (1)

Conal
Conal

Reputation: 18587

While those solutions are correct, they're not inevitable, because multiplication and addition are not injective. In this case, you can fill in just m in line 22, ie distrib {m = m}.

Upvotes: 3

Related Questions