Hot answers tagged

21 votes

What should a proof of correctness for a typechecker actually be proving?

That's a good question! It asks what we expect from types in a typed language. First note that we can type any programing language with the unitype: just pick a letter, say ...
user avatar
  • 26.6k
19 votes
Accepted

Why an infinite type hierarchy?

Actually, the approach of the CoC is more expressive -- it permits arbitrary impredicative quantification. For example, the type $\forall a.\; a \to a$ can be instantiated with itself to get $(\forall ...
user avatar
14 votes
Accepted

Defining inductive types in intensional type theory purely in terms of type-theoretic data

It turns out that $W$ types plus identity types (eq/= in Coq) allow you to construct pretty much all the general inductive types ...
user avatar
12 votes

Formal semantics of OCaml in Coq

Have you seen Arthur Charguéraud's PhD thesis, Characteristic Formulae for Mechanized Program Verification? Rather than building the type system and small-step semantics as inductive relations, he ...
user avatar
10 votes
Accepted

What should a proof of correctness for a typechecker actually be proving?

The question can be interpreted in two ways: Whether the implementation does implement a given typing system $T$? Whether the typing system $T$ does prevent the errors you think it should? The ...
user avatar
9 votes

Why an infinite type hierarchy?

I'll compliment Neel's (excellent, as usual) answer with a bit more exposition on why levels are used in practice. The first important limitation of CoC is that it is trivial! A surprising ...
user avatar
  • 13.2k
9 votes
Accepted

Examples of Universe inconsistency in normal use of dependent types

This is a hard question to answer, in part because it's unclear what it means to get something "by accident". Regularly, though, people run into the ...
user avatar
  • 13.2k
8 votes
Accepted

Is there a formalization of normalization of impredicative system F?

Coq without Prop is not strong enough, because it's basically Martin-Löf type theory with universes. Coq with Prop is strong enough, because you can encode sets of normalizing terms via predicates $S :...
user avatar
8 votes
Accepted

What exactly is "large elimination"?

You are incorrect about the definition of large elimination: it refers to the ability to build values of type $\mathrm{Type}$ by eliminating an inductive value. The canonical example: ...
user avatar
  • 13.2k
8 votes

Formal semantics of OCaml in Coq

You could be interested in Jacques Garrigue's A Certified Implementation of ML with Structural Polymorphism and Recursive Types, which establishes the soundness of static and dynamic semantics and ...
user avatar
  • 1,882
7 votes
Accepted

Law of excluded middle in MLTT

Law of excluded middle does not make intuitionistic logic inconsistent; intuitionistic logic is in many regards a subset of classical logic (of course classical logic can't have proof objects and ...
user avatar
  • 1,131
6 votes
Accepted

What's wrong with this LEAN proof?

Your example is not true, that's why you cannot prove it. If we assume your example is true (which we do using the sorry tactic), then we can prove ...
user avatar
6 votes
Accepted

Impredicativity + large eliminations (with no excluded middle) in Coq

No: strong elimination of large inductive types (SELIT) is itself inconsistent because it breaks the layering of universes by trivially allowing you to smuggle a large value in a Prop box and take it ...
user avatar
  • 382
6 votes
Accepted

How does axiom K contradict univalence?

You will certainly find it natural that most types, like structures, admit different isomorphisms. Just take the type $\textbf{2}$, with inhabitants $0_\textbf{2}$ and $1_\textbf{2}$. It admits 2 ...
user avatar
  • 176
5 votes
Accepted

`f_equal` isn't doing anything

The f_equal tactic does not do anything because what you are trying to prove is not true. You assumed that the first components (...
user avatar
  • 26.6k
5 votes

Has the compactness theorem for FOL been formalized in Coq/Isabelle/etc?

Compactness for FOL was done in HOL by John Harrison, and reported at TPHOLs 1998. See Formalizing basic first order model theory.
user avatar
5 votes
Accepted

How to prove that a circular prop is uninhabited?

You should use False instead of 1>2 in the conclusion of the theorem. Using indirect ways of denoting an impossible ...
user avatar
5 votes
Accepted

Representations of Planar Graphs in Coq

The obvious resource for planar graphs in Coq would be the (modern port of) the four color theorem in Coq/SSReflect, by Georges Gonthier (and others) which obviously does need to define planar graphs. ...
user avatar
  • 13.2k
5 votes
Accepted

Universe polymorphism: the inference of universes and their constraints

It's complicated because universe constraints are simplified during inference (in order to avoid an explosion of constraints). Have a look at: Matthieu Sozeau and Nicolas Tabareau: Universe ...
user avatar
  • 26.6k
5 votes
Accepted

Equality of decidable proofs?

As Neel points out if you work under the "propositions are types" then you can easily come up with a type whose equality cannot be shown decidable (but it is of course consistent to assume that all ...
user avatar
  • 26.6k
5 votes

What should a proof of correctness for a typechecker actually be proving?

There are a few different things you could mean by "prove that my typechecker works". Which, I suppose, is part of what your question is asking ;) One half of this question is proving that your type ...
user avatar
5 votes
Accepted

Defining finite sets inductively in a proof assistant?

There are many variants of finite sets in constructive mathematics. One that can be defined using just inductive definitions, and is therefore amenable to formalization in type theory, is the ...
user avatar
  • 26.6k
4 votes

How can you build a coinductive memoization table for recursive functions over binary trees?

It's easy enough to get the recursion pattern to work with sized types. Hopefully the sharing is preserved through compilation![1] ...
user avatar
  • 141
4 votes

Representations of Planar Graphs in Coq

I just wanted to make some additional comments not already covered by Cody's nice answer, and also address question (2). First, Gonthier goes into detail about the representation of planar maps used ...
user avatar
4 votes

How to prove that a circular prop is uninhabited?

I think you need induction here to help you show that there is no term like C2 (C1 (C2 (C1 .... I also think you need to strengthen your induction hypothesis, ...
user avatar
  • 11k
4 votes

How would I go about learning the underlying theory of the Coq proof assistant?

The current Software Foundations book does explain all this later on: https://softwarefoundations.cis.upenn.edu/lf-current/ProofObjects.html So if you're following the book, just read on :)
user avatar
4 votes

Dependent eliminator for empty type in intensional Martin-Löf type theory

$\text{absurd} : (A : \text{U}) \to 0 \to A$ and $\text{elim} : (A : 0 \to \text{U}) \to (x : 0) \to A\,x$ are equivalent. To go right, use $\text{absurd}\,(A\,x)\,x$. To go left, use $\text{elim}\,(\...
user avatar
3 votes

Featherweight Generic Java formalization in Coq

I guess somewhat more realistic task would be to find Coq's formalisation of FJ itself (probably with some extensions, but not necessarily FGJ). The one which I googled easily is: Encoding ...
user avatar
3 votes
Accepted

Reverse contraposition

It is not provable without additional axioms. In fact, it implies double negation elimination (take $B=\top$), which in turn is equivalent to the excluded middle.
user avatar
  • 13.2k
3 votes

Modeling objects (OOP) in dependent type theory

There is a substantially expanded follow paper Andreas Abel, Stephan Adelsberger, Anton Setzer: Interactive Programming in Agda - Objects and Graphical User Interfaces. It contains an Agda library ...
user avatar

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