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
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