时间戳

首页 > 解决方案 > 在 coq 中实现/指定排列组

coq - 在 coq 中实现/指定排列组

问题描述

我正在尝试在 coq 中实现/指定排列组（对称组）。这进行了一段时间，直到我试图证明身份实际上就是身份。我的证明停留在证明命题“可逆”与命题“x可逆”完全相同id * x。

这两个命题实际上是一样的吗？我是否试图证明一些不正确的事情？有没有更好的方法来指定排列组（作为一种类型）？

(* The permutation group on X contains all functions between X and X that are bijective/invertible *)
Inductive G {X : Type} : Type :=
| function (f: X -> X) (H: exists g: X -> X, forall x : X, f (g x) = x /\ g (f x) = x).

(* Composing two functions preserves invertibility *)
Lemma invertible_composition {X : Type} (f g: X -> X) :
    (exists f' : X -> X, forall x : X, f (f' x) = x /\ f' (f x) = x) ->
    (exists g' : X -> X, forall x : X, g (g' x) = x /\ g' (g x) = x) ->
     exists h  : X -> X, forall x : X, (fun x => f (g x)) (h x) = x /\ h ((fun x => f (g x)) x) = x.
Admitted.

(* The group operation is composition *)
Definition op {X : Type} (a b : G) : G :=
    match a, b with
    | function f H, function g H' => function (fun x => f (g x)) (@invertible_composition X f g H H')
    end.

Definition id' {X : Type} (x : X) : X := x.

(* The identity function is invertible *)
Lemma id_invertible {X : Type} : exists g : X -> X, forall x : X, id' (g x) = x /\ g (id' x) = x.
Admitted.

Definition id {X : Type} : (@G X) := function id' id_invertible.

(* The part on which I get stuck: proving that composition with the identity does not change elements. *)
Lemma identity {X: Type} : forall x : G, op id x = x /\ @op X x id = x.
Proof.
    intros.
    split.
    - destruct x.
      simpl.
      apply f_equal.
      Abort.

标签： coq

解决方案

我相信如果不假设额外的公理，就无法证明您的陈述：

proof_irrelevance:
  forall (P : Prop) (p q : P), p = q.

当底层G函数为：

Require Import Coq.Logic.ProofIrrelevance.

Inductive G X  : Type :=
| function (f: X -> X) (H: exists g: X -> X, forall x : X, f (g x) = x /\ g (f x) = x).

Arguments function {X} _ _.

Definition fun_of_G {X} (f : G X) : X -> X :=
  match f with function f _ => f end.

Lemma fun_of_G_inj {X} (f g : G X) : fun_of_G f = fun_of_G g -> f = g.
Proof.
destruct f as [f fP], g as [g gP].
simpl.
intros e.
destruct e.
f_equal.
apply proof_irrelevance.
Qed.

X（附带说明一下，显式声明参数通常G比隐式声明更好。Coq 很少能X自行判断应该是什么。）

有了fun_of_G_inj，应该可以identity简单地通过将其应用于每个等式来显示，因为对于任何fun a => (fun x => x) (g a)都等于。gg

如果您想将此表示用于组，您最终可能还需要功能可扩展性公理：

functional_extensionality:
  forall X Y (f g : X -> Y), (forall x, f x = g x) -> f = g.

该公理在Coq.Logic.FunctionalExtensionality模块中可用。

如果要将逆元素定义为函数，则可能还需要某种形式的选择公理：g从存在证明中提取逆元素是必要的。

如果您不想假设额外的公理，则必须对排列组施加限制。例如，您可以将注意力限制在具有有限支持的元素上——即固定 的所有元素的排列X，除了有限集。有多个库允许您以这种方式处理排列，包括我自己的扩展结构。

推荐阅读