Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Proper morphisms for family of functions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proper morphisms for family of functions


Chronological Thread 
  • From: Vadim Zaliva <vzaliva AT cmu.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Proper morphisms for family of functions
  • Date: Fri, 1 Jan 2016 10:49:38 -0800
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=vadim.zaliva AT west.cmu.edu; spf=None smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-ob0-f172.google.com
  • Ironport-phdr: 9a23:MQDAAR+/x/XwXf9uRHKM819IXTAuvvDOBiVQ1KB90e8cTK2v8tzYMVDF4r011RmSDduds6oMotGVmp6jcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47AblHf6ke/8SQVUk2mc1EleKKtQsb7tIee6aObw9XreQJGhT6wM/tZDS6dikHvjPQQmpZoMa0ryxHE8TNicuVSwn50dxrIx06vrpT4wJk2+CNJ/vkl6sRoUKPgfq1+Q6YLIi4hNjUL7cHqsFHxRA+O+HJUBnsEmx5JHQHt5xTnGJr9r32p5aJGxCCGMJiuHvgPUjO44vIzRQ==


On Dec 31, 2015, at 19:06 , Gregory Malecha <gmalecha AT gmail.com> wrote:

One thing to note about [O] is that it is trivially true (unless there is something that I am missing). In particular,

Theorem Proper_eq : forall f : nat -> nat, Proper (eq ==> eq) f.
Proof.  compute. destruct 1; reflexivity. Qed.

This basically says that all functions respect Libniz equality. Perhaps you have a weaker equivalence relation that makes this non-trivial?

Mathclasses re-defines (=) notation to point to `equiv` not `eq`. So my f_proper actually means:

  f_proper : Proper ((equiv) ==> (equiv)) (op).

And I want to rewrite wrt this equality.

From the very helpful discussion here it looks like Abishek’s approach is the best way to go and I will try to implement it. Thanks!

Sincerely,
Vadim Zaliva

--
CMU ECE PhD candidate
Mobile: +1(510)220-1060
Skype: vzaliva




Archive powered by MHonArc 2.6.18.

Top of Page