Share Your Experience: Take the 2024 Developer Survey

# Questions tagged [coq]

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

66 questions
Filter by
Sorted by
Tagged with
52 views

### formalization of partial function for counting

I need assistance in defining axioms for partial functions in total function theory that is available in Coq. Specifically, I'm looking for a constructive definition of a partial function that ...
53 views

### Defining 2 inductive propositions relying on each other in Coq

I'm pretty beginner in Coq. I want to formalize negative and positive occurrence of an atom in a proposition inside coq the definition is as down below: I want to define this property as an Inductive ...
299 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, ...
391 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
63 views

### Coq stuck on proof for Theorem eqblist_true

I'm stuck on this proof for the theorem eqblist_true. So far what I have is: ...
1 vote
75 views

### How do program types such as natural numbers figure into the Curry-Howard Isomorphism?

In Coq, the nat, the type of natural numbers, has type Set. By the Curry-Howard Isomorphism, all propositions of type ...
120 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 ...
1 vote
59 views

### Why discriminate the base case allows me to complete the induction proof?

I have a successful completed proof which used induction. but I essentially proved the goal on the base case by tactic discriminate. Why is this induction proof ...
• 155
1 vote
195 views

### Is there a tactic to help resolving existential quantifiers in Coq?

I am working on Software Foundations Volume 1 on my own it is its 2019 version by the way, and I have reached to its lesson Inductively Defined Propositions, and there, for almost one month I have ...
• 25
1 vote
51 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: ...
• 155
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
75 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 ...
• 2,194
1 vote
59 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 ...
• 113
247 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
1 vote
109 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 ...
33 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 ...
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
197 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 ...
187 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
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
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
326 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
590 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
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: ...
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