Unanswered Questions
157 questions with no upvoted or accepted answers
22
votes
0
answers
568
views
Categorical semantics of Agda
I would like to know the state of the art regarding the categorical semantics of the type theory implemented by Agda — or at least some approximation of that type theory that is amenable to ...
- 3,190
20
votes
0
answers
234
views
What is known about performance bottlenecks in proof assistants?
Background
In my personal experience, the biggest bottleneck to broader adoption of proof assistants (in industry and mathematics) is the effort it takes to engineer proofs. (In lines of code, for ...
- 1,112
20
votes
0
answers
275
views
Can we automatically get around set-theoretic difficulties?
One of the main technical annoyances of working with (large) categories is the variety of set-theoretic difficulties that come about with it: if we use ZFC as background logic, then those large ...
- 1,013
15
votes
0
answers
211
views
Code generation from Locales and Sublocales in Isabelle
Problem Description
I stumbled on this limitation/misunderstanding several times when using locales and sublocales in Isabelle. As a minimal example, let us extend the locale from the example in ...
- 1,128
13
votes
0
answers
369
views
Unintentionally proven false theorem with type-in-type outside logic and foundations?
We are all familiar with Russell's paradox, and it is known that Per Martin-Löf proved that type-in-type is normalizing and consistent (which is false), by accidentally using an assumption in his meta-...
13
votes
0
answers
575
views
How to speed up Lean?
I've recently been writing my first somewhat serious proof in Lean. While doing that, I noticed that Lean gets slower very fast with increasing length of the proof (slower in the sense that whenever I ...
- 1,165
12
votes
0
answers
169
views
Rules for mutual inductive/coinductive types
Some proof assistants, like Agda and maybe Coq, allow families of mutually defined types, or nested definitions of types, in which some are inductive and others are coinductive. I have no idea what ...
- 3,190
12
votes
0
answers
197
views
Do any automated theorem provers have the ability to stop, save state, reboot computer, restore state, continue?
With automated theorem provers knowing ahead of time how long the search will take or even if it will find a solution is unknown. Often for long running searches one eventually just has to halt the ...
- 2,846
10
votes
0
answers
187
views
Is there a proof assistant (or an embedding) for the (co)end calculus?
A Higher-Order Calculus for Categories describes a system where you can conveniently perform manipulations with categories, functors, Yoneda embeddings etc. An example of the rules is: $$\frac{\Gamma ,...
- 2,846
10
votes
0
answers
318
views
What's "Swedish" style of doing type theory or proof assistants?
Jon Sterling said Conor McBride's universe polymorphism proposal to be:
seems to have worked well in Swedish experiments
I wonder, what does "Swedish" mean here? What kind of type theory ...
- 1,165
10
votes
0
answers
175
views
What are the practical differences between intensional and extensional type theories?
It is already proved that MLTT with equality reflection is equivalent to MLTT with an intensional equality, plus UIP and function extensionality. So theoretically the differences between intensional ...
- 4,025
9
votes
0
answers
308
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 ...
- 91
9
votes
0
answers
133
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
8
votes
0
answers
172
views
Graph algorithms in Coq
We’re looking for a good library for reasoning about graphs in Coq. Some key features with would want to support include:
Topological sorting (ideally along with other graph algorithms)
Manipulation ...
- 81
8
votes
0
answers
298
views
What would a fully classical and fully univalent ITP and library look like?
Consider two developments in dependent type theory:
Lean’s mathlib library (as well many other ITP libraries) is unashamedly fully classical. There is no ...
- 9,105
7
votes
0
answers
81
views
How do I write a minimal working example (MWE) in Coq to demonstrate some problem?
To get help with some incomplete proof script or definition in Coq, or demonstrate some failing (e.g., Ltac) tactic or command, I am often asked to write a minimal working example (MWE) of Coq ...
- 425
7
votes
0
answers
102
views
How to improve/understand typechecking performance in Agda?
I've recently been trying to do some basic formalization of category theory in Agda. As part of this I need to prove a bunch of basic properties around products/monoidal categories. A bunch of these ...
- 171
7
votes
0
answers
195
views
What was the first proof assistant with eta equality for records?
The Agda language supports eta equality for (non-(co)inductive) record types:
...
- 506
7
votes
0
answers
92
views
What is focusing and how do I use it?
I have heard the term "focusing" with respect to the sequent calculus (System LK) and related calculi like the $\bar{\lambda} \mu \tilde{\mu}$-calculus. What is focusing and how do I use it?
...
- 2,868
7
votes
0
answers
163
views
Tutorial implementations of extensional type theories
There are cool projects out there that covers the basic principles of implementing dependent type theories as very spartan proof assistants. These projects helped a lot when I learned about (...
- 4,025
7
votes
0
answers
78
views
Is any theorem prover able to prove quadratization relations without knowing the proof strategy that humans used?
Motivation
In discrete optimization, our goal is often to optimize a function of binary variables, such as:
$$\tag{1} {\scriptsize
5 - 3b_1 - b_2 - b_3 + 2b_1b_3 - 3b_2b_3 + 2b_1b_2b_3 - 3b_4 + ...
- 1,165
7
votes
0
answers
147
views
Could the Incredible Proof Machine work automatically with Metamath if rules of Metamath can be automatically translated into IPM custom logic blocks?
The Incredible Proof Machine (pdf) is a visual means of doing proofs.
The Incredible Proof Machine can also be extended to do custom logics (Section 2.7 Custom logics).
Metamath has thousands of ...
- 2,846
6
votes
0
answers
98
views
What are "empty compositions", and why are they bad?
Empty hcomps and empty systems are often mentioned in the context of cubical type theory, in particular related to the efficiency of evaluation, for example here and here. What exactly are they, and ...
- 4,025
6
votes
0
answers
170
views
Coq - Are there functions which are provably equal but not definitionally equal?
In Coq, are there types A,B and functions f, g : A -> B such that f = g propositionally ...
6
votes
0
answers
182
views
How does the modality-based irrelevance compare to universe-based irrelevance (`Prop`)?
I understand proof irrelevance implementation as one of the two language features listed below:
Prop as SProp in Coq or ...
- 6,306
6
votes
0
answers
120
views
In VSCoq, how to issue an arbitrary Gallina query via the prompt?
I’m currently trying out Visual Studio + VSCoq, having previously used Emacs + Proof General for Coq, and there’s one part of my usual workflow that I haven’t managed to replicate yet. Is there a way ...
6
votes
0
answers
82
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 ...
- 9,105
6
votes
0
answers
189
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 ...
- 136
6
votes
0
answers
136
views
How to write heavily indexed proofs?
I've been playing with hereditary substitution. However, things get very awkward because substitution isn't total unless you index by the environment somehow.
In my old approach terms were not indexed ...
- 2,868
6
votes
0
answers
114
views
Is every logical theory embeddable in a dependently typed extensional type theory?
In category theory by the Yoneda embedding every category $\mathcal{C}$ is a subcategory of a category of presheafs $[\mathcal{C}^{\text{op}}, \text{Set}]$. Every category of presheafs is a topos and ...
- 2,868
6
votes
0
answers
156
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,846
6
votes
0
answers
232
views
Can Agda proofs be trusted and do they conform to a specific, well-defined type theory?
When using Agda proofs, how can you know whether to trust it? Also, do they conform to a specific, well-defined type theory?
Credit
- 9,722
6
votes
1
answer
197
views
Tools to formally verify programs written in languages supported by the GNU Compiler (GCC)
Is there a website that maintains a list, or is there a list, of tools that support verification of programs written in languages supported by the GCC compiler front ends: C, C++, Objective-C, Fortran,...
- 406
5
votes
0
answers
244
views
Mere propositions and Consistency with Impredicativity, Excluded Middle and Large Elimination
Setup
Current Understanding
I've recently been trying to learn about the interaction of Impredicative Polymorphism, Large Elimination and Excluded Middle (notably, inconsistency). Notably, this is ...
- 73
5
votes
0
answers
229
views
Proof-theoretic strength of HOL compared to predicative dependent types
By HOL I mean something like inference rules of HOL Light with the 3 axioms of infinity, extensionality and choice ($\varepsilon$ operator).
By predicative dependent types, I am thinking of MLTT + W-...
- 547
5
votes
0
answers
168
views
What are the conditions for Agda to detect that induction-recursion has a least fixed point?
This is a 3rd in a series of questions, spurred by my attempts to encode an argument by Danielsson [1] [2] regarding existence of syntactically non-strictly positive datatype.
The idea (rephrased):
...
- 107
5
votes
0
answers
111
views
Can we bring unification results under cofibrations outside?
Say we have an elaborator which supports metavariables and solve them on flex-rigid cases (with the obvious occurrence checking and scope checking). If we do such unification under a cofibration, do ...
- 6,306
5
votes
0
answers
220
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 ...
- 429
5
votes
0
answers
108
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.
- 2,290
5
votes
0
answers
163
views
Prove equality in a record type
I am trying to prove something about monoids an categories. This results in the following (partial) proof:
...
- 265
5
votes
0
answers
95
views
What is the relation of $\lambda^\to$ and $\lambda^{\to\times}$ to cartesian closed categories?
I am learning about the categorical semantics of type theory. I've written some preliminary results in Agda. In particular, I partially proved that the contexts and substitutions of simply-typed ...
- 4,025
4
votes
0
answers
69
views
Automatic proofs concerning inequalities
I've heard that Isabelle can be used to get automatic answers to questions like this:
lemma "∃ x :: real . 2 /3 < x ∧ x < 3 /4"
Of course, this one ...
4
votes
0
answers
40
views
Implementing object-logics in Isabelle Best Practices?
I'm patching up Isabelle/Mizar to work with Isabelle2023, and I am wondering what are the best practices for implementing an object logic in Isabelle? (Usually there is great documentation for ...
- 1,574
4
votes
0
answers
120
views
Proving "proof methods" as theorems in type-theory based proof systems
For example, suppose we have proved associativity of some binary operator $+ : T \to T$ as
add_assoc : forall (x y : T), x + y + z = x + (y + z).
We can thus prove ...
- 41
4
votes
0
answers
64
views
Using CoqHammer from Ltac2
As it seems most likely to me, due to the special way arguments are evaluated in CoqHammer tactics (I tried to read the source code in OCaml but unfortunately I didn't understand much of it), it is ...
4
votes
0
answers
106
views
Independence of function extensionality
Who first realized that function extensionality cannot be proved within vanilla MLTT, or some variations of it? Now to my knowledge the simplest way to show this is by syntactic models. But surely ...
- 4,025
4
votes
0
answers
32
views
How to prove that a non-negative nat is positive in J-Bob?
I am trying to prove the following fact while learning the J-Bob language: that any non-negative natural number is positive (with my proof attempts below).
The fact seems simple enough. However, I ...
- 2,210
4
votes
0
answers
293
views
Does Lean have a function that reads a file "at compile time"?
Is there some "pure" function that reads a file before the program is type-checked and returns its contents as a string or something, for example if the file ...
- 161
4
votes
0
answers
152
views
Does Lean 4 have syntax to refer to the current thing being defined?
If I am defining a function (using def for example) then is there some way to refer to the function being defined inside its definition without using the name of ...
- 41
4
votes
0
answers
180
views
Is it possible to have a cubical type theory with pattern matching on the identity path?
We have the lovely dependent pattern matching on refl constructor of identity type in systems like Agda, but the same feature is missing for Cubical Agda. People ...
- 6,306