Questions tagged [coq]
Coq is a formal proof management system. It is often referred to as a proof assistant.
316
questions
0
votes
1
answer
6
views
What to import to use le_not_gt_iff?
According to the documentation, there should be a Lemma le_not_gt_iff in Coq.Structures.OrdersFacts, but I haven't succeeded in referencing it.
I am trying to prove ...
- 149
0
votes
1
answer
27
views
Arguing with sumbools
I have the following definitions:
Variables Sd_pre : nat -> Prop.
Definition Sd_dec : forall t, { Sd_pre t } + { ~Sd_pre t }.
Admitted.
And the following are ...
- 149
3
votes
2
answers
73
views
A $\mu$-recursive function converges at an input, how to find the output?
Summary: I want to implement an interpreter for $\mu$-recursive functions which, for any $\mu$-recursive function $f$ and input $\mathbf{x}$, returns $f \left( \mathbf{x} \right)$ if it is defined.
...
- 83
3
votes
2
answers
75
views
Using if in Fixpoint
I have this recursive function I am trying to define by way of Fixpoint, but the if condition is giving me trouble.
...
- 149
2
votes
3
answers
531
views
What is a positive coinductive type and why are they so bad?
What is a positive coinductive type and why are they so bad?
This question is specifically within the context of Coq and is inspired by this question, the opening lines of which are:
Since positive ...
- 3,053
1
vote
1
answer
69
views
Best practices: Should I prefer definitions or iff when defining predicates?
I am a beginner in Coq, and I have a proposition I defined in this way:
...
- 149
5
votes
4
answers
2k
views
Less ridiculous way to prove that an Ascii character compares equal with itself in Coq
How do you prove that an Ascii character compares equal with itself in Coq idiomatically?
In the course of trying to prove a random exercise in Logical Foundations, I wanted to prove the following ...
- 3,053
3
votes
1
answer
199
views
Finding reflexive, transitive closure
I got a relation like: R: A -> A -> bool.
Using this, I need to find an Rclose: A -> A -> bool such that ...
- 131
1
vote
1
answer
26
views
Feeding rewrites and other hints into an omnibus tactic
How do I feed rewrites that I've marked as safe into a custom tactic?
I'm trying to write shorter Coq proofs with more of the easy stuff hidden. To that end, in the script below I proved that ...
- 3,053
1
vote
4
answers
199
views
Formalizing "finite or infinite" in Coq
In Coq, I am trying to formalize the notion of a finite or infinite sequence, e.g. of natural numbers: call it a run, and call ...
- 249
1
vote
2
answers
241
views
Why did this proof succeed without function extensionality?
I'm very confused as to why a proof of a lemma succeeded without function extensionality.
I'm messing around with some trivial Coq proofs for manipulating pseudosequences of the form ...
- 3,053
3
votes
1
answer
116
views
How to use SSReflect to prove commutativity and associativity of addition idiomatically?
How do you prove commutativity and associativity of addition idiomatically using SSReflect?
I am trying to learn SSReflect so I have another tool in my belt for ...
- 3,053
1
vote
1
answer
48
views
Applying an axiom from a class in a proof
I'm trying to represent Boole-Schroder Algebra in Coq, and am trying to use apply to start a proof using one of my defined axioms, but I'm getting an "unable ...
1
vote
1
answer
95
views
Trying to use 'Equations'
Examples from Chlipala's book
https://mattam82.github.io/Coq-Equations/examples/Examples.MoreDep.html
...
- 105
2
votes
1
answer
68
views
Checking if a goal is *definitely wrong* by testing it against random examples in Coq
I'm currently poking around in a medium-sized Coq codebase that I didn't write and am not very familiar with ... and I'm trying off and on to make progress on some lemmas where the proof attempt was <...
- 3,053