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.
(*
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.