Questions tagged [proof-assistants]

Applications that allow to create formal proofs. They assist the user by finding partial and checking complete proofs. General questions about proof assistants can also be asked on the Proof Assistants Stack Exchange site.

Filter by
Sorted by
Tagged with
48 votes
6 answers
10k 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 ...
Guy Coder's user avatar
  • 5,101
23 votes
2 answers
3k 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 ...
Gilles 'SO- stop being evil''s user avatar
21 votes
4 answers
4k views

How hard would it be to state P vs. NP in a proof assistant?

GJ Woeginger lists 116 invalid proofs of P vs. NP problem. Scott Aaronson published "Eight Signs A Claimed P≠NP Proof Is Wrong" to reduce hype each time someone attempts to settle P vs. NP. ...
Isinlor's user avatar
  • 325
20 votes
1 answer
1k 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 ...
Guy Coder's user avatar
  • 5,101
18 votes
3 answers
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. ...
Guy Coder's user avatar
  • 5,101
17 votes
4 answers
406 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 ...
user avatar
16 votes
4 answers
983 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 ...
Guy Coder's user avatar
  • 5,101
16 votes
2 answers
462 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,...
Guy Coder's user avatar
  • 5,101
12 votes
1 answer
852 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 ...
Guy Coder's user avatar
  • 5,101
10 votes
2 answers
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, ...
user11942's user avatar
  • 161
10 votes
0 answers
454 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 ...
Jason Hu's user avatar
  • 632
8 votes
1 answer
577 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 ...
Jason Hu's user avatar
  • 632
8 votes
2 answers
688 views

What are the implications of Homotopy Type Theory?

I've recently come across the topic of homotopy type theory and I'm interested to learn more. I have a very limited background in type theory. Can anyone tell me, in functional programming terms or ...
thoughtpolice's user avatar
8 votes
1 answer
176 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 ...
dukereg's user avatar
  • 295
6 votes
2 answers
710 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 ...
PhD's user avatar
  • 337
6 votes
2 answers
801 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". ...
MaiaVictor's user avatar
  • 4,127
6 votes
2 answers
348 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 ...
john mangual's user avatar
  • 1,951
6 votes
1 answer
256 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 ...
Guy Coder's user avatar
  • 5,101
6 votes
1 answer
1k 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 ...
MarkokraM's user avatar
  • 385
5 votes
4 answers
959 views

Curry-Howard isomorphism and non-constructive logic

My understanding of the Curry–Howard correspondence is that it shows an isomorphism between constructive logic (also called intuitionistic logic) and computer programs in appropriate typed languages. ...
Weier's user avatar
  • 231
5 votes
2 answers
1k 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 ...
alim's user avatar
  • 1,014
5 votes
2 answers
603 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 ...
user1868607's user avatar
  • 2,194
5 votes
2 answers
139 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 ...
Charlie Parker's user avatar
5 votes
1 answer
729 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 ...
Lance's user avatar
  • 2,223
5 votes
2 answers
497 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 $ \mathit{refl} $"? In https://agda.readthedocs.io/en/v2.5.4.1/language/without-k.html#without-k, K-...
ice1000's user avatar
  • 940
5 votes
1 answer
193 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 ...
user1868607's user avatar
  • 2,194
5 votes
1 answer
1k views

Euclidean Algorithm in Coq

Question How do I write more intuitive proofs of the two following results in Coq? ...
user11942's user avatar
  • 161
5 votes
0 answers
65 views

Can we simulate any dependent datatype with `Eq`?

Consider the canonical homogeneous equality type: Eq : (A : Set) -> A -> A -> Set, with constructor ...
Joey Eremondi's user avatar
4 votes
2 answers
239 views

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

This code depends on agda-stdlib: ...
ice1000's user avatar
  • 940
4 votes
1 answer
582 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 ...
dokkat's user avatar
  • 121
4 votes
1 answer
123 views

Agda: Which part does this type introduce universe inconsistency?

I was trying to prove following lemma, ...
Jason Hu's user avatar
  • 632
4 votes
1 answer
331 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 ...
Amaral's user avatar
  • 41
4 votes
2 answers
400 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 ...
formalizer's user avatar
4 votes
0 answers
288 views

Can every sentence of first-order logic be converted into an equisatisfiable equation in Boolean algebra?

There may be some theoretical literature, unknown to me, that addresses this question. If possible, I would like a practical approach to this problem. My attempt involves the use of an equational ...
Patrick Browne's user avatar
3 votes
2 answers
279 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 ...
The Pointer's user avatar
3 votes
1 answer
504 views

How to get an element from an existential proposition in Type theory proof assistant (Lean prover)

I am trying to implement set theory in type theory from scratch, just for self pedagogical purposes. Specifically, I'm using the Lean Prover, and defining the element-of relation from scratch using ...
user56834's user avatar
  • 3,752
3 votes
1 answer
284 views

Building non-classical logics in Agda & Coq

Is it possible to construct different systems of logic in Coq or Agda? I ask because I'm interested in using a proof assistant to construct (and verify) theorems in things like many-valued logics, ...
Kevin Flowers Jr's user avatar
3 votes
1 answer
286 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 ...
Jason Hu's user avatar
  • 632
3 votes
1 answer
1k 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 ...
Elliot Gorokhovsky's user avatar
3 votes
1 answer
254 views

Is mutual inductive type definition essential in coq core language?

I'm studying Coq's core language and I found that mutual inductive type definition is in it. https://coq.inria.fr/refman/language/core/inductive.html#theory-of-inductive-definitions Before I read the ...
12412316's user avatar
  • 133
3 votes
1 answer
146 views

Find a threshold such that one function is always bigger than the other

Given the recursively defined function $c$: $$c(m,n)=\begin{cases}0&\text{for }m=0\\ n^2+n+1&\text{for }m = 1\text{ and }n\ge 0\\ c(m-1, 1)&\text{for }m>1\text{ and }n=0\\ c(m-1,c(m,n-...
Monika's user avatar
  • 183
3 votes
1 answer
461 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 ...
user3368561's user avatar
3 votes
1 answer
77 views

The underlying type theory of HOL/Isabelle

Is there a good source on the type theory of HOL/Isabelle/other HOL-based LCF-style theorem provers?
xuq01's user avatar
  • 1,190
3 votes
0 answers
63 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\...
user avatar
2 votes
1 answer
615 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 ...
john mangual's user avatar
  • 1,951
2 votes
2 answers
627 views

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

I have the following code: ...
user56834's user avatar
  • 3,752
2 votes
1 answer
95 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 ...
ice1000's user avatar
  • 940
2 votes
1 answer
354 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. ...
the_martian's user avatar
2 votes
1 answer
170 views

Difference between $\Rightarrow$, $\Longrightarrow$ and $\rightarrow$ in Isabelle/HOL?

I haven't been able to find a good explanation of how these are different and relate to each other. I know that $\to$ is part of HOL and $\Rightarrow$ and $\Longrightarrow$ part of Isabelle, but it ...
user56834's user avatar
  • 3,752
2 votes
2 answers
289 views

Given an array $A$ and an index $c$, prove there always exists a subarray whose sum $\pmod {i} = 0$

Given an array $A$ of positive integers with size $m$ and an array index $c$ (indexing starts at $1$). Prove using mathematical induction over $m$ that there always exists a contiguous subarray $S$ in ...
Monika's user avatar
  • 183