All Questions

19
votes
2answers
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
4answers
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
1answers
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
1answers
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
2answers
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
1answers
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
3answers
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
1answers
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
3answers
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
1answers
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...

Previous Next