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 Nat.add_le_mono.
apply Nat.add_le_mono.
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.
rewrite <- Nat.pow_add_r.
replace (1 + (k - 1)) with k.
reflexivity.
rewrite <- Nat.add_comm.
symmetry.
apply Nat.sub_add. (* This is where I'm stuck *)
admit.
+ rewrite H.
admit.
+ admit.
+ admit.
+ admit.
Admitted.
```

Any hints?

`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`

.

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.

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

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) -> _ > _).
Admitted.
```

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.

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.

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

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.

@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.
```

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!

Kard Zorn has marked this topic as resolved.

Last updated: Jun 14 2024 at 18:01 UTC