Questions tagged [applications]
Use this tag when the question is about using a Proof Assistant for a purpose, how would you apply the Proof Assistant to solve a particular problem. Do not use this tag if it relates to a software application. Do not use this tag to ask about apps.
38 questions
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
2
votes
1
answer
78
views
Benefit of having `r+` as a constructor of the regex type
I was looking at this paper.
https://cs.ioc.ee/~tarmo/papers/firsov-uustalu-cpp13.pdf
It describes an agda implementation that generates NFAs corresponding
to a given regular expression.
For the type ...
- 173
2
votes
1
answer
187
views
Need help to prove that a variable is extracted using pattern matching from a pair (or a dependent pair) in Lean 4
everyone! I'm new to Lean4, and I'm practicing to write a proof.
I write a function that returns several values, proofs or functions, and I pack them in a nested dependent pair. I wanna create new ...
- 21
2
votes
1
answer
127
views
Packaging Mathematical Structures in Coq: Help Understanding a Definition
Context
I am a relatively new user to Coq with a decent understanding of the basics of dependent type theory and am midway through chapter 2 of the Software Foundations Series of books. I want to ...
- 133
5
votes
1
answer
286
views
Universe polymorphism and Coq standard library
When developing in Coq with the Universe Polymorphism flag on, the standard library introduces unwelcome universe constraints because it is universe monomorphic.
Is there an alternative standard ...
- 107
1
vote
0
answers
72
views
Embedding proof assistance in an application
Context
Perhaps this is too open-ended a question for StackExchange, in which case I apologize, but otherwise here goes:
I have a project I'm toying around with, the core of which is what I'd call &...
- 111
2
votes
1
answer
749
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
3
votes
1
answer
300
views
Debug autorewrite in Coq
I often meet proofs using autorewrite which Coq takes a while to process for some reason. (Setoid rewriting)
I then manually figure out which rewrite rules were ...
- 244
4
votes
1
answer
332
views
Why is it hard to formalize informal proofs?
Say I have some informal but rigorous argument in line with eg real analysis. Currently, it is a massive PITA to do algebraic manipulations in proof assistants like Coq or Isabelle. However, in ...
- 41
5
votes
1
answer
137
views
Universe polymorphism and modules in Coq
The following code (without universe polymorphism) is accepted by Coq (8.16.0) :
...
- 214
10
votes
2
answers
2k
views
How can we formalize a game where each player is a program having access to opponent's code?
How can we define in a proof assistant (eg., Coq) a notion of a 2-player game, where each player is a program that has access to the opponent's source code?
Background: In Open Source Game Theory, we ...
3
votes
0
answers
59
views
.CoqMakefile.d required by CoqMakefile but not generated
I am trying to use CoqMakefile to automatically build my Coq project in Coq 8.15.2.
When I did this the compilation failed because a file ".CoqMakefile.d" was expected by make but did not ...
- 206
8
votes
2
answers
1k
views
Using proof assistants to generate fast code
Proof assistants allow to state that
$$A(BC) = (AB)C$$
with $A$,$B$,$C$ compatible matrices,
Is there a formal system that takes this sort of equations to choose among interpretation strategies of ...
- 263
1
vote
1
answer
167
views
Proving that applicative functors compose
For simplicity, here an applicative functor means (in a proof assistant based on dependent type theory) the Haskellian applicative functor, bundled with its equational laws.
This I can of course brute ...
- 4,772
13
votes
1
answer
1k
views
What are some good (bad) examples of "green slime"?
I know what this roughly is. But when I'm explaining to a friend, I have trouble pulling out examples from my head. Are there any minimal working examples (maybe "minimal non-working examples&...
- 4,772