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.
94
questions
-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 ...
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 ...
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.
...
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+ (...
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 ...
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 ...
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 ...
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 ...
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, ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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-...
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 ...
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 ...
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 ...
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 ...
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. ...
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 $(...
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:
...
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 ...
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 ...
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 ...
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 ...
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 ...
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-...
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 ...
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.
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 ...
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 $...
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 ...
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)
...
-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 ...
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 \...
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?
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:
...
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-...
2
votes
2
answers
624
views
How to prove this obvious theorem in type theory (LEAN prover)
I have the following code:
...
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". ...
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\...
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 ...
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 ...
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 ...
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 ...