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
12
votes
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 ...
7
votes
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 ...
6
votes
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 ...
3
votes
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 ...
2
votes
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)
2
votes
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 ...
2
votes
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 ...
1
vote
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 ...
1
vote
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: ...
1
vote
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 ...
0
votes
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 ...