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
34
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
158
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
251
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
163
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
32
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
136
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
98
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
205
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
138
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
301
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
36
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
225
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
97
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
141
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
1
vote
1
answer
62
views
Question about default definitions in fields
In Unclarity about Preorder class in Lean4 I asked why the third and fourth field (lt and lt_iff_le_not_le) in the definition of MyPreorder below would both be necessary, as one follows from the other ...
- 153
1
vote
0
answers
61
views
Peano Arithmetic in LEAN4 [duplicate]
Kia ora!
I am trying to implement the Peano axioms and prove some simple theorems about the natural numbers in LEAN4. However, I am not sure how to encode the first two (as presented here) axioms in ...
user2426
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
1
answer
69
views
Reasoning about non reflexive equalities & type conversions
Following-up from the answers to this question, reasoning about conversions between types that have decidable equalities is somewhat trivial (here I'm taking nat as ...
- 63
0
votes
1
answer
47
views
0
votes
1
answer
41
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,095
0
votes
1
answer
96
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
0
votes
1
answer
178
views
What am I doing wrong when proving the add_right_cancel theorem?
So, as mentioned in my previous two questions, I have been using The Natural Number Game to help me teach myself how to use the mathematical proof assistant Lean4.
I am currently trying to complete ...
- 145
0
votes
1
answer
120
views
Shortcut proof by calculation for addition/subtraction, "The Mechanics of Proof", and mathlib4
In Macbeth's book 'The Mechanics of Proof,' the author provides a tactic called addarith to eliminate the need to write calc ...
0
votes
1
answer
174
views
In Lean 4 how to use an implication in a hypothesis?
I am experimenting with my own "natural numbers" (Peano), so I don't want to use Lean 4's natural number tactics (such as add_comm or cancellation). How can the following be proved? It ...
- 31
0
votes
1
answer
172
views
In lean 4, how do I give names to variables when using `split`?
Sort of related to In lean 4, how do I refer to variables with names like `a✝`
When I use split to pull apart a match, I get a ...
- 479
0
votes
1
answer
165
views
In lean4 why is induction only rewriting the goal, and not the known facts?
When I do induction over a variable $x$ in lean 4, why isn't $x=0$ available as a fact in the base case of the induction? Without this fact, I can't rewrite other facts in order to make the induction ...
- 479
0
votes
1
answer
145
views
What is the idiomatic way in Coq to write recursive functions over product types?
I need to write a recursive function in Coq that takes an argument with type T and produces a result with type option T. The problem is, the recursive invocation is not properly on a subterm of its ...
- 282
0
votes
0
answers
40
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,095
0
votes
1
answer
257
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