Agda中inspect使用困惑：匹配id true为何出现false≡false证据？

open import Data.Bool
open import Data.Unit
open import Function using (id)
open import Relation.Binary.PropositionalEquality

what? : Bool → ⊤
what? true with id true | inspect id true
... | true  | [  true≡true  ] = {!!}
... | false | [ false≡false ] = {!!} -- why?
what? false = tt

疑问 #

当我们对类型为Reveal id · true is true的inspect id true进行模式匹配时，Agda为何会在第二个洞位中提供false ≡ false的证据？

原因解析 #

Agda的with语句模式匹配是基于类型结构枚举所有可能的模式组合，不会提前计算表达式的具体值来过滤逻辑上不可能的分支：

• inspect f x会生成包含f x结果和对应等式证据的类型Reveal f · x is y，其中y在模式匹配阶段被视为可匹配任意值的变量，因此Agda会枚举y取true和false的两种情况。
• 即便id true从定义上必然等于true，模式匹配时依然会生成id true为false的分支。此时Agda会把id true这个表达式绑定为false，对应的等式证据自然推导为false ≡ false——这是模式匹配绑定带来的结果，而非逻辑上成立的等式。
• 这个分支实际上不可能被执行到，因为id true的结果只能是true，你可以用⊥-elim这类工具消除这个矛盾分支。

内容的提问来源于stack exchange，提问作者PaulProgrammerNoob