在Coq中实现Boruvka算法 [英] Implement Boruvka's algorithm in Coq

问题描述

我正在尝试在Coq中进行Boruvka算法，但是我坚持了最后一部分.下面是我的代码:

I am trying to do Boruvka algorithm in coq, but I stuck in the last part. Below is my code:

From LF Require Export Lists.
From LF Require Export Basics.
Require Import Coq.Lists.List.

Definition vertics := list(nat).
Definition edges := list(nat*nat*nat).
Definition Graph := (vertics, edges).


(*takes in a list of edges from the graph and returns the edge with the smallest weight.*)
Fixpoint minEdge (l: edges)(m: nat*nat*nat): nat*nat*nat :=
match l with
  | nil => m
  | cons h t => match h, m with
                | (a,b,w), (a2,b2,m) => if (leb w m) 
                 then (minEdge t (a,b,w))
                 else (minEdge t (a2,b2,m))
                end
  end.

(*takes in a node and check whether the node has been visited in the new graph*)
Fixpoint first_visit(v: vertics) (node: nat): bool:=
match v with
  | nil =>true
  | cons h t => if (eqb h node)
           then false
           else first_visit t node
end.

(*takes in a node that is going to be removed and return the updated list*)
Fixpoint remove_node (node : nat) (vertics : list nat) : list nat :=
match vertics with
  | nil => nil
  | y::tl => if (eqb node y) 
             then (remove_node node tl)
             else y::(remove_node node tl)
    end.

(*takes in a node that has been visited and then remove it from the graph*)
Definition remove_visitied_node (l: vertics)(m: nat*nat*nat): vertics :=
match m with
  | (a,b,w) => (remove_node a (remove_node b l))
end. 

Notation "x :: l" := (cons x l)
                     (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
Check [1;2].

(*takes in a node and adds the node to the minimum spanning tree.*)
Definition add_node (v:list nat) (m: nat*nat*nat): vertics :=
match v, m with
  | [], (a,b,w) => [a; b]
  | e, (a,b,w) =>  if ((first_visit e a) && (first_visit e b))
                   then e++[a;b]
                   else if (first_visit v a)
                        then e++[a]
                        else if(first_visit v b)
                        then e++[b]
                        else v

end.

(*takes in an edge and adds the edge to the minimum spanning tree.*)
Definition add_edges (e: list (nat*nat*nat)) (m: nat*nat*nat): edges :=
  e++[m].

(*takes in an edge and removes it from the graph.*)
Fixpoint remove_edge (e: edges) (m: nat*nat*nat) : edges :=
match e with
  | nil => nil
  | h::t => match h,m with
            | (a1,b1,w1), (a2,b2,w2) => if ((eqb a1 a2) && (eqb b1 b2) && (eqb w1 w2))
                                        then t
                                        else h::(remove_edge t m)
            end
end.

(* function returns the first edge from the list*)
Definition first_edge (e: edges) : (nat*nat*nat) :=
match e with
  | [] => (0,0,100)
  | hv::tv => hv
end.

(* boruvka construct a new graph with adding the smallest edge to the new graph until all nodes are visited*)
Fixpoint boruvka (min_tree: edges*vertics) (e: edges) (v: vertics): edges*vertics :=
match v with
  | [] => min_tree
  | x => (boruvka (add_edges e (minEdge e (first_edge e)),(add_node v (minEdge e (first_edge e))))
                  (remove_edge e (minEdge e (first_edge e)))
                  (remove_visitied_node x (minEdge e (first_edge e))))
end.

最后一个定义会弹出一个错误消息，如下所示:无法猜测到减小的fix参数.有人知道我该如何解决吗?我已经检查了错误味精，似乎coq不能在一个函数中组合这么多函数.IDK如何在不结合所有这些功能的情况下实现Boruvka?

The last definition pops an error msg like this: Cannot guess decreasing argument of fix. Anyone know how can I fix this? I've checked the error msg, it seems like coq cannot combine so many functions in one function. IDK how can I implement Boruvka without combining all these functions?

推荐答案

为使Fixpoint的自动终止检查有效，必须使用结构上较小的参数来调用任何递归调用.例如，当您在树上进行计算时，可以在子树上递归.

For Fixpoint's automatic termination check to work, any recursive call must be called with a structurally smaller argument. For example, when you are computing over a tree, you can recurse over the subtrees.

在您的情况下，您考虑的是 v 的不同情况，但是随后您将 v 作为参数传递给递归函数，因此自动检查器无法知道您是否也许正在创造一个无限循环.

In your case you are considering different cases of v but then you send v as an argument to your recursive function, so the automatic checker can't know if you are perhaps creating an infinite loop.

要解决这个问题，您将必须提供某种证据，证明某物正在减少-可能是树的高度，边缘和顶点的部分数量等，以及用该证明作为递减论证.

To solve that, you will have to provide some kind of proof that something is decreasing - it could be the height of the tree, the number of parts in edges and vertices, etc., and use that proof as the decreasing argument.

如果使用 Require Import Program.和 Program Fixpoint ... ，您将获得更多工具来证明您的程序确实可以递归.

If you use Require Import Program. and Program Fixpoint ... you get some more tools to prove that your program really recurses.

在您的情况下，列表顶点的长度似乎应该减少，因此添加注释 {measure(length v)} .

In your case, it looks like the length of the list vertices should be decreasing, so add the annotation {measure (length v)}.

Require Import Program.
Program Fixpoint boruvka (min_tree: edges*vertics) 
      (e: edges) (v: vertics) {measure (length v)}: edges*vertics := 
   ...
End.

Next Obligation.

然后您就陷入了证明模式，需要证明这一点

Then you are thrown into proof mode and need to prove that

length (remove_visitied_node v (minEdge e (first_edge e))) <
length v

这篇关于在Coq中实现Boruvka算法的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！