Ranked trees

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


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)).
  intros H1 H2. right. apply concat_map_el. now exists t.

  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.
  intros H1 x H2. inversion H1. auto.


  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).
    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.

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

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

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

  Lemma tree_swap_perm p p' :
    (forall a, a el names t -> p a = p' a) -> (p *> t) = (p' *> t).
    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).

  Permutations preserve wellrankedness

  Fact perm_tree_wr p :
    Perm p -> Twr (p *> t).
    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.

  Wellranked trees are nominal

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

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

End Action.