Questions tagged [induction]
Anything related to mathematical induction principle and techniques applied to computing. Please DO NOT USE this tag for math-only questions since they are off-topic on SO. This tag may be used for math-related questions only if it involves some programming activity or software tools (e.g. automatic theorem proving, etc.).
induction
266
questions
0
votes
2
answers
46
views
How to induct on mapped sets or...?
Working on verifying a version of the counting inversions algorithm. I feel like pairMapSize has everything it needs but it times out instead. I could try to do induction on slices of the array but I ...
- 1,110
0
votes
0
answers
49
views
Proof on inductive sets
I am trying to wrap my brain around proofs on inductive sets and I am failing miserably.
This is what I have so far:
theory MyTheory
imports Main
begin
inductive_set S where
emptyI: "{} ∈ S&...
- 29
0
votes
1
answer
58
views
What `dependent induction` tactic does in Coq and how to use it
Can you please provide me with high-level explanation on which usecases dependent induction / dependent destruct tactics have, and how they work (I would be grateful for explanation high-level enough ...
- 463
0
votes
1
answer
41
views
Coq inductive not right form
I have troubles with a not well formed IH (or I am making mistakes).
From stdpp Require Import mapset.
From stdpp Require Import gmap.
From stdpp Require Import options.
From stdpp Require Import ...
-2
votes
3
answers
73
views
Is this the best loop variant for the following code which takes in a sorted array of integers and determines if theres are ints x,y that equal k
Would "there exists a pair x,y in the subarray arr[left:right+1] that sums up to k." be a good loop variant for the code below which determines given a sorted array of integers if there is a ...
- 9
-2
votes
1
answer
114
views
Structural induction on binary trees
Consider the following function definitions :
data Tree a = Leaf a | Node a (Tree a) (Tree a)
sumLeaves :: Tree a -> Integer
sumLeaves (Leaf x) = 1
sumLeaves (Node _ lt rt) = sumLeaves lt + ...
0
votes
1
answer
157
views
Proving a Type is Uninhabited in Agda
I've been learning Agda recently and I've been making a lot of progress but I'm stuck on one thing: proving that a type is NOT inhabited.
I have a relation on Bools defined as follows:
data Test : Rel ...
- 69
1
vote
2
answers
72
views
Definition by minimization in Coq
Assume P: nat -> T -> Prop is a proposition that for any given t: T,
either there exists a k: nat such that P holds for all numbers greater than or equal to k and no number less than k.
or P k ...
0
votes
1
answer
306
views
Proving a covariance inequality in Dafny, use contradiction?
I am trying to prove the following property in Dafny: covariance(x,y) <= variance(x) * variance(y), where x and y are real.
First of all, I would like to know if I am interpreting covariance and ...
- 726
0
votes
2
answers
121
views
Dafny: property '2*x*y <= x^2+y^2' holds with primitive operations (like 'x*x'), but not when I define operations in my own (like 'power(x,2)')
I am trying to prove a property in Dafny, which makes use of powers.
Concretely, this one: forall x,y in Reals : 2xy <= x^2+y^2. I implemented this idea in the following lemma:
lemma ...
- 726
-1
votes
1
answer
167
views
What algorithm can I use to compute 2022^n (given n \in N)? How can I prove the correctness (maybe induction?) and what's the upper bound used?
I have to use n-1 multiplications but I am confused about proving the correctness of the algorithm and finding the upper bound.
How do I do/show that??
I know 2022 = 20*(100+1)+2
2022 = 2000+20+2 ......
2
votes
0
answers
316
views
How does one pick the proper loop invariant to prove an algorithm's correctness?
We started with loop invariants last week and our professor proposed this question to work on at home. I've been following along the slides/lectures but I am having so much trouble with identifying a ...
- 21
1
vote
2
answers
311
views
How does Dafny support induction if Z3 does not?
Dafny has the option to set {:induction false}. Also, as far as I know, whenever we use assertions in Dafny, what happens below it that it constructs proof obligations and then calculates on them ...
- 726
1
vote
1
answer
123
views
Induction on recursive problems
Let ��(𝑛) be defined recursively as follows: 𝑇(1) = 𝑐 and 𝑇(𝑛) = 𝑇(⌊n/2⌋) + 𝑐 for all integers 𝑛 ≥ 2, where 𝑐 is an arbitrary positive constant. Prove by induction on 𝑛 that 𝑇(𝑛) ≤ 𝑐log𝑛...
- 53
2
votes
1
answer
214
views
Implementing an algorithm in Python to compute a function verifying an induction formula
I have a real function V taking its values in S*{1,...,N} where S is a finite set containing elements of the form (s_0,s_1), where s_0,s_1 are reals. V follows an "induction formula" of the ...
- 53