0

I am trying to make a weighted tree library for some stuff I would like to do in Coq. Each edge of a tree should have a real number valued weight. One of the operations I want is a prune function which prunes leaf edges from the tree if they have weight 0.

The following code is my set-up for the trees:

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.

Here is my current attempt at a prune function. Coq does not accept it because 0%R is not a co-inductive type. 

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.

So I have a few questions:

  1. Most importantly: How do I fix the above code so that it prunes the tree of leaf edges of zero weight?
  2. Does checking whether something like w=0%R even make sense? I suppose one should think of this as saying if we have a proof that w = 0%R. Is this right?
  3. Are there shorter ways of writing lines like: (cons (INode w l') l) => (cons ((INode (Wtype A)) w l') ((wt_prune_list A) l))? I know I could have matched with (cons (INode _) _) but then it seems I have no good way of constructing the other side. It would be nice if there was something like (cons (INode _1) _2) => (cons (INode _1) ((wt_prune_list A) _2) where Coq could figure out that _1 represents multiple arguments in the same way that it does with _.
4

1 回答 1

4

The problem here is that the definition of real numbers in the standard Coq library is not computational, but axiomatic. What this means is that there is no way to compute with real numbers in Coq, only prove things about them. An alternative would be to use rational numbers, or even plain natural numbers.

There is also a subtle conceptual issue with your code: it is using purely logical entities instead of computational ones, i.e. your functions are working with Prop instead of bool. Props don't really produce an answer like bool does; in particular, you can't test whether a Prop is true or false, like you did in wt_prune_list. Going in detail about this difference would be too much for this answer, but to a first approximation you can think of Prop as things you can try to prove interactively, whereas bool is just another datatype like nat or list.

Here's how you can fix this:

  • Coq has no generic equality operator that produces a bool. The reason for that is that there is no generic procedure to determine whether two values are equal or not. The = you are using is actually producing a Prop. Thus, you need to pass to wt_contains an additional function eqb : A -> A -> bool that tests whether two elements are equal. When instantiating wt_contains on a particular type, you'll have to write a version of eqb for that type. The EquivDec type class in the standard library can make this less awkward to program with.

  • In wt_prune_list, you will also have to test whether a number is zero using the equality operator for that number type (e.g. Qeq_bool for rationals, beq_nat for natural numbers).

  • Use the boolean or || instead of \/.

Finally, there is nothing to achieve the effect of the _1 pattern you suggested, unfortunately.

于 2013-11-12T00:44:52.040 回答