Questions tagged [coq]
Coq is an interactive theorem prover.
62
questions
3
votes
3
answers
110
views
Formalization of matching logic (logic behind K Framework)
Is there any mechanization for matching logic (any flavor)?
I only find study about K Framework rules to Deducti translation, but this is both not covering to matching logic and not internalizing the ...
- 295
-1
votes
1
answer
83
views
Notation problem
The following problem arises when I try to define a new notation. I have a function
f : A -> A -> A -> A -> Type
Then I want special notation for the ...
1
vote
1
answer
76
views
Can I define nested mutually dependent types in Coq?
I am trying to model the following in Coq, which works fine in Haskell (below is Haskell code):
...
- 13
8
votes
3
answers
1k
views
Yet another constructive (Coq) proof that `nat -> nat -> nat` is not bijective. How to explain it to myself?
Here is a Coq proof I've came up with:
...
- 212
0
votes
1
answer
86
views
A Coq question : How to prove the image of the two same valued variables under a function are same?
I want to prove the following Coq theorem.
However, I couldn't proceed.
Please, give me an advice if possible.
Thank you.
Require Import QArith.
Variable f : Q -> Q.
Theorem function (x y : Q) :
x ...
- 111
1
vote
1
answer
207
views
Defining functions on non-inductive types using LEM in Coq
I'm trying to prove statements about homomorphisms in Coq. Specifically, about in which cases the existence of some set of homomorphisms implies the existence of a specific other homomorphism. I'm ...
- 11
3
votes
2
answers
448
views
How does axiom K contradict univalence?
I have seen it claimed several times that axiom K is inconsistent with univalence (e.g. here and here), but I have never seen a proof sketch. Specifically, I'm curious about how this manifests in the ...
2
votes
1
answer
172
views
Dependent eliminator for empty type in intensional Martin-Löf type theory
In calculus of inductive constructions you can just say that the empty type is the type with no constructors and it automatically builds the dependent eliminator.
But let's say I'm setting up ...
user61651
6
votes
1
answer
505
views
Defining inductive types in intensional type theory purely in terms of type-theoretic data
To define a (non-indexed) W-type all we need is a type $A:U$ and a function $B:A\to U$ and we get a type $W_{a:A}B(a)$. To check that this definition is valid we only need to check that the ...
user61651
6
votes
1
answer
556
views
Impredicativity + large eliminations (with no excluded middle) in Coq
It is known that impredicativity + large eliminations + excluded middle is inconsistent. Prop is impredicative and consistent with excluded middle, but does not ...
- 117
0
votes
0
answers
84
views
What do we call a type system where any term of any type ultimately parses down to $*:\mathbf{1}$?
If a type system allows inductive types (as in e.g. Coq) then we can coin new primitive constants that inhabit types. For example $0:\mathbb{N}$ is constructed when defining $\mathbb{N}$ and does not ...
- 11
2
votes
1
answer
351
views
Defining finite sets inductively in a proof assistant?
To represent finite sets within coq, we either use something like ListSet, which are just definitions on top of list, or we ...
- 595
1
vote
0
answers
81
views
Journals or conferences to submit formally verified libraries?
This is a soft question aimed at understanding whether there is any value to publishing formally verified libraries. I have formally verified (in Coq) implementations of:
synthetic differential ...
- 595
5
votes
0
answers
179
views
On the interpretation of coinduction in type theory
The notion of (co)datatype can be modeled satisfactorily in category theory as fixed-points of polynomial functors. Then, (co)induction principles are derived from initial algebras/terminal ...
- 921
3
votes
0
answers
129
views
Have the proofs in Buss's "On Goedel’s Theorems on Lengths of Proofs" been formalized (mechanically checked)?
The paper On Gödel's theorems on lengths of proofs I: Number of lines and speedup for arithmetics contains quite interesting results on proof length. But some of the details are still, to me, a bit ...
- 1,530
2
votes
1
answer
161
views
Lack of atomic propositions in the Calculus of Constructions from ATTAPL textbook
I am working through the Dependent Types chapter from Advanced Topics in Types and Programming Languages (ATTAPL) by Benjamin Pierce et al. I am confused with the calculus presented Fig 2-7 (Calculus ...
- 31
0
votes
0
answers
94
views
Proposition terms vs types in Coq
Consider the following div function written in Coq. It takes in a proof that the divider is non-zero.
Definition div (n d:nat) (pf: ~(d = 0)) := n/d.
Focus on <...
- 31
9
votes
0
answers
301
views
Model of Coq (pCuIC) in higher toposes?
Can the type theory of Coq (pCuIC) be modeled in all higher Grothendieck toposes?
First of all, even the set theoretical model is not complete (e.g. inductive types in Prop). Although, this is ...
- 195
2
votes
2
answers
326
views
Representations of Planar Graphs in Coq
I would like to formalize some simple properties of planar graphs in the Coq proof assistant.
1) How are planar graphs formalized in the Coq proof assistant? Is there a "standard" definition that is ...
- 616
8
votes
0
answers
617
views
An axiom for John Major's Equality
In the the standard library of Coq, there is the axiom:
Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y.
Why isn't it provable? Can it be reduced ...
- 381
3
votes
1
answer
355
views
Universe polymorphism: the inference of universes and their constraints
When making a universe polymorphic definition in Coq, universes and their constraints are automatically inferred. Are they somewhat the most general ones (in a sense similar to the principal type ...
- 381
1
vote
0
answers
334
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:
<...
- 1,177
2
votes
1
answer
477
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?
- 1,177
9
votes
2
answers
314
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 ...
- 618
9
votes
2
answers
2k
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 + ...
- 201
13
votes
3
answers
1k
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 ...
- 249
14
votes
2
answers
1k
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 ...
- 631
3
votes
0
answers
142
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$?
8
votes
1
answer
542
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 ...
- 255
2
votes
1
answer
730
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 ...
- 123
4
votes
1
answer
471
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 ...
- 41
1
vote
1
answer
790
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 q ...
- 777
4
votes
0
answers
127
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 ...
- 523
0
votes
1
answer
189
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 ...
- 159
3
votes
0
answers
179
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:
...
- 31
5
votes
3
answers
1k
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 ...
- 1,762
9
votes
1
answer
920
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 ...
- 93
20
votes
2
answers
951
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, ...
- 303
0
votes
1
answer
1k
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
2
answers
352
views
How to prove that a circular prop is uninhabited?
Consider the following inductive definition of "ElProp" in coq:
...
- 145
40
votes
4
answers
7k
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, ...
- 1,762
25
votes
2
answers
3k
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-...
- 471
6
votes
1
answer
808
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)
...
- 161
4
votes
1
answer
2k
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 ...
- 49
5
votes
1
answer
299
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 ...
- 51
-2
votes
1
answer
264
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.
...
- 33
2
votes
0
answers
388
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:
<...
- 33
-2
votes
1
answer
593
views
Coq definition with unusual syntax (Definition ... Defined.)
While examining the package Library ZFC.Sets, I found the following definition:
...
- 107
16
votes
2
answers
834
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?
- 169
25
votes
1
answer
2k
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?)
- 251