現在、CoqのRed-Black Treesで遊んでいて、nat
のリストを注文して、MSetRBT
モジュールを使用して赤黒のツリーに保存できるようにしたいと考えています。そのためCoq/SSreflectで注文されたseq
示すように、私はseq_lt
を定義している:
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.
はこれまでのところ、私は示すことができた:
Lemma lt_not_refl p : seq_lt p p = false.
Proof.
elim: p => //= ? ?; by rewrite eq_refl.
Qed.
など
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.
しかし、私は次のことを証明するのに苦労しています:
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.
帰納法を使用して最後の補題が実行可能かどうかはわかりませんが、私は数時間それをしていて、この時点からどこに行くのか分かりません。 seq_lt
の定義に問題はありますか?
注意事項証明スタイルに:インデントをご確認ください。 'by'はターミネータです(' by tac1; tac2.' wrong: 'tac1; by tac2'); 'move =>'は 'move =>'より優先されます。 'case:(a ejgallego
@ejgallego:ありがとう、ありがとう! – VHarisop