# Questions tagged [coq]

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

11 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
0answers
216 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 ...
0answers
553 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 ...
0answers
600 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 ...
0answers
77 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 ...
0answers
49 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)
0answers
48 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 ...
0answers
28 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 ...
0answers
50 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 ...
0answers
39 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: ...
0answers
96 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 ...
0answers
145 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 ...