Questions tagged [coq]

Coq is a formal proof management system. It is often referred to as a proof assistant.

Filter by
Sorted by
Tagged with
0 votes
1 answer
20 views

Induction error on mutually defined types in Coq

I want to define two types that depend on each other ...
matteo_c's user avatar
  • 131
1 vote
1 answer
48 views

How do I debug Gallina (Coq) code?

I have some complex functional code in Gallina that I run under Coq. From time to time bugs emerge and I need to debug the code. Is there a way to debug the code from Coq, or am I stuck with doing ...
Pietro Braione's user avatar
4 votes
2 answers
114 views

Ltac - run tactic for each hypothesis of given pattern

Especially in the context of lia, which can sometimes fail to prove a theorem in the form of forall x, x <> 0 -> P x ...
shooqie's user avatar
  • 171
3 votes
1 answer
96 views

Coq's elimination restriction corner cases -- when can you eliminate Prop's into Type?

In order to ensure soundness, and to keep axioms like proof irrelevance admissible, Coq has an "elimination restriction" on inductive types in Prop. ...
JoJoModding's user avatar
3 votes
1 answer
80 views

Tricks for proving equalities under type cast

I sometimes stumble across proofs that prove equalities in the form of forall a b (p: a = b), C a = match p with | eq_refl => C b end without resorting to ...
shooqie's user avatar
  • 171
4 votes
2 answers
299 views

Reasoning about CwFs in a proof assistant

I've been chatting with folks on Mastodon about this but the perspective there is markedly Agda-focused, so I thought I'd ask here for some broader opinions. What tools/libraries are there for ...
Joey Eremondi's user avatar
0 votes
1 answer
88 views

Natural deduction in Coq

I am trying to verify the proofs by natural deduction from Ryan and Huth based on the information in Natural deduction with coq proof assistant. Here is Example 1.13 and its proof. Step 4 is ...
Moti's user avatar
  • 23
2 votes
1 answer
130 views

Induction scheme on two arguments for custom type in Coq

I've been working on formalizing a Hilbert deductive system within Coq. I have the following definition for a term in first-order logic: ...
Circuit Craft's user avatar
2 votes
1 answer
53 views

Proving a logic riddle in Coq : testing equivalence in an Inductive set

I'm trying to formalize in Coq the following riddle and its solution Alice, Bob and Charlie are one of each role: a truth teller (always tells the truth) a liar (always lies) and a spy (can lie or ...
Johan Buret's user avatar
1 vote
1 answer
71 views

Can Coq grab some data over HTTP and then write the data as declartions in Coq itself?

The data I'm referring to is just an easy to understand JSON format of objects / arrows and the styling information about the arrows. For example, if an arrow is two-headed I need in Coq locally to ...
Daniel Donnelly's user avatar
2 votes
1 answer
155 views

Organizing a Coq proof

What would be a more convenient better way to solve this proof in a less clustered/confusing way? ...
randomguest0002's user avatar
-2 votes
2 answers
79 views

Help with strong induction

I have the following definition of divisibility by 3. ...
deleted_user0972's user avatar
1 vote
1 answer
140 views

Equivalence Relations COQ

I am also unfamiliar and trying to solve proofs relative to the topic Relations and Divisibility but I would like to solve such COQ proof theorems. I am not quite sure how to solve proofs like this ...
deleted_user0972's user avatar
0 votes
1 answer
131 views

Induction COQ Question

Just practicing some induction proofs and was wondering what would be the fastest and most effective way to solve this proof and proofs similar to this? ...
deleted_user0972's user avatar
7 votes
2 answers
1k views

Is it possible to make a proof assistant program based on ZFC?

I heard that many proof assistant programs are made based on the type theory. For me, as a mathematician, when I met Coq at first, it is difficult to accustomed with it. So I have a question. Is it ...
with-forest's user avatar
1 vote
0 answers
44 views

Help with proofs in analysis

