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
2 votes
1 answer
26 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
51 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
121 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
106 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
61 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?
4 votes
1 answer
87 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
133 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 ...
4 votes
1 answer
80 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
74 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 ...
  • 340
4 votes
2 answers
221 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: ...
  • 340
7 votes
1 answer
367 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
5 votes
1 answer
105 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 ...
5 votes
0 answers
82 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.
6 votes
1 answer
204 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 ...
's user avatar
2 votes
1 answer
176 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
6 votes
2 answers
251 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 ...
's user avatar
8 votes
2 answers
685 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,786
9 votes
1 answer
504 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
16 votes
1 answer
308 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 ...
  • 509
9 votes
1 answer
155 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 ...
  • 509
8 votes
2 answers
286 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
3 votes
2 answers
165 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-...
  • 2,593
9 votes
2 answers
212 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 ...
2 votes
2 answers
71 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 ...
  • 2,593
3 votes
1 answer
102 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 ...
  • 2,593
12 votes
2 answers
206 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 ...
  • 2,593
5 votes
1 answer
118 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 ...
  • 2,593
5 votes
1 answer
67 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
4 votes
2 answers
76 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 ...
  • 2,593
2 votes
1 answer
125 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, ...
  • 998
14 votes
4 answers
176 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&...
4 votes
3 answers
109 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 ...
  • 2,593
10 votes
1 answer
124 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$ ...
  • 295
16 votes
2 answers
208 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? ...
34 votes
8 answers
1k 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 - ...