Questions tagged [coq]
Coq is an interactive theorem prover based on the Calculus of Inductive Constructions.
67
questions
0
votes
0
answers
45
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 ...
0
votes
1
answer
42
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 ...
3
votes
1
answer
226
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, ...
4
votes
3
answers
267
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 ...
- 2,960
0
votes
0
answers
53
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
1
vote
0
answers
73
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 ...
- 31
2
votes
1
answer
98
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 ...
- 31
1
vote
1
answer
58
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
2
answers
159
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
0
answers
50
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
3
votes
1
answer
46
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
2
votes
0
answers
59
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,240
2
votes
0
answers
67
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,240
1
vote
1
answer
56
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
2
votes
1
answer
139
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
1
answer
102
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
0
answers
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 ...
3
votes
1
answer
209
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
-1
votes
1
answer
175
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 ...
- 1
5
votes
1
answer
163
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
11
votes
1
answer
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
3
votes
1
answer
230
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
5
votes
1
answer
287
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
4
votes
4
answers
475
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:
...
- 2,960
5
votes
1
answer
560
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:
...
- 245
3
votes
0
answers
132
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
2
votes
1
answer
156
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
2
votes
2
answers
226
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
1
answer
406
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 ...
- 475
0
votes
1
answer
195
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" ...
- 2,163
4
votes
1
answer
93
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
1
answer
272
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
14
votes
1
answer
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 ...
- 243
4
votes
1
answer
268
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
2
votes
1
answer
246
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?
...
- 612
8
votes
1
answer
543
views
What does instantiating existential variables with out of scope variable imply?
I have following unfinished proof of a lemma:
...
- 612
16
votes
1
answer
4k
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:
...
- 271
22
votes
1
answer
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 ...
- 499
1
vote
1
answer
580
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:
...
- 25
3
votes
2
answers
534
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
3
votes
1
answer
419
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 ...
- 388
10
votes
1
answer
342
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
13
votes
2
answers
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
12
votes
0
answers
275
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 ...
- 241
5
votes
2
answers
522
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 ...
- 151
1
vote
2
answers
118
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
...
- 111
7
votes
2
answers
210
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
6
votes
0
answers
685
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,790
7
votes
0
answers
625
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 ...
- 71
5
votes
2
answers
432
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,790