Require Import Arith List Bool. From Equations Require Import Equations. Set Implicit Arguments. Inductive btree (T : Type) : Type := Leaf | Node (val : T) (t1 t2 : btree T). Arguments Leaf {T}. Fixpoint rev_tree {T : Type} (t : btree T) : btree T := match t with | Leaf => Leaf | Node x t1 t2 => Node x (rev_tree t2) (rev_tree t1) end. Fixpoint count {T : Type} (p : T -> bool) (t : btree T) : nat := match t with | Leaf => 0 | Node x t1 t2 => (if p x then 1 else 0) + (count p t1 + count p t2) end. Definition size {T : Type} (t : btree T) := count (fun x => true) t. Lemma count_rev_tree {T} (p : T -> bool) t : count p (rev_tree t) = count p t. Proof. induction t as [ | a t1 IH1 t2 IH2]. easy. simpl. rewrite IH1. rewrite IH2. rewrite (Nat.add_comm (count p t2)). easy. Qed. Require Import Wellfounded. Definition size_ind {T : Type} : forall P : btree T -> Prop, (forall t, (forall t', size t' < size t -> P t') -> P t) -> forall t, P t := well_founded_induction (wf_inverse_image _ _ _ (@size T) PeanoNat.Nat.lt_wf_0). Check size_ind. Lemma size1 {T} (a : T) t1 t2 : size t1 < size (Node a t1 t2). Proof. unfold size; simpl. unfold lt; apply Peano.le_n_S, Nat.le_add_r. Qed. Lemma size2 {T} (a : T) t1 t2 : size t2 < size (Node a t1 t2). Proof. unfold size; simpl. unfold lt; apply Peano.le_n_S; rewrite Nat.add_comm; apply Nat.le_add_r. Qed. Lemma redo_count_rev_tree {T} (p : T -> bool) t : count p (rev_tree t) = count p t. Proof. induction t as [t IH] using size_ind. destruct t as [ | a t1 t2]. easy. simpl. rewrite IH. rewrite IH. rewrite (Nat.add_comm (count p t2)). easy. apply size1. apply size2. Qed. Section redo_rev. Variable (T : Type). Definition ltt (t1 t2 : btree T) := size t1 < size t2. Equations redo_rev_tree (t : btree T) : btree T := redo_rev_tree t by rec t ltt := redo_rev_tree Leaf := Leaf ; redo_rev_tree (Node a t1 t2) := Node a (redo_rev_tree t2) (redo_rev_tree t1). Next Obligation. apply size2. Qed. Next Obligation. apply size1. Qed. End redo_rev. Lemma same_rev T (t : btree T) : redo_rev_tree t = rev_tree t. Proof. apply (redo_rev_tree_elim (fun t x => x = rev_tree t)). easy. intros a t1 t2 IH1 IH2; simpl; rewrite IH1, IH2. easy. Qed.