Newest Questions
1,566 questions
0
votes
0
answers
21
views
How to fix SPASS GUI editor bug
I successfully downloaded the Theorem Prover SPASS GUI v3.7 on Windows 7 and it works fine.
But, any changes to Input are ignored - it appears that the Run button does not use the live editor buffer. ...
- 31
0
votes
1
answer
35
views
How to find a substring in a string in Lean 4?
Does the Lean 4 standard library has a function for deciding whether a string is a sub-string of another string?
For example, in python and other languages, one can use the ...
- 3,340
4
votes
1
answer
227
views
In ITT, are all provable equalities in the empty context provable by refl?
For context, I am reading "Principles of Dependent Type Theory".
Intensional Type Theory is a dependent type theory where we take out equality reflection to make type conversion decidable. I'...
- 111
0
votes
0
answers
61
views
How to use Lean to generate a program in python?
I read that there are performance bottlenecks for proof assistants, and
verification of software often has 10x--100x as many lines of proof as
lines of code being verified.
I guess there is also ...
- 3,340
3
votes
2
answers
381
views
Proving an order relation between two concrete real numbers (Lean)
I've been using Lean for a few weeks now, but I've hit a simple roadblock: I have reduced my main goal in a theorem to the statement 0 < 0.5, but I have no idea ...
- 33
1
vote
1
answer
67
views
Matching Singleton Sets in Lean4
In Lean4, suppose x has type (Set Nat) × Nat. What is a clean, idiomatic way to pattern match to see if the set is a singleton.
...
0
votes
1
answer
111
views
Proof of completeness theorem in first order logic
I am starting to program a proof assistant in Python. The proof assistant will be based in FOL. I might be interested in proving the soundness and completeness theorem for first-order logic in my ...
- 109
2
votes
1
answer
47
views
3
votes
1
answer
142
views
Why is Lean4 an intensional type theory?
In the document of Lean4 I know that the foundation of Lean4 is a kind of intensional type theory. If I understand that correctly, by extensional type theory we mean that there is only one constructor ...
- 133
0
votes
0
answers
41
views
Reasoning About TAPL Unification in Rocq
I'm new to Rocq and want to reason about the TAPL version of Robinsons Unification algorithm.
I've managed to implement the algorithm using 'Program Fixpoint', but even after satisfying all the ...
- 1
9
votes
2
answers
931
views
What efforts have there been in trying to automate diagrammatic proofs in category theory?
Crossposting note: This is a crosspost from a question I first asked in MathOverflow.
———————————————————————————————————————————
Perhaps one of the biggest issues when carrying out research in ...
- 231
3
votes
0
answers
86
views
What's the current state of the art in the formalisation of spectral sequence arguments in Lean?
Recently I've been wondering about whether or not have there been formalisation efforts involving spectral sequences, in particular in Lean. To this end, I've been trying to better understand the ...
- 231
1
vote
3
answers
123
views
4
votes
1
answer
131
views
What is the standard equivalent of an Ltac match in lean4?
In rocq, it is very common to write tactics which look for specific patterns in the goal or context, like for example this:
...
- 155
1
vote
1
answer
95
views
Prove an inequality in Rocq
I'm trying to prove some facts about a function which outputs one of two strings based on an inequality operation on two integers. I haven't gotten very far before hitting a wall, how would I proceed ...
- 15
2
votes
2
answers
92
views
Data structure for context in STLC
I formalized simply typed lambda calculus using a list of pairs as context implementation:
...
- 621
2
votes
0
answers
61
views
Wanted: API for theorem prover
My Prolog program generates small statements in Peano Arithmetic (0,s,+,$\times$,=, $\neq$, $\forall$,$\exists$ ). Currently I manually use WebSPASS to prove the statement (or its negation). If it ...
- 31
3
votes
1
answer
127
views
Is there a model that contradicts `@eq Type t1 t2 -> @eq Prop t1 t2` or can it be proven?
It is easy to prove forall t1 t2 : Prop, @eq Prop t1 t2 -> @eq Type t1 t2.
The converse can be proven if we assume univalence.
Can it be proven without ...
- 1,709
1
vote
0
answers
88
views
What is the status of Software Foundations ports to Lean 4, and what is the canonical alternative?
What are all the known attempts to port the Software Foundations (Coq) textbook series to Lean 4, and what is their current status?
If there is no complete port, what is the community's canonical ...
- 551
1
vote
1
answer
126
views
What is Isabelle's new antiquotation syntax for cite?
If I use Isabelle's markup for citations in the document preparation system as one usually finds it online, Isabelle issues warnings:
...
- 491
0
votes
0
answers
47
views
How to use the lean4 syntax/macro rules in BNF style?
I am trying to understand how Lean4's syntax and macro expansions work. I initially guessed is that it works like Backus Normal Form. My example seems to work to some extent:
...
- 3,340
2
votes
1
answer
156
views
Prove bisimilarity of coinductive streams
Suppose the following definition of an infinite stream in rocq:
CoFixpoint test x: traceinf :=
Econsinf x (test x).
It seems that wanting to prove ...
- 229
0
votes
1
answer
59
views
Small step reduction of terms with saving intermediate results
I am trying to play with lambda calculus basic rules in coq language.
I read the chapter about reduction rules in coq documentation.
I wrote the following:
...
- 621
5
votes
2
answers
169
views
Comparison of expressive power of GADTs and Inductive types
I am trying to wrap my head around some different 'classes' of types I have heard about that are used in dependently types languages, and how they compare to each other. This is my current ...
- 165
0
votes
1
answer
68
views
How to perform inductive proofs for Lean Vector?
I learned Vector (list/array with known length) from Idris2, and experienced some cultural shock when encountering Lean's definition of Vector. In Idris, Vector is directly an inductive definition, ...
- 3,340
3
votes
1
answer
221
views
Create a “constant” to avoid writing the same expression several times in tactics
Is it possible in Rocq tactics / Ltac, to create a new variable with an expression as value, to allow writing simply this variable instead of the whole expression when needed?
I could imagine creating ...
- 133
6
votes
1
answer
234
views
Why does CCHM cubical type theory use De Morgan cubes and not Boolean cubes?
Why does CCHM cubical type theory (and hence also cubical Agda) use De Morgan cubes and not Boolean cubes?
It possibly has something to do with Lemma 2.1 in these notes by Coquand, but I've never ...
- 161
0
votes
1
answer
73
views
Lean4: Cannot run the blueprint of sphere-eversion
I downloaded the sphere-eversion project
( https://github.com/leanprover-community/sphere-eversion)
I tried to build the blueprint following the instruction written in the site above:
lake exe cache ...
- 21
1
vote
0
answers
58
views
How to call unix shell commands in Lean 4?
For interacting with the OS, I was wondering whether Lean4 has standard functions to call unix shell commands?
Basically, I am looking for the Lean equivalent of python's ...
- 3,340
0
votes
1
answer
74
views
How to inductively define Lean4 Vector in Idris2 style?
In Idris2, Vector is defined here inductively in terms of nil and cons as follows:
...
- 3,340
0
votes
2
answers
146
views
Loss of information when performing induction on a relation between a variable and a value
In a Coq/Rocq proof, I want to use an hypothesis relating two terms by the reflexive closure of a relation. I defined a reflexive closure as follows:
...
- 11
3
votes
1
answer
80
views
Dealing with heterogeneous noConfusion / injectivity of dependent inductives
Normally one uses Foo.noConfusion to invoke injectivity of inductive constructors
...
- 800
2
votes
1
answer
755
views
2
votes
0
answers
59
views
How to make Lean use non-standard git repo for mathlib?
I sometimes work in different regions of the world, and the connection to the standard lean/mathlib repository is often times unstable. I was wondering:
Is it possible to configure lake in Lean 4 to ...
- 3,340
6
votes
2
answers
538
views
What is the most accepted library for floats in Lean4?
I'm working on a project in Lean4 that involves formalizing numerical analysis algorithms, and I need to be able to formally reason about floating-point numbers.
My understanding is that Lean4's ...
- 551
3
votes
0
answers
61
views
How to replay a derivation in Lean
Suppose in Lean 4 we have derived a term t of a given type A and bound it to a name:
...
- 12.9k
1
vote
1
answer
144
views
How does the universe-level constraint solver of Rocq work?
Observation 1.
#[universes(polymorphic=yes)]
Axiom foo@{u} : Type@{u} -> Type@{u}.
Inductive bar (A : Set) : Set :=
| mkbar : foo A -> bar A.
Since the ...
- 491
0
votes
1
answer
85
views
How to coerce/convert constant to the type of a given variable?
Given two terms x and y of unknown types, is there a way in Lean 4 to coerce one term to the type of the other term?
I know that ...
- 3,340
1
vote
3
answers
204
views
Conditional probability in Mathcomp?
Isn't conditional probability implemented in Rocq/Mathcomp?
Some effort in this direction is made in this article (with a finiteness restriction) but I see no mention in Mathcomp/analysis' probability....
- 387
0
votes
1
answer
148
views
Can formal reasoning really prove that any code is correct?
I’ve been thinking about this lately — we have all these formal verification tools, theorem provers, type systems, etc., and they do work for specific cases like compilers or microkernels.
But when it ...
- 1
3
votes
2
answers
197
views
What exactly does the "generalizing" clause do in Lean4's induction?
Lean4's documentation says the following about the generalizing clause in the induction command ...
- 3,340
3
votes
2
answers
874
views
How can dependently-typed proof assistants treat equivalent definitions symmetrically?
In standard mathematics, there is the notion of "equivalent definitions" of something. For example, we can define the Fibonacci sequence directly via recursion or by using a more performance-...
- 93
5
votes
1
answer
116
views
Path over path for a higher inductive type
I'm working with the closed modality from Modalities in HoTT and Synthetic Tait Computability, which is the following higher inductive type in Cubical Agda.
...
- 65
2
votes
0
answers
87
views
Is there a Lean 4 FFI for python?
The Lean 4 documentation says that
Lean offers efficient interoperability with any language that supports
the C ABI.
I know that this includes C and C++. But I was just wondering:
Is there a Foreign ...
- 3,340
-4
votes
1
answer
167
views
How can Coq accept an unsound proof if the kernel is correct? (failure modes, examples, and mitigations)
I’m trying to assemble a clear, expert-level answer to a common worry: Even if Coq’s kernel is correct, how can a proof still “pass” in Coq and yet be logically unsound? I’m looking for a canonical ...
- 551
1
vote
0
answers
55
views
Rocqs module inclusion (<+) and implementation (<:) results in Nat not being an OrderedType
So I have a small example that doesn't work:
From Coq Require Import PeanoNat.
Require Import FMapList.
Module Import VarMap := FMapList.Make(Nat).
Gives:
...
- 133
4
votes
0
answers
69
views
How to write a DSL in a file instead of in source code in Lean 4?
I am reading the chapter Embedding DSLs By Elaboration from Meta Programming in Lean4 (and other sources) about building a domain specific language in Lean 4. In the final example (quoted below) and ...
- 3,340
3
votes
1
answer
181
views
When can a formally-verified program be converted into a proof-producing program?
I'm sorry if this question is a little long and rambling, but I've been thinking about this for a while and would like to know if there's a systematic way to think about the following.
When creating a ...
- 93
0
votes
0
answers
77
views
Using $\eta$-extensionality principle to derive $\Gamma \vdash f\doteq g : \prod_{x : A} B(x)$?
Given:
$$
\Gamma \vdash f:\prod_{x:A} B(x) \\
\Gamma \vdash g:\prod_{x:A} B(x) \\
\Gamma, x:A \vdash f(x)=g(x) : B(x) \\
$$
Derive (write down the intermediate derivation tree) using $\eta$-...
1
vote
0
answers
102
views
Instantiate a HB class from its axioms
I'm trying to define the Dirac measure as a probability:
...
- 387