Define polymorphic inductive type tree in coq

user_14180392 0
Viewed 217

I got stuck on the exercise to prove my defined tree height is 3. I've found the binary tree coq code online, but the tree I defined is not a binary tree. The node contains arbitrary number.

tree pic attach: tree

Below is my code for the tree:

Inductive tree (X:Type) : Type :=
  | empty : tree X
  | branch : X -> list (tree X) -> tree X.

Arguments tree {X}.
Arguments empty {X}.
Arguments branch {X}.

Definition mytree :=
  branch 1 [ branch 5 [ branch 2 [empty] ] ;  branch 8 [empty] ;
          branch 7 [ branch 3 [empty];branch 4 [empty] ] ].

Fixpoint height {X: Type} (node: @tree X) : nat :=
  match node with
  | empty => 0
  | branch _ l => S (match l with 
                        | [] => 0
                        | h::t => S (height h)
                       end)
  end.

Below is the unit test. I tried to prove that my tree height is 3 (shown as pic)

Example test_height:
  height mytree = 3.
Proof.
  simpl.

after i simpl it, it showed: 6 = 3: 1 subgoal ______________________________________(1/1) 6 = 3

I guess is BC one or more functions that I defined previously are wrong. But I am not sure which one is it and why they are wrong? Could anyone help or give me some hint? Thank you so much

PS: there's also a hint for the exercise stated:

Hint: You may need to define mutually recursive functions using let expressions.

And it gives how let expression works as below: • Naming a recursive function (needs keyword fix):

Definition a := let fix f (x:nat) := match x with
| O => O
| S y => f y
end
in f 2.

But I am not sure how to use this let in my exercise.

coq
2 Answers

You've defined the height function incorrectly. You should define height by the pseudocode

height empty = 0
height (branch _ children) = 1 + max [height child | child in children]

where the max should return 0 if children is empty. Once you've defined the height function correctly, you should just be able to use reflexivity to prove the proposition.

user_119123420 
Fixpoint height {X: Type} (t: tree X) : nat :=
  match t with
  | emp_tr _ => 0
  | node_tr _ l => let fix height_list (ltrees: list (tree X)) :=  
               match ltrees with
               | [] => 0
               | htr :: ttr => max (height htr) (height_list ttr)
               end
               in 1 + height_list l
  end.

Used let to solve.

user_141803920
Related