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

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

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.

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: Sep 30 2023 at 06:01 UTC