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,949
questions
0
votes
0
answers
7
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
37
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,355
0
votes
3
answers
36
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
50
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
39
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,091
0
votes
3
answers
65
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
26
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
41
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
54
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
60
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