Library mathcomp_eulerian.perm_compress

From mathcomp Require Import all_ssreflect fingroup perm.
From mathcomp_eulerian Require Import ordinal_reindex.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.


Section DropPerm.
Variables (n : nat) (s : {perm 'I_n.+1}).

Fact drop_fun_ne (i : 'I_n) : s ord_max != s (lift ord_max i).
Proof. by apply/eqP ⇒ /perm_inj /eqP; rewrite (negbTE (neq_lift _ _)). Qed.

Definition drop_fun (i : 'I_n) : 'I_n := sval (unlift_some (drop_fun_ne i)).

Lemma drop_funE i : s (lift ord_max i) = lift (s ord_max) (drop_fun i).
Proof. by rewrite /drop_fun; case: (unlift_some _) ⇒ /= j → _. Qed.

Lemma drop_fun_inj : injective drop_fun.
Proof. by move⇒ i1 i2 /(congr1 (lift (s ord_max))); rewrite -!drop_funE ⇒ /perm_inj/lift_inj. Qed.

Definition drop_perm : {perm 'I_n} := perm drop_fun_inj.

Lemma drop_permE i : drop_perm i = drop_fun i.
Proof. by rewrite permE. Qed.

Lemma lift_drop_permE i :
  lift (s ord_max) (drop_perm i) = s (lift ord_max i).
Proof. by rewrite drop_permE -drop_funE. Qed.

End DropPerm.


Section LiftPerm.
Variables (n : nat) (k : 'I_n.+1) (t : {perm 'I_n}).

Definition lift_fun (i : 'I_n.+1) : 'I_n.+1 :=
  match unlift ord_max i with
  | Some j ⇒ lift k (t j)
  | None ⇒ k
  end.

Lemma lift_fun_ord_max : lift_fun ord_max = k.
Proof. by rewrite /lift_fun unlift_none. Qed.

Lemma lift_fun_lift i : lift_fun (lift ord_max i) = lift k (t i).
Proof. by rewrite /lift_fun liftK. Qed.

Lemma lift_fun_inj : injective lift_fun.
Proof.
move⇒ i1 i2; rewrite /lift_fun.
case: unliftP ⇒ [j1 ->|->]; case: unliftP ⇒ [j2 ->|->] //.
- by move/lift_inj/perm_inj→.
- by move/eqP; rewrite eq_sym (negbTE (neq_lift _ _)).
- by move/eqP; rewrite (negbTE (neq_lift _ _)).
Qed.

Definition lift_perm : {perm 'I_n.+1} := perm lift_fun_inj.

Lemma lift_permE i : lift_perm i = lift_fun i.
Proof. by rewrite permE. Qed.

Lemma lift_perm_ord_max : lift_perm ord_max = k.
Proof. by rewrite lift_permE lift_fun_ord_max. Qed.

Lemma lift_perm_lift i : lift_perm (lift ord_max i) = lift k (t i).
Proof. by rewrite lift_permE lift_fun_lift. Qed.

Lemma lift_perm_ne_k i : i != ord_max → lift_perm i != k.
Proof.
case: (unliftP ord_max i) ⇒ [j ->|-> /eqP//] _.
by rewrite lift_perm_lift eq_sym neq_lift.
Qed.

End LiftPerm.


Section Cancellation.
Variable n : nat.

Lemma drop_perm_lift_perm (k : 'I_n.+1) (t : {perm 'I_n}) :
  drop_perm (lift_perm k t) = t.
Proof.
apply/permP ⇒ i; apply: (@lift_inj _ (lift_perm k t ord_max)).
by rewrite lift_drop_permE lift_perm_lift lift_perm_ord_max.
Qed.

Lemma lift_perm_drop_perm (s : {perm 'I_n.+1}) :
  lift_perm (s ord_max) (drop_perm s) = s.
Proof.
apply/permP ⇒ i; rewrite lift_permE /lift_fun.
by case: (unliftP ord_max i) ⇒ [j|]->//; rewrite lift_drop_permE.
Qed.

Lemma lift_perm_ord_max_eq (k : 'I_n.+1) (t : {perm 'I_n}) :
  (lift_perm k t) ord_max = k.
Proof. exact: lift_perm_ord_max. Qed.

End Cancellation.