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
282 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 ...
Jannis Limperg's user avatar
8 votes
0 answers
655 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 ...
KarenS's user avatar
  • 81
6 votes
0 answers
707 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 ...
Jake's user avatar
  • 3,810
3 votes
0 answers
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 ...
CuriousKid7's user avatar
2 votes
0 answers
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 ...
user1868607's user avatar
  • 2,194
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 ...
Maciej Poleski's user avatar
1 vote
0 answers
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 ...
user3565552's user avatar
1 vote
0 answers
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: ...
Sajuuk's user avatar
  • 155
1 vote
0 answers
104 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 ...
Konstantin Solomatov's user avatar
0 votes
0 answers
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 ...
arshiamoeini's user avatar
0 votes
0 answers
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: ...
Chloe's user avatar
  • 1
0 votes
0 answers
172 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 ...
user7358's user avatar
  • 101