From Stdlib Require Import List Lia
  Logic.FunctionalExtensionality Logic.PropExtensionality.
Import ListNotations.

Definition node := list bool.

Definition isleaf (height : nat) (p : node) : Prop :=
  length p = height.

Definition in_complete_tree (height : nat) (p : node) : Prop :=
  length p ≤ height.

Definition prefix (p q : node) : Prop :=
  ∃ r, q = p ++ r.

Lemma prefix_refl (p : node) : prefix p p.

Lemma prefix_nil (p : node) : prefix [] p.

Lemma prefix_trans (p q r : node) :
  prefix p q → prefix q r → prefix p r.

Lemma prefix_length_le (p q : node) :
  prefix p q → length p ≤ length q.

Lemma prefix_eq_of_equal_length (p q : node) :
  prefix p q → length p = length q → p = q.

Definition occupied_leaf
    (height : nat) (bitmap : node → Prop) (p : node) : Prop :=
  isleaf height p ∧ bitmap p.

Definition nonempty_bitmap (height : nat) (bitmap : node → Prop) : Prop :=
  ∃ p, occupied_leaf height bitmap p.

Definition induced_nodes
    (height : nat) (bitmap : node → Prop) (p : node) : Prop :=
  ∃ l, isleaf height l ∧ bitmap l ∧ prefix p l.

Record rooted_connected_subtree
    (height : nat) (subtree : node → Prop) : Prop := {
  subtree_in_tree :
    ∀ p, subtree p → in_complete_tree height p;
  subtree_root :
    subtree [];
  subtree_ancestor_closed :
    ∀ p q, prefix p q → subtree q → subtree p;
}.

Definition contains_occupied_leaves
    (height : nat) (bitmap subtree : node → Prop) : Prop :=
  ∀ l, isleaf height l → bitmap l → subtree l.

Definition contains_exactly_occupied_leaves
    (height : nat) (bitmap subtree : node → Prop) : Prop :=
  ∀ l, isleaf height l → (subtree l ↔ bitmap l).

Definition every_node_on_occupied_path
    (height : nat) (bitmap subtree : node → Prop) : Prop :=
  ∀ p, subtree p → ∃ l, isleaf height l ∧ bitmap l ∧ prefix p l.

Definition minimal_connected_subtree
    (height : nat) (bitmap subtree : node → Prop) : Prop :=
  rooted_connected_subtree height subtree ∧
  contains_exactly_occupied_leaves height bitmap subtree ∧
  every_node_on_occupied_path height bitmap subtree ∧
  ∀ candidate,
    rooted_connected_subtree height candidate →
    contains_occupied_leaves height bitmap candidate →
    ∀ p, subtree p → candidate p.

Lemma induced_nodes_in_tree height bitmap :
  ∀ p, induced_nodes height bitmap p → in_complete_tree height p.

Lemma induced_nodes_root height bitmap :
  nonempty_bitmap height bitmap →
  induced_nodes height bitmap [].

Lemma induced_nodes_ancestor_closed height bitmap :
  ∀ p q,
    prefix p q →
    induced_nodes height bitmap q →
    induced_nodes height bitmap p.

Lemma induced_nodes_rooted_connected height bitmap :
  nonempty_bitmap height bitmap →
  rooted_connected_subtree height (induced_nodes height bitmap).

Lemma induced_nodes_exact_leaves height bitmap :
  contains_exactly_occupied_leaves height bitmap
    (induced_nodes height bitmap).

Lemma induced_nodes_path_property height bitmap :
  every_node_on_occupied_path height bitmap
    (induced_nodes height bitmap).

Lemma induced_nodes_minimal height bitmap :
  ∀ candidate,
    rooted_connected_subtree height candidate →
    contains_occupied_leaves height bitmap candidate →
    ∀ p,
      induced_nodes height bitmap p → candidate p.

Theorem induced_nodes_minimal_connected_subtree height bitmap :
  nonempty_bitmap height bitmap →
  minimal_connected_subtree height bitmap
    (induced_nodes height bitmap).

Lemma minimal_connected_subtree_iff_induced height bitmap subtree :
  minimal_connected_subtree height bitmap subtree →
  ∀ p, subtree p ↔ induced_nodes height bitmap p.

Theorem induced_subtree_exists_unique height bitmap :
  nonempty_bitmap height bitmap →
  ∃! subtree,
    minimal_connected_subtree height bitmap subtree.

Theorem merkle_commitments_induced_subtree_lemma height bitmap :
  nonempty_bitmap height bitmap →
  ∃! subtree,
    rooted_connected_subtree height subtree ∧
    contains_exactly_occupied_leaves height bitmap subtree ∧
    every_node_on_occupied_path height bitmap subtree ∧
    (∀ candidate,
      rooted_connected_subtree height candidate →
      contains_occupied_leaves height bitmap candidate →
      ∀ p, subtree p → candidate p).