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
0
votes
0
answers
7
views
The uniform inheritance condition of coercions to dependent types in Coq
I'm encoding a HOAS in Coq, but my coercions are not working well.
Here is a MWE:
From Coq Require Import ZArith String.
Variant tag := A | B.
Variant const := Unit | Int : Z -> const.
Inductive ...
- 1,854
0
votes
0
answers
14
views
Try to understand SSReflect's "have" and square bracket
I tried to understand square braket patterns I have seen in different proofs. So I followed the SSReflect example, and tried serveral patterns:
Lemma test : True.
Proof.
have : exists v : nat, v > ...
- 1
0
votes
2
answers
35
views
Lightweight ways to prove an assembly language steps from a certain state to another state after variable number of instructions in Coq
I want to prove that a compiler that I wrote for a toy language is correct. I defined a predicate P which relates the runtime configuration of the source toy language and the target toy assembly.
The ...
- 79
0
votes
0
answers
39
views
How can I solve the "term type wrong" errror in coq?
I am building up a system which contains both Family of sets and function, and I'm facing lots of errors that goes:
"The term "_" has type "_" while it is expected to have ...
- 1
0
votes
1
answer
71
views
Install coq proof assistant from source - switch package not determined
On an M1 Mac under macOS Sonoma 14.5, I'm trying to install from source coq version 2023.11.0. At the step of "create opam switch", I get following error:
[CP.2023.11.0.patch_ocaml] ...
- 777
1
vote
1
answer
45
views
Tac to derive contradiction from circular equality (ie. smarter to discriminate)
Inductive Foo : Type :=
| foo : Foo
| bar : Foo -> Foo.
Lemma Foo_contr f:
bar f = f -> False.
Proof.
intros H.
induction f as [|f IH].
- discriminate.
- injection H.
apply IH....
- 4,375
0
votes
3
answers
38
views
Coq repeating "destruct" for disjunctive hypothesis causing unwanted destruction in the end
I need to prove a theorem involving 2 variables a and b, a hypothesis H specifying the possible values of a (a = v1 \/ a = v2 \/ ... \/ a = vn), and a hypothesis H0 specifying values of b (b = v1' \/ ...
- 79
0
votes
1
answer
51
views
How to make OCaml (or Coq) code from the llvmir code using vellvm framework
I'm studying vellvm framework.
How can I verify simple function on C with vellvm?
I know that I can use assertions inside .ll code
; ASSERT EQ: i32 0 = call i32 @foo(i32 0)
but I want more
This is the ...
0
votes
0
answers
40
views
How to apply simple lemma with complex instantiation in Coq?
I have a goal that looks like (A <-> B) -> ~A with complex expressions A and B, and I want my goal to become ~B.
I tried creating a simple Lemma that (A <-> B) -> ~A -> ~B
Section ...
- 8,101
0
votes
3
answers
68
views
Induction on Inductive Type Without Base Case in Coq
I'm trying to understand why a particular proof in Coq works. Here is the inductive type definition and the theorem I'm trying to prove:
Inductive my_s : Type :=
| loop (s : my_s).
Theorem p_of_s : ...
- 176
0
votes
2
answers
47
views
Functional Extensionality for Propositional Functions
I've created the following simple definitions for representing sets of objects of type X as functions X -> Prop and defined various operations such as cup (union). However, before I get started ...
- 2,811
0
votes
0
answers
26
views
Coq dictionary implementations supporting custom key domain that are easy to prove equivalence?
I need to implement a dictionary type in Coq, whose keys need to be from an inductive type defined by myself, and I need to make it easy to prove equivalence between dictionaries. What are some good ...
- 79
0
votes
0
answers
27
views
Applying lemma using Vectors in Coq
I have proved the following
Lemma exists_distribution:
forall (a:Prop)(Omega:Set)(p:Omega->Prop),
(exists x:Omega, p x->a)<->
((exists x:Omega,~(p x))\/(exists x:Omega,a)).
Now I would ...
- 21
0
votes
0
answers
45
views
Frama-C with Coq interactive prover
I am trying to run Frama-C on a small code sample.
It works pretty well:
# frama-c -wp bubble_sort.c
[kernel] Parsing bubble_sort.c (with preprocessing)
[wp] Warning: Missing RTE guards
[...
1
vote
1
answer
59
views
How to use lambda functions in COQ
I'm struggling with the basic syntax and I'm going to need to see some examples. I get the impression that I need to declare a polymorphic type param.
Notation "'λ' x .. y , t" := (fun x =&...
1
vote
0
answers
40
views
How to match implication without prior intros?
I am trying to write a tactic to check if my goal is an implication without having to introduce anything beforehand.
Furthermore I would like this tactic to be compatible with any amount of variables ...
- 21
2
votes
2
answers
64
views
Is there a lightweight way to define a mutable dictionary that can return all of its keys in Coq?
I want to define a mutable dictionary that can return all of its keys in its domain. Keys don't have to be ordered. I searched in the coq library doc on the internet and didn't seem to find anything ...
- 79
1
vote
1
answer
72
views
Constructing proof terms inside a recursive function
Just starting with Coq, trying to write a list insertion function that will return either the new list, or if the provided index was illegal, a proof thereof using sumor. I'm fine with the recursion, ...
- 117
1
vote
1
answer
49
views
Coq notation defined inside a module expecting type without module prefix
I'm writing a compiler and its proof for a toy language, and I have files L1, L2, C, and P, where L1 and L2 contain the abstract syntax and operational semantics of languages l1 and l2, C containing ...
- 79
0
votes
2
answers
72
views
How can I prove that theorem in coq: (x | a) -> (x | b) -> x <= (gcd a b)?
I have this realization of greatest common divisor:
Fixpoint gcd_ (m n d : nat) : nat :=
match d with
| 0 => if (m =? 0) then n else m
| S k => if (m mod S k =? 0) && (n mod S k =? 0) ...
0
votes
1
answer
58
views
Beta-reduction after delta-reduction in unfold tactic
According to the coq manual, the unfold tactic performs delta reduction on a definition, followed by several other reductions, including beta-reduction.
It seems that sometimes, to trigger beta-...
- 97
-4
votes
1
answer
335
views
Can a dependently typed language be Turing complete? [closed]
It seems as though dependently typed languages are often not Turing complete. Why can we not allow every function to have general recursion (which would make the language Turing complete), instead of ...
0
votes
2
answers
40
views
Convert list to vector in coq
I'm pretty new to using coq and I'm a bit confused about vectors. I want to convert a list into a vector with the same content. I'm trying pattern matching, but it keeps throwing errors about the ...
- 113
0
votes
1
answer
55
views
Defining mutually recursive types in Coq?
Suppose I have types A,B,C,D,E,F. One of the constructors of A takes an argument with type F; a constructor of B requires A, a constructor of D requires arguments of types C and A, E requires D and F ...
- 79
1
vote
1
answer
39
views
How to mix sections with hints in Coq?
I am writing something heavily involving typeclasses and I would like to utilize hints to ease proving local lemmas as well as exported theorems.
For instance, consider
Class MyClass (A : Type) :=
...
- 6,859
0
votes
3
answers
87
views
Lemma about a graph in Coq
I need to prove a Lemma in Coq, about a connected graph with certain properties:
the vertices of the graph are of type V:Type, and there is a function f: V -> nat which associates a natural number ...
- 97
0
votes
1
answer
117
views
Error: Cannot find a physical path bound to logical path Strands. in coq
I have coq file and was working on it for days but now the file giving me following error:
Error: Cannot find a physical path bound to logical path Strands.
also the required packages are as under:
...
- 11
-1
votes
2
answers
92
views
How to prove that forall n m, n <= m -> m <= n -> n = m
Theorem le_trans: forall n m o, n <= m -> m <= o -> n <= o.
Proof.
intros n m o Lnm Lmo.
generalize dependent Lnm.
generalize dependent n.
induction Lmo.
- intros. apply Lnm.
- ...
0
votes
1
answer
72
views
Is there an intuitionistic proof of `(A -> B \/ C) -> (A -> B) \/ (A -> C)`?
Following is a useful lemma in classical propositional logic.
(A -> B \/ C) <-> (A -> B) \/ (A -> C).
The backward direction is easily proved. But I could not find an intuitionistic ...
0
votes
2
answers
97
views
Eliminating impossible branches in Coq dependent pattern matching
I'm having troubles with understanding pattern matching on dependent types. Let's say we have following code:
Variant Op := op1 | op2.
Variant Res : Op -> Set :=
| r1 : Res op1
| r2 : Res op2
| rb ...
0
votes
1
answer
35
views
How to use coq to prove this firstn and nth question?
Theorem fiset_ref_fact : forall (r r' n : nat) (f f' D g g' h h' : list nat) (b b' : bool),
length f = n /\ n > 0 /\ r < n /\
h = firstn r f /\
h' = (app h ((nth r f 0)::nil)) /\ r' = r + ...
- 1
1
vote
1
answer
40
views
InteractionTrees library - simple program on ASM
I am trying to write simple program on ASM (a simple control-flow-graph language) from this tutorial:
InteractionTrees -> ASM.v
My final goal is to prove its correctness, using the library's ...
1
vote
1
answer
80
views
Installing Coq on Windows on GitHub Actions succeeds on a repo, and fails on another repo
I'm trying to install Coq on Windows on GitHub Actions, but seeing strange results.
I tried the following script, but couldn't install Coq because of the missing gmp.h error.
name: CI
on:
push:
...
- 874
0
votes
1
answer
45
views
How to instruct `auto` to simplify the goal during proof search?
A minimal example of my issue looks as follows:
Goal let x := True in x.
This is immediately solved by simpl. auto., but auto. does not work.
In my actual case, the search tree is a bit bigger than ...
- 6,859
0
votes
0
answers
54
views
Inductive from CoInductive?
It is possible to represent CoInductive using parts that are Inductive.
As a simple example,
CoInductive stream A :=
| SCons : A -> stream A -> stream A
.
Arguments SCons {A}.
CoInductive ...
- 419
0
votes
1
answer
61
views
Is is possible to rename a coq term?
Sorry, I'm not sure if the title is the adequate question.
I have been going through Logical Foundations. In the Lemma "double_plus" i solved it with this solution:
Lemma double_plus : ...
- 71
1
vote
1
answer
46
views
Coq : mutually recursive definitions with [mrec] in InteractionTrees Library
I'm studying this great library for Representing Recursive and Impure Programs in Coq
I am having problems with mutual recursion (very first example in documentation gives me an error)
https://...
0
votes
2
answers
87
views
Is there a function that returns a list of values with specific type in OCaml?
In Haskell, using listify with Data can extract values of a specific type from a deeply nested structure without lots of getters. For example, with the following code:
{-# LANGUAGE DeriveDataTypeable #...
- 874
2
votes
1
answer
85
views
How to prove (X !-> 3) =[ <{ X := X + 2 }> ]=> (X !-> 5)?
I know how to prove 3 + 2 = 5 using Imp, defined in Software Foundations, Volume 1.
Definition plus2_3_is_5: Prop := forall (st: state),
(X !-> 3) =[ <{ X := X + 2 }> ]=> st -> st X = ...
1
vote
1
answer
52
views
Showing polynomial equality in coq/ssreflect
I am trying to prove equality of polynomials by explicit computation in coq. Here's an example showing where I get stuck:
From mathcomp Require Import all_ssreflect all_algebra.
Set Implicit ...
- 201
-1
votes
1
answer
44
views
Syntax of the case tactic in coq
Can someone explain to me what the following coq tactic is doing?
case x : fun H => [|[]] // _.
How would I rewrite this using destruct?
Even better, can anyone point me to somewhere in the coq ...
- 201
0
votes
0
answers
69
views
Why assuming singleton elimination and definitional proof irrelevance leads to UIP, in Coq?
I was reading the paper Definitional proof-irrelevance without K, which states, in page 3, that
If proof irrelevance holds for the equality type, every equality has at most one proof, which is known ...
1
vote
1
answer
43
views
Understanding nat_ind2 in Logical Foundations
As an alternative induction principle of nat, nat_ind2 is defined like so:
Definition nat_ind2 :
forall (P : nat -> Prop),
P 0 ->
P 1 ->
(forall n : nat, P n -> P (S(S n))) ->
...
- 205
0
votes
1
answer
58
views
What `dependent induction` tactic does in Coq and how to use it
Can you please provide me with high-level explanation on which usecases dependent induction / dependent destruct tactics have, and how they work (I would be grateful for explanation high-level enough ...
- 463
0
votes
2
answers
63
views
Split multiple conjuncts in the goal
Is there a tactic to split multiple conjuncts in a goal into subgoals?
If I have the goal P /\ Q /\ R, I want to split it to produce three subgoals at once:
P, Q, and R
I can't seem to find any info ...
- 205
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