CODEWITHSUNDEEP
coqcoq-tacticssreflect
VHarisop
VHarisop

Reputation: 2826

Ordered seq in Coq/SSreflect

I am currently playing around with Red-Black Trees in Coq and would like to equip lists of nat with an order, so that they can be stored at a red-black tree using the MSetRBT module.

For that reason, I have defined seq_lt as shown:

Fixpoint seq_lt (p q : seq nat) := match p, q with
  | _, [::] => false
  | [::], _ => true
  | h :: p', h' :: q' =>
    if h == h' then seq_lt p' q'
    else (h < h')
end.

So far, I've managed to show:

Lemma lt_not_refl p : seq_lt p p = false.
Proof.
  elim: p => //= ? ?; by rewrite eq_refl.
Qed.

as well as

Lemma lt_not_eqseq : forall p q, seq_lt p q -> ~(eqseq p q).
Proof.
  rewrite /not. move => p q.
  case: p; case: q => //= a A a' A'.
  case: (boolP (a' == a)); last first.
  - move => ? ?; by rewrite andFb.
  - move => a'_eq_a A'_lt_A; rewrite andTb eqseqE; move/eqP => Heq.
    move: A'_lt_A; by rewrite Heq lt_not_refl.
Qed.

However, I'm struggling in proving the following:

Lemma seq_lt_not_gt p q : ~~(seq_lt q p) -> (seq_lt p q) || (eqseq p q).
Proof.
  case: p; case: q => // a A a' A'.
  case: (boolP (a' < a)) => Haa'.
  - rewrite {1}/seq_lt.
    suff -> : (a' == a) = false by move/negP => ?.
    by apply: ltn_eqF.
  - rewrite -leqNgt leq_eqVlt in Haa'.
    move/orP: Haa'; case; last first.
    + move => a_lt_a' _; apply/orP; left; rewrite /seq_lt.
      have -> : (a == a') = false by apply: ltn_eqF. done.
    + (* What now? *)
Admitted.

I am not even sure if the last lemma is doable using induction, but I've been at it for a few hours and have no idea as to where to go from this point. Is the definition of seq_lt problematic?

Upvotes: 2

Views: 193

Answers (1)

ejgallego
ejgallego

Reputation: 6852

I am not sure what is your problem with induction but the proof seems straightforward:

Local Notation "x < y" := (seq_lt x y).
Lemma seq_lt_not_gt p q : ~~ (q < p) = (p < q) || (p == q).
Proof.
elim: p q => [|x p ihp] [|y q] //=; rewrite [y == x]eq_sym eqseq_cons.
by case: ifP => h_eq; [exact: ihp | rewrite orbF ltnNge leq_eqVlt h_eq negbK].
Qed.

If you are gonna use orders I suggest thou you use some of the libraries extending ssreflect to that purpose; I seem to recall that Cyril Cohen had a development on github. Note that the lemmas on orders have a slightly different form in mathcomp (example ltn_neqAle), so you can also do:

Lemma lts_neqAltN p q : (q < p) = (q != p) && ~~ (p < q).
Proof.
elim: p q => [|x p ihp] [|y q] //=; rewrite eqseq_cons [y == x]eq_sym.
by case: ifP => h_eq; [apply: ihp | rewrite ltnNge leq_eqVlt h_eq].
Qed.

This could work a bit better for rewriting.

p.s: I suggest this proof for your second lemma:

Lemma lt_not_eqseq p q : seq_lt p q -> p != q.
Proof. by apply: contraTneq => heq; rewrite heq lt_not_refl. Qed.

Upvotes: 4

Related Questions