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
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 ...
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 ...
- 11
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 ...
- 361
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
2
votes
2
answers
94
views
Inductive Proof for a Recursive Prefix Checking Function
The problem involves proving, using mathematical induction, the correctness of the recursive function presenza_strg (comments are in italian sorry for that)
/*Controlla in maniera ricorsiva se s1 è ...
0
votes
0
answers
53
views
Linearizability proof of a toy SET implementation over a filesystem
I'm currently studying concepts related to linearizability and I struggle with going from the linearization points of an implementation to the actual proof of linearizability.
As far as I have ...
- 1
1
vote
1
answer
173
views
Unexpected token in Hyperbolic geometry undecidability proof with lean 4
I am trying to use Lean 4 to reduce the halting problem to hyperbolic geometry to prove the undecidability of hyperbolic geometry, having problems with the diagonalization of the Turing machines, also ...
0
votes
2
answers
83
views
I'm having difficulty definining a property in Coq, not sure how to approach
I've implemented a proof system from a paper in Coq, as shown below.
Term proof System
Require Import Ensembles.
Definition Var := nat.
Definition Name := nat.
Inductive Term: Type :=
| VarTerm (v: ...
1
vote
0
answers
106
views
What is the proper why to generate an instance from Lean4 GetElm class type?
Trigger
I am writing an exercise in Functional Programming in Lean. The example shows a way to generate an instance for GetElem' (NonEmptyList α) Nat α .. with a bound. I explain it as to implement ...
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 ...
- 2,183
0
votes
0
answers
106
views
How to prove the sliding window algorithm works to find the largest non repeating substring
Doing the leetcode problem https://leetcode.com/problems/longest-substring-without-repeating-characters/ I found this solution:
def lengthOfLongestSubstring(self, s: str) -> int:
left = 0
...
1
vote
0
answers
53
views
Expected number of full neighbors of a Voronoi cell in $\mathbb{R}^3$
Given a Voronoi diagram in three dimensions, what is the expected number of full neighbors E(C) of a Voronoi cell?
Two adjacent cells are considered full (or Gabriel) neighbours in R^3 if the line ...
- 33
0
votes
3
answers
190
views
Time complexity analysis of data structures
I got a bit confused about analzsis of data structure basic operation like inserting or deleting.
when I am asked about creating an data structure that support deleting operation, or inserting in O(1),...
- 119
0
votes
1
answer
95
views
Dafny simple proof about giving change not working
I want to prove that the following code returns a given amount (money) in 5 and 3 bills/coins:
function sum(ns: seq<nat>): nat
{
if |ns| == 0 then
0
else
ns[0] + sum(ns[1..])
}
...
- 106k