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
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
4
votes
2
answers
209
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,073
9
votes
2
answers
449
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
2
votes
2
answers
92
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,073
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,073
14
votes
2
answers
331
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,073
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,073
5
votes
1
answer
78
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
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,073
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
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
5
votes
3
answers
532
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,073
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
20
votes
2
answers
735
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
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