Questions tagged [proof-assistants]

A proof assistant is an application program that helps humans construct machine-checked proofs.

Filter by
Sorted by
Tagged with
2
votes
0answers
60 views

Small kernel (i.e. proof-verifier) for Agda?

Proof-assistants usually include a lot of machinery that assists in the creation of proofs. The creation process may be unsound without risking the soundness of the proof-assistant if the alleged ...
6
votes
1answer
218 views

Fixed set of type constructors to simulate all intensional inductive families?

I'm wondering, are there small dependent calculi that can simulate a language with inductive families (that is, has a type isomorphic to each inductive family, at least as powerful of induction ...
6
votes
1answer
152 views

Structural equality of Pi Types with heterogeneous equality?

I'm trying to implement a proof of the following type: ...
2
votes
2answers
189 views

Representations of Planar Graphs in Coq

I would like to formalize some simple properties of planar graphs in the Coq proof assistant. 1) How are planar graphs formalized in the Coq proof assistant? Is there a "standard" definition that is ...
4
votes
0answers
49 views

Formalization of Interval Newton methods in a proof assistant or theorem prover

I am undertaking the task of formalizing Interval Newton Methods in Isabelle. To the best of my knowledge this hasn't been formalized in other proof assistants or theorem provers. However, I want to ...
6
votes
2answers
99 views

Formal semantics of tactics

Tactics are supposed to represent inference rules in a system, and it might seem unnecessary at first to formalize the semantics of tactics; nevertheless, modern theorem provers can have pretty ...
5
votes
0answers
182 views

Is Agda sound as a proof system? [closed]

I've asked the same question on CSSE but with no luck (https://cs.stackexchange.com/questions/89611/is-agda-sound-as-a-proof-system). Therefore I ask it again here in cstheory and hope that more ...
18
votes
1answer
501 views

Formally Verified Complexity Theory

Is there any ongoing project to formally verify the theorems and proofs of complexity theory using a proof assistant like Coq? Are there any boundaries to doing this?
0
votes
1answer
149 views

Is Buchberger's algorithm or Wu's method valuable theoretically when we have the Tarski–Seidenberg theorem?

Is Buchberger's algorithm or Wu's method valuable theoretically when we have the Tarski–Seidenberg theorem? In other words, could the Tarski–Seidenberg theorem subsume Buchberger's algorithm and Wu's ...
5
votes
1answer
117 views

Using ϵ -unification and Knuth-Bendix completion to automatically proof theorems about groups

This is a follow-up question. In my previous question, I presented Welder proof assistant and I stated that I want to automate proofs about basic field theory. The only answer to this post states that ...
6
votes
3answers
282 views

Proving running time upper bounds for algorithms in dependent type theory

Proof assistants are a valuable tool for verifying the correctness of proofs of mathematical theorems. When dealing with proofs of correctness of algorithms, one is not only interested on showing ...
10
votes
3answers
849 views

What should a proof of correctness for a typechecker actually be proving?

I've been programming for several years, but am very unfamiliar with theoretical CS. I've recently been trying to study programming languages, and as part of that, type checking and inference. My ...
14
votes
2answers
466 views

Proof assistant usage in complexity theory research?

Considering the topics covered at a conference like STOC, are any algorithm or complexity researchers actively using COQ or Isabelle? If so, how are they using it in their research? I assume most ...
8
votes
0answers
183 views

Is there a known automatic proof of the independence of the continuum hypothesis?

In 2002, L.C. Paulson gave a mechanized proof of the consistency of the axiom of choice by formalizing $V=L$ and its consistency. We could ask whether there is a formalized proof of the independence ...
29
votes
1answer
1k views

Has a proof checker bug ever invalidated a major proof?

Most (all?) proof assistants have soundness bugs fixed on occasion. However, from those I've seen these bugs are usually difficult to come across unintentionally, and results proved before the bug is ...
5
votes
1answer
316 views

Where is the quote “Informal proofs are algorithms, formal proofs are code” from?

Does anyone know the origin of the quote, Informal proofs are algorithms; formal proofs are code. Its made in Benjamin C. Pierce et al.'s Software Foundations.
6
votes
1answer
174 views

Is there a theory of overloading types?

There is a sound theory of overloading operators and functions realized by type classes in Haskell, and to rougher extent by traits in Rust, etc. In mathematics however, there are many situations ...
2
votes
1answer
82 views

