864 questions
1
vote
1
answer
78
views
Array Reverse Proof by Dafny
Regarding the array reversal problem, I guess loop invariants are logically correct, based on the symmetry of the elements in the array and their relationship after reversal.
However, I don’t ...
- 13
0
votes
2
answers
249
views
proving Predicate logic with Isabelle
I'm trying to prove the following lemma:
lemma myLemma6: "(∀x. A(x) ∧ B(x))= ((∀x. A(x)) ∧ (∀x. B(x)))"
I'm trying to start by eliminating the forall quantifiers, so here's what I tried:
...
- 49.7k
3
votes
1
answer
94
views
Is there a way to check for an instance of a class (with Haskell extensions)?
I am currently writing common theorems of intuitionistic logic in Haskell using the Curry-Howard isomorphism:
import Data.Void
type a :> b = a -> b -- implies
type a :+ b = Either a b -- or
data ...
- 156k
1
vote
2
answers
65
views
Trying to prove the multiset of a sequence is equal to the multiset of that sequence broken up
I'm having trouble proving this within a while loop in Dafny:
assert multiset(seqa) == multiset(seqa[..i] + seqa[i..]);
Note:
An invariant exists ensuring that 0 <= i <= |seqa|.
There are no ...
- 1,309
0
votes
1
answer
261
views
The security of Zero knowledge proof performance
I recently learned to study the security of zero-knowledge proofs.
It seems from the Wikipedia, that the most popular example is the Ali Baba cave. I have a question about the security of the zero-...
CommunityBot
- 1
1
vote
3
answers
8k
views
Formal proof for P → Q ≡ ¬P ∨ Q in Fitch
I'm trying to construct a formal proof for 'P → Q ≡ ¬P ∨ Q' in Fitch. I know this is true, but how do I prove it?
- 479
18
votes
4
answers
69k
views
I need help proving that if f(n) = O(g(n)) implies 2^(f(n)) = O(2^g(n))) [closed]
In a previous problem, I showed (hopefully correctly) that f(n) = O(g(n)) implies lg(f(n)) = O(lg(g(n))) with sufficient conditions (e.g., lg(g(n)) >= 1, f(n) >= 1, and sufficiently large n).
...
- 33.7k
6
votes
2
answers
148
views
substitution in proofs with recursive formulas
The following problem and partial solution are from Richard Bird's Thinking Functionally with Haskell (pp 132-133, 139)
given
foldl f e (x:xs) = foldl f (f e x) xs
foldl f e [] = e
Prove foldl (@) e ...
- 31k
21
votes
5
answers
4k
views
Functional proofs (Haskell)
I failed at reading RWH; and not one to quit, I ordered Haskell: The Craft of Functional Programming. Now I'm curious about these functional proofs on page 146. Specifically I'm trying to prove 8.5.1 ...
- 31k
0
votes
0
answers
179
views
What would P=NP tell us for a proof?
An exercise I've been working on is "Prove that there is no efficient 5/4-approximation toChromaticNumber unless P=NP.
My question is what would P=NP tell us? Let's say we "Suppose P=NP" in our proof....
0
votes
1
answer
124
views
Providing and using proofs as arguments to a function in Rocq
I am having trouble with a piece of Rocq code that I think has to do with providing a proof argument to a function, but I am not sure.
Here's the relevant code. The code below typechecks:
Require ...
- 311
1
vote
3
answers
2k
views
All maximal independent sets of a matroid have the same cardinality
How to prove that all maximal independent sets of a matroid have the same cardinality.
Provided a matroid is a 2-tuple (M,J ) where M is a finite set and J is a
family of some of the subsets of M ...
- 2,985
0
votes
0
answers
38
views
Proving the Log Matching property in Raft consensus protocol
I have been trying to understand the Raft protocol for quite some time now. One thing that has always stumped me is the proof of the Log Matching property. One of my concerns is that the proof in the ...
- 118
3
votes
3
answers
938
views
Floyd's Algorithm to detect cycle in linked list proof
I've seen several proofs for Floyd's algorithm in several posts inside and outside stack overflow. All of them proves the second part of the algorithm that is, why the method to find the start of the ...
15
votes
4
answers
5k
views
Proof that Fowler's money allocation algorithm is correct
Martin Fowler has a Money class that has a money allocation routine. This routine allocates money according to a given list of ratios without losing any value through rounding. It spreads any ...
- 1,016