Stream: Coq users

Topic: ✔ tree membership prop

Lessness (Jul 17 2022 at 20:47):

Inductive tree A :=
  | leaf: A -> tree A
  | forest: list (tree A) -> tree A.

I have this definition of tree type. And I want to define fixpoint that is True if tree contains some element x. (Like In for lists.)

My first try was failure (with Recursive definition of tree_has_leaf is ill-formed message):

Fixpoint tree_has_leaf {A} (i: A) (t: tree A) {struct t}: Prop :=
  match t with
  | leaf _ x => x = i
  | forest _ l => Exists (fun x => tree_has_leaf i x) l
  end.

Li-yao (Jul 17 2022 at 20:59):

Try using fold_right instead.

Lessness (Jul 17 2022 at 21:03):

Thank you! It worked like a charm.

Fixpoint tree_has_leaf {A} (i: A) (t: tree A) {struct t}: Prop :=
  match t with
  | leaf _ x => x = i
  | forest _ l => fold_right (fun x => and (tree_has_leaf i x)) True l
  end.

Notification Bot (Jul 17 2022 at 21:06):

Lessness has marked this topic as resolved.

Gaëtan Gilbert (Jul 17 2022 at 21:10):

(probably you want or/False not and/True)

Lessness (Jul 17 2022 at 21:33):

Gaëtan Gilbert said:

(probably you want or/False not and/True)

Yes, thank you!

Last updated: Oct 05 2023 at 02:01 UTC