Questions tagged [beginner]
Questions asked by a beginner user of proof assistants. We make an effort to be extra kind to such users.
90
questions
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
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
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
2
answers
135
views
ACL2: Is there a way to check that a Skolem function does what it says on the tin?
I have been trying various things to try to prove that the product of two positive rationals is positive in ACL2, see here for one attempt.
Recently, I entered the following Skolem function via ...
- 3,053
0
votes
1
answer
40
views
ACL2 Prove that the product of two positive numbers is positive
Here's a trivial book that proves that addition and multiplication of positive integers are positive.
Interestingly, ACL2 can also prove out of the box that x + y ...
- 3,053
2
votes
1
answer
43
views
Coq cannot `simple apply reflexivity` in custom tactic
The fast reflexivity tactic shown below is very interesting. It exposes some of the unification machinery by disabling it.
I'm planning on going back and using it in the first part of Software ...
- 3,053
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,053
7
votes
3
answers
190
views
Why is $\Bbb Z = \Bbb N$ independent of Lean?
In this answer, it is noted
For a silly example, in ZFC with the usual encoding, $\mathbb{Z} \neq \mathbb{N}$, but in Lean it is well-known that this is independent. Of course in both ZFC or Lean, ...
- 173
0
votes
1
answer
46
views
2
votes
1
answer
93
views
What does `induction ... in ...` do in Coq?
I'm self-studying the Semantics course, and met the following proof script in the warmup directory:
...
- 123
3
votes
1
answer
142
views
Help needed for Lean4 book Interlude exercise
In 3. Interlude of the Functional Programming in Lean book, one of the exercises asks the reader to prove by simp some few theorems, one of them is ...
- 133
4
votes
1
answer
262
views
Dealing an equality with coq. - beginner's question
I am studying the sf book - ProofObjects.v file.
I'm confused with "equality__leibniz_equality_term" exercise.
...
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
0
votes
1
answer
89
views
Using lean4 to prove subset properties
I'm learning Lean4.
I'm trying to prove in lean4 these basic properties of subsets:
$ X \subseteq X $
$ X \subseteq Y , Y \subseteq Z \Rightarrow X \subseteq Z$
$ X \subseteq Y , Y \subseteq X \...
- 3