SHARE
TWEET

Untitled

a guest Oct 17th, 2019 87 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. Require Import PeanoNat.
  2. Require Import List.
  3.  
  4. (* Print list. *)
  5. (* Shows definition for the <list> type *)
  6. (* nil = null list *)
  7. (* cons 0 nil = constructs a new list with elements 0 and nil *)
  8. (* 2::1::0    = constructs a new list with elements 2 1 and 0 *)
  9. (* cons = :: -> constructs new list *)
  10. (* app = ++ -> appends to list*)
  11.  
  12. Inductive btree :=
  13. | empty : btree
  14. | node  : btree->nat->btree->btree.
  15.  
  16. Fixpoint searchBT (t:btree) (value:nat) : bool :=
  17. match t with
  18. | empty       => false
  19. | node l v r  =>
  20.     if v =? value then
  21.       true
  22.     else
  23.       orb (searchBT l value) (searchBT r value)
  24. end.
  25.  
  26. (* Ex 1 *)
  27. Fixpoint inOrdineBT (t:btree) : list nat :=
  28. match t with
  29. | empty       => nil
  30. | node l v r  => (inOrdineBT l) ++v:: (inOrdineBT r)
  31. end.
  32.  
  33. (*
  34. Definition Zero := (node empty 0 empty).
  35. Definition One := (node empty 1 empty).
  36. Definition Two := (node Zero 2 One).
  37.  
  38. Compute inOrdineBT Two.
  39. *)
  40.  
  41. (* Ex 2 *)
  42. Fixpoint siblings (t:btree) (val:nat) : btree :=
  43. match t with
  44. | empty       => empty
  45. | node l v r  =>
  46.   match l with
  47.   | empty         => siblings r val
  48.   | node ll lv lr =>
  49.     if lv =? val then r
  50.     else
  51.       match r with
  52.       | empty         => siblings l val
  53.       | node rl rv rr =>
  54.         if rv =? val then l
  55.         else
  56.           empty
  57.       end
  58.   end
  59. end.
  60.  
  61. Fixpoint parent (t:btree) (val:nat) : btree :=
  62. match t with
  63. | empty       => empty
  64. | node l v r  =>
  65.   match l, r with
  66.   | node ll lv lr, node rl rv rr =>
  67.     if orb (lv =? val) (rv =? val) then t
  68.     else
  69.       match (parent l val) with
  70.       | empty => (parent r val)
  71.       | _     => (parent l val)
  72.       end
  73.   | _, _                         =>
  74.     match (parent l val) with
  75.       | empty => (parent r val)
  76.       | _     => (parent l val)
  77.     end
  78.   end
  79. end.
  80.  
  81. Fixpoint degree (t:btree) (val:nat) : nat :=
  82. match t with
  83. | empty       => 0
  84. | node l v r  =>
  85.   if v =? val then
  86.     match l, r with
  87.     | empty, empty                  => 0
  88.     | node ll lv lr, node rl rv rr  => 2
  89.     | _, _                          => 1
  90.     end
  91.   else
  92.     degree l val + degree r val
  93. end.
  94.  
  95. Definition Zero := (node empty 0 empty).
  96. Definition One := (node empty 1 empty).
  97. Definition Two := (node Zero 2 One).
  98.  
  99. Compute parent Two 0.
  100. Compute parent Two 1.
  101. Compute parent Two 2.
  102.  
  103. Compute degree Two 0.
  104. Compute degree Two 1.
  105. Compute degree Two 2.
  106.  
  107. Compute siblings Two 0.
  108. Compute siblings Two 1.
  109. Compute siblings Two 2.
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top