## Stream: Coq users

### Topic: ✔ Stuck proving mergesort time complexity.

#### Vinícius Melo (Apr 29 2022 at 22:38):

I'm stuck trying to prove that 1<=k.

l: list nat
e: (length l <=? 1) = false
IHn: forall k : nat,
length (firstn (length l / 2) l) = 2 ^ k ->
T_mergesort (firstn (length l / 2) l) <= k * 2 ^ k
IHn0: forall k : nat,
length (skipn (length l / 2) l) = 2 ^ k ->
T_mergesort (skipn (length l / 2) l) <= k * 2 ^ k
k: nat
H: length l = 2 ^ k
H0: 2 <> 0 -> 2 ^ k = 2 * 2 ^ (k - 1) -> 2 ^ (k - 1) = 2 ^ k / 2
---------------------------------------------------------------------------
1/1
1 <= k


This is my code:

Theorem T_mergesort_complexity: forall l k, length l = 2^k -> T_mergesort l <= k * 2^k.
Proof.
intro l.
functional induction (T_mergesort l).
- intros.
simpl in H.
pose proof Nat.pow_eq_0_iff.
specialize (H0 2 k).
destruct H0.
symmetry in H.
lia.
- intros.
apply Nat.le_trans with (((k-1)*2^(k-1)) + ((k-1)*2^(k-1)) + 2^k).
apply IHn.
rewrite H.
rewrite firstn_length_le.
+ pose proof Nat.div_unique_exact.
specialize (H0 (2^k) 2).
specialize (H0 (2^(k-1))).
symmetry.
apply H0.
auto.
change 2 with (2^1) at 2.
replace (1 + (k - 1)) with k.
reflexivity.
symmetry.
apply Nat.sub_add.   (* This is where I'm stuck *)
+ rewrite H.


Any hints?

#### James Wood (Apr 29 2022 at 23:28):

2 ^ k = length l >= 2 = 2 ^ 1 by H and e, then surely there's some lemma saying that 2 ^ m >= 2 ^ n -> m >= n.

#### Vinícius Melo (Apr 29 2022 at 23:52):

James Wood said:

2 ^ k = length l >= 2 = 2 ^ 1 by H and e, then surely there's some lemma saying that 2 ^ m >= 2 ^ n -> m >= n.

What about the H0 hypothesis? Informally, I could just use H0 to show, by contradiction, that k >= 1, right? But I'm not sure how to do that in Coq.

#### Alexander Gryzlov (Apr 30 2022 at 00:16):

This might be useful as a reference: https://github.com/clayrat/fav-ssr/blob/trunk/src/sorting.v#L253-L305

#### Vinícius Melo (Apr 30 2022 at 05:31):

James Wood said:

2 ^ k = length l >= 2 = 2 ^ 1 by H and e, then surely there's some lemma saying that 2 ^ m >= 2 ^ n -> m >= n.

Lemma n_gt_or_eq_1 : forall (l: list nat) (k m n:nat),
(length l <=? 1 = false /\ length l = 2 ^ k) -> (2 ^ k  >= 2 ^ 1).
Proof.
intuition. assert (length l > 1).
- Search (((_ <=? _) = false) -> _ > _).



I'm not sure how to proceed with this contradiction proof.

Alexander Gryzlov said:

This might be useful as a reference: https://github.com/clayrat/fav-ssr/blob/trunk/src/sorting.v#L253-L305

Thanks! I will take a look into that.

#### Paolo Giarrusso (Apr 30 2022 at 08:27):

FWIW, H0 does not let you prove that k >= 1 (informally or formally). After case distinction on k (I mean destruct k) the k = 0 case reduces to 2 <> 0 -> 1 = 2 -> 1 = 1 / 2 (not sure what that division reduces to). That’s an implication from the false premise 1 = 2, so you learn nothing from it.

#### Karl Palmskog (Apr 30 2022 at 08:37):

this is a statement of the efficiency of the MathComp encoding of mergesort: https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/path.v#L936-L947

#### Karl Palmskog (Apr 30 2022 at 08:40):

essentially: the $i$-th item in the ss list here has size $2^i$, if it isn't empty:

Fixpoint merge_sort_push s1 ss :=
match ss with
| [::] :: ss' | [::] as ss' => s1 :: ss'
| s2 :: ss' => [::] :: merge_sort_push (merge s2 s1) ss'
end.


Hence, only perfectly balanced merges are performed.

#### James Wood (Apr 30 2022 at 08:59):

@Kard Zorn I don't know which libraries you're using, but I got this as a composition of leb_nle (which converts the boolean equation into proposition ~ (m <= 1)), then not_le (which converts the not-<= into a >, which unfolds into a >=).

Require Import Arith.
Import Nat.

Goal forall m, (m <=? 1) = false -> m >= 2.
intros m H.
eapply not_le.
eapply leb_nle.
exact H.
Qed.


#### Vinícius Melo (Apr 30 2022 at 15:47):

Paolo Giarrusso said:

FWIW, H0 does not let you prove that k >= 1 (informally or formally). After case distinction on k (I mean destruct k) the k = 0 case reduces to 2 <> 0 -> 1 = 2 -> 1 = 1 / 2 (not sure what that division reduces to). That’s an implication from the false premise 1 = 2, so you learn nothing from it.

Indeed, I was a little sleepy last night. I had to use e and H to prove it. With all the help, it worked!

#### Notification Bot (Apr 30 2022 at 15:47):

Kard Zorn has marked this topic as resolved.

Last updated: Feb 01 2023 at 12:30 UTC