Hot answers tagged

36

$\mathtt{Prop}$ is very useful for program extraction because it allows us to delete parts of code that are useless. For example, to extract a sorting algorithm we would prove the statement "for every list $\ell$ there is a list $k$ such that $k$ is ordered and $k$ is a permutatiom of $\ell$". If we write this down in Coq and extract without using $\mathtt{...


21

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 U, and say that every program has type U. This isn't terribly useful, but it makes a point. There are many ways to understand types, but from a programmer's point of view the following ...


20

$\mathrm{Prop}$ is impredicative, which create a very expressive proof system. However it is "too" expressive in the following sense: $$ \mathrm{impredicative\ Prop} + \mathrm{large\ elimination} + \mathrm{excluded\ middle} $$ is inconsistent. Usually you want to keep the possibility to add the excluded middle, so one solution is to keep large elimination ...


19

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 a.\; a \to a) \to (\forall a.\; a \to a)$, which is not possible with a universe hierarchy. The reason it is not widely used is because impredicative ...


14

Even if you are not interested in extracting programs, the fact that Prop is impredicative allows you to build some models which you can't build using a predicative tower of universes. IIRC Thorsten Altenkirch has a model of System F using Coq's impredicativity.


14

It is important to understand that there is a spectrum from deep to shallow. You model the parts of your language deeply that should somehow participate in some inductive argument about the construction of it, the remainder is better left in the shallow see of direct semantics of the substrate of the logic. For example, when you want to reason about Hoare ...


12

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 gives a technique for converting Caml programs into characteristic formulas. This are basically a generalization of predicate transformer semantics to support a ...


10

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 former is really a question in program verification and has little to do with typing. Just needs showing that your implementation meets its specification, see Andrej'...


10

The issue seems to be confusion resulting from a confluence of two factors: I was using a stale version of Agda (2.3.0.1). It appears that prior to 2.3.2, Agda simply wasn't checking strict positivity of the indices of constructor results (see the bug I linked elsewhere in the thread). A closer reading of Dybjer's Inductive Families paper suggests that he ...


9

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 observation is that there is no type for which you can prove that it has more than one element, much less an infinite number of them. Adding just 2 universes gives you ...


8

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 properties of type inference for a ML language with (recursion and) structural polymorphism, thus formalizing one of the more advanced corners of OCaml (...


8

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 Universe Inconsistency error of Coq, as some quick googling will show (e.g. here). This certainly sometimes happens by accident, sometimes in the attempt at showing inconsistencies or testing the limits of the ...


7

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 there are other diffrences). In Agda you can use the postulate keyword for such things. The following could be added to your postulates. $LEM : \{A : Set\} \to A \...


7

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 : \mathrm{Term} \to \mathrm{Prop}$, and impredicative universal quantification lets you express arbitrary intersections.


6

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 false. The proof goes as follows. We first pick x to be 0 and p to be the property that a number n is equal to 0. So p x is p 0 is 0 == 0 which is obviously true. Your example now provides us with the proof that ...


6

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: bool_to_type : bool -> Type := fun b => match b with | true => Unit | false => Empty Where Unit and Empty are inductive types with 1 and 0 ...


5

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 types have decidable equality), such as $\mathbb{N} \to \mathbb{N}$. If we understand "proposition" as a more restricted kind of type, then the answer depends on ...


5

The f_equal tactic does not do anything because what you are trying to prove is not true. You assumed that the first components (VN_value) of m and n are equal, but what about the second components (VN_prop), how do you intend to prove they are equal? Also note that we cannot decompose the equation {| VN_value := m_value; VN_prop := m_prop |} = {| ...


5

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


5

You should use False instead of 1>2 in the conclusion of the theorem. Using indirect ways of denoting an impossible proposition is an unnecessary complication. False is the impossible proposition used in the standard library. In order to prove that ElProp R1 is uninhabited, you need to prove that ElProp R2 is uninhabited, and vice versa. You need ...


5

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 theory is good enough to prove whatever properties about the language. Andrej's answer tackles this area very well imo. The other half of the question is —...


5

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 Polymorphism in Coq, Interactive Theorem Proving - 5th International Conference, ITP 2014 Beta Ziliani & Matthieu Sozeau: A Unification Algorithm for Coq featuring ...


5

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. It's not immediately obvious to me how planar graphs are characterized, though the relevant file is here and it seems to involve a combination of Euler ...


5

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 Notherian finiteness by Thierry Coquand and Arnaud Spiwack. The idea is to define a set or a type $A$ to be finite if the following holds: every sequence $a : \mathbb{N}...


4

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, because you don't just need to know that ElProp C1 is uninhabited, but that ElProp C2 is as well. I proved this using an auxiliary lemma Theorem excircular_help : forall y, forall x:(ElProp y), y = ...


4

A possible reason for the difference, as your own remarks hint, is impredicativity. Coq historically had an impredicative set (still available as a flag i believe!) Quoting Adam Chlipala's book http://adam.chlipala.net/cpdt/html/Universes.html The Coq tools support a command-line flag -impredicative-set, which modifies Gallina in a more fundamental way ...


4

It is not clear to me how induction helps with the lemma you are trying to prove, so I'll take an alternative approach. Firstly, I prove two helper lemmas that break apart and put back together ==> with --> at the tail, rather than at the start. Based on these lemmas, I can manipulate the result using your definition of eval to get the desired result....


4

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 :)


4

It's easy enough to get the recursion pattern to work with sized types. Hopefully the sharing is preserved through compilation![1] module _ where open import Size open import Data.Nat data BT (i : Size) : Set where Leaf : BT i Branch : ∀ {j : Size< i} → BT j → BT j → BT i record Memo (A : Set) (i : Size) : Set where coinductive field leaf :...


4

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 for the formalization of 4CT in his technical report A computer-checked proof of the Four Colour Theorem. This representation is based on the classical (and ...


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