The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

I minimised my problem to this:

Require Import Le List Setoid Morphisms.

Notation "A .1" := (projT1 A) (at level 0).
Notation "A .2" := (projT2 A) (at level 0).

Definition le_dec: forall m n, {m<=n} + {n<m}.
  refine (
    fix f m n: {m<=n} + {n<m} :=
    match m, n with
    | O, _ => left _ _
    | _, O => right _ _
    | S mm, S nn => match f mm nn with
                    | left _ => left _ _
                    | right _ => right _ _ end end);
 [ apply le_0_n |
   apply le_n_S; apply le_0_n |
   apply le_n_S; assumption |
   apply le_n_S; assumption ].
Defined.

Definition eq_dec: forall (m n:nat), {m=n} + {m<>n}.
  refine (
    fix f (m n:nat): {m=n} + {m<>n} :=
    match m, n with
    | O, O => left _ _
    | S mm, S nn => match f mm nn with
                    | left _ => left _ _
                    | right _ => right _ _ end
    | _, _ => right _ _ end);
 [ reflexivity |
   apply O_S |
   apply not_eq_sym, O_S |
   f_equal; assumption |
   apply not_eq_S; assumption ].
Defined.


Definition fin n := { i: nat | i <= n }.

Definition vect A n := fin n -> A.
Definition vect_eq {A n} (v1 v2: vect A n) := forall i, v1 i = v2 i.
Definition vect_swap {A n} (i j: fin n) (v: vect A n): vect A n :=
 fun m => if eq_dec i.1 m.1 then v j else if eq_dec j.1 m.1 then v i else v m.

Instance vect_eq_Equiv A n: Equivalence (vect_eq (A:=A) (n:=n)).
 split; unfold Reflexive, Symmetric, Transitive, vect_eq; congruence.
Qed.
Instance vect_swap_Proper A n i j: Proper (vect_eq ==> vect_eq) (vect_swap (A:=A) (n:=n) i j).
 unfold Proper, respectful, vect_eq, vect_swap; intros; repeat destruct eq_dec; auto.
Qed.


Definition transp n := prod (fin n) (fin n).
Definition perm n := list (transp n).

Definition vect_transp {A n} (v: vect A n) (t: transp n) := vect_swap (fst t) (snd t) v.
Definition vect_perm {A n} (p: perm n) (v: vect A n) := fold_left vect_transp p v.

Definition transp_eq {n} (t1 t2: transp n) := forall A (v: vect A n), vect_eq (vect_transp v t1) (vect_transp v t2).
Definition perm_eq {n} (p1 p2: perm n) := forall A (v: vect A n), vect_eq (vect_perm p1 v) (vect_perm p2 v).


Instance transp_eq_Equiv n: Equivalence (transp_eq (n:=n)).
 split; unfold Reflexive, Symmetric, Transitive, transp_eq; intros;
 [ reflexivity | symmetry | rewrite H ]; auto.
Qed.
Instance vect_transp_Proper A n: Proper (vect_eq ==> transp_eq ==> vect_eq) (vect_transp (A:=A) (n:=n)).
 unfold Proper, respectful, transp_eq, vect_transp; intros; rewrite H; auto.
Qed.

Instance perm_eq_Equiv n: Equivalence (perm_eq (n:=n)).
 split; unfold Reflexive, Symmetric, Transitive, perm_eq; intros;
 [ reflexivity | symmetry | rewrite H ]; auto.
Qed.
Instance vect_perm_Proper A n: Proper (perm_eq ==> vect_eq ==> vect_eq) (vect_perm (A:=A) (n:=n)).
 unfold Proper, respectful; intros.
 Admitted.

On Sat, Jul 5, 2014 at 5:11 PM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

Okay, it's here now.

Apologies, it's obvious now that I'm too ill for anything that needs thinking.

On Sat, Jul 5, 2014 at 4:55 PM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

Okay, it's here. I forgot to change mail again, hope the friend will not complain.

On Sat, Jul 5, 2014 at 4:35 PM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

Sorry, will push it soon.

On Sat, Jul 5, 2014 at 4:12 PM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

Here it is:
https://github.com/zaarcis/linear_algebra_in_Coq/blob/master/permutations.v

I could not prove "Instance vect_perm_Proper" which I have put Admitted now.

I will be grateful for any hints.

Thanks,

Ilmars