0

Coq でやりたいことのために、加重ツリー ライブラリを作成しようとしています。ツリーの各エッジには、実数値の重みが必要です。私が必要とする操作の 1 つは、重みが 0 の場合にツリーから葉のエッジを削除するプルーニング関数です。

次のコードは、ツリーのセットアップです。

Require Import Coq.Reals.Reals.
Require Import Coq.Lists.List.

Section WeightedTrees.

Inductive wtree' (A : Type)  : Type :=
  | Null : wtree' A
  | LNode : A -> wtree' A
  | INode : A -> list (wtree' A) -> wtree' A.

Inductive Wtype (A : Type) : Type := W: R -> A -> Wtype A.

Definition wtree (A : Type) := wtree' (Wtype A).

(* Helper: checks whether a tree contains an element *)
Fixpoint wt_contains {A : Type} (a : A) (t : wtree A) : Prop :=
match t with
  | Null => False
  | LNode (W w a') => a' = a
  | INode (W w a') l => a' = a \/ (fold_left or (map (wt_contains a) l) True)
end.

これがプルーン関数での私の現在の試みです。0%R は共誘導型ではないため、Coq はそれを受け入れません。

Fixpoint wt_prune_list {A : Type} (l:list (wtree A)) : (list (wtree A)) :=
match l with
| nil => nil
| (cons Null l) => (cons (Null (Wtype A)) (wt_prune_list l))
| (cons (INode w l') l) => (cons ((INode (Wtype A)) w l') ((wt_prune_list A) l))
| (cons (LNode (W w a')) l) => 
  if w = 0%R then
    (wt_prune_list l)
  else 
    (cons (LNode (W w a')) (wt_prune_list l))
end.

だから私はいくつかの質問があります：

  1. 最も重要なこと: 重みがゼロのリーフ エッジのツリーを剪定するように上記のコードを修正するにはどうすればよいですか?
  2. のようなものが理にかなっているかどうかを確認していますかw=0%R? という証明があれば、これはこう言っていると考えるべきだと思いますw = 0%R。これは正しいですか？
  3. 次のような短い行の書き方はあります(cons (INode w l') l) => (cons ((INode (Wtype A)) w l') ((wt_prune_list A) l))か? 一致させることができたのはわかっていますが(cons (INode _) _)、反対側を構築する良い方法がないようです. の場合と同じように複数の引数を表す(cons (INode _1) _2) => (cons (INode _1) ((wt_prune_list A) _2)Coq が見つけられるようなものがあればいいのですが。_1_
4

1 に答える 1