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
57
votes
10
answers
9k
views
Proof assistants for beginners - a comparison
What is a good starting point to learn about proof assistants?
The answer will invariably depend on the area of interest: mathematics (and its areas, e.g. algebra,combinatorics, analysis, logic), CS - ...
- 711
20
votes
2
answers
736
views
What is the difference between refl and rfl in Lean 3?
I already know that refl is called a tactic, and that rfl is a term; can you explain with examples how they technically differ? ...
- 410
16
votes
1
answer
333
views
Formalizations of unsolved problems
Is there a library (for any proof assistant) which provides formalized definitions of unsolved problems? To clarify, I mean some collection that correctly defines unsolved problems in the language of ...
- 519
14
votes
2
answers
332
views
Tools for checking the consistency of a type theory
My question is twofold:
How do you define consistency (analogously to the concept in first-order logic) in the context of a type theory?
Are there any tools that can check consistency?
I have seen a ...
- 3,095
14
votes
4
answers
266
views
What mathematical topics should I learn first before I start using proof assistants?
I'm a theoretical computer scientist and my research is focused mainly on structural and algorithmic graph theory. Recently I've been very interested in using proof assistants.
As a "pet project&...
- 143
13
votes
1
answer
180
views
Representing $\Bbb RP^2$ in Lean: building a type representing a particular set
I need to work with the set of all lines in the Cartesian plane. For my context, the natural way to think of this is that a line can be described by an equation $Ax + By + C = 0$, where $A$ and $B$ ...
- 367
9
votes
2
answers
451
views
Comparison between proof assistants for coinductive structures and proofs
I have a quite vague and naïve question: what are the differences between the different proof assistants regarding coinduction?
My motivation is that I'd like to formalize some proofs, basically about ...
- 229
9
votes
1
answer
642
views
How to define curry in Lean
I just started with Lean and with this nice SE.
In the official web book/tutorial, when explaining definitions https://leanprover.github.io/theorem_proving_in_lean/index.html they ask to complete this ...
- 193
9
votes
1
answer
181
views
Generating valid statements without a proof goal
Given some initial list of assumptions, I'd like to generate some true statements which follow from them without seeking a specific proof goal. I only need a small number of consequences from those ...
- 519
8
votes
2
answers
837
views
Explanation of Coq math-comp repositories
How are the Coq math-comp account and repositories related?
Details
One of my side goals is to try to keep the tags on this site meaningful and useful.
Today I ran into this question:
How to prove ...
- 2,846
8
votes
2
answers
533
views
Strong induction on ℕ with function α → ℕ
I have the following problem. I have a type $\alpha$, function $f : \alpha \to \mathbb{N}$ and predicate $P : \alpha \to \mathrm{Prop}$ and I want to prove that for all $a : \alpha, P a$.
How could ...
- 137
7
votes
3
answers
199
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
7
votes
1
answer
924
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 ...
- 81
6
votes
1
answer
334
views
How to replace a function by its body
I have this function:
Definition bexp x y := bexp_r x y [true].
And I have this goal:
value (bexp [] y) = 0 ^ value y
I want ...
user1231
6
votes
2
answers
274
views
Problem proving a binary add function
I'm fairly new to the Coq language and I want to prove a function that does an binary add from numbers represented as a list (least significant bit upfront).
I have created this badd function that ...
user1231
6
votes
1
answer
243
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 ...
- 1,502
5
votes
4
answers
3k
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,095
5
votes
3
answers
534
views
How do you import part of the standard library in Coq?
How do you import part of the standard library in Coq?
How do you import Nat specifically?
Why is reporting Nat not required to ...
- 3,095
5
votes
2
answers
1k
views
How do I express a negative premise in Coq?
I would like to express a transition system in the style of the small-step operational semantics as found in volume 2 of "Software foundations". Unfortunately my transition system has rules ...
- 282
5
votes
2
answers
290
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 ...
- 153
5
votes
1
answer
173
views
How to implement first-order relational structures in Coq?
I'm trying to define a first-order relational structure in Coq.
I have a way to define a pre-first-order-relational-structure, which is not a standard notion, but seems simple enough.
I also have a ...
- 3,095
5
votes
1
answer
79
views
Referencing previous fields when constructing new structure
Let's say I have a simple structure
structure foo : Type :=
(a : ℕ)
(b : list (fin a))
when defining the field b I can ...
- 137
5
votes
1
answer
524
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 ...
- 479
5
votes
1
answer
366
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:
...
5
votes
1
answer
170
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 ...
- 151
5
votes
1
answer
702
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 ...
- 153
5
votes
1
answer
180
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 ...
- 51
5
votes
0
answers
109
views
Display style proofs using Coq
How to display proofs using in Gentzen tree style and (or) Fitch-style, using CoqIDE or JsCoq?
PS: I'm rookie used coq.
- 51
4
votes
2
answers
120
views
Proof Review: Basic theorem about ternary relations in Coq
I'm proving a simple fact about ternary relations in Coq as an exercise.
I'm interested in ternary relations at the moment because they are a simple thing that can represent a finitary consequence ...
- 3,095
4
votes
2
answers
210
views
Coq defining a hierarchy of collections of integers with infinitely many "levels"
I'm trying to formalize a small part of higher-order arithmetic in Coq as an exercise (Wikipedia article for second-order arithmetic).
It's straightforward to formalize something resembling second-...
- 3,095
4
votes
2
answers
351
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:
...
- 350
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
2
answers
85
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 ...
- 479
3
votes
1
answer
143
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
3
votes
2
answers
231
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
1
answer
175
views
Code Review: Proving that a simple propositional logic satisfies Aristotle's Thesis
I'm proving that a simple propositional logic satisfies Aristotle's thesis.
I'm curious how to improve the code in question.
Here are the things I know that are wrong with it:
I'm using ...
- 3,095
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,095
3
votes
1
answer
101
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:
...
- 175
3
votes
1
answer
141
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)
...
- 479
3
votes
1
answer
98
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 ...
- 317
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
3
votes
0
answers
92
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?
2
votes
2
answers
256
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 ...
- 145
2
votes
1
answer
449
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 ...
- 143
2
votes
1
answer
82
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 ...
- 350
2
votes
1
answer
206
views
Lemma about splitting of homogeneous polynomial equations into irreducible equations
Proof assistants, and Lean, are completely new to me.
How can I derive the following simple lemma in Lean?
How can I let Lean check if the lemma is correctly written?
How can I let Lean check if the ...
- 131
2
votes
2
answers
93
views
Coq produce instance of a type `{x : T | P x}` inside an explicit definition given an `x'` of type `T`
I'm trying to formalize a simple type system in Coq as an exercise.
I have a type Item and a type {x : Item | IsNormal Item}. If ...
- 3,095
2
votes
1
answer
298
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 ...
- 479
2
votes
1
answer
176
views
Defining Lists and Prove Associativity of Append [closed]
When I saw this question asking what is the "Hello, World!" for proof assistants I immediately thought of that exercise. Not a long time after this answer by Couchy was proposed.
Therefore, ...
- 1,128
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,095