Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange
Join us in building a kind, collaborative learning community via our updated Code of Conduct.

Coq is an interactive theorem prover.

1
vote
0answers
93 views

Is it possible to type Ackermann function with (stratified variant of) System F?

I was surprised to find no open-source implementation of Ackermann function in pure System F as an illustrative example. I finally managed to implement it myself in Haskell using Church encoding: <...
2
votes
1answer
75 views

Is there a formalization of normalization of impredicative system F?

In particular Agda seems not strong enough to prove that. Is the predicative Calculus of Inductive Constructions universes (Coq without Prop) sufficient? How about with the impredicative Prop?
8
votes
2answers
153 views

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

The StreamMemo library for Coq illustrates how to memoize a function f : nat -> A over the natural numbers. In particular when ...
3
votes
1answer
201 views

What exactly is “large elimination”?

I'm studying type theory (mostly Coq) and often encounter the term "large elimination", usually when talking about type universes hierarchy consistency, for example: impredicative polymorphism + ...
8
votes
3answers
635 views

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

I've been programming for several years, but am very unfamiliar with theoretical CS. I've recently been trying to study programming languages, and as part of that, type checking and inference. My ...
11
votes
2answers
760 views

Formal semantics of Ocaml in COQ

The semantics of a large subset of Ocaml, called OCamllight, was formalized in HOL by Owens several years ago. More recently, a type theoretical semantics of a smaller subset of Ocaml was implemented ...
3
votes
0answers
116 views

What is the largest complexity class that a non-Turing complete proof assitant, like Coq, can achieve? [duplicate]

Given that all functions in Coq will terminate, it cannot cover the entire $RE$. So what is the class it can achieve? Is it $R$?
6
votes
1answer
261 views

Examples of Universe inconsistency in normal use of dependent types

