2014-11-19 01:57:17 +00:00
|
|
|
import logic data.nat
|
2015-10-13 22:39:03 +00:00
|
|
|
open eq.ops nat algebra
|
2014-11-19 01:57:17 +00:00
|
|
|
|
|
|
|
inductive tree (A : Type) :=
|
2015-02-26 01:00:10 +00:00
|
|
|
| leaf : A → tree A
|
|
|
|
| node : tree A → tree A → tree A
|
2014-11-19 01:57:17 +00:00
|
|
|
|
|
|
|
namespace tree
|
|
|
|
|
|
|
|
definition height {A : Type} (t : tree A) : nat :=
|
2015-02-11 20:49:27 +00:00
|
|
|
tree.rec_on t
|
2014-11-19 01:57:17 +00:00
|
|
|
(λ a, zero)
|
|
|
|
(λ t₁ t₂ h₁ h₂, succ (max h₁ h₂))
|
|
|
|
|
|
|
|
definition height_lt {A : Type} : tree A → tree A → Prop :=
|
|
|
|
inv_image lt (@height A)
|
|
|
|
|
|
|
|
definition height_lt.wf (A : Type) : well_founded (@height_lt A) :=
|
|
|
|
inv_image.wf height lt.wf
|
|
|
|
|
|
|
|
theorem height_lt.node_left {A : Type} (t₁ t₂ : tree A) : height_lt t₁ (node t₁ t₂) :=
|
2015-04-18 17:50:30 +00:00
|
|
|
lt_succ_of_le (le_max_left (height t₁) (height t₂))
|
2014-11-19 01:57:17 +00:00
|
|
|
|
|
|
|
theorem height_lt.node_right {A : Type} (t₁ t₂ : tree A) : height_lt t₂ (node t₁ t₂) :=
|
2015-04-18 17:50:30 +00:00
|
|
|
lt_succ_of_le (le_max_right (height t₁) (height t₂))
|
2014-11-19 01:57:17 +00:00
|
|
|
|
|
|
|
theorem height_lt.trans {A : Type} : transitive (@height_lt A) :=
|
2014-11-22 08:15:51 +00:00
|
|
|
inv_image.trans lt height @lt.trans
|
2014-11-19 01:57:17 +00:00
|
|
|
|
2015-10-13 22:39:03 +00:00
|
|
|
example : height_lt (leaf (2:nat)) (node (leaf 1) (leaf 2)) :=
|
2014-11-19 01:57:17 +00:00
|
|
|
!height_lt.node_right
|
|
|
|
|
2015-10-13 22:39:03 +00:00
|
|
|
example : height_lt (leaf (2:nat)) (node (node (leaf 1) (leaf 2)) (leaf 3)) :=
|
2014-11-19 01:57:17 +00:00
|
|
|
height_lt.trans !height_lt.node_right !height_lt.node_left
|
|
|
|
|
|
|
|
end tree
|