在Coq/SSreflect中排序seq

我目前正在玩coq中的紅黑樹，並希望配備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的定義是否存在問題？

來源

2017-06-23 VHarisop

舉證式的注意事項：檢查壓痕; 'by'is是終結符（正確的'tac1; tac2.'錯誤：'tac1; by tac2'）; 'move =>'比'move =>'更受青睞。類似的情況：（a ejgallego

@ejgallego：注意，謝謝！ – VHarisop

我不知道什麼是感應你的問題，但似乎證明直截了當：

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.

如果你要使用命令，我建議你使用一些擴展ssreflect該目的的庫;我似乎記得Cyril Cohen在github上有一個開發。需要注意的是訂單引理在mathcomp（例如ltn_neqAle）形式稍有不同，所以你也可以這樣做：

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.

這可能是工作重寫好一點。

P.S：我認爲這證明了你的第二個引理：

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

來源

2017-06-24 01:13:16 ejgallego

在Coq/SSreflect中排序seq

回答

相關問題