Unanswered Questions
20 questions with no upvoted or accepted answers
20
votes
0
answers
243
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,142
6
votes
1
answer
209
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,...
- 436
5
votes
0
answers
116
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,330
4
votes
0
answers
142
views
How do I write a definition/theorem with an arbitrary number $n$ of types?
I am trying to use mathlib to write the definition of a monoidally well-pointed monoidal category. This definition goes like: For all parallel pairs of morphisms $f, g : A_1 \otimes \cdots \otimes A_n ...
- 41
4
votes
0
answers
125
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
3
votes
0
answers
71
views
Manipulating Summations ∑ and telescopic sums in Lean 4
I want to prove the following lemma:
...
3
votes
0
answers
54
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 ...
- 2,662
3
votes
0
answers
101
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
0
answers
47
views
Countermodel generators for constructive logics
Is there any software out there that can generate countermodels in some form for non-theorems in a constructive logic? I am especially interested in generating countermodels for theorems that are ...
- 3,561
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
0
answers
101
views
Proof Checking for State Machines Similar to TLA+
I'm wanting to find a modern proof assistant that I can use for modeling distributed systems or similar protocols/algorithms.
TLA+ is the most commonly used language in that field, but I recently ...
- 11k
2
votes
0
answers
43
views
Problem working with FMapWeakList and Parametrized Records
Consider the following definition of a record R, parametrized over an arbitrary eqType:
...
- 65
2
votes
0
answers
111
views
Algebraic manipulation: what is the best tool?
I have a set of algebraic axioms. I need to prove an equation, an algebraic law. What I did was applying "trivial" rewrite rules by a theorem prover from both ends, and then an automatic ...
- 323
2
votes
0
answers
85
views
Formally verified email or communication?
This question is contextualized by having an account hacked which is prompting me to move towards something I’ve long wanted to anyway.
I would like to consider the simplest possible formally verified ...
1
vote
0
answers
30
views
ACL2 and modular arithmetic
I'm trying to prove Motrellin's lemma in ACL2.
$$ \forall m, n \in \mathbb{N} \mathop. 2m = 3n \to 2 \mid n $$
I recently completed a very long-winded Coq proof of it and I'm trying to figure out how ...
- 3,561