Stream: Coq Workshop 2021

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

Christian Doczkal (Jul 02 2021 at 09:37):

Video Presentation by @Dominik Kirst and collaborators

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:

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?

Théo Winterhalter (Jul 02 2021 at 10:04):

I was wondering as well if Iris had this.

Christian Doczkal (Jul 02 2021 at 10:04):

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

Dominik Kirst (Jul 02 2021 at 10:05):

yep, no de Bruijn indices in Iris

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."

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

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,

Cyril Cohen (Jul 02 2021 at 10:16):

$\lambda \lambda \lambda 2 0 1$

Enrico Tassi (Jul 02 2021 at 10:16):

Reading indexes is ... exactly

Meven Lennon-Bertrand (Jul 02 2021 at 10:18):

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

Théo Winterhalter (Jul 02 2021 at 10:18):

Reading the 0th variable is ok.

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

Meven Lennon-Bertrand (Jul 02 2021 at 10:22):

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

Pierre Courtieu (Jul 02 2021 at 10:23):

Is that how you separate them from mathematicians too?

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]

Dominik Kirst (Jul 02 2021 at 10:26):

(and that's just a single nested quantifier)

Meven Lennon-Bertrand (Jul 02 2021 at 10:27):

Ok you’ve convinced me there, all hail names

Last updated: Apr 16 2024 at 20:02 UTC