Questions tagged [beginner]

Questions asked by a beginner user of proof assistants. We make an effort to be extra kind to such users.

Filter by
Sorted by
Tagged with
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: ...
Dave's user avatar
  • 165
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. ...
Johan Buret's user avatar
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": ...
Eugen Lindorfer's user avatar
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 ...
CrSb0001's user avatar
  • 145
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 ...
CrSb0001's user avatar
  • 145
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 ...
CrSb0001's user avatar
  • 145
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 ...
Lewis Baxter's user avatar
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 ...
antilope's user avatar
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 ...
probablygrigsby's user avatar
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 ...
Lewis Baxter's user avatar
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: ...
Blankino's user avatar
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) ...
probablygrigsby's user avatar
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 ...
user avatar
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 ...
Craig Gidney's user avatar
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. ...
Craig Gidney's user avatar
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...
Craig Gidney's user avatar
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 ...
Craig Gidney's user avatar
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) ...
Craig Gidney's user avatar
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 ...
Craig Gidney's user avatar
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: ...
Craig Gidney's user avatar
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: ...
Craig Gidney's user avatar
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 ...
Craig Gidney's user avatar
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 ...
Craig Gidney's user avatar
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: ...
Felipe's user avatar
  • 63
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
Tim Eric's user avatar
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 &...
Eric Anderson's user avatar
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 ...
Nate Glenn's user avatar
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 ( ...
Jorge Agra's user avatar
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 ...
noCrayCray's user avatar
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 ...
noCrayCray's user avatar
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 ...
Julián's user avatar
  • 143
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 ...
wizzwizz4's user avatar
  • 495
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 ...
Johan Buret's user avatar
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 ...
Felipe's user avatar
  • 63
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 ...
Pietro Braione's user avatar
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 ...
Pietro Braione's user avatar
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 ...
Chesium's user avatar
  • 51
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 ...
B.Rolando's user avatar
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 ...
Pieter Cuijpers's user avatar
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 ...
Pieter Cuijpers's user avatar
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 ...
Pieter Cuijpers's user avatar
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) ...
Malcolm Sharpe's user avatar
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?
Jacob woolcutt's user avatar
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: ...
Fernando Bailey's user avatar
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 ...
Agnishom Chattopadhyay's user avatar
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 ...
IsAdisplayName's user avatar
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 ...
zacque's user avatar
  • 350
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: ...
zacque's user avatar
  • 350
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 ...
gmod's user avatar
  • 81
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 ...
nilo de roock's user avatar