# All Questions

**19**

votes

**2**answers

1104 views

### Difference between type parameters and indices?

I am new to dependent types and am confused about the difference between the two. It seems people usually say a type is parameterized by another type and indexed by some value. But isn't there no dist...

**11**

votes

**4**answers

4758 views

### coqide - can't load modules from same folder

I can't load modules that are in same folder in CoqIde.
I'm trying to load sources from Software Foundations, I'm running coqide in folder that contains SF sources with coqide or coqide ./, then afte...

**8**

votes

**1**answers

548 views

### How or is that possible to prove or falsify `forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.` in Coq?

I want to prove or falsify forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q. in Coq. Here is my approach.
Inductive True2 : Prop :=
| One : True2
| Two : True2.
Lemma True_has_one : ...

**5**

votes

**1**answers

293 views

### Why are logical connectives and booleans separate in Coq?

I come from a JavaScript/Ruby programming background and am used to this being how true/false works (in JS):
!true
// false
!false
// true
Then you can use those true/false values with && l...

**5**

votes

**2**answers

457 views

### How to install SSReflect and MathComp in Linux?

I have successfully installed Coq 8.6 and CoqIDE in Linux (Ubuntu 17.04). However, I don't know to proceed in order to add SSReflect and MathComp to this installation. All the references that I have c...

**3**

votes

**1**answers

275 views

### Structural recursion on a dependent parameter

I'm trying to write the sieve of Eratosthenes in Coq. I have a function crossout : forall {n:nat}, vector bool n -> nat -> vector bool n. When the sieve finds a number that is prime, it uses cro...

**41**

votes

**3**answers

4296 views

### What are the strengths and weaknesses of the Isabelle proof assistant compared to Coq?

Does Isabelle/HOL proof assistant have any weaknesses and strengths compared to Coq?

**7**

votes

**1**answers

191 views

### Is there a minimal complete set of tactics in Coq?

I have seen a lot of Coq tactics that are overlapping each other in function.
For example, when you have the exact conclusion in the hypothesis, you can use assumption, apply, exact, trivial, and ma...

**5**

votes

**3**answers

279 views

### Nested recursion and `Program Fixpoint` or `Function`

I’d like to define the following function using Program Fixpoint or Function in Coq:
Require Import Coq.Lists.List.
Import ListNotations.
Require Import Coq.Program.Wf.
Require Import Recdef.
Indu...

**5**

votes

**1**answers

871 views

### Why Coq doesn't allow inversion, destruct, etc. when the goal is a Type?

When refineing a program, I tried to end proof by inversion on a False hypothesis when the goal was a Type. Here is a reduced version of the proof I tried to do.
Lemma strange1: forall T:Type, 0>0...