使用Coq证明辅助工具证明排列

Question

我正在研究Coq上的排列，定义如下：

Definition Tperm := list (nat* nat).

我有一个Tperm -> nat -> nat类型的act函数，它返回通过排列传递的自然参数的图像。我还有一个Tperm -> list(nat)类型的atoms函数，它返回由排列修改的所有自然数。

所以现在，我必须证明这个引理：Lemma act_atoms: forall pi a, ~act(pi)(a) = a -> In a (atoms(pi)).

我已经在pi上通过归纳开始了证明，但在证明了第一个子目标后被卡住了。任何帮助都将不胜感激。下面是动作和原子的定义。

Fixpoint act (t : Tperm) (i : nat) : nat := match t with
|nil => i
|cons(k,l) p => if(beq_nat(act p i) k) then l
                  else if(beq_nat(act p i) l) then k
                  else act p i
end.

Fixpoint atoms (t : Tperm) : list(nat) :=
match t with
  |nil => nil
  |cons(k,l) nil => cons k (cons l nil)
  |cons(k,l) p => cons k (atoms p)
end.

Answer 1

这是一个证据。请注意，我不建议以这种方式形式化排列。

Require Import Coq.Arith.PeanoNat Coq.Lists.List.
Import ListNotations.

Definition tperm := list (nat * nat).

Fixpoint act (pi : tperm) (a : nat) :=
  match pi with
  | (i,s) :: r => if Nat.eqb i a then s else
                  if Nat.eqb s a then i else act r a
  | []         => a
  end.

Definition atoms (pi : tperm) := concat (map (fun p => [fst p; snd p]) pi).

Lemma act_atoms pi a : act pi a <> a -> In a (atoms pi).
Proof.
induction pi as [| [i s] pi ihpi]; simpl.
+ now auto.
+ now destruct (Nat.eqb_spec i a); destruct (Nat.eqb_spec s a); auto.
Qed.

如您所知，第一种情况微不足道。其次，我们必须对原子是否等于置换i =? a的当前元素进行案例分析。进行此类案例分析的一个非常有效的方法是使用“反射”引理。

事实就是这样，证据是我们通过使用归纳假设得出的结论。