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
3
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
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
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 ...
0
votes
0
answers
38
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
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....
- 1,438
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 ...
- 78
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' \/ ...
- 1,378
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 : ...
3
votes
2
answers
366
views
Frama-C 23 and Coq
After installing Frama-C (23), Why3, and Coq on macOS I ran the command
rm -f ~/.why3.conf ; why3 config detect
The following message was shown
Found prover Coq version 8.10.2, but no Why3 libraries ...
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 ...
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 ...
- 136
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
[...
