coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Reasoning about CIC in Coq + univalence

From: Yannick Forster <yannick AT yforster.de>
To: <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Reasoning about CIC in Coq + univalence
Date: Tue, 13 Oct 2020 23:39:21 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=Pass smtp.pra=yannick AT yforster.de; spf=Pass smtp.mailfrom=yannick AT yforster.de; spf=None smtp.helo=postmaster AT vela.uberspace.de
Ironport-phdr: 9a23:popZqx9gX8CPK/9uRHKM819IXTAuvvDOBiVQ1KB42+scTK2v8tzYMVDF4r011RmVBNqdtaoMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+5p/ebx9JiTahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRh/2hikJNDA28m/XhcJtgq1UvB2svAZwz5LbYYyPKPZzZL3RcNUHTmRBRMZRUClBD5u+YIQVCeoBO+dYoJX+p1ATrRW+AhOsBPjzyjBWnH/9wKo30uQ7HgHA2gwgHs4BsHfPodT1OqcSVvq1zLLUzTrddfNawyry55bRfx0nvPqDUq5+f9DLxkkzCwPKkE+QqYr9Mj6I1OkDvHSX4/diWO+xlWIqtR19rzqvy8oiloXEiYMYx03F+Ct53Is5ONO2RFBlbNOlE5ZdtyKXOYR5T84/R2xlvjsxxL4euZOjeCUHyI4rywPQZvGJaYSE/xDuWPiLLTtlgH9pZrSyjAuo/0e60O3zTMy03U5KriVbltnMsWgA1wLN5ciDUPRx5Fqh1i2R2ADJ8eFEOVo7mrbFJJI737E/iIIfsUXFHiDohEX7lKube0U+9uS15OnqbK/qqoKeOoNqkA3yL6AjltKnDeQ9KAcOXmyb+eqm1L3k+E30WLVLgecwkqnfsZDVOccbq7W5Ag9b1YYj8Q2/Dyu439QCh3UIMUxKdAqdj4f1I1HOPOz4DfCnjluwlzdr3unKMaHlApXQNXfOi6zhfLZ4605E0gU/19Ff55ROCrEAOv3/QEHxtMaLRiM+Zli/xP+iA9Fg3KsfX3iOC+mXKvWBn0WP47ceKu+KZYQW8Bj6MeM56uSm2W4wn1kcdqqBzJUQcmukE+4gL0jPMimkucsIDWpf5ll2d+ftklDXCWcONUb3ZLo143QAMKzjDYrHQdn80qKM2C79A5dbfHteA1uBV3vlJd3dCqU8LRmKK8okqQQqEL2oSosvzxar7VSo2rRgNPHI9zdeuZ+xjYEptd2Wrgk78HlPN+rYy3uEFjomj20PXSQq0bo5rUEvk1o=

Hi Talia,

MetaCoq embeds all of Coq in Coq. Given that your tool is really a tool concerned with Coq (right?), MetaCoq might be a good fit. One of the initial motivations of the project was exactly to enable the verification of plugins.

If you give more context about the kind of theorem you want to prove about your tool I can try to help more how feasible it is to express that in MetaCoq.

Best

Yannick

On 13 October 2020 23:33:01 Talia Ringer <tringer AT cs.washington.edu> wrote:

Hi again!

I'd like to try out a proof about one of my tools, but to do so I need to introspect on the behavior of inductive constructors and eliminators, so I guess I need an embedding of CIC. It's OK for the purpose of this proof to use univalence, since my tool's metatheory is univalent. Is there an embedding of CIC I can play with, maybe in CoqHoTT?

Talia

[Coq-Club] Reasoning about CIC in Coq + univalence, Talia Ringer, 10/13/2020
- Re: [Coq-Club] Reasoning about CIC in Coq + univalence, Yannick Forster, 10/13/2020
  - Re: [Coq-Club] Reasoning about CIC in Coq + univalence, Talia Ringer, 10/13/2020