# Names and permutations of names

Require Export Base.

Lemma not_disj (A B : Prop) :
~A -> ~B -> ~(A \/ B).
Proof.
intros H1 H2 [|]; auto.
Qed.

Definition Name := prod nat nat.

Implicit Type a b c : Name.

Definition rk a := snd a.

Instance char_eq_dec :
eq_dec Name.
Proof. auto. Qed.

Lemma name_eq a b :
a = b <-> fst a = fst b /\ rk a = rk b.
Proof.
split.
- intros. subst. auto.
- intros [H1 H2]. destruct a, b; auto.
Qed.

Lemma name_rk_neq a b :
rk a <> rk b -> a <> b.
Proof.
intros H1 H2 % name_eq. apply H1, H2.
Qed.

Hint Resolve name_eq name_rk_neq.

(*
A NameF is a function on names
*)

Definition NameF : Type := Name -> Name.

Implicit Type p : NameF.

Definition compose p p' :=
fun a => p (p' a).

Notation "p ** q" := (compose p q) (at level 40).

Definition Inv p p' : Prop :=
forall a, p' (p a) = a /\ p (p' a) = a.

(*
A permutation is a rank preserving action that has an inverse.
Making it a Prop on NameF instead of a Type turned out to be easier.
*)

Definition Perm p :=
(forall a, rk a = rk (p a)) /\ (exists p', Inv p p').

Hint Unfold Perm.

Lemma perm_inv p p' a :
Inv p p' -> p' (p a) = a.
Proof.
intros H. apply H.
Qed.

Lemma perm_inv' p p' a :
Inv p p' -> p (p' a) = a.
Proof.
intros H. apply H.
Qed.

(* Simpl tactic to solve inverse permutations on names *)
Ltac solve_perm_inv_name :=
unfold compose;
match goal with
| [ H : Inv ?p ?q |- ?p (?q ?a) = ?a ] => now apply perm_inv'
| [ H : Inv ?p ?q |- ?q (?p ?a) = ?a ] => now apply perm_inv
| [ H : Inv ?p ?q |- ?a = ?p (?q ?a) ] => symmetry; now apply perm_inv'
| [ H : Inv ?p ?q |- ?a = ?q (?p ?a) ] => symmetry; now apply perm_inv
end.

Hint Extern 4 => solve_perm_inv_name.

Lemma perm_id :
Perm id.
Proof.
unfold Perm, id, Inv. split; try reflexivity. exists id. now split.
Qed.

Lemma name_id p a :
id a = a.
Proof. reflexivity. Qed.

Lemma name_assoc p p' a :
(p ** p') a = p (p' a).
Proof. unfold compose. reflexivity. Qed.

(*
An action on Name is just a NameF is trivially a sym action.
*)

Fact sym_action_name :
forall a, id a = a /\ forall p q, (p**q) a = p (q a).
Proof.
intros. split.
- now apply name_id.
- intros p q. now apply name_assoc.
Qed.

(*
A permutation is bijective. Injectivity is useful in some proofs.
*)

Lemma perm_inj' p p' a b:
Inv p p' -> p a = p b <-> a = b.
Proof.
intros HP. split; try now intros ->.
intros H1. pose (HPa := HP a). pose (HPb := HP b).
destruct HPa as [HPa _], HPb as [HPb _]. congruence.
Qed.

Lemma perm_inj p a b:
Perm p -> p a = p b <-> a = b.
Proof.
intros [_ [p' HP]]. apply (perm_inj' a b HP).
Qed.

Lemma perm_inv_shift p p' a b :
Inv p p' -> p' b = a <-> b = p a.
Proof.
intros H1. pose (Ha := H1 a). pose (Hb := H1 b). destruct Ha, Hb. split; congruence.
Qed.

(*
The inverse property of two actions is commutative
*)

Lemma inv_comm p p' :
Inv p p' -> Inv p' p.
Proof.
intros H1. unfold Inv in *. intros a. specialize (H1 a). intuition.
Qed.

Lemma perm_inv_compose p p' :
Inv p p' -> forall c, (p ** p') c = c.
Proof.
intros H1 c. unfold compose. specialize (H1 c) as [_ H1]. exact H1.
Qed.

(*
The composition of 2 permutations still satisfies all permutaiton conditions
*)

