# Ranked trees

Require Export Base.
Require Export Perm.
Require Export Lists.

## Definition

Inductive Tree : Type :=
TrA : Name -> list Tree -> Tree.

Implicit Types t : Tree.

(*
A default tree used for nth
*)

Definition DTR :=
TrA (0,0) nil.

Fixpoint names t : list Name :=
match t with TrA a xs => a :: (concat (map names xs)) end.

Lemma tree_name_in_sub a t a' l:
a el (names t) -> t el l -> a el (names (TrA a' l)).
Proof.
intros H1 H2. right. apply concat_map_el. now exists t.
Qed.

(*
A tree is wellranked, if
1. the list of subtrees is wellranked,
2. the length of the list of subtrees agrees with the rank of the name
*)

Inductive Twr : Tree -> Prop :=
treewrA a l : (forall t, t el l -> Twr t) -> |l| = rk a -> Twr (TrA a l).

Hint Resolve treewrA.

Lemma tree_wr_sub a l :
Twr (TrA a l) -> forall x, x el l -> Twr x.
Proof.
intros H1 x H2. inversion H1. auto.
Qed.

## Action

(*
A permutation applied to a tree.
*)

Fixpoint apply_perm p t : Tree :=
match t with TrA a xs => TrA (p a) (List.map (apply_perm p) xs) end.

Notation "p *> t" := (apply_perm p t) (at level 40).

Section Action.

Variable t : Tree.
Hypothesis HW : Twr t.

Lemma tree_assoc p p' :
(p ** p') *> t = p *> (p' *> t).
Proof.
induction HW as [a l H1 H2 _]. simpl. unfold compose in *. f_equal.
rewrite map_map. apply map_ext_in. intros t H3. apply H2; auto.
Qed.

Lemma tree_id :
id *> t = t.
Proof.
induction HW as [a l H3 H4 _]. simpl. f_equal.
rewrite map_ext_in with (g := (fun t => t)); auto using map_id.
Qed.

(*
( *> ) is a sym action for wellranked trees.
*)

Fact tree_sym :
id *> t = t /\ forall p q, (p ** q) *> t = p *> (q *> t).
Proof.
split.
- now apply tree_id.
- intros p q. now apply tree_assoc.
Qed.

Lemma tree_swap_perm p p' :
(forall a, a el names t -> p a = p' a) -> (p *> t) = (p' *> t).
Proof.
induction HW as [a l H1 H2 H3]. intros H4. simpl. f_equal.
- apply H4. now left.
- apply map_ext_in. intros t H5. apply H2; auto.
intros b H6. apply H4, (tree_name_in_sub a H6 H5).
Qed.

(*
Permutations preserve wellrankedness
*)

Fact perm_tree_wr p :
Perm p -> Twr (p *> t).
Proof.
induction HW as [a l H1 H2 H3]. intros H4. simpl. constructor.
- intros s [s'[<- H7]] % in_map_iff. apply H2; auto.
- destruct H4 as [H4 _]. now rewrite map_length, <- H4.
Qed.

(*
Wellranked trees are nominal
*)

Fact tree_nominal p :
(forall a, a el names t -> p a = a) -> p *> t = t.
Proof.
intros H1. rewrite tree_swap_perm with (p' := id); trivial. apply tree_id.
Qed.

Fact perm_apply_inv p p' :
Inv p p' -> t = p *> (p' *> t).
Proof.
intros H2.
rewrite <-(tree_assoc p p'), tree_swap_perm with (p':=id); try assumption.
- now rewrite tree_id.
- intros. apply H2.
Qed.

End Action.