agda - 为什么等式推理链无法满足平凡可解的约束？

Question

以下 Agda 代码：

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)
  ∎

产量：

_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

在我输入之后C-c C-l。
（注意： “22,6-13”表示“distrib”这个词的第二次出现。）

我不明白为什么不能满足约束。它们似乎很容易解决：

_m_18 = m
_a_19 = a
_b_20 = b

Answer 1

虽然这些解决方案是正确的，但它们并非不可避免，因为乘法和加法不是单射的。在这种情况下，您可以只填写m第 22 行，即distrib {m = m}.