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
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
1
answer
149
views
How to see the value under Exists in Lean?
My understanding of dependent typing is that it allows typing functions to constrain their behavior. Say I have a Lean object
...
- 13
1
vote
2
answers
245
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,095
1
vote
1
answer
157
views
How do I prove a record related lemma?
I'm new to coq. I would appreciate it if you could help me.
Consider the following definition:
Record person:= mk_person { p_name : t1; p_age : t2}.
How to prove ...
- 11
1
vote
1
answer
27
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,095
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,095
1
vote
1
answer
96
views
Assistance using destruct on an equality proof for functors
Context
I am currently learning how to use the Coq proof assistant and am at the level where I know the fundamentals of dependent-type theory and have done most of the "Software Foundations" ...
- 133
1
vote
1
answer
120
views
What do I need to import from MathLib to make `induction a with d hd` work?
I know that I need to import Mathlib to make rewrite [x] at h work. But induction a with d hd...
- 479
1
vote
3
answers
202
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 ...
- 282
1
vote
1
answer
133
views
Need help with induction proof in Lean for $0+d=d$
So I have been trying to learn Lean and have managed to find this resource called the "Natural Number Game" which is supposed to help me learn Lean.
I am learning Lean to help me understand ...
- 145
1
vote
1
answer
281
views
In lean 4, how do I refer to variables with names like `a✝`
When I have a tactic state that mentions a variable name like a✝, is there a way to refer to it? When I use this variable name in my code, it says it doesn't exist.
...
- 479
1
vote
1
answer
35
views
Case assumption missing from tactic state in lean4
I'm trying to prove a <= max(a, b) by case. I have this:
...
- 479
1
vote
1
answer
220
views
how to prove 2+2+a=4+a in lean4?
It should be simple but dig it for a while and still not successful.
theorem example (a : R) : 2 + 2 + a = 4 + a := ...
can someone help to figure out how to do next? many thanks
- 11
1
vote
1
answer
96
views
confused about stlc from Programming Language Foundations
I have two related quetions. I made my way to STLC and Typechecking from Programming Lang Foundations, yet I am more or less mentally stuck at the STLC chapter, hence many things related to it are ...
- 71
1
vote
1
answer
138
views
İnduction/inversion and others in coq
I'm trying to learn Coq using the software foundations. I somehow made it to the 2nd volume but I'm struggling writing proofs on my own. Especially whether I should be using inversion or induction.
I ...
- 71