Episode #125 of the Stack Overflow podcast is here. We talk Tilde Club and mechanical keyboards. Listen now

Questions tagged [proof-assistants]

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

Filter by
Sorted by
Tagged with
43
votes
6answers
8k views

Learning Automated Theorem Proving

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. Note that these topics are not easily digested ...
20
votes
2answers
2k views

Recursive definitions over an inductive type with nested components

Consider an inductive type which has some recursive occurrences in a nested, but strictly positive location. For example, trees with finite branching with nodes using a generic list data structure to ...
19
votes
1answer
980 views

Types of Automated Theorem Provers

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. Which are the relevant automated theorem provers? I ...
16
votes
4answers
358 views

Has Anyone Actually Created a System that Writes Computer Programs from specification?

Has anyone ever actually written a system (software or detailed explanation on paper with simple examples) that generates computer programs? I input $Prime(x) \wedge x<10$ and it creates a program ...
16
votes
2answers
360 views

Why do some inference engines need human assistance while others don't?

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. Why is it that automated theorem provers, i.e. ACL2,...
15
votes
4answers
646 views

Is there a repository for the hierarchy of proofs?

I am self-learning proof assistants and decided to start on some basic proofs and work my way up. Since proofs are based on other proofs and so form a hierarchy, is there a repository of the hierarchy ...
15
votes
3answers
3k views

Why is unification so important to inference engines?

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. I keep reading about the Unification Algorithm. ...
11
votes
1answer
630 views

The “CPS” approach has done great harm to performance in SML/NJ; reasoning desired

In a comment to Learning F#: What books using other programming languages can be translated to F# to learn functional concepts? Makarius stated: Note that the "CPS" approach has done great harm to ...
10
votes
0answers
287 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 ...
9
votes
1answer
111 views

Can a type system serve as a proof assistant for foreign functions?

Given that: A language with very expressive type systems (e.g. Idris) can also have escape mechanisms like foreign function interfaces/unsafePerformIO. There are proof assistants that can be used to ...
9
votes
2answers
2k views

Theorem Proofs in Coq

Background I am learning assistance, Coq, on my own. So far, I have completed reading Yves Bertot's Coq in a Hurry. Now, my goal is to prove some basic results concerning the natural numbers, ...
7
votes
1answer
505 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 ...
6
votes
2answers
289 views

Can we prove that $1 + 2 + \dots + n = \frac{n(n+1)}{2}$ using a computer program?

Chapter 7 of The Haskell Road to Logic Math and Programming discusses induction and recursion. Haskell is strongly typed and we can define the natural numbers ...
6
votes
1answer
169 views

Looking for a book that derives and constructs a model checking application

I am teaching myself program verification and am currently learning proof assistants. I have the book Handbook of Practical Logic and Automated Reasoning which gives the proofs necessary for the ...
5
votes
2answers
492 views

Given the “programs as proofs” isomorphism, how do we know that the program isn't lying?

I've been studying constructive type theory (CTT) and one of the things that I'm not clear on is the proof part: Proving the correctness of a program in a form of a proof that's nothing but the ...
5
votes
2answers
168 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 ...
5
votes
1answer
150 views

Procedure to automatically solve field theorems in a SMT solver

I'm working with the Welder proof assistant. Basically, this system uses basic inference rules to modify the goal one wants to proof. At a latter step, the modified goals are passed to a SMT solver to ...
5
votes
1answer
945 views

Euclidean Algorithm in Coq

Question How do I write more intuitive proofs of the two following results in Coq? ...
5
votes
0answers
58 views

Can we simulate any dependent datatype with `Eq`?

Consider the canonical homogeneous equality type: Eq : (A : Set) -> A -> A -> Set, with constructor ...
4
votes
2answers
166 views

Why cannot match $ Bool \equiv Bool $ with $ refl $ while $1 \equiv 1$ can?

This code depends on agda-stdlib: ...
4
votes
2answers
410 views

What makes a proof assistant a proof assistant?

You open a code editor, define a syntax with lambdas, a few primitives. Then you invent some nice computation rules, some cool typing rules, and write a corresponding interpreter and "type checker". ...
4
votes
2answers
637 views

What is a quotient structure?

I was reading a paper here, and it mentioned "quotient structure" in the following sentence (third page, second paragraph of the paper) In order to obtain a representation of terms truly isomorphic ...
4
votes
1answer
477 views

Why are dependently typed languages such as Agda used for proofs, if supercompilers for simpler typed languages can do the same?

Proof assistants such as Agda can be used to assert properties about programs, such as "the double of a number is even". Interestingly, supercompilers can be used for the same purpose, creating ...
4
votes
2answers
199 views

Is there a fundamental reason/limitation, such as $P \not = NP$, that prevents computers from being able to do mathematics (proofs, etc.)?

I'm a student, so I apologise if this is an idiotic question: Is there a fundamental reason/limitation, such as $P \not = NP$, that prevents computers from being able to do mathematics (posing ...
4
votes
1answer
79 views

Agda: Which part does this type introduce universe inconsistency?

I was trying to prove following lemma, ...
4
votes
2answers
70 views

