CODEWITHSUNDEEP
permutationcoq
Simon Defontaine
Simon Defontaine

Reputation: 125

Proof on permutations with Coq proof assistant

I am working on permutations on Coq, defined as follows:

Definition Tperm := list (nat* nat).

I have an act function of type Tperm -> nat -> nat that returns the image of the natural passed in parameter by the permutation. I also have an atoms function of type Tperm -> list(nat) that returns all the naturals that are modified by the permutation.

So now, I have to prove that lemma: Lemma act_atoms: forall pi a, ~act(pi)(a) = a -> In a (atoms(pi)).

I have started a proof by induction on pi, but am stuck after proving the first subgoal. Any help would be appreciated. Below are the definitions of act and atoms.

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.

Upvotes: 1

Views: 433

Answers (1)

ejgallego
ejgallego

Reputation: 6852

Here is a proof. Note that I dont't recommend fomalizing permutations that way.

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.

As you know, the first case is trivial. Secondly, we have to do case analysis on whether the atom is equal to the current element of the permutation i =? a. A very efficient way to do such case analysis is to use a "reflection" lemma.

  • It that is the case, the proof is trivial.
  • Otherwise, we conclude by using the induction hypothesis.

Upvotes: 1

Related Questions