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

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