Explanation of proof of why connectedness is not conjunctively local of any order $k$

I was reading Minsky's and Papert's book on perceptrons and I was reading theorem 0.6.1 and I was having a hard time understanding it. The theorem was about proving that the property "connected" was ...
4
votes
1answer
153 views

What does it mean if we disable K-rule in Agda?

TL;DR: Can I say, "K-rule in Agda enables people to match $ \forall a.a \equiv a $ with $ refl $"? In https://agda.readthedocs.io/en/v2.5.4.1/language/without-k.html#without-k, K-rule is introduced ...
4
votes
1answer
214 views

Proof on tree size using Isabelle

I'm trying to learn a little bit about Isabelle and proofs in general, and it's uses in Programming Language Theory. I'm following a book, "Concrete Semantics with Isabelle/HOL". I'm still in the ...
3
votes
1answer
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 ...
3
votes
1answer
275 views

How come identity encodes absurdity

From P5 in this paper: https://hal.inria.fr/hal-01094195/file/CIC.pdf Using this purely functional part, it is possible to encode many int eresting notions. For instance ∀ C : Prop , C ...
3
votes
1answer
331 views

How would one prove the pigeonhole principle with a SAT solver?

Suppose I wanted to find a proof of the pigeonhole principle or show that no proof shorter than $L$ exists. I understand that proof-checking is in NP, so I could write a CNF formula that is ...
3
votes
1answer
256 views

Is it possible to implement dependent types by any object oriented language supporting inheritance and classes?

When I was reading Agda tutorial, I noticed resemblance between dependent type declarations and class definitions which I've been primarily used to work with. I'm not totally sure how much sense this ...
3
votes
2answers
253 views

Simple question COQ

I'm a beginner in the coq proof assistant, so sorry if my question is silly. I would like to prove properties of a mathematical object. For clarity I will describe an over-simplified version of my ...
3
votes
0answers
53 views

A book introducing proof theory needed (many-sorted FOL, classical non-Gentzen calculus, satisfiability in partial algebras, induction)

We define a signature as a triple $$\Sigma\ =\ (S,F,\mathrm{type})$$ where $S$ is a set of sorts, $F$ a set of $n$-ary function symbols $f$ of the type $\mathrm{type}(f)$ $=$ $(M_1,\dotsc,M_n\...
2
votes
1answer
458 views

Can we prove mathematical induction statements in Lisp?

My previous question Can we prove that $1 + 2 + \dots + n = \frac{n(n+1)}{2}$ using a computer program? has a problem that it tries to cover too much ground. Here is a related question motivated by ...
2
votes
2answers
142 views

How to prove this obvious theorem in type theory (LEAN prover)

I have the following code: ...
2
votes
1answer
53 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 ...
2
votes
1answer
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. ...
2
votes
1answer
126 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 ...
2
votes
0answers
48 views

How to lexically list sentences in peano arithmetic?

I am working on building a toy automated theorem prover, What I want to do is to efficiently generate sentences in peano arithmetic, that I can attempt to verify as True/False/requires-more-resources ...
2
votes
0answers
29 views

How does supercompilers relate to macro tree transducers?

Supercompilers can be used as a generalisation of deforestation of a functional program. Macro Tree Transducers composition can be used to the same effect, using a completely different approach. What ...
1
vote
3answers
150 views

Is Goedel's 1st theorem not algorithmically derivable?

First let me explain what I mean by algorithmically derivable. An algorithm must be able to come up with the proof without prior knowledge of the proof, in the same way mathematicians and computer ...
1
vote
2answers
66 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 ...
1
vote
1answer
63 views

Tool for generating all the consequences of the logical theory (general logic programming framework)?

I am reading article https://arxiv.org/pdf/cs/0511055v1.pdf (about defeasible deontic logic) and it mentions on page 10 the operator T that constructs extension (set of immediate consequences) from ...
1
vote
2answers
155 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 ...
1
vote
1answer
53 views

Number of words in $L$ of length $n$?

Be $L$ a formal language over the alphabet $\Sigma$. $L$ can be defined by induction: $L^0 = \{\epsilon\}$ and for $i>0: L^i = \Sigma*L^{i-1}$. Means that $|L^n|$ is the number of words in $L$ of ...
1
vote
1answer
118 views

Let M be an $\epsilon$-NFA and let $S\subseteq Q$. Prove $\epsilon (S) = \epsilon (\epsilon (S))$

Let M be an $\epsilon$-NFA and let $S\subseteq Q$. Prove $\epsilon (S)= \epsilon (\epsilon (S))$. I would like to prove this by contradiction but I don't know if my idea is correct. Definition of $...
1
vote
1answer
73 views

Which word could I use for the pumping lemma?

I have a problem to start my proof because I do not find a word $w$ where I can use the pumping lemma. Task: Be $\sum { =\left\{ a,b,c \right\} } $ and $S=\left\{ bx{ c }^{ m }|x\in { \left\{ a,b \...
1
vote
2answers
133 views

Structural induction on generic list

In preparation for an exam, I've come upon the following problem. Given the constructors : ...
1
vote
0answers
20 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 ...