## 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$

#### 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: Feb 09 2023 at 02:02 UTC