Require Import Nat.
Require Import Lia.
Require Import Coq.Arith.Compare_dec.

Inductive tree : Type :=
| leaf (n : nat)
| node (l : tree) (r : tree).

Fixpoint tree_max (t : tree) : nat :=
  match t with
  | leaf x => x
  | node l r => max (tree_max l) (tree_max r)
  end.

Fixpoint insert (x : nat) (t : tree) : tree :=
  match t with
  | leaf y => node (leaf (min x y)) (leaf (max x y))
  | node l r => if x <? (tree_max l) then
        node (insert x l) r
      else
        node l (insert x r)
  end.

Lemma max_min : forall n m, max n m >= min n m.
Proof.
  intros. lia.
Qed.

Lemma min_P : forall (P : nat -> Prop) n m, P n -> P m -> P (min n m).
Proof.
intros P n m Hn Hm.
  destruct (le_lt_dec n m) as [H | H].
  - apply min_l in H. rewrite H. assumption.
  - apply le_S in H. apply min_r in H. simpl in H. injection H as H0. rewrite H0. assumption.
Qed.

Lemma max_P : forall (P : nat -> Prop) n m, P n -> P m -> P (max n m).
Proof.
intros P n m Hn Hm.
  destruct (le_lt_dec m n) as [H | H].
  - apply max_l in H. rewrite H. assumption.
  - apply le_S in H. apply max_r in H. simpl in H. injection H as H0. rewrite H0. assumption.
Qed.
  

Inductive all (P : nat -> Prop) : tree -> Prop :=
| all_leaf : forall n, P n -> all P (leaf n)
| all_node : forall l r, all P l -> all P r -> all P (node l r).

Lemma all_insert : forall (P : nat -> Prop) x t, P x
                                 -> all P t
                                 -> all P (insert x t).
Proof.
  intros. induction t.
  - apply all_node; apply all_leaf.
    + inversion H0. apply min_P; assumption.
    + inversion H0. apply max_P; assumption.
  - simpl. destruct (x <? tree_max t1).
    + apply all_node. inversion H0. apply IHt1. assumption.
      inversion H0. assumption.
    + apply all_node. inversion H0. assumption. inversion H0.
      apply IHt2. assumption.
Qed.


Lemma max_n_m : forall x n m, x <? n = false -> x <? m = false -> (x <? max n m <> true ).
Proof.
  intros x n m H1 H2.
  destruct (le_lt_dec n m) as [H | H].
  - apply max_r in H. rewrite H. intro Hc. rewrite H2 in Hc. discriminate.
  - apply le_S in H. apply max_l in H. simpl in H. injection H as H0. rewrite H0. intros Hc. rewrite H1 in Hc. discriminate.
Qed.
  

Lemma max_insert : forall x t, x <? tree_max t = true -> tree_max (insert x t) = tree_max t.
Proof.
  intros. induction t.
  - simpl. simpl in H. unfold ltb in H. apply leb_complete in H.
    rewrite max_r. apply max_r. apply le_S in H. apply le_S_n. assumption.
    apply max_min.
  - destruct (x <? tree_max t1) eqn:Hbt1; simpl; rewrite Hbt1; simpl.
    + rewrite IHt1; reflexivity.
    + destruct (x <? tree_max t2) eqn:Hbt2.
      * rewrite IHt2; reflexivity.
      * contradiction (max_n_m x (tree_max t1) (tree_max t2) Hbt1 Hbt2).
Qed.


Inductive Sorted : tree -> Type :=
| sorted_leaf : forall n, Sorted (leaf n)
| sorted_node : forall l r,
    all (fun x => x >= (tree_max l)) r ->
    Sorted l ->
    Sorted r ->
    Sorted (node l r).

Theorem insert_invariant : forall x t , Sorted t -> Sorted (insert x t).
Proof.
  intros.
  induction H.
  - apply sorted_node; try apply sorted_leaf.
    + apply all_leaf. apply max_min.
  - simpl. destruct (x <? tree_max l) eqn:Hx; apply sorted_node; try assumption.
    + apply max_insert in Hx. rewrite Hx. assumption.
    + apply all_insert.
      * apply leb_complete_conv in Hx. apply le_S_n. assumption.
      * assumption.
Qed.