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
-3 votes
0 answers
38 views

Huffman and its enhancement technique called blocking

One enhancement for the Huffman coding algorithm is a technique known as blocking, in which blocks of size k input symbols are encoded simultaneously.Sketch a proof: For any set of input symbols and ...
user168526's user avatar
0 votes
1 answer
13 views

Transform OTM for Problem π to DTM ∈ DSPACE(n)

Given an Oracle Turing machine ($OTM$) that solves Problem π in max. 2n space, so $O(n)$ space and $O(n^2)$ time. Is there a DTM that can solve $π$ in $O(n)$ space if time doesn't matter? (The length ...
Theorynoob's user avatar
5 votes
4 answers
938 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
0 votes
1 answer
99 views

How to start with verifying a formal proof programmatically?

I heard the terms "theorem provers" and "proof assistants" tossed around before (which I assumed to be the same up until a couple seconds ago), and also of Coq, Idris, Agda, TLA+ (...
toraritte's user avatar
  • 105
0 votes
1 answer
51 views

Defining 2 inductive propositions relying on each other in Coq

I'm pretty beginner in Coq. I want to formalize negative and positive occurrence of an atom in a proposition inside coq the definition is as down below: I want to define this property as an Inductive ...
asha soroushpoor's user avatar
0 votes
0 answers
22 views

How do you prove a presence of GAN generated samples being exactly (or almost exactly) identical to real observations?

Suppose that $X\in\mathcal{X}$ is data in abstract space and $Z\in\mathcal{Z}$ is random noise vectors in latent space over a defined prior $P(Z)$ (e.g., Gaussian). Then, let $G$ and $D$ denote ...
auckydocky's user avatar
0 votes
2 answers
838 views

DFA and NFA Equivalence Proof

I'm taking a Theory of Computation class and we went over the proof to show that for any NFA there is an equivalent DFA, which I understand the proof fully in this case. But if it were in reverse, for ...
KJC_'s user avatar
  • 1
1 vote
1 answer
150 views

Proving transitivity in an intuitionistic type theory without the K rule

In Agda, if I disable axiom $\mathbb{K}$ I'm not able to prove $$ \forall\{A : \textbf{Set}\}\{a\ b : A\}\{p\ q : a \equiv b\} \to p \equiv q, $$ which I guess is normal since the system does not ...
A confused dove's user avatar
3 votes
1 answer
274 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
2 votes
1 answer
164 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,692
0 votes
1 answer
92 views

Mechanically proving element non-membership

I'm facing a (possibly simple) problem while proving a theorem. I need to show that under several (true) assumptions, some element is not in a set. Such assumptions are all met and there is are ...
Chaos's user avatar
  • 543
0 votes
1 answer
85 views

What's so difficult about computer verifiable proofs?

What's so hard about creating a piece of software with as minimal as possible mathematical axioms, defining a formal language in which one can create new constructs based on the existing ones, and ...
user14789259's user avatar
0 votes
0 answers
37 views

Please help me fix / finish this Fitch proof, I am stuck

Using the Fitch application and only Intro and Elim rules (& REIT if necessary), prove that $$\forall x \forall y (P(x) \implies Q(y)) \iff (\exists x P(x) \implies \forall y Q(y))$$ is a logical ...
timmer's user avatar
  • 1
1 vote
1 answer
53 views

Need help understanding Knuth's proof that: The set of all pure words is well-ordered by the relation >

In the paper linked below by Knuth and Bendix, theorem 1: The set of all pure words is well-ordered by the relation '$>$' has a proof that I can't seem to follow despite staring at it all day. I ...
frabrooks's user avatar
1 vote
1 answer
79 views

Time complexity of algorithms

I have some questions that I don't understand about time complexity. Given that the worst case complexity of the algorithm $A$ is $O(f(n))$ and the best case complexity of $A$ is $Ω(g(n))$. It ...
Math4me's user avatar
  • 249
3 votes
1 answer
242 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
1 vote
1 answer
158 views

Non-trivial difference(s) between Computer Algebra System and Proof Assistant

Disclaimer: I am not even an expert user of these two kinds of software. I understand that the trivial difference between proof assistants and CAS is that in proof assistants, the goal is to show that ...
prash's user avatar
  • 111
2 votes
1 answer
115 views

What are the differences between LCF's Theorem and Automath's Prop?

How are the fundamental approaches to proving theorems by LCF and Automath different? Considering their modern descendants - Isabelle for LCF and Coq for Automath, both rely on type checking to do ...
user3565552's user avatar
1 vote
1 answer
19 views

Does n^(1-1/d) always dominate log^d(n)

Hi I am currently learning about orthogonal range search and found two data structures with two different runtimes and wanted to proof that one always dominates the other. So I found out about k-d-...
MatthiasPichler's user avatar
8 votes
2 answers
660 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
4 votes
0 answers
286 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
2 votes
1 answer
159 views

What were the shortcomings of Robinson's resolution procedure?

Paulson et alii. From LCF to Isabelle/HOL say: Resolution for first-order logic, complete in principle but frequently disappointing in practice. I think complete means they can proof any true ...
user1868607's user avatar
  • 2,194
2 votes
0 answers
75 views

Difference between the logic and the type system of a proof assistant?

In Comparing Mathematical Provers (section 4.1), Wiedijk classifies logics and type systems of different proof assistants? I do not see what he means by type system of the assistant. He only says: A ...
user1868607's user avatar
  • 2,194
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
1 vote
1 answer
64 views

Need hint for bipartiteness proof

I am given a graph $G = (V, E)$ with $N$ connected components and $G^\prime = (V^\prime, E^\prime)$, where for each $v \in V$ there is $v_1, v_2 \in V^\prime$ and for each $(u, v) \in E$ there is $(...
Tom Finet's user avatar
  • 258
1 vote
3 answers
282 views

Prove simple theorems in Haskell in automated way

I would like to prove in Haskell, whether in vanilla Haskell or using some libraries / tools, some simple theorems such as: ...
Борат Сагдиев's user avatar
2 votes
2 answers
288 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
1 vote
3 answers
244 views

Proving a solution for the $n$-Queens Puzzle

Given an $n$ x $n$ board, assume that $n \geq 5$ and that $n$ is not divisible by $2$ or $3$. Prove that the following positioning of $n$ queens $Q_0, Q_2, ..., Q_{n-1}$ works, i.e no two queens ...
Karla's user avatar
  • 181
1 vote
1 answer
109 views

on coq: Why is the proof complete after proving only for one induction when we have more than one variable?

So I'm learning coq. And I came across the proof for associativity in addition forall (a b c : nat) Appearntly when we do ...
Archy Will He 何魏奇's user avatar
0 votes
1 answer
142 views

Coding Theory Optimal Code with given max length

Why do we need at least 2 Code Words of the max length in optimal Codes? Any why do they just differ in their Prefix? Could someone give me more insight into this? Have to proof that for a given ...
Rapiz's user avatar
  • 51
3 votes
1 answer
502 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,692
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
0 votes
1 answer
185 views

Show that a problem is NP-Complete

The problem is, K_longestPath: We are given a graph in which some of the vertices are "cities". No two cities have an edge between them, thus every city must be at distance at least 2 from each ...
C. Cristi's user avatar
  • 187
0 votes
1 answer
98 views

Can someone pelase give a counter example of it? If a problem is in NP then there is no known polynomial time algorithm to solve it

Is there any known polynomial time algorithm to solve a problem which that problem is in NP. I was told is False but can't think of any counter example now.
Maxfield's user avatar
  • 227
1 vote
0 answers
73 views

Prove that grammar $S \to aSc | \epsilon | bBc$ ,$B \to bBc | \epsilon$ generates language $\{a^ib^jc^{i+j} | i,j \ge 0 \}$

Prove that grammar $G$ with productions: $S \to aSc|\epsilon | bBc$ $B\to bBc | \epsilon$ Generates language $ L = \{a^ib^jc^{(i+j)}$ | $i,j \ge 0 \} $ Step 1. Prove $L(G) \subseteq L$ . We are ...
Mandy's user avatar
  • 177
1 vote
1 answer
365 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 $...
Mandy's user avatar
  • 177
2 votes
0 answers
36 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 ...
Enrico Blash's user avatar
0 votes
1 answer
382 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) ...
L22324's user avatar
  • 19
-1 votes
1 answer
175 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 ...
CCOthers's user avatar
1 vote
1 answer
96 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 \...
Lisa.Neust'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
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
5 votes
2 answers
492 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
2 votes
2 answers
624 views

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

I have the following code: ...
user56834's user avatar
  • 3,692
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
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
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
5 votes
2 answers
596 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
3 votes
1 answer
452 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
5 votes
1 answer
728 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,193