# Questions tagged [proof-assistants]

Applications that allow to create formal proofs. They assist the user by finding partial and checking complete proofs.

59 questions
Filter by
Sorted by
Tagged with
19 views

### Good Reference For Design And implementation Of Proof-Assistant

Hello I'm searching for any good review article or book about the design an implementation of a proof-assistant, something such as the Dragon book for programming language. My background is ...
65 views

### How to remove a universal quantifier in Lean theorem prover

I am working with two binary relations: g_o and pw_o, and I've defined pw_o below: constants {A : Type} (g_o : A → A → Prop) ...
45 views

### Why proving the solution of a problem is polynomial time is sufficient enough to say that it is a NP prolbem? [duplicate]

Why proving that we can verify the solution of a problem is polynomial time is sufficient enough to say that the problem is nondeterministic polynomial time? Please note: this is not a question on how ...
73 views

52 views

### What does Dv mean in $F\star$ language?

In the $F\star$ tutorial it says Dv, the effect of a computation that may diverge; what does diverge mean here? It's not explained and it confuses me. I guess ...
161 views

### Explanation of implication-introduction rule

I read in Proofs and Types by Girard et alii. the following excerpt that talks about the calculus of natural deduction: Now a sentence at a leaf (of the deduction tree) can be dead, when it no ...
123 views

### What are the implications of Lean not having the type Set?

In Coq we have an impredicative base type, called Prop, and a predicative base type, called Set, both of type ...
452 views

### How to Efficiently Define the Natural Numbers in Type Theory

A while ago I wondered about how Proof Assistants like Coq prove $m \leq n$ and the like. It looks like they actually need to traverse the natural numbers based on the successor/predecessor ...
504 views

### Is Coq synthetic or analytic?

In CMU's HoTT course, lecture 1, which can be found here: https://scs.hosted.panopto.com/Panopto/Pages/Viewer.aspx?id=0945cc7f-48b7-4803-81af-e7193a3f461d At 33:52, Harper was giving parallel ...
154 views

### What to prove and how to prove it

In learning about proof theory, I am interested to know how to go about "proving properties of a program". I don't exactly see yet what needs to be proven, nor how to prove it, which leads to this ...
64 views

### Definition of InLeft and InRight

So in reading I have come across the terms "InLeft" and "InRight" and I am unable to find a concrete definition for it. I have found it used in the specification for COQ, and in some notes on ...
286 views

### Is Agda sound as a proof system?

I was browsing Agda's stdlib source code, since I was trying to get into it seriously and therefore wanted to know more. I was amazed at that Agda is way more developed than I thought and it's ...
129 views

### Find the loop invariant of the given while loop

I don't know how to find a loop invariant. I'm not sure where to start. Can anyone find the loop invariant of the given program and explain your method please. ...
79 views

### Agda: Which part does this type introduce universe inconsistency?

I was trying to prove following lemma, ...
291 views