In dependent types, Type : Type results in inconsistency (Girard's or Hurken's paradox). Are there examples of universe inconsistency (where assuming ...
0
votes
1answer
205 views

`f_equal` isn't doing anything

I'm trying to do the following thing: take a set (here, nat, for the sake of simplicity), define a subset of "valid" values (here, even numbers), and then prove ...
5
votes
1answer
331 views

Featherweight Generic Java formalization in Coq

I've been searching for some nice formalization of FGJ (Featherweight Generic Java) in Coq. I am going to develop an extension of FGJ in Coq, so I hope there is an appropriate Coq implementation which ...
1
vote
1answer
420 views

What's wrong with this LEAN proof? [closed]

I'm learning to use the LEAN theorem prover and I got stuck in a proof of a simple fact in first-order logic: $$ p(x) \rightarrow \forall x p(x) $$ My code is the following: variables (A : Type) (p ...
4
votes
0answers
119 views

major applied focuses of different proof assistants

Currently, what are the major applied focuses (if any applications can be deserved such a distinction) of different proof assistants, such as the following? If there are significant differences ...
0
votes
1answer
133 views

Is there an algorithm to generate proof in Coq? [closed]

I try to imagine using Coq to implement large and complicated software with specifications and proof. However, the manual work of writing proof is daunting. As a Coq newbie, to specify an insertion ...
3
votes
0answers
141 views

Type theoretic equivalent of isomorphism class

How one defines the notion of isomorphism class in type theory? For concreteness I will describe what I mean with an example in Coq. Suppose I have a record ToyRec: ...
5
votes
3answers
639 views

Law of excluded middle in MLTT

Is it possible to add law of excluded middle to Martin-Löf type theory as an axiom? It seems to me, that it's possible to add it to Coq since Coq has a module for non-constructive reasoning. Also, it ...
9
votes
1answer
502 views

Equality of decidable proofs?

I want to know if the decidability of equality of two decidable proofs of the same proposition can be proved without any additional axioms in Calculus of Inductive Constructions. Specifically, I want ...
17
votes
2answers
522 views

Why an infinite type hierarchy?

Coq, Agda, and Idris have an infinite type hierarchy (Type 1 : Type 2 : Type 3 : ...). But why not do it instead like λC, the system in the lambda cube that's closest to the calculus of constructions, ...
0
votes
1answer
569 views

Reverse contraposition

While it is trivial to prove contraposition ∀ A B: Prop, (A → B) → (~B → ~A) using Coq, is it equally trivial to prove the reversed form: ...
1
vote
2answers
228 views

How to prove that a circular prop is uninhabited?

Consider the following inductive definition of "ElProp" in coq: ...
30
votes
3answers
3k views

Why does Coq have Prop?

Coq has a type Prop of proof irrelevant propositions which are discarded during extraction. What are the reason for having this if we use Coq only for proofs. Prop is impredicative, so Prop : Prop, ...
24
votes
2answers
2k views

Why do Agda and Coq disagree on strict positivity?

I've stumbled across a confusing disagreement between Agda and Coq that is not obviously related to the most well known distinctions between their type theories (e.g., (im)predicativity, induction-...
5
votes
1answer
542 views

Induction over a transitive relation in Coq

I have the current problem when using induction with Coq: I have states ST, which are pairs (A,B), where A are Addresses (nat) and B are Memories (A parameter) ...
4
votes
1answer
1k views

Defining Mutually Recursive functions in Coq

This question is related to (but not the same as): How to define a function inductively on two arguments in Coq? In particular, I used those techniques (defining a second fixed point function) and ...
5
votes
1answer
243 views

How to describe the set of “all computable functions” using Coq?

Would the set of all computable functions be just the set of all maps of the form f : forall n : nat, P n -> nat where ...
-2
votes
1answer
245 views

Problem in embedding

I want to embed PPTL(a kind of logic) in Coq. Because of its complex semantics, I just embed its systax. ...
2
votes
0answers
326 views

Encoding a logic in Coq

I want to encode a logic into Coq. The semantics of the logic are very complex and I just want to encode the syntax, axioms, inference rules. I use deep embedding, but I can't use notation like: <...
-2
votes
1answer
519 views

Coq definition with unusual syntax (Definition … Defined.)

While examining the package Library ZFC.Sets, I found the following definition: ...
11
votes
1answer
466 views

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

I've been searching for a formalization of the compactness theorem for FOL, but haven't found any. Is anyone aware of such a development or related work?
21
votes
1answer
1k views

Class of functions computable by Coq

Since it does not allow nonterminating computation, Coq is necessarily not Turing-complete. What is the class of functions that Coq can compute? (is there an interesting characterization thereof?)
12
votes
3answers
676 views

Modeling objects (OOP) in dependent type theory

I am interested in modeling objects, from object oriented programming, in dependent type theory. As a possible application, I would like to have a model where I can describe different features of ...
7
votes
1answer
1k views

How to use induction without Fixpoint definition in Coq?

I want to verify a program written in C. I am using Jessie to translate the (pre/post)conditions of the program to Coq. In Coq I will make a proof. Sometimes I need recursive definitions. ...
0
votes
2answers
638 views

Proving that inclusion is antisymmetric in Coq

I'm a Coq newbie and I'd like to prove that the inclusion relation is antisymmetric, that is: $\forall x\forall y(x\subseteq y\land y\subseteq x\rightarrow x=y)$. I wrote the following thing: ...
9
votes
2answers
280 views

Does the order of declarations in an inductive type matter?

I was wondering if the order of declarations of an inductive type can matter. For example in Coq you can define Nat either by: ...
16
votes
3answers
1k views

What is the role of predicativity in inductive definitions in type theory?

We often want to define an object $A \in U$ according to some inference rules. Those rules denote a generating function $F$ which, when it is monotonic, yields a least fixed point $\mu F$. We take $A :...
36
votes
4answers
3k views

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

I'm going over the course notes at CIS 500: Software Foundations and the exercises are a lot of fun. I'm only at the third exercise set but I would like to know more about what's happening when I use ...
17
votes
1answer
2k views

Prove proof irrelevance in Coq?

Is there a way to prove the following theorem in Coq? Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2. EDIT: An attempt to give a brief ...
20
votes
1answer
1k views

Where is the proof that Coq + Excluded Middle is consistent

I've seen (and heard) it claimed that it is safe to add the classical axiom of excluded middle to Coq, but I can not seem to find a paper supporting this claim. The papers I see listed on the Coq wiki ...
2
votes
2answers
258 views

formalizing a statement about the expressive power of programming languages wrt divergence

In the Coq'Art book the authors mention in passing that any language that can calculate all computable functions must also be able to express diverging computations. Or in other words, there can be no ...
13
votes
1answer
4k views

How to define a function inductively on two arguments in Coq?

How can I convince Coq that the recursive function given below terminates? The function takes two inductive arguments. Intuitively, the recursion terminates because either argument is decomposed. ...
44
votes
3answers
4k views

Shallow versus Deep Embeddings

When encoding a logic into a proof assistant such as Coq or Isabelle, a choice needs to be made between using a shallow and a deep embedding. In a shallow embedding logical formulas are written ...
15
votes
2answers
929 views

Eliminating cofix in Coq proof

While trying to prove some basic properties using coinductive types in Coq, I keep running into the following problem and I cannot get around it. I've distilled the problem into a simple Coq script as ...