Bestellte Reihenfolge in Coq/SSreflect

Question

Ich spiele gerade mit Red-Black Trees in Coq und möchte Listen von nat mit einer Bestellung ausstatten, so dass sie an einem rot-schwarzen Baum mit dem MSetRBT Modul gespeichert werden können.

Aus diesem Grund habe ich seq_lt wie gezeigt definiert:

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. 

Bisher habe ich zu zeigen geschafft: Allerdings

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

sowie

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. 

Ich habe Mühe, folgendes zu beweisen:

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. 

Ich bin nicht einmal sicher, ob das letzte Lemma mit Induktion machbar ist, aber ich bin seit ein paar Stunden dabei und habe keine Ahnung, wohin ich von diesem Punkt aus gehen soll. Ist die Definition von seq_lt problematisch?

Answer 1

Ich bin nicht sicher, was ist Ihr Problem mit Induktion aber der Beweis scheint einfach:

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. 

Wenn Sie gonna verwenden Aufträge sind schlage ich vor, du einige der Bibliotheken erstreckt ssreflect zu diesem Zweck verwendet werden; Ich erinnere mich, dass Cyril Cohen eine Weiterentwicklung von GitHub hatte. Beachten Sie, dass die Lemmata auf Bestellungen haben eine etwas andere Form in MathComp (Beispiel ltn_neqAle), so können Sie auch tun:

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. 

Dies könnte zum Neuschreiben etwas besser funktionieren.

P. S: Ich schlage vor, diesen Beweis für Ihre zweite Lemma:

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