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,952
questions
1
vote
1
answer
58
views
How do I apply (S n' <=? m) = true to S n' <= m? [closed]
Trying to complete a Coq proof but I ended up getting stuck on the last goal. I transformed the goal to S n' <= m and have a hypothesis (S n' <=? m) = true, but am unable to unify these.
I tried ...
- 15
0
votes
1
answer
201
views
Software Foundations (lf): proving leb_plus_exists and plus_leb_exists
I've been working through Volume 1 of Software Foundations, and I can't get past a pair of optional questions in Logic.v. Anyone have any idea what to do?
Theorem leb_plus_exists : forall n m, n <=?...
- 15
0
votes
1
answer
71
views
Coq/Ltac: is it possible to design a tactic that says the goal is proved when a decision procedure proves it, without the proof term?
I am designing a Coq tactic that calls a decision procedure, which answers yes/no, without giving a proof term. When I get yes, I would like to say Ltac that the goal is proved.
Is there a way to do ...
1
vote
1
answer
56
views
Proving some theorems on the function index in Coq
I’m trying to implement an index function in Coq. I’ve written this code:
Notation grid := (list nat).
Fixpoint index_aux (n : nat) (g : grid) (i : nat) : option nat :=
match g with
| [] => ...
- 379
0
votes
1
answer
86
views
How to prove this in Coq
Lemma x: forall P Q: Set -> Prop,
forall f: Set -> Set,
forall x, (P x -> Q (f x)) ->
(exists x, P x) -> (exists x, Q x).
I try to do it many ...
- 15
0
votes
1
answer
110
views
Why does coq not recognize that `None = Some v` is false?
I have a function:
Fixpoint eval (fuel : nat) (env : environment) (e : exp) :=
match fuel with
| 0 => None
| S fuel' => (...)
end
I'm now proving a property of such ...
- 147
2
votes
0
answers
71
views
How to make Spoq generate high-level specifications in Coq (not just AST) for the functions in LLVM IR
I am trying to use Spoq framework (and on GitHub) to translate code from C to Coq.
I faced problem - I am getting only low-level specifications for my functions (just AST), but I want to get high-...
0
votes
1
answer
35
views
Does import not only import but also change existing definitions?
Using the following Coq code:
Search "prod_uncurry_subdef".
Require Import Arith.
Search "prod_uncurry_subdef".
prints out the following:
prod_uncurry_subdef: forall [A B C : Type]...
- 4,572
0
votes
1
answer
64
views
In Coq, what would be the steps to prove the correctness of a function that solves puzzles like Sudoku or Takuzu?
What would be the general steps to prove the correctness of a function that solves puzzles, for example Sudoku or Takuzu?
- 379
2
votes
0
answers
58
views
How to define a recursive notation with overlapping production?
I am working with labelled transition systems and I want to conveniently express sequences of transitions. I defined the transition type as Inductive Trans : Label -> State -> State -> Prop ...
- 6,859
0
votes
1
answer
39
views
Dependent equality with 2 different type functions
How do you work with dependent types where the function making the type differs?
I'm working on a problem where I have 2 dependent types where the
types are indexed in different ways. I want to show ...
- 419
0
votes
3
answers
156
views
Efficient Record Construction in Coq: Is Direct Proof Inclusion Possible?
I want to define a small record in Coq which also includes certain conditions. In addition I want a definition to create a record in an easy way. Here is my approach:
Require Import Arith.
(* Define ...
- 4,572
2
votes
1
answer
87
views
Equivalence of inductive and recursive
I have two definitions for factorial of a natural number. One is an inductive definition and the other is a fixpoint. I would like to prove the equivalence of these two definitions, but haven't been ...
- 469
-1
votes
1
answer
67
views
Iris/Coq replacing literal
I am using Iris for Coq, but I am stuck on something.
Here, I want to get the snd value, l', from hd'. Then I can use IH with Hl and Hphi to finish the goal. Does anyone know how to replace hd' in ...
1
vote
1
answer
137
views
How to prove (X × Y = ∅) <-> (X = ∅) ∨ (Y = ∅)
I wish to prove the lemma below using Coq and mathcomp.classical_sets.
Let A × B - product of some sets, i.e. {(z1, z2) | z1 ∈ A /\ z2 ∈ B}
Then (A × B = ∅) <-> (A = ∅) ∨ (B = ∅)
My proof is ...
- 13