3

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
dbanas
  • 1,707
  • 14
  • 24
  • 1
    If `m * n = _m_1 * _n_1`, why couldn't `_m_1` be 1, and `_n_1` be the whole product? Agda won't boldly guess for you, she only picks the inevitable. – Trebor Feb 04 '22 at 19:59

1 Answers1

3

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}.

Conal
  • 18,517
  • 2
  • 37
  • 40
  • That worked. Thank you, @Conal! – dbanas Feb 04 '22 at 19:03
  • Conal, does your solution work, because the section: (m *), is injective? – dbanas Feb 10 '22 at 00:11
  • I don't know why providing `m` suffices. Note that `m *_` is only injective when `m ≢ 0`. – Conal Feb 10 '22 at 02:14
  • 1
    Just to be concrete: `_m_18 = m`, `_a_19 = 0`, `_b_20 = a + b` is another solution to the second constraint. You can see how it quickly becomes unclear whether the obvious solution is unique. – mudri Feb 12 '22 at 22:15
  • 2
    As for why specifying `m = m` is enough: indeed `m *_` is judgementally injective. I believe the reasoning is that `_*_` is defined by cases on the first argument, so while that argument is stuck, the whole application of `_*_` is stuck. Being stuck means that `m * n = m * n′` judgementally exactly when `n = n′` (because there is no other computation we could do to make `m * n` and `m * n′` into the same expression). Then, because `m * a` is stuck, `(m * a) + (m * b)` is stuck, so you can unify the `_+_`es against each other and eventually fill `a` and `b`. – mudri Feb 12 '22 at 22:31