Proof software for Primitive Recursive Arithmetic

Primitive Recursive Arithmetic is a critical foundational system in mathematics at large, and all the more so in areas studying constructive reasoning and/or computability such as Theoretical Computer ...
8
votes
1answer
578 views

Humanifying computer-generated or computer assisted proofs

I remember reading a blog post displaying two versions of the same proof, one written by a human and the other by a machine, and asked the readers to tell which is which. Trying to google the post ...
7
votes
1answer
182 views

Formalized priority argument

A priority argument, an important proof technique in recursion theory, was introduced by Friedberg and Muchnik, to solve Post's Problem, i.e., the existence of two r.e. sets that do not Turing reduce ...
22
votes
5answers
821 views

Curious about computer-assisted NP-completeness proofs

In the paper "THE COMPLEXITY OF SATISFIABILITY PROBLEMS" by Thomas J. Schaefer, the author has mentioned that ...
16
votes
1answer
1k views

Formalizing Homotopy Type theory in Idris

Looking at the homotopy type theory blog one can easily find a lot of library formalizing most of Homotopy Type Theory in Agda and Coq. Is there anyone aware if there is any similar attempt to ...
1
vote
0answers
113 views

looking for notable applications of ASP (Answer Set Programming) in TCS

a recent difficult question of interest to the group[1] by GB has possibly led to verification of a new graph property by dspyz, by use of Answer Set Programming/ASP. via sophisticated logic ...
26
votes
1answer
516 views

Interesting algorithms in the formalization of the Feit-Thompson theorem?

It looks like George Gonthier and his collaborators have finished formalizing the Odd Order Theorem. In his earlier work on the Four Color Theorem, Gonthier invented a bunch of new algorithms (...
-2
votes
1answer
545 views

Coq definition with unusual syntax (Definition … Defined.)

While examining the package Library ZFC.Sets, I found the following definition: ...
14
votes
0answers
290 views

Proof assistant formalizations of Finite Model Theory

I'm wondering if anyone knows of a formalization (even limited) of any part of finite model theory in any of the major proof assistants. (I'm most familiar with Coq, but Isabelle, Agda, etc. would ...
16
votes
3answers
1k views

What is the role of predicativity in inductive definitions in type theory?

We often want to define an object $A \in U$ according to some inference rules. Those rules denote a generating function $F$ which, when it is monotonic, yields a least fixed point $\mu F$. We take $A :...
40
votes
4answers
3k views

How would I go about learning the underlying theory of the Coq proof assistant?

I'm going over the course notes at CIS 500: Software Foundations and the exercises are a lot of fun. I'm only at the third exercise set but I would like to know more about what's happening when I use ...
44
votes
3answers
3k views

How do 'tactics' work in proof assistants?

Question: How do 'tactics' work in proof assistants? They seem to be ways of specifying how to rewrite a term into an equivalent term (for some definition of 'equivalent'). Presumably there are formal ...
18
votes
1answer
3k views

Prove proof irrelevance in Coq?

Is there a way to prove the following theorem in Coq? Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2. EDIT: An attempt to give a brief ...
12
votes
6answers
2k views

Proof assistant for writing mathematics

I'd like to write mathematical proofs using some proof assistant. Everything will be written using first order logic (with equality) and natural deduction. The background is set theory (ZF). For ...
28
votes
1answer
826 views

Is there a reasonable automated proof system for TCS theorems?

Suppose I wanted to formalize Turing's proof regarding the halting problem so that a machine could check it. Some of the well-known automated theorem proving systems include Mizar, Coq, and HOL4. I ...
14
votes
1answer
5k views

How to define a function inductively on two arguments in Coq?

How can I convince Coq that the recursive function given below terminates? The function takes two inductive arguments. Intuitively, the recursion terminates because either argument is decomposed. ...
47
votes
3answers
4k views

Shallow versus Deep Embeddings

When encoding a logic into a proof assistant such as Coq or Isabelle, a choice needs to be made between using a shallow and a deep embedding. In a shallow embedding logical formulas are written ...
15
votes
2answers
990 views

Eliminating cofix in Coq proof

While trying to prove some basic properties using coinductive types in Coq, I keep running into the following problem and I cannot get around it. I've distilled the problem into a simple Coq script as ...