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
0
votes
1answer
62 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) ...
1
vote
0answers
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 ...
0
votes
1answer
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 ...
4
votes
1answer
149 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 ...
2
votes
1answer
51 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 ...
1
vote
1answer
72 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
0answers
28 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?
0
votes
0answers
31 views

Computational type theorists: how do you compare terms for equality here?

I am attempting to implement Simple Type Theory in the language D. How do you compare subterms to a term $R$ for the sake of computing the covering abstractors of $R$ in $M$? By reference (class ...
4
votes
2answers
160 views
2
votes
2answers
120 views
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
119 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 ...
4
votes
2answers
404 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". ...
5
votes
2answers
144 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 ...
1
vote
2answers
148 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 ...
3
votes
1answer
445 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 ...
7
votes
1answer
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 ...
1
vote
2answers
62 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 ...
10
votes
0answers
283 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 ...
2
votes
1answer
124 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. ...
4
votes
1answer
78 views

Agda: Which part does this type introduce universe inconsistency?

I was trying to prove following lemma, ...
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 ...
0
votes
2answers
277 views

greedy algorithms - minimizing total payment

The question: I want to buy $n$ books. In the book store there's a big sale according to which, if you buy three books, then the cheapest book in any triplet costs only 20% of its full price. Let $...
2
votes
1answer
244 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 ...
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 ...
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 ...
1
vote
0answers
72 views

Universal theorem proving algorithms for sequent calculus (e.g. for cut-free logics)?

Some of the logics admit Gentzen-style sequent calculus. Are there universal algorithms that allow to find proof (derivation of the proof) in sequent caculus for every hypthetical theorem? Some of ...
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 ...
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 ...
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 ...
9
votes
1answer
109 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 ...
4
votes
2answers
607 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
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
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 ...
3
votes
1answer
309 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 ...
1
vote
0answers
51 views

Use of Mizar for algorithm specification and automatic analysis and discovery of algorithms?

Is it possible to use Mizar Mathematical Library for the specification of algorithms at the same detalization level as the implementation of the algorithm in industrial programming language? Mizar ...
0
votes
0answers
39 views

How far meta-logical frameworks are from universal logic?

I am investigating metalogical-frameworks like Isabelle/Pure (very few information), http://twelf.org/wiki/Main_Page, http://abella-prover.org/ for encoding of new logics. And natural question arises -...
1
vote
1answer
61 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 ...
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 ...
1
vote
2answers
132 views

Structural induction on generic list

In preparation for an exam, I've come upon the following problem. Given the constructors : ...
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 ...
2
votes
1answer
457 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 ...
6
votes
2answers
288 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 ...
4
votes
1answer
208 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 ...
5
votes
2answers
485 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 ...
4
votes
1answer
470 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 ...
3
votes
2answers
246 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 ...
0
votes
2answers
37 views

Proof for factors of a number

I was trying to prove the following: if x%(x/2) != 0 or x%(x/2) == 0 then x%(x/y) != 0 or x%(x/y) == 0 such that y = [2,4) So I am trying to figure out ...
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 ...
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 ...