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

Question

以下代码来自perm.vSsreflect Coq 库。我想知道这个结果是什么。

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

这样做是为了反转对子f : T -> T'域的限制A \subset T是满射的任何函数T'。换句话说，如果你给我一个在应用于所有元素的y结果列表中的那个，那么我可以找到你一个这样的那个。请注意，这主要依赖于一个有限类型且具有可判定相等性的事实。的正确性在上面使用的引理中说明。fAx \in Af x = yTT'iinvf_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_inv s类型{perm T}为perm_inv s * s = s * perm_inv s = 1. 因此，您可以将其视为说该类型{perm T}在逆条件下是封闭的，这允许您将大量 ssr 机制用于有限群和幺半群。