Skip to main content
Share Your Experience: Take the 2024 Developer Survey

Questions tagged [coq]

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

12 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
12 votes
0 answers

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 ...
Jannis Limperg's user avatar
8 votes
0 answers

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 ...
KarenS's user avatar
  • 81
6 votes
0 answers

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 ...
Jake's user avatar
  • 3,810
3 votes
0 answers

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 ...
CuriousKid7's user avatar
2 votes
0 answers

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 ...
user1868607's user avatar
  • 2,194
2 votes
0 answers

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

If we remove subtyping ( from CIC we will lose some expressive power. But is that power necessary for a programming ...
Maciej Poleski's user avatar
1 vote
0 answers

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 ...
user3565552's user avatar
1 vote
0 answers

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: ...
Sajuuk's user avatar
  • 155
1 vote
0 answers

Representing inductive types

I implemented dependently typed lambda calculus in the spirit of this article: The calculus, works and I experimented with it and like it. However, I ...
Konstantin Solomatov's user avatar
0 votes
0 answers

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 ...
arshiamoeini's user avatar
0 votes
0 answers

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: ...
Chloe's user avatar
  • 1
0 votes
0 answers

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 ...
user7358's user avatar
  • 101