I would like to prove this in real analysis, but I’m finding it difficult to do it in Coq. Can someone help me, please. If $f(x_j)$ is non-linear $x_j \geq 0$, and $f(x_j) \geq 0$, and $f(0) = 0$, and ...
Felipe Morelli's user avatar
1 vote
1 answer
125 views

How to deduce this equality based on the fact that these two terms must be the same?

Brief (but possibly inaccurate) Summary: I have a proposition H : Prop1 p q. When I use inversion on the proposition, I get ...
Agnishom Chattopadhyay's user avatar
0 votes
1 answer
60 views

Reasoning about non reflexive equalities & type conversions

Following-up from the answers to this question, reasoning about conversions between types that have decidable equalities is somewhat trivial (here I'm taking nat as ...
Felipe's user avatar
  • 63
0 votes
1 answer
36 views

Coq: Proving snd divmod doesn't depend on parameter q?

I have another proof I'm trying to complete in Coq involving the Divmod function, but the inductive case has a different value of q for the divmod function. The q parameter is only involved in the ...
Tony Peterson's user avatar
1 vote
2 answers
126 views

Weird use of equality in Coq

I have a situation that is kind of like this: ...
sudgy's user avatar
  • 193
2 votes
1 answer
77 views

Debug autorewrite in Coq

I often meet proofs using autorewrite which Coq takes a while to process for some reason. (Setoid rewriting) I then manually figure out which rewrite rules were ...
8bc3 457f's user avatar
  • 224
6 votes
4 answers
626 views

Inductive vs. recursive definitions

In Coq there are two ways to define a new type on an inductive type: Using Inductive and using Fixpoint. What are pros and cons ...
8bc3 457f's user avatar
  • 224
3 votes
1 answer
46 views

Coq: Unify with a pattern and get the result

I want to do change t with (f _), where t is a term and f is a function, but ...
Qinshi Wang's user avatar
1 vote
1 answer
59 views

Can I show Coq equality of types without using a mapping between the types?

Say that I have a list structure and a lemma: ...
Bas Laarakker's user avatar
0 votes
2 answers
124 views

How to prove basic lemmas about divisibility in Coq?

...
itsFrank's user avatar
1 vote
2 answers
192 views

Dependent sum and equality with Coq

I have types B and A n where n:nat. I want to prove that ...
Pavel Shuhray's user avatar
2 votes
1 answer
127 views

Rewriting with heterogeneous equality (JMeq)

Consider the below (reproducible) snippet: ...
Felipe's user avatar
  • 63
1 vote
1 answer
92 views

How to prove this correctness principle of transposition of lists of lists in Coq?

I have defined the function transpose as follows: ...
Agnishom Chattopadhyay's user avatar
1 vote
0 answers
44 views

How do I prove this property about a factorial specification in Coq?

Notes: This post got pretty long... my apologies but hopefully somebody can take the time to look through it. Also, some of the code below uses terms that are defined elsewhere in my file and not ...
bodacious_bandit's user avatar
6 votes
2 answers
208 views

Is there a formalism of "coinductive" data types with negative occurrences?

Consider the following program in Haskell: ...
Sebastian Graf's user avatar
1 vote
1 answer
66 views

How do I prove an expression in Coq that involves pattern matching?

I'm working on a proof in Coq and my proof state is as follows: ...
bodacious_bandit's user avatar
2 votes
1 answer
88 views

How to prove a statement about sublists?

I create sublist from list in this way: ...
hch's user avatar
  • 121
-4 votes
1 answer
187 views

How do I prove this theorem with induction in COQ

...
HELLOBIRD 892's user avatar
1 vote
3 answers
97 views

Model and Prove Unsigned Integer Operation Wrapping Behavior in Coq

I'm learning Coq and trying to do something useful with it. For daily programming tasks, especially binary parsing, one of the things I must deal with is to check and handle integer arithmetic ...
kbridge4096's user avatar
5 votes
1 answer
310 views

Why can't I use let bindings to pattern match a 3-tuple in Coq?

Consider the following Axiom foo : nat -> nat * nat. Definition fooX (x : nat) := let (y, z) := foo x in y + z. which is fine. Now, consider ...
Agnishom Chattopadhyay's user avatar
4 votes
3 answers
261 views

Rewrite with definitional equality and dependent types

In Coq, there are some terms that are equal by definition, but there's not an easy way to replace one value with the other inside a proof. The two ways that I know that work in general are to use the ...
sudgy's user avatar
  • 193
0 votes
1 answer
115 views

I don't know how to fire up coqtail

I installed coq and coqtail in my computer. According to this page: https://github.com/whonore/Coqtail Im now supposed to use the command CoqStart to launch the plugin. However, when I type ":...
Raul Gomez's user avatar
1 vote
0 answers
82 views

How to reason about equality between different datatypes?

I am working on a verification project where the specification uses the following inductive datatype to represent bitvectors (MIT's bbv) ...
Felipe's user avatar
  • 63
3 votes
2 answers
211 views

How to abstract over function arity in Lean and Coq?

Given types $A, B$ I would like to express the type of all functions $f$ for which there exists an $n \in ℕ$ such that $f$ has type $A^n \to B$. And possibly in such a way, that for $a_1, \dots, a_n : ...
8bc3 457f's user avatar
  • 224
1 vote
1 answer
69 views

Coq Induction on Hypothesis destroys the Hypothesis

I'm trying to prove something in coq I have and Inductive prop type named in_order_merge which is a relation between three lists that shows third one is in_order merge of first two, here is the ...
asha soroushpoor's user avatar
1 vote
2 answers
50 views

Destructing transitivity hypothesis on simple predicate logic

I'm new to Coq and am working on some exercises with predicate logic. In one of the exercises, a transitivity hypothesis is defined as follows: ...
Kitando's user avatar
  • 11
2 votes
1 answer
85 views

Program Fixpoint decreasing on measure produces unsolvable goal

I have trouble understanding how to produce more sensible goal in the obligation ...
M B's user avatar
  • 63
1 vote
1 answer
81 views

an argument why stack blocks are never unexpectedly freed in the RTL intermediate language in CompCert

I apologize if this is not the right site to ask this, as the question is not about a proof assistant per se, but about a particular formalization. In the semantics of the RTL intermediate language in ...
David Monniaux's user avatar
2 votes
2 answers
123 views

How to get rid of opaque proof-terms in computation

My goal is to construct list of vectors from filtered by length list of lists Something like Compute foo [[1;2]; [3]; [4;5]]. (* [[1;2]%vector; [4;5]%vector] *) My ...
M B's user avatar
  • 63
1 vote
1 answer
78 views

Coq abilities and usage

What abilities does coq have apart from simple proofs? Can it complete induction? Can I use it to solve polynomial equations? Can I use it to prove bijections?
massive coq's user avatar
1 vote
3 answers
90 views

Two-step induction of inductive predicate on Streams

If I want to have an induction principle for nats from n to n+2, I can define and prove this ...
matteo_c's user avatar
  • 131
0 votes
2 answers
126 views

Why can't I write a function that doesn't take a type argument besides Set, Prop, or Type?

I'm trying to make a "formal" model of a C++ domain specific language. One thing the language has is a notion of a "reducer" where you take an array and add up all the elements. I ...
sdpoll's user avatar
  • 123
0 votes
2 answers
60 views

Stream of all finite prefixes of a stream

If I want to construct of list of all (obviously finite) prefixes of a list, I can define this function: ...
matteo_c's user avatar
  • 131
1 vote
3 answers
138 views

How do I express a fixpoint of a decreasing argument that is not a subterm of the function's argument?

I have a recursively defined function in Coq whose arguments in the recursive invocations are surely decreasing, but Coq cannot understand this fact since they are not subterms of the function's ...
Pietro Braione's user avatar
0 votes
1 answer
104 views

What is the idiomatic way in Coq to write recursive functions over product types?

I need to write a recursive function in Coq that takes an argument with type T and produces a result with type option T. The problem is, the recursive invocation is not properly on a subterm of its ...
Pietro Braione's user avatar