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
9
votes
2
answers
2k
views
What is a constructor in Coq?
I am having trouble understanding the principles of what a constructor is and how it works.
For example, in Coq, we have been taught to define the natural numbers like this:
Inductive nat : Type :=
...
- 275
16
votes
3
answers
4k
views
Keeping information when using induction?
I am using the Coq Proof Assistant to implement a model of a (small) programming language (extending an implementation of Featherweight Java by Bruno De Fraine, Erik Ernst, Mario Südholt). One thing ...
- 415
5
votes
2
answers
368
views
Using forall within recursive Function definition
I'm trying to use Function to define a recursive definition using a measure, and I'm getting the error:
Error: find_call_occs : Prod
I'm posting the whole source code at the bottom, but my function ...
- 223
12
votes
1
answer
2k
views
Forall introduction in coq?
I'm trying to (classically) prove
~ (forall t : U, phi) -> exists t: U, ~phi
in Coq. What I'm trying to do is prove it contrapositively:
1. Assume there is no such t (so ~(exists t: U, ~phi))
...
- 223
2
votes
1
answer
707
views
How to write Definitions without arguments in Coq?
I have the following Inductive type defined in Coq.
Inductive natlist : Type :=
| nil : natlist
| cons : nat -> natlist -> natlist.
Notation "x :: l" := (cons x l) (at level 60, right ...
- 415
73
votes
4
answers
12k
views
What are the practical limitations of a non-turing complete language like Coq?
As there are non-Turing complete languages out there, and given I didn't study Comp Sci at university, could someone explain something that a Turing-incomplete language (like Coq) cannot do?
Or is ...
- 134k
5
votes
1
answer
992
views
Help with a Coq proof for SubSequences
I have the defined inductive types:
Inductive InL (A:Type) (y:A) : list A -> Prop :=
| InHead : forall xs:list A, InL y (cons y xs)
| InTail : forall (x:A) (xs:list A), InL y xs -> InL y (...
- 8,563
3
votes
2
answers
1k
views
Proving Predicate Logic using Coq - Beginner Syntax
I'm trying to prove the following in Coq:
Goal (forall x:X, P(x) /\ Q(x)) -> ((forall x:X, P (x)) /\ (forall x:X, Q (x))).
Can someone please help? I'm not sure whether to split, make an assumption ...
- 31
13
votes
4
answers
2k
views
Proving f (f bool) = bool
How can I in coq, prove that a function f that accepts a bool true|false and returns a bool true|false (shown below), when applied twice to a single bool true|false would always return that same value ...
- 19.9k
22
votes
5
answers
4k
views
proofs about regular expressions
Does anyone know any examples of the following?
Proof developments about regular expressions (possibly extended with backreferences) in proof assistants (such as Coq).
Programs in dependently-typed ...
user108761
7
votes
5
answers
3k
views
How to prove (forall x, P x /\ Q x) -> (forall x, P x)
How does one prove (forall x, P x /\ Q x) -> (forall x, P x) in Coq? Been trying for hours and can't figure out how to break down the antecedent to something that Coq can digest. (I'm a newb, ...
- 1,795
2
votes
2
answers
536
views
How do I write ∀x ( P(x) and Q(x) ) in Coq?
I'm trying out Coq, but I'm not completely sure what I'm doing. Is:
Theorem new_theorem : forall x, P:Prop /\ Q:Prop
Equivalent to:
∀x ( P(x) and Q(x) )
Edit: I think they are.
- 443
9
votes
6
answers
2k
views
Interactive math proof system
I'm looking for a tool (GUI preferred but CLI would work) that allows me to input math expressions and then perform manipulations of them but restricts me to only mathematically valid operations. Also,...
- 77.7k