coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Proper morphisms for family of functions

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Proper morphisms for family of functions
Date: Tue, 29 Dec 2015 15:36:31 -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-pa0-f48.google.com
Ironport-phdr: 9a23:YT9SAB3e+ym25a7csmDT+DRfVm0co7zxezQtwd8ZsegUL/ad9pjvdHbS+e9qxAeQG96LtbQc06L/iOPJZy8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL2PbrnD61zMOABK3bVMzfbSrXNaKx+2MlMmMuLTrKz1SgzS8Zb4gZD6Xli728vcsvI15N6wqwQHIqHYbM85fxGdvOE7B102kvpT4r9Zf9HFbvOtk/MpdW437eb45RPpWFmcIKWcwsfPiuRjGBTmG4noCWy1CjAhBBwnb5TnxW4q3vyfn4LkukBKGNNH7GOhnEQ+p6L1mHUfl

I have a family of functions defined like this:

f: forall i, i<n -> A -> A

where {A:Type} and {n:nat}. Now I need to specify that for all ‘i’
A->A are proper wrt. my custom equality (equal). In other words
for all ‘i’ following holds:

`{pF: !Proper ((equal) ==> (equal)) f}

What is the best way to specify this, so I can make use of it in
setoid rewriting?

Thanks!

Sincerely,
Vadim Zaliva

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

[Coq-Club] Proper morphisms for family of functions, Vadim Zaliva, 12/30/2015
- Re: [Coq-Club] Proper morphisms for family of functions, Abhishek Anand, 12/30/2015
  - Re: [Coq-Club] Proper morphisms for family of functions, Vadim Zaliva, 12/31/2015
    - Re: [Coq-Club] Proper morphisms for family of functions, Gregory Malecha, 12/31/2015
      - Re: [Coq-Club] Proper morphisms for family of functions, Vadim Zaliva, 12/31/2015