Frequent Questions
175 questions
10
votes
1
answer
363
views
Alternatives to universe levels
All of the type theory based proof assistants that I have seen have an infinite hierarchy of type universes to avoid the type of types being a term of itself. Are there alternative systems which could ...
- 101
9
votes
2
answers
894
views
Construction of inductive types "the hard way"
Most theorem provers simply axiomize inductive types (or equivalently W types) in the abstract which is fine.
But I'm curious about explicit constructions of inductive types within the theory.
I ...
- 2,898
9
votes
1
answer
240
views
How does the elimination rule of the heterogeneous equality type imply a weak version of K?
A heterogeneous equality type has the former $$\cfrac{\Gamma\vdash A~\texttt{type} \quad \Gamma\vdash B~\texttt{type} \quad \Gamma\vdash a:A \quad \Gamma\vdash b:B}{\Gamma\vdash a\simeq b~\texttt{type}...
- 6,532
9
votes
0
answers
142
views
Has there been any work on automated translation of tactic proofs to everyday language?
There are times when I've completed a proof with a lot of backwards reasoning, and I've kind of lost the thread of what I've actually done. It would be nice if there was something that could ...
- 373
9
votes
3
answers
414
views
Could proof assistants be used to prove that some piece of code is free of bugs?
Formal verification is
the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of ...
- 731
8
votes
4
answers
255
views
What's the difference between a universe level and a natural number?
It seems that universe levels are just a type generated by a zero constant and a successor constructor (like in Agda), so why don't we adapt natural numbers as universe levels?
In Lean, it is also ...
- 6,532
8
votes
2
answers
356
views
What's “conservativity” in terms of type theory and how is it useful?
I have heard that an extension to a type theory can be said to be conservative, which means it may add new formulae to the original type theory, for example new type formers and their intro/elim rules ...
- 6,532
8
votes
2
answers
1k
views
Is it possible to make a proof assistant program based on ZFC?
I heard that many proof assistant programs are made based on the type theory.
For me, as a mathematician, when I met Coq at first, it is difficult to accustomed with it.
So I have a question.
Is it ...
- 387
7
votes
3
answers
263
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
2
answers
1k
views
How to run the main function in lean 4?
I am following the lean 4 tutorial and see a main function as follows:
...
- 2,662
7
votes
1
answer
582
views
How important is global choice (a la Lean, HOL Light, Isabelle/HOL) practically?
Choice is indispensable for much of modern classical mathematics. Therefore, most proof assistants offer it as part of their standard library. The most powerful version is sometimes called global ...
- 10.3k
6
votes
1
answer
254
views
Can we completely erase propositions in the type checker?
Related question on semantic side: How much of trouble is Lean's failure of normalization, given that logical consistency is not obviously broken?
Suppose we have an impredicative universe of ...
- 6,532
6
votes
1
answer
158
views
Architecture of Isabelle: What parts are written in SML? What parts are written in Scala? What does the boundary look like?
My question is based on this question, which asks about swapping out different SML implementations when building Isabelle.
I've read on Wikipedia that Isaballe is written in Scala and SML.
Based on ...
- 3,561
6
votes
2
answers
854
views
Is there a complete index of Lean 4 tactics?
I'm wondering if Lean 4 tactics are documented anywhere, in a way comparable to the API documentation for mathlib.
(Sorry for brevity...will edit if this is unclear.)
- 443
6
votes
0
answers
92
views
What are Generic Arguments in Coq and how are they structured in their OCaml code?
I was trying to figure out why it seems that in a Coq generic argument there seems to be 3 arguments to the constructor GenArg when according to me there should ...
- 383
6
votes
1
answer
795
views
How to install Lean-4 stable only?
I followed Lean documentation to install Lean 4 on my Ubuntu Linux (20.04 LTS) using the elan option described there, and updated it to Lean4 ...
- 2,662
6
votes
0
answers
202
views
How does one systematically traverse OCaml representations of Coq ASTs terms?
I want to be able to (tree) traverse Coq terms (e.g. in OCaml or using their s-expression representation in any language).
My main challenge is to figure out how to do this systematically because I ...
- 383
6
votes
0
answers
158
views
Is there a consolidated or partial list noting the use of quasiquotation with provers?
In checking to see if any provers (proof assistants, theorem provers, interactive theorem prover) make use of quasiquotation I was quickly surprised at what started showing up with a Google search.
...
- 2,856
6
votes
1
answer
175
views
Does Agda have breaking changes?
Since Agda is software and sometimes software has breaking changes, e.g. Python 2 vs Python 3 (ref), does Agda have any significant breaking changes that one would need to be concerned about?
Also ...
- 2,856
5
votes
2
answers
246
views
Standard ML is used for many proof systems. Is there a recommended implementation to use for Isabelle?
Is there a recommended implementation of Standard ML to use for Isabelle?
Note: An answer should strive to include why that implementation (noted in build instructions is acceptable). While not needed ...
- 2,856
5
votes
1
answer
343
views
Why can addition be used in pattern matching Nats but not multiplication
Here's a simple dummy function in Lean 4:
def foo : Nat → Nat
| (m*2) => m
| (m+2) => m
| (m+1) => m
| (0) => 0
Lean has no trouble ...
- 253
5
votes
1
answer
203
views
List of general purpose Coq sublanguages for defining custom tactics
I've been tweaking the Coq plugin template recently to try to get a feel for writing custom Coq tactics in OCaml.
It's tricky. You need to define an .mlg file (...
- 3,561
5
votes
3
answers
2k
views
Are there computable functions which can't be expressed in Lean?
Lean, unlike e.g. Haskell, makes you prove that recursive definitions of functions will eventually terminate, if the compiler can't do it by using structural recursion, by using ...
- 53
5
votes
0
answers
230
views
An algorithm for the substitution of formulas for predicates in first order logic
I am trying to find a detailed description of the definition of substitution of formulas for predicates in first order logic and an implementation of this as a function in Lean or Haskell. The aim is ...
- 439
5
votes
1
answer
767
views
Graph Theory in Lean
I can't find an implementation of graph theory in Mathlib. Am I overlooking the file, or is it particularly difficult to do this, or has no one been interested in taking this on yet?
If it hasn't been ...
- 516
5
votes
2
answers
347
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
3
answers
931
views
Creating a proof assistant for first order logic in Haskell
I am planning to implement a FOL proof assistant in Haskell. What are some useful libraries and implementations I should be looking at?
Here are some further details. I have a simple proof checker for ...
- 439
5
votes
2
answers
248
views
Algorithm for the locally nameless representation used by Lean
I have heard that Lean uses the locally nameless representation for handling binders, yet if I input an expression that has a bound variable in it, the bound variable is not displayed using its de ...
- 439
5
votes
1
answer
148
views
Libraries of formally stated theorems with proofs verified by humans
This answer by Kevin Buzzard talks, among other things, about incremental progress made in Lean's mathlib vs Isabelle.
There's a lot in that answer that I don't understand, but one thing that seems ...
- 3,561
5
votes
1
answer
719
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 ...
- 511
4
votes
1
answer
204
views
Error `Abstracting over the term leads to a term which is ill-typed` when doing a destruct
I'm trying to make a version of nth that cannot fail because it knows that the index is inbounds. So far, so good:
...
- 189
4
votes
1
answer
344
views
Natural deduction with coq assistant prover
I want to mimic natural deduction proofs in coq ; for instance the proof I made for "A /\ B -> B /\ A" is for now
...
- 143
4
votes
2
answers
234
views
what is needed to move from design by contract to using a more advanced prover?
In "normal" programming languages such as C++ we regularly use design by contract.
The absolute bare minimum for this is to define:
pre-conditions (expects)
post-conditions (ensures) &...
- 151
4
votes
3
answers
606
views
How to prove the termination of Ackermann in Lean?
I'm trying to write the Ackermann function and prove it terminates in Lean 4
...
- 141
4
votes
1
answer
76
views
When installing Agda does one have to be attentive to a version?
If I want to install Agda do I have to be attentive to versions, breaking changes, etc.?
A comment from an earlier question noted
Agda version for installed libraries
- 2,856
4
votes
2
answers
480
views
Is there a "standard" encoding or model of material set theory in type theory?
I am a little aware of various attempts to axiomize set theory within a theorem prover. Is there a standard kind of encoding of sets? An organic model to interpret set theories into? I would like to ...
- 2,898
4
votes
1
answer
127
views
How can I prove has_esp when using mathcomp.analysis?
How can I prove the following goal (which I believe to be true) using mathcomp.analysis?
...
- 167
3
votes
1
answer
148
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,561
3
votes
2
answers
399
views
How do you know a formal proof (mechanized within a Proof Assistant) really is correct?
Running a proof assistant as a user and focusing on a given formal proof, how can one assert that there are no unexpected errors or "bugs" that could invalidate the provided proof?
More ...
- 1,348
3
votes
4
answers
241
views
What provers are using quote, quotations or quasiquotations?
This is a related question to
Is there a consolidated or partial list noting the use of quasiquotation with provers?
for which it seems there is no answer. However as there might be an answer some ...
- 2,856
3
votes
1
answer
297
views
What is a pattern in dependent pattern matching?
I am trying to understand dependent pattern matching while reading Goguen, McBride, and McKinna (2006)'s paper, but couldn't quite grasp the concept. I know regular pattern matching in functional ...
- 2,662
3
votes
2
answers
219
views
Reference request for an introduction to higher-order logic
I'm looking for an introductory text or other materials on higher order logic, with a minimum of assumed background knowledge beyond first order logic.
- 439
3
votes
1
answer
420
views
3
votes
1
answer
396
views
Dependent replacement in Lean
I'm stuck on proving extensionality results for my dependent structures in Lean 4. It's turning out to be very difficult to show equalities for these dependent structures, since I require a kind of ...
3
votes
1
answer
182
views
Why unknown identifier for a declared variable in Lean 4
I'm trying to follow the Introductory Proof with Lean 4 - Natural Numbers but I get unknown identifier 'b' and the same happens with all the variables except ...
- 133
3
votes
1
answer
360
views
Definitional vs propositional equality
Theorem Proving in Lean highlights a distinction between definitional and propositional equality when creating recursive functions:
The example above shows that the defining equations for ...
- 283
2
votes
1
answer
279
views
Is type checking in "Ideal Lean" computably enumerable?
There are actually two type theoretic foundations of Lean given in Mario Carneiro's master's thesis. They are the same, except for how definitional equality is treated:
“algorithmic” definitional ...
- 10.3k
2
votes
0
answers
127
views
How can this code about square matrices be fixed?
I am writing code that involves square matrices and their square-symmetries, but I cannot get to the bottom of it: in particular, I aim to define matrix transformations (that actually compute ...
- 587
2
votes
5
answers
546
views
LEM, the halting problem, the curry-howard correspondence -> deep connection?
I posted the following on the math stackexchange, but it occurs to me that this might be a more (or at least equally?) appropriate forum:
It was recently said to me by a prominent mathematician, who I ...
user3074
2
votes
1
answer
73
views
Setup Autocorres and Use with Isabelle for C programs
In the past few days, I have read a few papers on Autocorres and I am excited about the tool and I want to use it in building my own C applications. At this point, I want to try it out but I am new to ...
user5121