Questions tagged [beginner]
Questions asked by a beginner user of proof assistants. We make an effort to be extra kind to such users.
7
questions with no upvoted or accepted answers
5
votes
0
answers
108
views
Display style proofs using Coq
How to display proofs using in Gentzen tree style and (or) Fitch-style, using CoqIDE or JsCoq?
PS: I'm rookie used coq.
- 51
3
votes
0
answers
52
views
Bounding Volume Proof Assistant Library
I am interested in learning Lean/Coq/Isabelle etc. and wanted to try to formalize Joseph O'Rourke's Minimum Bounding Box Algorithm. I do not have much experience with proof assistant tools.
Is there a ...
- 31
3
votes
0
answers
92
views
Where is the discriminate tactic defined in Coq?
One can read the Coq documentation about discriminate tactic here.
Were is this tactic actually defined?
2
votes
0
answers
33
views
Problem working with FMapWeakList and Parametrized Records
Consider the following definition of a record R, parametrized over an arbitrary eqType:
...
- 63
1
vote
0
answers
62
views
Embedding proof assistance in an application
Context
Perhaps this is too open-ended a question for StackExchange, in which case I apologize, but otherwise here goes:
I have a project I'm toying around with, the core of which is what I'd call &...
- 111
0
votes
0
answers
39
views
Intuitive understanding of limits of `intuition` tactic in Coq
On an intuitive level, why does intuition get stuck in cases where the proof can be unblocked with a destruct?
What options are ...
- 3,073
0
votes
1
answer
233
views
An installation error in "Mathematics in Lean"
I have just started learning Lean 4 using Mathematics in Lean in Visual Studio Code, and I ran into a problem right away. I get the following error message:
...
- 1