Stream: Coq Workshop 2021

Topic: [S2T1] A Toolbox for Mechanised First-Order Logic


view this post on Zulip Christian Doczkal (Jul 02 2021 at 09:37):

Video Presentation by @Dominik Kirst and collaborators

view this post on Zulip Cyril Cohen (Jul 02 2021 at 09:56):

@Yannick Forster I'm glad you could make sense of our FLoC 2018 discussion about HOAS -> DeBrujin :joy:

view this post on Zulip Yves Bertot (Jul 02 2021 at 10:03):

Question by Theo Winterhalter really thought provoking! Not only the goals have to go through some "display machinery" but also the lemmas that have already been proved. Is there is a similar problem in Iris proof mode?

view this post on Zulip Théo Winterhalter (Jul 02 2021 at 10:04):

I was wondering as well if Iris had this.

view this post on Zulip Christian Doczkal (Jul 02 2021 at 10:04):

Doesn't iris use a shallowly embedded logic? Does that mean they have Coq names available?

view this post on Zulip Dominik Kirst (Jul 02 2021 at 10:05):

yep, no de Bruijn indices in Iris

view this post on Zulip Théo Winterhalter (Jul 02 2021 at 10:13):

Beyond that, it made me think of the talk of yesterday: "A graphical user interface framework for formal verification. Edward William Ayers, Mateja Jamnik and William Gowers."

view this post on Zulip Meven Lennon-Bertrand (Jul 02 2021 at 10:15):

I think it is one order of magnitude less hard to read de Bruijn than to write it, though

view this post on Zulip Enrico Tassi (Jul 02 2021 at 10:16):

Meven Lennon-Bertrand said:

I think it is one order of magnitude less hard to read de Bruijn than to write it, though

Reading De Buijn levels is very easy,

view this post on Zulip Cyril Cohen (Jul 02 2021 at 10:16):

λλλ201\lambda \lambda \lambda 2 0 1

view this post on Zulip Enrico Tassi (Jul 02 2021 at 10:16):

Reading indexes is ... exactly

view this post on Zulip Meven Lennon-Bertrand (Jul 02 2021 at 10:18):

True, when the same variable changes number because of a binder, you die

view this post on Zulip Théo Winterhalter (Jul 02 2021 at 10:18):

Reading the 0th variable is ok.

view this post on Zulip Enrico Tassi (Jul 02 2021 at 10:19):

In Coq's code indexes start at 1 (why is a mystery to me), so if you see a 0 you can probably prove False

view this post on Zulip Meven Lennon-Bertrand (Jul 02 2021 at 10:22):

Coq’s developers are true mathematicians, that’s how you separate them from computer scientists

view this post on Zulip Pierre Courtieu (Jul 02 2021 at 10:23):

Is that how you separate them from mathematicians too?

view this post on Zulip Dominik Kirst (Jul 02 2021 at 10:24):

Meven Lennon-Bertrand said:

True, when the same variable changes number because of a binder, you die

Already the indices in the replacement scheme of ZF are not fun to chase:
fun_rel phi ~> ∀ ∃ ∀ $0 ∈ $1 ↔ ∃ $0 ∈ $3 ∧ phi[$0 .: $1 .: Nat.add 4 >> var]

view this post on Zulip Dominik Kirst (Jul 02 2021 at 10:26):

(and that's just a single nested quantifier)

view this post on Zulip Meven Lennon-Bertrand (Jul 02 2021 at 10:27):

Ok you’ve convinced me there, all hail names


Last updated: Aug 11 2022 at 01:03 UTC