Ssreflect中的perm_invK引理证明了什么？

Question

以下代码来自Ssreflect库中的perm.v。我想知道结果是什么。

Lemma perm_invK s : cancel (fun x => iinv (perm_onto s x)) s.
Proof. by move=> x /=; rewrite f_iinv. Qed.

Answer 1

Ssreflect中的定义可能涉及很多概念，有时很难理解实际发生了什么。让我们对此进行部分分析。

iinv (在fintype.v中定义)具有类型

iinv : forall (T : finType) (T' : eqType) (f : T -> T') 
              (A : pred T) (y : T'),
         y \in [seq f x | x in A] -> T

这样做的目的是反转对子域A \subset T的限制在T'上是满射的任何函数f : T -> T'。换句话说，如果您给我一个y，它在将f应用于A的所有元素的结果列表中，那么我可以为您找到一个这样的x \in A，即f x = y。请注意，这在很大程度上依赖于这样一个事实，即T是一个有限类型，并且T'具有可判定的相等。在上面使用的引理f_iinv中说明了iinv的正确性。

perm_onto具有类型codom s =i predT，其中s是定义在有限类型T上的某种置换。顾名思义，这就是说s是投射的(很明显，因为它是内射的，通过perm.v中的排列定义，以及域和协域是相同的事实，这是显而易见的)。因此，fun x => iinv (perm_onto s x)是将元素x映射到元素y的函数，使得s y = x。换句话说，它与s相反。perm_invK只是简单地说明这个函数确实是逆函数(更准确地说，它是s的左逆)。

然而，实际有用的定义是perm_inv，它显示在下面。它所做的是将fun x => iinv (perm_onto s x)与其正确性证明perm_invK打包在一起，以定义类型为{perm T}的perm_inv s的元素，使得perm_inv s * s = s * perm_inv s = 1。因此，你可以把它看作是类型{perm T}在逆之下是封闭的，这允许你在有限群和么半群等方面使用大量的ssr机制。