The Coq mailing list

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

I learned about "pose proof" and, actually, "(e)transitivity" too. And importance of not introducing too much.

Big thank you, Daniel!

On Sat, Jul 5, 2014 at 6:25 PM, Daniel Schepler <dschepler AT gmail.com> wrote:

Lemma const_vect_perm_Proper A n p: Proper (vect_eq ==> vect_eq)
  (vect_perm (A:=A) (n:=n) p).
Proof.
 induction p; intros v1 v2 ?; simpl; trivial;
 pose proof vect_swap_Proper; unfold Proper, respectful in *;
 unfold vect_transp; 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.

 pose proof const_vect_perm_Proper; unfold Proper, respectful in *;
 etransitivity; eauto.
Qed.
--
Daniel Schepler

On Sat, Jul 5, 2014 at 7:32 AM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:
> 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
>>>>
>>>>
>>>
>>
>