Lemma perm_compose_perm p p' :
Perm p -> Perm p' -> Perm (p ** p').
Proof.
intros [H1 [q H2]] [H3 [q' H4]]. split; unfold compose.
- intros a. rewrite <-(H1 (p' a)), <-(H3 a). reflexivity.
- exists (q' ** q). unfold compose. split.
+ specialize (H2 (p' a)) as [-> _]. specialize (H4 a) as [-> _]. reflexivity.
+ specialize (H4 (q a)) as [_ ->]. specialize (H2 a) as [_ ->]. reflexivity.
Qed.

Lemma perm_inv_perm p p' :
Perm p -> Inv p p' -> Perm p'.
Proof.
intros [H1 _] H3. split.
- intros a. specialize (H1 (p' a)). specialize (H3 (a)) as [H3 H4].
rewrite H4 in H1. symmetry. exact H1.
- exists p. apply inv_comm, H3.
Qed.

Lemma perm_rk a b p :
Perm p -> rk a = rk b -> rk (p a) = rk (p b).
Proof.
intros [H1 _] H2. now rewrite <-H1, <-H1.
Qed.

Hint Resolve perm_rk perm_id perm_compose_perm perm_inv_perm inv_comm perm_inj perm_inj'.

## Transpositions

(*
A permutation that swaps two names is called a transposition.
*)

Definition transp a b : NameF :=
fun c => if Dec (c = a) then b else if Dec (c = b) then a else c.

Notation "a \$ b" := (transp a b)(at level 30).

(*
To resolve a transposition, two decisions have to be performed.
This tactic solves frequent trivial cases thereof.
*)

Ltac solve_dec :=
unfold compose, transp;
repeat match goal with
| [ |- context [Dec (?a = ?b)] ] => decide (a = b); try subst; try congruence
| [ H : context [Dec (?a = ?b)] |- _ ] => decide (a = b); try subst; try congruence
| [ H : ?p ?a = ?p ?b |- _ ] => apply perm_inj in H; try subst; try congruence; trivial
end.

(*
Transpositions are self-inverse.
*)

Lemma transp_inv a b :
Inv (a \$ b) (a \$ b).
Proof.
unfold Inv.
assert(H: forall c, (a\$b) ((a\$b) c) = c) by (intros; solve_dec).
intros c. unfold transp; split; apply H.
Qed.

Lemma transp_perm a b :
rk a = rk b -> Perm (a \$ b).
Proof.
intros H1. split.
- intros c. solve_dec.
- exists (a \$ b). apply transp_inv.
Qed.

Lemma transp_perm' a b p :
Perm p -> rk a = rk b -> Perm (p a \$ p b).
Proof.
intros [H1 H2] H3. split.
- intros c. unfold transp.
decide(c=p a); subst; auto.
decide(c=p b); subst; auto.
- exists (p a \$ p b). apply transp_inv.
Qed.

Lemma transp_rk a b :
Perm (a \$ b) -> rk a = rk b.
Proof.
intros [H1 _]. rewrite (H1 a). unfold transp. now decide(a=a).
Qed.

Lemma transp_perm_iff a b :
rk a = rk b <-> Perm (a \$ b).
Proof.
split. intros.
- now apply transp_perm.
- now apply transp_rk.
Qed.

Lemma transp_rk' a b c d :
(rk a = d /\ rk a = rk b /\ rk b = rk c) -> rk ((a\$b) c) = d.
Proof.
intros [H1 [H2 H3]]. solve_dec.
Qed.

Lemma transp_apply a b :
(a\$b) a = b.
Proof.
unfold transp. decide (a=a) as [E|]; auto.
Qed.

Lemma transp_compose p a b c :
Perm p -> (p ** a\$b) c = (p a \$ p b ** p) c.
Proof. intros. solve_dec. Qed.

Lemma transp_swap a b c :
(a \$ b) c = (b \$ a) c.
Proof. solve_dec. Qed.

Lemma transp_id a b :
(a\$a) b = b.
Proof. solve_dec. Qed.

Hint Resolve transp_id.

Lemma transp_diff a b c d :
d<>a -> d<>b -> d<>c -> d <> (a\$b) c.
Proof. intros. solve_dec. Qed.

Lemma transp_chain a b c d :
a <> b -> a <> c -> b <> c -> (b\$c ** a\$b) d =
(a\$b ** a\$c) d.
Proof. intros. solve_dec. Qed.

Lemma transp_chain'' a b c d :
a <> b -> a <> c -> c <> b -> (c\$b ** a\$c) d =
(a\$c ** a\$b) d.
Proof. intros. solve_dec. Qed.

Lemma transp_chain' a b c d e :
d<>c -> b<>a -> (((a\$c)b) \$ d ** a\$c) e =
(((b\$d)a) \$ c ** b\$d) e.
Proof. intros. solve_dec. Qed.

Hint Resolve transp_inv transp_compose transp_perm transp_perm'.