如何在Agda中用函数定义替换填补类型洞？

要将类型洞中的tm-sim tm替换为它的定义(G tm) · (G tm)，可以通过以下两种实用方式操作：

1. 直接手动展开定义 #

由于tm-sim的定义是透明的（Agda默认会识别这种直接的等式定义），你可以直接在类型洞中把tm-sim tm替换为(G tm) · (G tm)，得到新的目标后继续构造证明：

refl-clos-sim tm l1 l2 = {! (G tm) · (G tm) · Config2ƛ ⟨ l1 ! Fin.suc Fin.zero ! l2 ⟩ ⋙ Config2ƛ ⟨ l1 ! Fin.suc Fin.zero ! l2 ⟩ !}

之后你可以基于这个新的目标，结合·、⋙的运算性质或G tm相关的引理来完成证明。

2. 使用rewrite改写目标类型 #

如果你需要明确基于定义等式来改写整个目标类型，可以用rewrite关键字结合定义的自反等式：

refl-clos-sim tm l1 l2 rewrite refl {x = tm-sim tm} = {!!}

此时Agda会自动将目标中的tm-sim tm替换为(G tm) · (G tm)，你可以在新的类型洞中继续完成证明。

另外，你可以在Agda交互模式中按下C-c C-n（normalize命令）输入tm-sim tm，验证其展开结果确实是(G tm) · (G tm)，确保替换的正确性。

内容的提问来源于stack exchange，提问作者Thiago Mendonça Ferreira Ramos