coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
Vadim Zaliva
--
CMU ECE PhD candidate
Mobile: +1(510)220-1060
Skype: vzaliva
- Re: [Coq-Club] Proper morphisms for family of functions, Gregory Malecha, 01/01/2016
- Re: [Coq-Club] Proper morphisms for family of functions, Vadim Zaliva, 01/01/2016
- <Possible follow-up(s)>
- Re: [Coq-Club] Proper morphisms for family of functions, Vadim Zaliva, 01/06/2016
- Re: [Coq-Club] Proper morphisms for family of functions, Abhishek Anand, 01/06/2016
- Re: [Coq-Club] Proper morphisms for family of functions, Vadim Zaliva, 01/06/2016
- Re: [Coq-Club] Proper morphisms for family of functions, Abhishek Anand, 01/06/2016
- Re: [Coq-Club] Proper morphisms for family of functions, Vadim Zaliva, 01/06/2016
- Re: [Coq-Club] Proper morphisms for family of functions, Abhishek Anand, 01/08/2016
- Re: [Coq-Club] Proper morphisms for family of functions, Vadim Zaliva, 01/06/2016
- Re: [Coq-Club] Proper morphisms for family of functions, Abhishek Anand, 01/06/2016
- Re: [Coq-Club] Proper morphisms for family of functions, Vadim Zaliva, 01/06/2016
- Re: [Coq-Club] Proper morphisms for family of functions, Abhishek Anand, 01/06/2016
Archive powered by MHonArc 2.6.18.