Coq中如何将假设内的隐式强制转换显式展示

问题1解答 #

是的，你的判断完全正确。Coq的强制转换是内核层面自动插入的隐式函数，当你声明Coercion T1_of: T1 >-> T2.后，所有预期T2类型、但实际传入T1类型值的位置，Coq都会自动补全T1_of调用。你看到的f P1只是默认打印规则隐藏了强制转换函数的简化展示，H的实际类型内核表示就是f (T1_of P1)。

问题2解答 #

有两种常用方案可以实现你的需求：

• 方案1：调整全局打印选项，让Coq显式输出所有强制转换
  执行命令：Set Printing Coercions.
  开启后所有隐式强制转换都会在打印时展示，你会直接看到H的类型显示为f (T1_of P1)。如果需要恢复默认打印样式，执行Unset Printing Coercions.即可。
• 方案2：在证明中显式改写假设的项结构
  直接对目标假设H使用change策略：change (f (T1_of P1)) in H.
  这个策略会直接把H的类型替换为显式带T1_of的形式，操作完全合法，不会改变项的内核一致性。

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