What's the deal with Deno? We talk with a major contributor to find out. Listen now.

Questions tagged [coq]

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

Filter by
Sorted by
Tagged with
1
vote
0answers
29 views

why is behaviour of simpl differ so much after a commutative operation and how to inspect simpl?

In Coq, while trying to prove a lemma mult_n_Sm for mult_comm, I have this equation in a proof: ...
2
votes
1answer
18 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 ...
2
votes
0answers
38 views

Can HOL be simulated in the CiC?

I was wondering if HOL (higher-order logic) can be simulated in the Calculus of Inductive constructions (CiC)
2
votes
0answers
41 views

Difference between the logic and the type system of a proof assistant?

In Comparing Mathematical Provers (section 4.1), Wiedijk classifies logics and type systems of different proof assistants? I do not see what he means by type system of the assistant. He only says: A ...
1
vote
1answer
44 views

Instantiating a class with a sig'd type in Coq

I can easily define a class that corresponds to the notion of a "monoidal structure" on a type M via ...
1
vote
1answer
26 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'': ...
1
vote
1answer
70 views

on coq: Why is the proof complete after proving only for one induction when we have more than one variable?

So I'm learning coq. And I came across the proof for associativity in addition forall (a b c : nat) Appearntly when we do ...
2
votes
0answers
24 views

What can we have in exchange if we drop subtyping from definition of Calculus of Inductive Constructions?

If we remove subtyping (https://coq.inria.fr/distrib/current/refman/language/cic.html#subtyping-rules) from CIC we will lose some expressive power. But is that power necessary for a programming ...
3
votes
1answer
85 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 ...
0
votes
0answers
20 views

Struggling with this Coq Proof

Fixpoint intersection (l1 l2 : natset) : natset := match l1 with | [] => [] | h :: t => if member h l2 then insert h intersection t l2 else intersection t l2 end. I need to write an ...
-1
votes
1answer
83 views

Stuck on proof in Coq

This is an exercise from Software foundations for my discrete math & functional programming class. I am a little stuck with the end of the code because it works for the first two examples but it ...
4
votes
1answer
96 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 ...
9
votes
1answer
1k 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 ...
3
votes
1answer
122 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 ...
4
votes
1answer
146 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 ...
4
votes
4answers
197 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: ...
5
votes
1answer
194 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: ...
3
votes
0answers
66 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 ...
2
votes
1answer
123 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 \...
2
votes
2answers
175 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 ...
2
votes
1answer
168 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 ...
0
votes
1answer
125 views

How CompCert “proves” different things in its codebase

In order to understand examples of formal proofs, I am interested in how CompCert applies "proof" techniques. Specifically, I am wondering what a particular example is of something CompCert "proves" ...
4
votes
1answer
80 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: ...
4
votes
1answer
180 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 ...
14
votes
1answer
892 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 ...
4
votes
1answer
177 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 ...
1
vote
1answer
181 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? ...
7
votes
1answer
369 views

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

I have following unfinished proof of a lemma: ...
13
votes
1answer
2k 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: ...
23
votes
1answer
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 ...
1
vote
1answer
351 views

How to prove T Z = Z for binary representation of natural numbers in Coq

I have defined an Inductive in Coq for binary representation of natural numbers as follows: ...
3
votes
2answers
383 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 ...
3
votes
1answer
380 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 ...
10
votes
1answer
282 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-...
12
votes
2answers
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: ...
12
votes
0answers
201 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 ...
5
votes
2answers
249 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 ...
1
vote
2answers
106 views

Substituting two different identifiers with the same identifier in Coq - why does this work?

I'm playing around with Coq and Software Foundations and is somehow very confused by something I took for granted since forever. To prove ...
7
votes
2answers
149 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 ...
6
votes
0answers
553 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 ...
7
votes
0answers
515 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 ...
5
votes
2answers
279 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 ...
1
vote
0answers
22 views

Importance of indexes in Type(i) in calculus of inductive constructions [duplicate]

So I am reading about the calculus of inductive constructions. And I see here and here that there hidden indexes that the user does not know about in the $Type$ sort. It says that they are ...
10
votes
2answers
1k 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 ...
4
votes
2answers
310 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 ...
9
votes
1answer
1k views

baz_num_elts exercise from Software Foundations

I'm at the following exercise in Software Foundations: ...
7
votes
1answer
230 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 ...
0
votes
0answers
139 views

Coq: default values for vectors

Let's say there is a vector of length $n$: Require Import Vector. Variable T:Type. Variable n:nat. Variable v:t T n. "list" gives a function "nth" that demands a ...
4
votes
2answers
313 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
vote
0answers
90 views

Representing inductive types

I implemented dependently typed lambda calculus in the spirit of this article: http://www.andres-loeh.de/LambdaPi/LambdaPi.pdf The calculus, works and I experimented with it and like it. However, I ...