Questions tagged [beginner]
Questions asked by a beginner user of proof assistants. We make an effort to be extra kind to such users.
73
questions
3
votes
1
answer
94
views
Stuck in a proof about sum types and nonempty lists
I have a hard time proving an apparently simple property or finding a counterexample. It is about sum types and nonempty lists.
I first define two basic functions about sum types:
...
1
vote
1
answer
75
views
Proving that equality is decidable on an ``Inductive Set``
I've managed to prove that equality within a type is indeed decidable.
...
2
votes
1
answer
94
views
Two steps induction in Lean4: how to obtain 2nd inductive hypothesis?
When trying to solve this example from "The Mechanics of Proof":
...
0
votes
1
answer
78
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 ...
2
votes
2
answers
176
views
How do I prove $\operatorname{succ}(a)$ cannot be equal to $0$ in Lean4?
So I have been using The Natural Number Game (as I have mentioned in my previous post) to learn Lean1. However, I am currently stuck on level 6/9 in the Algorithm world, where I am supposed to prove ...
1
vote
1
answer
104
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 ...
2
votes
1
answer
108
views
In Lean 4 how to substitute equals in an expression with other variables?
I can use 'subst' to prove that if a=b and a is positive then b is positive:
example (a b : Peano) (h1 : a = b) (h2 : pos a) : pos b := Eq.subst h1 h2
How do I ...
1
vote
1
answer
99
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
...
0
votes
1
answer
91
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
107
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 ...
0
votes
1
answer
107
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:
...
2
votes
1
answer
162
views
Verifying a basic function with Lean4
I have this simple structure to represent a person:
structure Person where
age: Nat
lifespan: Nat
deriving Repr
This function takes a Person and either (a) ...
1
vote
0
answers
60
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 ...
0
votes
1
answer
74
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 ...
0
votes
1
answer
144
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.
...
1
vote
1
answer
86
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...
5
votes
1
answer
433
views
Why is lean 4 behaving differently on my machine vs in the natural number game?
In the lean 4 version of the natural number game at https://adam.math.hhu.de/#/g/leanprover-community/NNG4/ , I can use tactics like apply x at h and ...
3
votes
1
answer
106
views
Print the version of lean that is running
In python, I can get the version of python I am using like this:
import sys
print(sys.version)
...
0
votes
1
answer
107
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 ...
2
votes
1
answer
94
views
Apply `unfold` once, instead of many times, in lean4
I have code that is similar in spirit to this:
...
1
vote
1
answer
33
views
Case assumption missing from tactic state in lean4
I'm trying to prove a <= max(a, b) by case. I have this:
...
2
votes
1
answer
218
views
How do I make the rational numbers 0 and 1/2 in lean4?
I'm trying to define a function that in python I would write:
def f(x: bool) -> float:
if x:
return 0.5
return 0.0
In lean 4 I tried writing ...
3
votes
2
answers
77
views
Shortening a 4-levels-of-match lean4 proof of the CHSH inequality
In the CHSH game, Alice (Bob) is given the value $x$ ($y$) and needs to pick a value $a$ ($b$) such that $a \oplus b = xy$. The CHSH inequality proves they can win at most 75% of the time with ...
2
votes
0
answers
30
views
Problem working with FMapWeakList and Parametrized Records
Consider the following definition of a record R, parametrized over an arbitrary eqType:
...
1
vote
1
answer
187
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
1
vote
0
answers
61
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 &...
1
vote
1
answer
116
views
Recursive type class for OfNat Even
I'm working my way through Functional Programming in Lean. There's an exercise to create an Even class to represent even natural numbers.
I was able to define ...
2
votes
1
answer
86
views
Metamath unification example
Basic question
Suppose we define a point and some related stuff:
x , y are reals
Point ( x , y )
Abscissa ( Point ( x , y ) ) = x
Ordinate ( Point ( x , y ) ) = y
And we want to have/prove:
Point ( ...
1
vote
1
answer
95
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 ...
1
vote
1
answer
88
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 ...
2
votes
1
answer
326
views
How to install dependencies correctly? [Cannot find a physical path bound to logical path]
There's this library I'd like to use. The idea is to be able to use this library with Require Import easily in any other *.v ...
2
votes
1
answer
127
views
How do I do for-all introduction in Isabelle?
It's pretty easy to prove something like this:
theory Scratch imports Main begin
theorem "foldl (Ī» x y. x) a b = a"
apply (induction b)
by auto
...
2
votes
1
answer
56
views
Proving a logic riddle in Coq : testing equivalence in an Inductive set
I'm trying to formalize in Coq the following riddle and its solution
Alice, Bob and Charlie are one of each role:
a truth teller (always tells the truth)
a liar (always lies)
and a spy (can lie or ...
0
votes
1
answer
63
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 ...
1
vote
3
answers
174
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 ...
0
votes
1
answer
122
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 ...
5
votes
1
answer
170
views
Is there an easy-to-learn GUI of proof assistants for teenagers in maths education?
I'm a high school sophomore and I have been interested in Interactive Theorem Proving for a year or two. I found it extremely hard for my peers (lack of knowledge in mathematical logic, type theories ...
1
vote
1
answer
135
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 ...
5
votes
1
answer
541
views
How to unfold definitions in Lean / find the right theorems to apply?
After a few days playing around with Lean4, I notice I keep running into the problem of how to find the right theorems to apply. The situation below is one I run into particularly often, so perhaps I ...
1
vote
1
answer
61
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 ...
5
votes
2
answers
243
views
Unclarity about Preorder class in Lean4
I realize the port of Mathlib to Lean4 is not finished yet, but I've run into a definition that I do not quite understand. I'm quite new at using theoremprovers as well as stackexchange, so please be ...
3
votes
2
answers
208
views
Coq: can `tauto` be used to prove classical tautologies?
When I experiment, I get inconsistent results.
Running the following code (with a proof included to double-check that it's provable)
...
3
votes
0
answers
83
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?
5
votes
1
answer
271
views
How to prove a property of a conditional statement without using tactics in Lean?
This doesn't work even though it is the simplest proof of an if statement that I can think of:
...
6
votes
1
answer
223
views
What are some good resources for Proof Assistant based exercises/puzzles for recreation and practice?
Proof Assistant based exercises and puzzles make for a good recreational activity, as well as help sharpen skills of users of said systems. There are many such equivalent resources for algorithmic ...
3
votes
1
answer
97
views
Using induction to define Indexed family of HITs in agda
I am looking to define a family of HITs parametrized by $\mathbb{N}$. I want $(-)$-glob : $\mathbb{N} \to Type$, so that $n$-glob is the n-dimensional glob. I know how to construct the n-$glob$ by ...
2
votes
1
answer
80
views
Why does my previously defined function expands/computes to itself?
Problem
I have a function leb defined in one of the (transitively) imported file: Types.v. However, calling it in my current ...
4
votes
2
answers
328
views
Why is my recursive definition of list_min ill-formed?
I'm new to Coq and I'm on my own (self-learning).
Question:
Define a function list_min that takes a list of natural numbers and returns the least element of the list.
Source
My solution:
...
7
votes
1
answer
812
views
What is the current state of proof assistants?
I am a high school senior going into college and I am applying to a scholarship in which I must write an essay about a potential future technology that would dramatically impact humans. I immediately ...
5
votes
1
answer
164
views
Looking for an entry point in the universe of proof assistants and proof IDE's
This is my first question in this part of StackExchange.
What I would like to achieve is the following.
Suppose I want to study ( or give a course on ) basic Real Analysis, I want to 1) document the ...