Questions tagged [coq]
Coq is a formal proof management system, semi-interactive theorem prover and functional programming language. Coq is used for software verification, the formalization of programming languages, the formalization of mathematical theorems, teaching, and more. Due to the interactive nature of Coq, we recommend questions to link to executable examples at https://x80.org/collacoq/ if deemed appropriate.
2,953
questions
1
vote
1
answer
62
views
Coq can't define an inductive proposition
My Coq compiler is not allowing for inductive propositions as:
Inductive relation : nat -> nat -> Prop :=
| A : relation 1 2
| B : relation 2 3.
Throws: Error: The reference B was not found ...
- 305
0
votes
1
answer
53
views
Coq Decreasing Argument mapping
I have a graph defined as follows.
Definition ldd_state : Type := gmap loc (nat * (loc * loc)).
This is a mapping from a loc (positive) to a value nat, and two children. Every node "lives" ...
0
votes
1
answer
36
views
The `specialize` tatic in Coq does not work well with typeclasses?
I have a simple question about using the specialize tactic in Coq for typeclass-based code. Specifically, I am using stdpp and I have a type lcmm_memory that is defined to be gmap nat lcmm_val.
Why ...
- 7,371
0
votes
2
answers
84
views
Multiple Assignements in a Coq Map to the same value
I'm given the following definition of com that sssigns new values to more than one variable in a single command.:
Inductive com : Type :=
| CSkip
| CAsgn (xs : list string) (es : list aexp) (* <...
1
vote
1
answer
68
views
Decider for lists In Fixpoint
I am relatively new to coq and i am not sure how to procede here.
I want to write a decidability function for the In Fixpoint of the list library like this:
Program Fixpoint InDec (s : K) (l : list K) ...
- 75
2
votes
0
answers
171
views
VSCoq Error: Connection to server got closed. Server will not be restarted
I am using VSCoq with Ubuntu and WSL for a Formal Methods class I am taking this semester. I had it working fine (a trial in and of itself), but am all of a sudden receiving the following errors:
[...
- 21
1
vote
1
answer
68
views
How do I move a let variable to a separate hypothesis?
In Coq, as a simplified example (using False to ignore the conclusion),
Theorem example
(f : nat -> bool)
(g : bool -> bool -> bool)
(cmplx :=
let a := f 0 in
let b := ...
- 419
0
votes
1
answer
41
views
Coq inductive not right form
I have troubles with a not well formed IH (or I am making mistakes).
From stdpp Require Import mapset.
From stdpp Require Import gmap.
From stdpp Require Import options.
From stdpp Require Import ...
0
votes
3
answers
101
views
How can I handle this `false = true` case?
I am trying to prove the following lemma.
Inductive bool : Type :=
| true
| false.
Lemma andb_true_iff : forall b1 b2 : bool,
b1 && b2 = true <-> b1 = true /\ b2 = true.
Proof.
...
- 2,695
0
votes
1
answer
41
views
Why can't I destruct or discriminate here?
I am proving the following theorem.
Definition excluded_middle := forall P : Prop,
P \/ ~ P.
Theorem not_exists_dist :
excluded_middle ->
forall (X:Type) (P : X -> Prop),
~ (exists x, ...
- 2,695
0
votes
1
answer
37
views
Why I can't use exact P if P is a Prop?
I am trying to prove contraposition. And my proof is like the following. It doesn't work.
Theorem contrapositive : forall (P Q : Prop),
(P -> Q) -> (~Q -> ~P).
Proof.
intros.
destruct ...
- 2,695
0
votes
1
answer
63
views
Why can't I perform rewrite tactic here?
I have already a theorem
Theorem plus_id_example : forall n m:nat,
n = m ->
n + n = m + m.
and I want to prove its "reverse form". So I have
Theorem plus_n_n_injective : forall n m,
...
- 2,695
0
votes
1
answer
33
views
Why we can't use "simpl" on `j = j -> x = y`?
I am trying to solve the injection_ex3 exercise in Software Foundation Volume 1.
I have the following prove
Example injection_ex3 : forall (X : Type) (x y z : X) (l j : list X),
x :: y :: l = z :: j ...
- 2,695
0
votes
1
answer
81
views
Coq Decision Diagram Multivalued Function
I am trying to accomplish something but am stuck.
To begin with, my work is based on a List Decision Diagram. This represents a multi-valued input binary output function.
Here, assume we have natural ...
1
vote
1
answer
71
views
Coq : Using a parametrized Type from within a Module
I'm trying to use Modules in my project and I made this small example to show what I'm struggling with.
Module Type A.
Parameter t : Type.
End A.
Module a : A.
Definition t := nat.
End a.
Module ...
- 305