Questions tagged [usage]

Questions asking how to properly and efficiently use Proof Assistants.

Filter by
Sorted by
Tagged with
5 votes
1 answer
167 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 ...
Jon's user avatar
  • 75
2 votes
1 answer
244 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 ...
Julián's user avatar
  • 143
2 votes
1 answer
75 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 ...
8bc3 457f's user avatar
  • 224
4 votes
1 answer
273 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 ...
user2013's user avatar
3 votes
1 answer
92 views

Universe polymorphism and modules in Coq

The following code (without universe polymorphism) is accepted by Coq (8.16.0) : ...
Dave's user avatar
  • 133
3 votes
0 answers
31 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 ...
Rincewind's user avatar
1 vote
1 answer
79 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 ...
Trebor's user avatar
  • 3,688
9 votes
1 answer
440 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&...
Trebor's user avatar
  • 3,688
10 votes
0 answers
159 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 ...
Trebor's user avatar
  • 3,688
11 votes
1 answer
227 views

How much duplication does universe polymorphism actually save us?

From my rough impression, in (formalizing) everyday mathematics we almost never use universe polymorphism in a way that stretches the proof-theoretic strength. It merely saves us some duplication. My ...
Trebor's user avatar
  • 3,688
12 votes
1 answer
320 views

Incorporating Markov's principle in various proof assistants

The Markov's principle states that if a Turing machine does not run forever, then it halts. Equivalently, if I have a function $f : \mathbb N \to \mathrm{Bool}$, such that I have proved that $\neg\neg ...
Trebor's user avatar
  • 3,688
15 votes
1 answer
327 views

Why should you "never resort to polymorphism when initiality would do"?

In the concluding statement of "universe hierarchies", Conor McBride calls it [...] that key lesson which I learned from James McKinna: never resort to polymorphism when initiality will do. ...
James Martin's user avatar
  • 1,015
2 votes
1 answer
145 views

Defining Lists and Prove Associativity of Append [closed]

When I saw this question asking what is the "Hello, World!" for proof assistants I immediately thought of that exercise. Not a long time after this answer by Couchy was proposed. Therefore, ...
Wno-all's user avatar
  • 1,088
5 votes
1 answer
77 views

General Guidelines and Tips for using Induction

There are many kinds of induction (induction over the natural numbers ⊂ structural induction ⊂ Noetherian induction), when do I use which flavour? And what should I keep in mind when doing proofs by ...
Wno-all's user avatar
  • 1,088
0 votes
1 answer
211 views

Can we use Proof Assistants beyond mathematics? [closed]

After receiving responses from this question as a Liberal Artist I'm interesting in other Proof Assistant appliances, beyond Mathematics and Software Verification. I was wondering: how one can use ...
taylor.2317's user avatar
  • 1,308
25 votes
3 answers
340 views

Examples of new mathematics discovered through formalization?

In his essay Why formalize mathematics?, Patrick Massot discusses several reasons behind why a working mathematician might be interested in proof formalization. One of the the reasons he discusses is, ...
46 votes
2 answers
1k views

Are some proof assistants better suited for given areas of math than others?

There are many different proof assistants out there, and I think it is reasonable to expect that more or less all results we prove in everyday mathematics can be proven in any of them. One nice way to ...
Wojowu's user avatar
  • 1,038
15 votes
3 answers
560 views

Proof Assistants for Vim Users

I remember the last time I was trying to get into proof assistants, I was discouraged by the lack of functionality for vim users. At the time, it seemed like a lot of powerful features (holes, etc) ...
HallaSurvivor's user avatar
7 votes
2 answers
688 views

How to run Agda?

I want to run Agda, but I do not know how to run functions. I need to run "Hello, World!"; how can I do this?
Fmbalbuena's user avatar
19 votes
2 answers
396 views

Usage and Importance of Proof Assistants

How would you explain so a beginner in simple terms why Proof Assistants are important, and how / why they are used?
taylor.2317's user avatar
  • 1,308
18 votes
3 answers
788 views

What is a Proof Assistant?

How would you explain to a beginner in simple terms, what a Proof Assistant is?
taylor.2317's user avatar
  • 1,308
25 votes
3 answers
809 views

What was the 1st Proof Assistant?

What was the first proof assistant? What was it used for? When and by who was it created? Is it still used today? And what was its purpose?
taylor.2317's user avatar
  • 1,308
9 votes
3 answers
367 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 ...
Glorfindel's user avatar