# All Questions

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...
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...
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 : ...
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...
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...
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...
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?
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...