All Questions
Tagged with coq type-theory
24
questions
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
1
answer
58
views
How to prove Theorem euclid_gcd : forall a b z, euclid a b z -> gcd a b z. using coq?
I am trying to prove euclid_gcd Theorem but Im getting stuck at the second case of the induction. most of the time I'm getting unify errors.
I will be glad for some help please.
Require Import Arith....
- 31
1
vote
2
answers
134
views
Is there a library for sets that works with bool in Coq?
I am looking to work with mathematical sets and subsets of some universal type.
I know this is normally represented as U -> Prop, such as in the Ensembles library.
I was wondering if there is ...
2
votes
1
answer
338
views
Agda: Failed to solve the following constraints: P x <= _X_53 (blocked on _X_53)
I'm writing Agda code as I read the HoTT book. I'm stuck on Lemma 2.3.9:
data _≡_ {X : Set} : X -> X -> Set where
refl : {x : X} -> x ≡ x
infix 4 _≡_
-- Lemma 2.1.2
_·_ : {A : Set} {x y z ...
1
vote
1
answer
68
views
Why coq doesn't use subtyping for logical or?
By subtyping, here I mean implicit coercion between types, not sig.
In programming languages, sum types have associated data and it matters which variant is being used, so e.g. A can not be a subtype ...
- 491
2
votes
2
answers
1k
views
Proof by contradiction in Coq
I am trying to understand the apparent paradox of the logical framework of theorem provers like Coq not including LEM yet also being able to construct proofs by contradiction. Specifically the ...
- 21
2
votes
1
answer
165
views
Can I prove "coinductive principles" about coinductive type?
Can I prove "coinductive principles" about coinductive type? For example, the pseudo code of the coinductive principle for the stream type would look like this:
Π P : Stream A -> Type.
Π ...
- 410
3
votes
1
answer
354
views
Can any additional axiom make Coq Turing complete?
Here I mean axiom as what we can define with the Axiom keyword in Coq Gallina, not with such command-line argument passing to Coq.
I know some axioms make Coq inconsistent. However, AFAIK they don't ...
- 787
3
votes
1
answer
392
views
How to prove that "Type <> Set" (i.e. Type is not equal to Set) in Coq?
Is there an equality or inequality relation between Type and Set in Coq ?
I am learning about Coq's type system and understand that the type of Set is Type@{Set+1}, and that the type of Type@{k} is ...
- 33
80
votes
1
answer
2k
views
Why is my definition not allowed because of strict positivity?
I have the following two definitions that result in two different error messages.
The first definition is declined because of strict positivity and the second one because of a universe inconsistency.
(...
- 1,480
1
vote
2
answers
59
views
Why does coq's typechecker reject my map definition?
I try to experiment with list's definition.
For example let's see this definition:
Inductive list1 : Type -> Type := nil1 : forall (A : Type), list1 A
| cons1 : ...
- 39
1
vote
2
answers
175
views
Representing Functions as Types
A function can be a highly nested structure:
function a(x) {
return b(c(x), d(e(f(x), g())))
}
First, wondering if a function has an instance. That is, the evaluation of the function being the ...
- 77.9k
4
votes
2
answers
141
views
Equality in Coq and in a paper of Awodey
In the paper
Univalence as a Principle of Logic, Awodey writes on page 7:
Let us consider the example of intensional versus extensional type theory. The extensional theory has an apparently “...
- 1,216
3
votes
1
answer
222
views
Is Z.le as defined in the standard library proof irrelevant?
In the Coq standard library, there is an enumerated type called comparison with three elements Eq,Lt,Gt. This is used to define the less-than or less-than-or-equal operators in ZArith: m < n is ...
- 423
7
votes
1
answer
182
views
Is there a type theory in which the equivalence of identically shaped inductive datatypes is representable?
Say I have two inductively defined datatypes:
Inductive list1 (A : Type) : Type :=
| nil1 : list1 A
| cons1 : A -> list1 A -> list1 A.
and
Inductive list2 (A : Type) : Type :=
| nil2 : ...
- 4,382