proof Questions
2
Solved
Suppose a scenario where you have an application config, the structure of which has changed a few times. To provide ease of use for users, you wish to allow automatic migration from each version to...
2
Solved
I'm now learning Kademlia network by reading the classical paper Kademlia: A Peer-to-peer Information System Based on the XOR Metric. I want to understand the complexity of its operation but still ...
Bolger asked 12/3, 2015 at 8:13
5
Solved
I have an interview question that I can't seem to figure out. Given an array of size N, find the subset of size k such that the elements in the subset are the furthest apart from each other. In oth...
2
Solved
When refineing a program, I tried to end proof by inversion on a False hypothesis when the goal was a Type. Here is a reduced version of the proof I tried to do.
Lemma strange1: forall T:Type, 0&g...
3
Solved
I can clearly see than N^2 is bounded by c2^N, but how do i prove it by using formal definition of big-O. I can simply prove it by M.I.
Here is my attempt..
By definition, there for any n>n0, the...
1
I am trying to prove that my implementation of Select Sort in Ada is correct. I have tried a few loop invariants, but using gnatprove only proves inner loop's invariant:
package body Selection with...
Hamnet asked 30/3, 2021 at 12:8
1
Solved
I aim to prove that the Horner's Rule is correct. To do so, I compare the value currently calculated by Horner with the value of "real" polynominal.
So I made this piece of code:
package ...
Uriel asked 24/3, 2021 at 18:7
3
I have two arrays of integers A and B both of size n. The cost of a pair is |A(i) - B(i)|.
I want to pair the n elements of A and B such that the sum of all costs across all A(i)s and B(i)s are min...
Allow asked 27/1, 2021 at 12:33
4
Solved
I want to display a proof tree in the style of a natural deduction within a web page.
I will get the data from a JSON file.
Whats the best way to display something like this?
Is it possible only ...
Disclaimer asked 25/4, 2013 at 10:28
5
How does one go about determining the height of a recursion tree, built when dealing with recurrence run-times? How does it differ from determining the height of a regular tree?
alt text http://h...
Tamishatamma asked 28/8, 2009 at 15:55
3
Solved
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)....
5
Solved
How does one prove (forall x, P x /\ Q x) -> (forall x, P x) in Coq? Been trying for hours and can't figure out how to break down the antecedent to something that Coq can digest. (I'm a newb, obvio...
1
Solved
In the standard library of Cubical Agda, there are finite multisets whose elegant definitions I reproduce below:
{-# OPTIONS --cubical --safe #-}
open import Cubical.Foundations.Prelude
infixr 2...
Neopythagoreanism asked 29/9, 2019 at 11:0
2
Solved
Coq simpl / unfold only once. (Replace part of goal with the result of one iteration of a function.)
I am an instructor at university for a class titled Type Systems of Languages and the professor used the following example for inductive proofs in Type Theory on the board last lecture:
Suppose, t...
Breaker asked 16/9, 2019 at 15:6
1
Solved
I'm following the official tutorial on Liquid Haskell, and stumbled upon what seems to be a "bug" in it.
The following code is present in the tutorial, and Liquid Haskell was supposed to check tha...
Henebry asked 27/7, 2019 at 23:23
5
Solved
It is well-known that applicative functors are closed under composition but monads are not. However, I have been having trouble finding a concrete counterexample showing that monads do not always c...
Senskell asked 23/10, 2012 at 15:41
0
This question is a request for references or explanation.
The main idea is: What if I add every axiom from standard library of Coq?
Will it raise a contradiction or they are well-adjusted to each o...
2
Solved
How do I show that anything follows from a value of a type with no constructors in Scala? I would like to do a pattern match on the value and have Scala tell me that no patterns can match, but I am...
Malvia asked 22/10, 2018 at 21:15
1
Solved
Im new in COQ and Im trying to proof the counterexample theorem.
Variable A B:Prop.
Hypothesis R1: ~A->B.
Hypothesis R2: ~B.
Theorem ej: A.
When we studied logics, we learn the RAA thechnic...
3
Solved
Suppose I want to prove following Theorem:
Theorem succ_neq_zero : forall n m: nat, S n = m -> 0 = m -> False.
This one is trivial since m cannot be both successor and zero, as assumed. Ho...
1
Solved
So, there is something known as a "universal property of fold", stating exactly following:
g [] = i; g (x:xs) = f x (g xs) <=> g = fold f i
However, as you probably now, there are rare cases l...
Melloney asked 6/3, 2018 at 19:22
0
I'm trying to prove that type-level function Union is associative, but I'm not sure how it should be done. I proved right identity and associativity laws for type-level append function and right id...
Unilateral asked 25/11, 2017 at 11:47
0
Monadic First Order Logic, where all predicates take exactly one argument, is a known decidable fragment of first order logic. Testing whether a formula is satisfiable in this logic is decidable, a...
Feinberg asked 7/11, 2017 at 6:37
2
Solved
I'm wondering, is there a commonly used library for vectors in coq, I.e. lists indexed by their length in their type.
Some tutorials reference Bvector, but it's not found when I try to import it.
...
Frohman asked 17/2, 2017 at 16:3
1
Solved
How can I have Idris automatically prove that two values are not equal?
p : Not (Int = String)
p = \Refl impossible
How can I have Idris automatically generate this proof? auto does not appear t...
1 Next >
© 2022 - 2025 — McMap. All rights reserved.