在coq中实现指定的换元组。

Question

我试图在coq中实现pecify permutation groups（对称群）。这在一段时间内很顺利，直到我试图证明身份实际上就是身份。我的证明卡在了证明命题 "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.

Answer 1

我相信，如果不假设额外的公理，就无法证明你的声明。

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) 等于 g 对于任何 g.

如果你想将这种表示法用于组，你可能最终还需要功能扩展性公理。

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

这个公理可以在 Coq.Logic.FunctionalExtensionality 模块。

如果你想把反元素定义为一个函数，你可能还需要某种形式的选择公理：它是提取反元素所必需的。g 从存在证明。

如果你不想假设额外的公理，你必须对你的换元组进行限制。 例如，你可以将你的注意力限制在有限支持的元素上 -- 也就是固定所有元素的换元组。X除了一个有限的集合。 有多个库允许你以这种方式处理排列组合，包括我自己的 延伸结构.