Skip to main content
8 votes

How do real-world proof assistants bind variables and check equality?

Variables λΠ uses the Bindlib library, and so do several other systems, see the paper Abstract Representation of Binders in OCaml using the Bindlib Library and package documentation. I have recently ...
7 votes

How do real-world proof assistants bind variables and check equality?

Idris 2 is self-hosted and as such it can use dependent types when specifying the operations on its own intermediate representations. Variables The core language is well-scoped by construction which ...
7 votes

Possible root cause(s) of the misunderstanding that DTT implies not Turing complete?

[Supplemental: I rewrote the answer so that any shred of vagueness is gone, as it was evoking religuous zeal, and I would prefer to stick to math. Everything is explained in terms of a widely accepted ...
Andrej Bauer's user avatar
  • 9,593
7 votes
Accepted

What are the principal differences between Agda's core type theory and Coq's?

I will answer the headline question and ignore UTT (I believe thinking of Agda as UTT causes more confusion than it solves). There are very many differences between the theories Agda and Coq implement,...
James Wood's user avatar
  • 1,053
7 votes

Binding variables to terms involving later variables

Great question Mike! Since Thierry Coquand's talk at the 1991 TYPES meeting in Edinburgh, and reading Martin Löf's "Mathematics of infinity" paper, and various things by Thierry subsequently,...
James McKinna's user avatar
6 votes

How do real-world proof assistants bind variables and check equality?

Since you asked about Lean, it uses De Bruijn indices and naive/explicit substitution for bound variables, unique names/locally nameless for free variables, and call by name with caching. The ...
6 votes

How do real-world proof assistants bind variables and check equality?

Core term definition In the latest version of Aya, we use locally nameless approach where names are represented by Java object identity (see this), and bound variables are integers (see this). Bound ...
5 votes

Binding variables to terms involving later variables

Coq (and probably Lean too): The answer for (vanilla) Coq is simple: it does not. Nothing is done to n to remember its relation to the pattern in the branch. The ...
Meven Lennon-Bertrand's user avatar
5 votes
Accepted

How to convert Agda's with statement to a helper function?

The based identity type _≡ n + m is the type family inductively generated by a single constructor refl : n + m ≡ n + m. This ...
Naïm Favier's user avatar
5 votes

Possible root cause(s) of the misunderstanding that DTT implies not Turing complete?

Is this perhaps a problem with 'common understanding' regarding what it means to be Turing complete? Indeed it is: a pop-science understanding of dependent types has led to this myth being deeply ...
gallais's user avatar
  • 1,256
5 votes
Accepted

How to provide proof for termination in Agda?

There are three possible approaches: Use a different algorithm, like division in stdlib, see div-helper. Use the well-founded induction library. There are many ...
ice1000's user avatar
  • 6,276
4 votes

How do real-world proof assistants bind variables and check equality?

Agda Variables in Agda are represented as de Bruijn indices, and there is a type of explicit substitutions that is used in many places throughout the typechecker. Reduction is done by a lazy abstract ...
4 votes

Has extensionality ever caused any problems in a mathematical proof?

Kind of fun to note that extensionality is inconsistent with the internal Church Thesis which states that every function $\mathbb{N}\rightarrow\mathbb{N}$ is realized by some Turing machine. In turn ...
cody's user avatar
  • 384
4 votes
Accepted

Has extensionality ever caused any problems in a mathematical proof?

Function extensionality is “safe“ in the sense that it is valid in traditional constructive mathematics, for example as practiced by Erret Bishop, as well as in any topos. It is also valid in homotopy ...
Andrej Bauer's user avatar
  • 9,593
4 votes

Examples of theories where tactic language is required for simple proofs

so far I do not see any reasons why the same reasoning would not work for the rest of SF Wait for (or jump straight to) at least https://softwarefoundations.cis.upenn.edu/slf-current/Rules.html ;) 3. ...
Alex Chichigin's user avatar
3 votes
Accepted

Can Hyperreal exist a axiom-free implementation in HoTT?

For a survey of formalizations of real numbers you can look at Formalization of real analysis: a survey of proof assistants and libraries by Sylvie Boldo, Catherine Lelay and Guillaume Melquiond. ...
Andrej Bauer's user avatar
  • 9,593
3 votes
Accepted

Is there a formalism of "coinductive" data types with negative occurrences?

I found my answer in Guarded Domain Theory and its implementation in Guarded Cubical Agda (implementing Ticked Cubical Type Theory). The following program type-checks ...
Sebastian Graf's user avatar
1 vote

What are the typechecking differences between records and iterated sigma types in Agda?

There is no typechecking difference because Sigma types are records in Agda. So generally, Sigma types represent a subset of the options one has for declaring record types (eta or no, inductive or no, ...
Joey Eremondi's user avatar
1 vote

Why doesn't the proof found by Agda's automatic search (with dot-prefixed patterns) work?

Dotted patterns are also known as inaccessible patterns. My understanding is that the matched bindings are inaccessible, because they are generated from index unification. That's why they are marked ...
ice1000's user avatar
  • 6,276

Only top scored, non community-wiki answers of a minimum length are eligible