Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [proof-assistants]

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

1
vote
1answer
32 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
15 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
19 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 ...
0
votes
0answers
18 views

A linear ordering of G that puts v before w iff there is no path from w to v [closed]

Is the following a good enough proof? Let $G'$ be the graph $G$ with an edge $e$ added from $v$ to $w$. We note that a linear ordering of the form we are looking for must respect all edges of $G$ ...
4
votes
2answers
145 views

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

This code depends on agda-stdlib: ...
2
votes
1answer
85 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
2answers
82 views
3
votes
2answers
381 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". ...
3
votes
0answers
41 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
37 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 ...
5
votes
2answers
112 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 ...
2
votes
1answer
91 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 ...
0
votes
0answers
58 views

proving the median in a min heap can be found in every level

I'm trying to prove that given a min heap with n distinct number with at least 3 nodes, that the median can be found in every level. I thought about trying to break the heap into to heaps according ...
3
votes
1answer
402 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
490 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
113 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 ...
0
votes
2answers
47 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
243 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
83 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
67 views

Agda: Which part does this type introduce universe inconsistency?

I was trying to prove following lemma, ...
0
votes
2answers
196 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
118 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
50 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
0answers
51 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
274 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
146 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
107 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
100 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
509 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
53 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
190 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
263 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
46 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
36 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
58 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
40 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
114 views

Structural induction on generic list

In preparation for an exam, I've come upon the following problem. Given the constructors : ...
5
votes
0answers
54 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
397 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
278 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
177 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
440 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 ...
3
votes
2answers
187 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
36 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 ...
4
votes
1answer
439 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 ...
16
votes
4answers
348 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 ...
5
votes
1answer
855 views

Euclidean Algorithm in Coq

Question How do I write more intuitive proofs of the two following results in Coq? ...
9
votes
2answers
1k 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, ...
0
votes
0answers
39 views

Recursive set - How to show a language is undecidable [duplicate]

I am currently working on the following task: A language L = {< M> | M(x) = x^2} is given. Now I need to show, that this language is not decidable. By the way, < M> is the Gödel number But ...