# Questions tagged [coq]

Coq is an interactive theorem prover based on the Calculus of Inductive Constructions.

66 questions
Filter by
Sorted by
Tagged with
10k views

### Learning Automated Theorem Proving

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. Note that these topics are not easily digested ...
• 5,101
3k views

### Recursive definitions over an inductive type with nested components

Consider an inductive type which has some recursive occurrences in a nested, but strictly positive location. For example, trees with finite branching with nodes using a generic list data structure to ...
2k views

### Is possible to prove undecidability of the halting problem in Coq?

I was watching the "Five Stages of Accepting Constructive Mathematics" by Andrej Bauer and he says that there is two kinds of proof by contradiction (or two things that mathematicians call proof by ...
406 views

### Has Anyone Actually Created a System that Writes Computer Programs from specification?

Has anyone ever actually written a system (software or detailed explanation on paper with simple examples) that generates computer programs? I input $Prime(x) \wedge x<10$ and it creates a program ...
5k views

### What is different between Set and Type in Coq? [closed]

AFAIU types can be a Set whose elements are programs or a proposition whose elements are Proofs. So based on this understanding: ...
2k views

### Monadic Second Order Logic for Dummies

I am programmer with a grip on automata, but not on logic. I read in papers that the two are very tightly related. Deterministic Finite Automata (DFA), Tree Automata and Visibly Pushdown Automata are ...
2k views

### Proving tautology with coq

Currently I have to learn Coq and don't know how to deal with an or : As an example, as simple as it is, I don't see how to prove: ...
• 425
2k views

### Standard constructive definitions of integers, rationals, and reals?

Natural numbers are defined inductively as (using Coq syntax as an example) Inductive nat: Set := | O: nat | S: nat -> nat. Is there a standard way to define ...
• 263
1k views

### baz_num_elts exercise from Software Foundations

I'm at the following exercise in Software Foundations: ...
• 123
282 views

### Is extensionality for coinductive datatypes consistent with Coq's logic?

Given a coinductive datatype, one can usually (always?) define a bisimulation as the largest equivalence relation over it. I would like to add an axiom stating that if two members of the type are ...
2k views

### Why does Coq include let-expressions in its core language

Coq includes let-expressions in its core language. We can translate let-expressions to applications like this: let x : t = v in b ~> (\(x:t). b) v I understand ...
• 565
1k views

### Polymorphism and Inductive datatypes

I'm curious. I've been working on this datatype in OCaml: ...
• 1,490
2k views

### Theorem Proofs in Coq

Background I am learning assistance, Coq, on my own. So far, I have completed reading Yves Bertot's Coq in a Hurry. Now, my goal is to prove some basic results concerning the natural numbers, ...
• 161
359 views

### Why are recursive types needed as primitives for proofs in dependent type systems?

I'm relatively new to type theory and dependent programming. I've been studying the calculus of constructions (CoC) and other pure type systems. I'm particularly interested in using it as a proof-...
• 711
2k views

### Does there exist any work on creating a Real Number/Probability Theory Framework in COQ?

COQ is an interactive theorem prover that uses the calculus of inductive constructions, i.e. it relies heavily on inductive types. Using those, discrete structures like natural numbers, rational ...
• 868
587 views

### What does instantiating existential variables with out of scope variable imply?

I have following unfinished proof of a lemma: ...
• 632
655 views

### Main differences between intuitionistic type theory and calculus of constructions (CoC)

Quoting Wikipedia "Many systems of type theory, such as the simply-typed lambda calculus, intuitionistic type theory, and the calculus of constructions, are also programming languages." I'm a Coq user ...
• 81
224 views

### Formalizing basic category theory in Coq

I'm a total beginner in Coq and I'm trying to implement some category theory stuff as an exercise. I surfed a little among git repos of the many avaible such implementations (HoTT, Awodey's Coq ...
• 311
272 views

### Can coq express its own metatheory?

I'm learning about language metatheory and type systems, and am using coq to formalize my study. One of the things I'd like to do is examine type systems that include dependent types, which I ...
• 209
589 views

### How does one know what statements in Coq require Induction?

I was trying to learn Coq using the famous book Software Foundations. In it I found the following: ...
• 3,040
2k views

### What is the difference between "definition" and "inductive" in Coq?

In Coq, you can use two different kinds of keywords to do definitions--Inductive and Definition. I do not understand the difference between an inductive and a definition, or when it is appropriate to ...
707 views

### Is the strictly positive condition in Coq and Agda an aproximation?

Languages like Coq and Agda enforce that their inductive types occur "strictly positively" in their definitions. That is, the type should not occur to the left of an arrow of an argument of a ...
• 3,810
569 views

### Proof of equality with destructuring let...in

I have some expression (f n in the example below) returning a tuple. I would like to prove that f n is equal to ...
625 views

### How does this use of "apply" in Coq work?

I'm working my way through software foundations. In the Chapter titled "Tactics", I'm able to prove this theorem in Coq: ...
588 views

### Coq --- non-terminating programs [duplicate]

People usually say Coq does not allow writing non-terminating functions. I have a question regarding that. Does Coq allow writing exactly all terminating functions? In other words, what are the ...
• 1,654
454 views

### Algorithmic type checking for Calculus of Inductive Constructions

So from reading "Advanced Topics in Types and Programming Languages" (ATTPL) I know of the calculus of constructions (CoC). It also presents the "algorithmic" type checking rules. Reading Coq's ...
• 3,810
325 views

### What types are propositions?

In the propositions-as-types paradigm, we are still faced with the question : what types are propositions ? I currently know 3 different answers : Coq's sort Prop ...
• 153
186 views

### Proving with co-induction principles

I'm going through Adam Chlipala's "Certified Programming with Dependent Types" (available here for convenience), and I'm a bit stuck at internalizing the introduction of co-induction principle for the ...
• 175
1k views

### Euclidean Algorithm in Coq

Question How do I write more intuitive proofs of the two following results in Coq? ...
• 161
387 views

### What is the runtime/time complexity of Coq’s (Dependent) Type Inference?

I remember learning in a class that type inference is decidable but usually takes a long time (e.g. type inference in OCaml is EXPTIME). I was wondering, since Coq allows programs/values themselves to ...
• 3,040
295 views

### In Coq, what does it mean to have an inductive type where the right-hand side of ":" is Prop?

I'm new to Coq, and my (rather limited) understanding is that inductive types are like algebraic datatypes in Haskell, so there is a constructor data T = A a with ...
• 195
95 views

### Why does substitution terminate?

I'm formalizing some properties of lambda calculus in Coq and I have some problems proving termination of substitution. My terms are defined as: ...
284 views

### Is impredicative Set consistent with the excluded middle?

While studying Coq, I found a few references that impredicative Set might not work well with classical axioms, in particular the axiom of choice. I'm working on a dependent type system based on the ...
• 711
400 views

### Simple question COQ

I'm a beginner in the coq proof assistant, so sorry if my question is silly. I would like to prove properties of a mathematical object. For clarity I will describe an over-simplified version of my ...
558 views

### I don't know how to prove a simple theorem used with fixpoint in Coq

I am a beginner in coq and want to prove the following theorem t1. First I used induction i and destruct j, but it got bogged ...
• 33
296 views

### Building non-classical logics in Agda & Coq

Is it possible to construct different systems of logic in Coq or Agda? I ask because I'm interested in using a proof assistant to construct (and verify) theorems in things like many-valued logics, ...
263 views

### positivity condition in Coq/CIC

I am recently learning the theory behind Coq and learnt that positivity condition guarantees termination of the program. But my question is, what would you think of the following definition? ...
• 632
273 views

### When can the coinduction hypothesis be used?

We can use the induction hypothesis when we are proving a property for a structure that is well-ordered. I am aware that there is a proof for this. When it comes to coinduction, I'm confused. One of ...
• 153
260 views

### For proof automation in Coq, when is it appropriate to use canonical structures or Equations instead of Ltac?

There are a few possible approaches to proof automation in modern Coq. Writing proof scripts with Ltac. This is the approach described in http://adam.chlipala.net/cpdt/, which the author uses to ...
• 131
177 views

### Is this a well founded inductive type? Can I express this in Coq?

the standard List type in Coq can be expressed as: Inductive List (A:Set) : Set := nil : List A | cons : A -> List A -> List A. as I understand, W-type ...
• 75
52 views

### Why isn't plus_assoc rewriting correctly?

First I have plus_assoc ready. Theorem plus_assoc : forall n m p : nat, n + (m + p) = (n + m) + p. for simplicity we omit the ...
• 155
473 views

### What are the implications of Lean not having the type Set?

In Coq we have an impredicative base type, called Prop, and a predicative base type, called Set, both of type ...
• 485
147 views

### An instance when you can eliminate propositional double negation in coq

Suppose st: string -> nat and X stands for the string 'X'. Given the hypothesis ...
• 229
230 views

### Proving parametricity for Gallina functions

I have the following definitions Definition nat'' {X : Type} := (X -> X) -> X -> X. Definition nat' := forall (X : Type), @nat'' X. And when I wanted to ...
431 views

### Type Theory and Principia Mathematica Part IV "Relation Arithmetic"

As type theory is a principle focus of modern computer science, its origins are in Bertrand Russel's theory of types, Principia Mathematica is both the origin of and is expressed in the theory of ...
• 404
246 views

### How to prove transitivity of < (Software Foundations exercise)?

I'm working through the "Properties of Relations" chapter of Software Foundations, but have got stuck on one of the exercises, lt_trans'': ...
• 141
160 views

### Understanding the definition of Positivity Constraints in Coq

In Interactive Theorem Proving and Program Development the authors explain constraints on constructors of inductive types in Coq. For inductive type $T$, a constructor must have the form \$t_1 \...
• 215
119 views

### What are the differences between LCF's Theorem and Automath's Prop?

How are the fundamental approaches to proving theorems by LCF and Automath different? Considering their modern descendants - Isabelle for LCF and Coq for Automath, both rely on type checking to do ...