Idris等式证明中如何通过解构(A s) = (A s')推导s = s'

可直接运行的完整实现代码：

data T = A String | B String

p : ((A s) = (A s')) -> (s = s')
p Refl = Refl

底层逻辑 #

Idris 的内置等式类型=仅存在一个构造子Refl，其核心定义为：

data (=) : a -> b -> Type where
  Refl : {x : a} -> x = x

该构造子的成立条件为：等式左右两侧的项必须完全严格相等，才能生成对应的证明实例。
当对输入的证明项执行Refl模式匹配时，Idris 类型检查器会自动完成以下推导流程：

• 输入项的类型为A s = A s'，匹配到构造子Refl即说明A s与A s'是完全相同的项
• 按照数据构造子的单射性规则：由同个构造子生成的两个值相等，当且仅当它们携带的所有参数完全相等。类型检查器会自动基于该规则推导得到s与s'是相同的项
• 此时证明目标s = s'完全满足Refl的构造要求，直接返回Refl即可完成证明

实现注意事项 #

• 无需手动对A构造子做额外解构，匹配Refl的过程已经完成了所有参数的统一校验
• 所有推导校验流程都在编译期完成，不存在运行时开销

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