如何理解(elimTF andP top)？基于Mathematical Components的技术咨询

问题1：andP为何能作为elimTF的第一个参数？ #

elimTF的第一个参数类型是reflect P b，而andP的类型是forall b1 b2 : bool, reflect (b1 /\ b2) (b1 && b2)——它是一个多态函数，并非直接的reflect类型，但Coq的类型推断会自动实例化andP的隐式参数，让它匹配reflect P b的要求：

在move=> lekn /andP的上下文里，栈顶的项是(n <= m) && (m <= k)，这是一个bool值，对应andP中的b1 && b2（其中b1 = (n <= m)，b2 = (m <= k)）。此时Coq会自动将andP实例化为andP (n <= m) (m <= k)，它的类型就是reflect ((n <= m) /\ (m <= k)) ((n <= m) && (m <= k))，完全符合elimTF第一个参数reflect P b的类型（这里P = (n <= m) /\ (m <= k)，b = (n <= m) && (m <= k)）。

简言之，andP是生成reflect实例的函数，在上下文约束下会被自动调用，生成符合要求的reflect项，而非直接传递多态类型本身。

问题2：elimTF的第三个参数c在哪里？ #

elimTF的第三个参数c就是栈顶的那个bool项——也就是(n <= m) && (m <= k)，对应视图模式逻辑里的top。

看elimTF的完整类型：

Lemma elimTF (P : Prop) (b c : bool) :
  reflect P b -> b = c -> if c then P else ~ P.

在/andP的转换逻辑(elimTF andP top)中：

1. andP实例化后，b就是(n <= m) && (m <= k)（来自andP的返回类型）；
2. top就是栈顶的(n <= m) && (m <= k)，也就是c的值；
3. 此时b = c就是(n <= m) && (m <= k) = (n <= m) && (m <= k)，这是自反等式，Coq会自动证明该前提，无需手动处理。

当c为true时（即栈顶&&结果为真），elimTF的结论就是P——也就是(n <= m) /\ (m <= k)，这正是视图模式想要转换的结果。

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