Video Presentation by @Dominik Kirst and collaborators

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

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?

I was wondering as well if Iris had this.

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

yep, no de Bruijn indices in Iris

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

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

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,

$\lambda \lambda \lambda 2 0 1$

Reading *indexes* is ... exactly

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

Reading the 0th variable is ok.

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

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

Is that how you separate them from mathematicians too?

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]`

(and that's just a single nested quantifier)

Ok you’ve convinced me there, all hail names

Last updated: Sep 15 2024 at 12:01 UTC