All Questions
Tagged with coq dependent-type
127
questions
-4
votes
1
answer
335
views
Can a dependently typed language be Turing complete? [closed]
It seems as though dependently typed languages are often not Turing complete. Why can we not allow every function to have general recursion (which would make the language Turing complete), instead of ...
0
votes
2
answers
97
views
Eliminating impossible branches in Coq dependent pattern matching
I'm having troubles with understanding pattern matching on dependent types. Let's say we have following code:
Variant Op := op1 | op2.
Variant Res : Op -> Set :=
| r1 : Res op1
| r2 : Res op2
| rb ...
0
votes
1
answer
39
views
Dependent equality with 2 different type functions
How do you work with dependent types where the function making the type differs?
I'm working on a problem where I have 2 dependent types where the
types are indexed in different ways. I want to show ...
- 419
1
vote
1
answer
43
views
List without gaps in Coq
How to define list of natural numbers without gaps in Coq?
For example [2, 1, 3] is valid list, but [5, 1, 3] is not because it have two gaps: between 1 and 3, 3 and 5.
I have try to ask Google, but ...
- 313
0
votes
2
answers
62
views
Programming in the Calculus of Inductive Constructions with Coq
Sometimes I want to write programs close to bare-bone CIC (Calculus of Inductive Constructions) to get a better grasp of the internal workings.
I then need to customize some settings to change the ...
- 157
1
vote
1
answer
100
views
Is Prop a subtype of Set?
I am surprised to see the following behavior:
Check ((True : Prop) : Set).
=============================================
(True : Prop) : Set
: Set
It however does not work the other way around:...
- 6,859
2
votes
2
answers
152
views
What's the role of unification in Coq's core type system?
When type checking proof terms, how does unification come into play after elaboration to the core language of Calculus of Inductive Constructions?
Specifically, when dealing with properties of ...
- 157
3
votes
1
answer
68
views
Why the `Let-in` construct cannot be defined as a derived form in a dependently-typed language?
In the "Typing rules" section of the coq reference manual, a note says "We may have 𝗅𝖾𝗍 𝑥:=𝑡:𝑇 𝗂𝗇 𝑢 well-typed without having ((λ𝑥:𝑇. 𝑢) 𝑡) well-typed (where 𝑇 is a type ...
- 157
0
votes
1
answer
81
views
Morphism signature for dependently-typed vectors in coq
I want to be able to rewrite terms inside the predicate P given to Coq.Vectors.Vector.Forall.
The first attempt does not work due to the missing quantification over n.
From Coq Require Import Vector ...
- 269
0
votes
1
answer
63
views
Coq: Unification fails with record
Here is a small instance of my problem:
Record ord : Type := mk_ord
{ tord: Type;
ole: tord -> tord -> Prop;
}.
Definition onat := mk_ord nat le.
Definition singl (O : ord) (e : tord O) : ...
- 269
1
vote
1
answer
45
views
How does one build the list of only true elements in Coq using dependent types?
I was going through the Coq book from the maths perspective. I was trying to define a dependently typed function that returned a length list with n trues depending on the number trues we want.
Coq ...
- 5,961
0
votes
1
answer
218
views
How does one define dependent type with named arguments in Coq without issues in unification in the constructors?
I want to defined a lenghted list but I like arguments with names at the top of the inductive definition. Whenever I try that I get unification errors with things I hoped worked and was forced to do a ...
- 5,961
4
votes
1
answer
340
views
Coq: trying to use dependent induction
I have the following definitions for type precision:
Require Import Coq.Program.Equality.
Inductive type : Set :=
| TInt
| TFun: type -> type -> type
| TStar
.
Reserved Infix "<|" ...
3
votes
1
answer
91
views
Relations with dependent types in Coq
I want to define a relation over two type families in Coq and have come up with the following definition dep_rel and the identity relation dep_rel_id:
Require Import Coq.Logic.JMeq.
Require Import Coq....
- 63
4
votes
2
answers
105
views
Difference between parameters and members of a class
I am new to Coq and was wondering what is the difference between the following things:
Class test (f g: nat -> nat) := {
init: f 0 = 0 /\ g 0 = 0;
output: ...another proposition about f and g....
- 149