Library GraphTheory.dom

From mathcomp Require Import all_ssreflect.
Require Import preliminaries digraph sgraph.

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

Set Bullet Behavior "Strict Subproofs".

Domination Theory

Hereditary and superhereditary properties

Section Hereditary.
Variable (T : finType).

Implicit Types (p : pred {set T}) (F D : {set T}).

Definition hereditary p : bool := [ (D : {set T} | p D), (F : {set T} | F \subset D), p F].

Definition superhereditary p : bool := hereditary [pred D | p (~: D)].

Proposition hereditaryP p :
  reflect ( D F : {set T}, (F \subset D) p D p F) (hereditary p).
  apply: (iffP forall_inP) ⇒ [H1 D F FsubD pD|H2 D pD].
  - exact: (forall_inP (H1 _ pD)).
  - apply/forall_inPF FsubD; exact: H2 pD.

Proposition superhereditaryP (p : pred {set T}) :
  reflect ( D F : {set T}, (D \subset F) p D p F) (superhereditary p).
  apply: (iffP (hereditaryP _)) ⇒ /= sh_p D F.
  all: by rewrite -setCS ⇒ /sh_p; rewrite ?setCK; auto.

Proposition maximal_indsysP p D : hereditary p
  reflect (p D v : T, v \notin D ~~ p (v |: D)) (maxset p D).
  move/hereditaryPp_hereditary; apply: (iffP maxset_properP).
  - casepD maxD; split ⇒ // v vD. apply: maxD.
    by rewrite setUC properUl // sub1set.
  - casepD max1D; split ⇒ // A /properP [subA [v vA /max1D vD]].
    apply: contraNN vD; apply: p_hereditary; by rewrite subUset sub1set vA.

Proposition minimal_indsysP p D : superhereditary p
  reflect (p D v : T, v \in D ~~ p (D :\ v)) (minset p D).
  rewrite minmaxsetsh_p; apply: (iffP (maximal_indsysP _ _)) ⇒ //=.
  all: rewrite ?setCK ⇒ -[pD H]; split ⇒ // v; move: (H v).
  all: by rewrite !inE ?setCU ?setCK ?negbK setDE setIC.

End Hereditary.

Weighted Sets

Section Weighted_Sets.
Variables (T : finType) (weight : T nat).
Implicit Types (A B S : {set T}) (p : pred {set T}).

Definition weight_set (S : {set T}) := \sum_(v in S) weight v.
Let W := weight_set.

Lemma leqwset A B : A \subset B W A W B.
Proof. moveAsubB ; by rewrite [X in _ X](big_setID A) /= (setIidPr AsubB) leq_addr. Qed.

Hypothesis positive_weights : v : T, weight v > 0.

Lemma wset0 A : (A == set0) = (W A == 0).
  - moveDempty ; rewrite /weight_set.
    move: Dempty →. exact: big_set0.
  - move⇒ /eqP weightzero.
    apply/eqP ; move: weightzero.
    apply: contraLR ⇒ /set0Pn. elimx xinD.
    apply: lt0n_neq0 ; rewrite /W /weight_set (bigD1 x) //=.

Lemma ltnwset A B : A \proper B W A < W B.
  move ⇒ /properP [AsubB].
  elimx xinB xnotinA.
  rewrite {2}/W /weight_set (big_setID A) /= (setIidPr AsubB).
  rewrite -[X in X _]addn0 addSn -addnS leq_add2l lt0n.
  rewrite -/(weight_set _) -wset0.
  by apply/set0Pn; x; apply/setDP.

Lemma maxweight_maxset p A : p A ( B, p B W B W A) maxset p A.
  movepA maxA. apply/maxset_properP; split ⇒ // B /ltnwset; rewrite ltnNge.

Lemma minweight_minset p A : p A ( B, p B W A W B) minset p A.
  movepA minA; apply/minset_properP; split ⇒ // B /ltnwset; rewrite ltnNge.

Lemma arg_maxset p A : p A maxset p (arg_max A p W).
Proof. by movepA; apply/maxweight_maxset; case: arg_maxP. Qed.

Lemma arg_minset p A : p A minset p (arg_min A p W).
Proof. by movepA ; apply/minweight_minset; case: arg_minP. Qed.

End Weighted_Sets.

Section Domination_Theory.

Variable G : sgraph.

Stable, Dominating and Irredundant Sets

Section Stable_Set.

Variable S : {set G}.

Definition stable : bool := [disjoint NS(S) & S].

Local Lemma stableP_alt :
  reflect {in S&, u v, ~~ u -- v} [ u in S, v in S, ~~ (u -- v)].
Proof. apply: equivP (in11_in2 S S). do 2 (apply: forall_inPP ⇒ ?). exact: idP. Qed.

Lemma stableEedge : stable = [ u in S, v in S, ~~ (u -- v)].
  symmetry ; rewrite /stable ; apply/stableP_alt/disjointPstS.
  - movex /bigcupP [y yS adjyx] xS.
    move: adjyx. rewrite in_opn. apply/negP. by apply: stS.
  - movex y xS yS. apply/negPadjxy.
    exact: (stS y (mem_opns xS adjxy) yS).

Proposition stableP : reflect {in S&, u v, ~~ u -- v} stable.
Proof. rewrite stableEedge ; exact: stableP_alt. Qed.

Proposition stablePn : reflect ( x y, [/\ x \in S, y \in S & x -- y]) (~~ stable).
  rewrite stableEedge.
  set E := _, _.
  have EE : (exists2 x, x \in S & exists2 y, y \in S & x -- y) E by firstorder.
  rewrite !negb_forall_in; apply: equivP EE; apply: exists_inPPx.
  rewrite negb_forall_in; apply: exists_inPPy. exact: negPn.

End Stable_Set.

Lemma stable0 : stable set0.
Proof. by apply/stableP⇒ ? ? ; rewrite in_set0. Qed.

Lemma st_hereditary : hereditary stable.
  moveD F FsubD /stableP Dstable.
  apply/stablePu v uinF vinF.
  move: (subsetP FsubD u uinF) ⇒ uinD.
  move: (subsetP FsubD v vinF) ⇒ vinD.
  exact: Dstable.

Section Dominating_Set.

Variable D : {set G}.

Definition dominating : bool := [ v, v \in NS[D]].

Local Lemma dominatingP_alt : reflect
  ( v : G, v \notin D exists2 u : G, u \in D & u -- v)
  [ (v | v \notin D), u in D, u -- v].
Proof. apply: forall_inPPv; exact: exists_inP. Qed.

Lemma dominatingEedge : dominating = [ (v | v \notin D), u in D, u -- v].
  apply/forallP/forall_inP ⇒ [H v vND |H v].
  - have [u udomv] := bigcupP (H v).
    rewrite in_cln; case/predU1P ⇒ [?|uv]; first by subst;contrab.
    by apply/exists_inP; u.
  - case: (boolP (v \in D)) ⇒ [|/H/exists_inP[u uD uv]]; last exact: mem_clns uv.

Proposition dominatingP : reflect
  ( v : G, v \notin D exists2 u : G, u \in D & u -- v) dominating.
Proof. rewrite dominatingEedge; apply/dominatingP_alt. Qed.

Lemma dominatingPn :
  reflect (exists2 v : G, v \notin D & {in D, u, ~~ u -- v}) (~~ dominating).
  rewrite dominatingEedge negb_forall_in.
  apply: exists_inPPx; exact: exists_inPn.

End Dominating_Set.

Lemma domT : dominating [set: G].
Proof. apply/forallPx. exact: (subsetP (set_sub_clns _)). Qed.

Lemma dom_superhereditary : superhereditary dominating.
  apply/superhereditaryPD F /subsetP DsubF /dominatingP Ddom.
  apply/dominatingPv vnotinF.
  have/Ddom [w winD wv]: v \notin D by apply: contraNN vnotinF; exact: DsubF.
   w ⇒ //; exact: DsubF.

Section Irredundant_Set.

Variable D : {set G}.
Implicit Types x y v w : G.

Definition private_set (v : G) := N[v] :\: NS[D :\ v].

Lemma privateP v w :
  reflect (v -*- w {in D, u, u -*- w u = v}) (w \in private_set v).
  apply: (iffP setDP); rewrite !in_cln ⇒ -[v_dom_w H]; split ⇒ //.
  - moveu inD u_dom_w; apply: contraNeq HuDv.
    apply/bigcupP; u; by [exact/setD1P|rewrite in_cln].
  - apply/negP ⇒ /bigcupP [u /setD1P [uDv /H]]. rewrite in_clnX {}/X.

Definition irredundant : bool := [ v : G, (v \in D) ==> (private_set v != set0)].

Proposition irredundantP: reflect {in D, v, (private_set v != set0)} irredundant.
  rewrite /irredundant ; apply: (iffP forallP).
  - moveH1 v vinD. by move/implyP: (H1 v) ⇒ /(_ vinD).
  - moveH2 v. apply/implyPvinD. by move: (H2 v vinD).

Proposition irredundantPn : reflect (exists2 v, v \in D & private_set v == set0) (~~ irredundant).
  rewrite /irredundant ; apply: (iffP forall_inPn) ; last first.
  - casex xinD H1. by x ; rewrite ?xinD ?H1.
  - casex xinD H2; rewrite negbK in H2. by x.

End Irredundant_Set.

Lemma irr0 : irredundant set0.
Proof. apply/irredundantPv ; by rewrite in_set0. Qed.

Lemma irr_hereditary : hereditary irredundant.
  moveD F FsubD /irredundantP Dirr.
  apply/irredundantPv vinF.
  move: (subsetP FsubD v vinF) ⇒ vinD.
  move: (Dirr v vinD).
  case/set0Pnx /privateP [vdomx H1]. apply/set0Pn; x.
  apply/privateP ; split⇒ //.
  moveu uinF udomx. move: (subsetP FsubD u uinF) ⇒ uinD.
  exact: (H1 u uinD udomx).

Fundamental facts about Domination Theory

Section Relations_between_stable_dominating_irredundant_sets.

Variable D : {set G}.

Theorem maximal_st_iff_st_dom : maxset stable D (stable D dominating D).
  rewrite -(rwP (maximal_indsysP _ st_hereditary)).
  rewrite /iff ; split ; last first.
  - move⇒ [ stableD /dominatingP dominatingD].
    split ⇒ // v vnotinD.
    have [w winD adjwv] := dominatingD _ vnotinD.
    apply/stablePn; v; w.
    by rewrite !inE eqxx winD sgP adjwv orbT.
  - move ⇒ [stableD H1]; split⇒ //.
    apply/dominatingPx xnotinD.
    have/stablePn [w [z [winDcupx zinDcupx adjwz]]] := H1 x xnotinD.
    case: (eqVneq z x) ⇒ [zisx|zisnotx].
    + by subst z; w ⇒ //; rewrite !inE (sg_edgeNeq adjwz) in winDcupx.
    + have zinD : z \in D by rewrite !inE (negbTE zisnotx) /= in zinDcupx.
       z ⇒ //.
      move: winDcupx; rewrite in_setU in_set1.
      case/predU1P ⇒ [|winD]; first by move<- ; rewrite sg_sym adjwz.
      have := stableP D stableD w z winD zinD.
      apply: contraR. by rewrite adjwz.

Theorem maximal_st_is_minimal_dom : maxset stable D minset dominating D.
  rewrite maximal_st_iff_st_dom ⇒ -[/stableP stableD dominatingD].
  apply/(minimal_indsysP _ dom_superhereditary); split⇒ // x xinD.
  apply/dominatingPn ; x ; first by rewrite in_setD1 eqxx andFb.
  movey /setD1P [_ yinD]. exact: stableD.

Theorem minimal_dom_iff_dom_irr : minset dominating D (dominating D irredundant D).
  rewrite -(rwP (minimal_indsysP _ dom_superhereditary)); split ; last first.
  - move⇒ [dominatingD /irredundantP irredundantD]; split ⇒ // v vinD.
    have/set0Pn [w /privateP [vdomw H1]] := irredundantD v vinD.
    apply/dominatingPn; w.
    + rewrite in_setD1 negb_and negbK orbC.
      case: (boolP (w \in D)) ⇒ //= /H1 → //. exact: dominates_refl.
    + moveu /setD1P [uneqv uinD].
      apply: contra_neqN uneqvuv.
      by apply: H1 ⇒ //; rewrite /dominates uv orbT.
  - move ⇒ [dominatingD H2] ; split⇒ //.
    apply/irredundantPv vinD.
    have/dominatingPn[w wnotinDminusv H3] := H2 v vinD.
    apply/set0Pn; w; apply/privateP ; split ; last first.
    + moveu uinD udomw.
      apply: contraTeq udomwuneqv.
      have uinDminusv : u \in D :\ v by rewrite in_setD1 uneqv uinD.
      rewrite /dominates negb_or (H3 u uinDminusv) andbT.
      by apply: contraNneq wnotinDminusv ⇒ <-.
    + rewrite /dominates ; case: (boolP (v == w)) ⇒ //= vneqw.
      move: wnotinDminusv ; rewrite in_setD1 eq_sym vneqw andTbwnotinD.
      have [u uinD] := dominatingP _ dominatingD w wnotinD.
      case: (boolP (u == v)) ⇒ [|uneqv] ; first by move/eqP→.
      have uinDminusv : u \in D :\ v by rewrite in_setD1 uneqv uinD.
      by rewrite (negbTE (H3 u uinDminusv)).

Theorem minimal_dom_is_maximal_irr : minset dominating D maxset irredundant D.
  rewrite minimal_dom_iff_dom_irr -(rwP (maximal_indsysP _ irr_hereditary)).
  move⇒ [dominatingD irredundantD]; split⇒ // v vnotinD.
  apply/irredundantPn; v; first by rewrite in_setU1 eqxx.
  apply: contraNT vnotinD ⇒ /set0Pn [x /privateP [vdomx xpriv]].
  have/bigcupP [u uinD udomx] := forallP dominatingD x.
  by rewrite -[v](xpriv u) -?in_cln // inE uinD orbT.

End Relations_between_stable_dominating_irredundant_sets.

Section Existence_of_stable_dominating_irredundant_sets.

Definition max_st := maxset stable.

Definition min_dom := minset dominating.

Definition max_irr := maxset irredundant.

Definition inhb_max_st := s2val (maxset_exists stable0).

Definition inhb_min_dom := s2val (minset_exists domT).

Definition inhb_max_irr := s2val (maxset_exists irr0).

Lemma inhb_max_st_is_maximal_stable : max_st inhb_max_st.
Proof. exact: (s2valP (maxset_exists stable0)). Qed.

Lemma inhb_min_dom_is_minimal_dominating : min_dom inhb_min_dom.
Proof. exact: (s2valP (minset_exists domT)). Qed.

Lemma inhb_max_irr_is_maximal_irredundant : max_irr inhb_max_irr.
Proof. exact: (s2valP (maxset_exists irr0)). Qed.

End Existence_of_stable_dominating_irredundant_sets.

Section Weighted_domination_parameters.

Variable weight : G nat.
Hypothesis positive_weights : v : G, weight v > 0.

Let W := weight_set weight.

Definition ir_w : nat := W (arg_min inhb_max_irr max_irr W).

Fact ir_min D : max_irr D ir_w W D.
  rewrite /ir_w.
  by case: (arg_minP W inhb_max_irr_is_maximal_irredundant) ⇒ A _ ; apply.

Fact ir_witness : exists2 D, max_irr D & W D = ir_w.
  rewrite /ir_w.
  case: (arg_minP W inhb_max_irr_is_maximal_irredundant) ⇒ D.
  by D.

Fact ir_minset D : max_irr D W D = ir_w minset max_irr D.
  movemax_irrD irD; apply: minweight_minset ⇒ // A.
  rewrite -/W irD; exact: ir_min.

Definition gamma_w : nat := W (arg_min setT dominating W).

Fact gamma_min D : dominating D gamma_w W D.
Proof. rewrite /gamma_w. case: (arg_minP W domT) ⇒ A _ ; apply. Qed.

Fact gamma_witness : exists2 D, dominating D & W D = gamma_w.
  rewrite /gamma_w.
  case: (arg_minP W domT) ⇒ D.
  by D.

Fact gamma_minset D : dominating D W D = gamma_w minset dominating D.
  movedomD gammaD; apply: minweight_minset ⇒ // A.
  rewrite -/W gammaD; exact: gamma_min.

Definition ii_w : nat := W (arg_min inhb_max_st max_st W).

Fact ii_min S : max_st S ii_w W S.
  rewrite /ii_w.
  by case: (arg_minP W inhb_max_st_is_maximal_stable) ⇒ A _ ; apply.

Fact ii_witness : exists2 S, max_st S & W S = ii_w.
  rewrite /ii_w.
  case: (arg_minP W inhb_max_st_is_maximal_stable) ⇒ S.
  by S.

Fact ii_minset D : max_st D W D = ii_w minset max_st D.
  movemax_stD iiD; apply: minweight_minset ⇒ // A.
  rewrite -/W iiD; exact: ii_min.

Definition alpha_w : nat := W (arg_max set0 stable W).

Fact alpha_max S : stable S W S alpha_w.
Proof. by move: S; rewrite /alpha_w; case: (arg_maxP W stable0). Qed.

Fact alpha_witness : exists2 S, stable S & W S = alpha_w.
Proof. by rewrite /alpha_w; case: (arg_maxP W stable0) ⇒ A; A. Qed.

Fact alpha_maxset S : stable S W S = alpha_w maxset stable S.
  movestS alphaS; apply: maxweight_maxset ⇒ // A.
  rewrite -/W alphaS; exact: alpha_max.

Definition Gamma_w : nat := W (arg_max inhb_min_dom min_dom W).

Fact Gamma_max D : min_dom D W D Gamma_w.
  move: D ; rewrite /Gamma_w.
  by case: (arg_maxP W inhb_min_dom_is_minimal_dominating).

Fact Gamma_witness : exists2 D, min_dom D & W D = Gamma_w.
  rewrite /Gamma_w.
  case: (arg_maxP W inhb_min_dom_is_minimal_dominating) ⇒ D.
  by D.

Fact Gamma_maxset D : min_dom D W D = Gamma_w maxset min_dom D.
  movemin_domD GammaD; apply: maxweight_maxset ⇒ // A.
  rewrite -/W GammaD; exact: Gamma_max.

Definition IR_w : nat := W (arg_max set0 irredundant W).

Fact IR_max D : irredundant D W D IR_w.
Proof. by move: D; rewrite /IR_w; case: (arg_maxP W irr0). Qed.

Fact IR_witness : exists2 D, irredundant D & W D = IR_w.
Proof. by rewrite /IR_w; case: (arg_maxP W irr0) ⇒ D; D. Qed.

Fact IR_maxset D : irredundant D W D = IR_w maxset irredundant D.
  moveirrD IRD; apply: maxweight_maxset ⇒ // A.
  rewrite -/W IRD; exact: IR_max.

Weighted version of the Cockayne-Hedetniemi domination chain.

Proposition ir_w_leq_gamma_w : ir_w gamma_w.
  rewrite /gamma_w.
  have [D domD minWD] := arg_minP W domT.
  have min_domD := minweight_minset positive_weights domD minWD.
  have max_irrD := minimal_dom_is_maximal_irr min_domD.
  exact: ir_min.

Proposition gamma_w_leq_ii_w : gamma_w ii_w.
  rewrite /ii_w.
  have [S max_stS _] := arg_minP W inhb_max_st_is_maximal_stable.
  have domS := minsetp (maximal_st_is_minimal_dom max_stS).
  exact: gamma_min.

Proposition ii_w_leq_alpha_w : ii_w alpha_w.
  rewrite /alpha_w.
  have [S stS maxWS] := arg_maxP W stable0.
  have max_stS := maxweight_maxset positive_weights stS maxWS.
  exact: ii_min.

Proposition alpha_w_leq_Gamma_w : alpha_w Gamma_w.
  rewrite /alpha_w.
  have [S stS maxWS] := arg_maxP W stable0.
  have max_stS := maxweight_maxset positive_weights stS maxWS.
  have min_domS := maximal_st_is_minimal_dom max_stS.
  exact: Gamma_max.

Proposition Gamma_w_leq_IR_w : Gamma_w IR_w.
  rewrite /Gamma_w.
  have [D min_domD _] := arg_maxP W inhb_min_dom_is_minimal_dominating.
  have irrD := maxsetp (minimal_dom_is_maximal_irr min_domD).
  exact: IR_max.

Theorem Cockayne_Hedetniemi_chain_w:
  sorted leq [:: ir_w; gamma_w; ii_w; alpha_w; Gamma_w; IR_w].
rewrite /sorted /= ir_w_leq_gamma_w gamma_w_leq_ii_w ii_w_leq_alpha_w.
by rewrite alpha_w_leq_Gamma_w Gamma_w_leq_IR_w.

Notation Cockayne_Hedetniemi_w i j :=
  (@sorted_leq_nth _ Cockayne_Hedetniemi_chain_w i j erefl erefl erefl).

Let gamma_w_leq_Gamma_w: gamma_w Gamma_w.
Proof. exact: (Cockayne_Hedetniemi_w 1 4). Qed.

End Weighted_domination_parameters.

Arguments ir_w : clear implicits.
Arguments gamma_w : clear implicits.
Arguments ii_w : clear implicits.
Arguments alpha_w : clear implicits.
Arguments Gamma_w : clear implicits.
Arguments IR_w : clear implicits.

Classic (unweighted) parameters (use cardinality instead of weight)

Section Classic_domination_parameters.

Definition ones : (G nat) := (fun _ ⇒ 1).

Let W1 : ({set G} nat) := (fun A#|A|).

Lemma cardwset1 (A : {set G}) : #|A| = weight_set ones A.
Proof. by rewrite /weight_set sum1dep_card cardsE. Qed.

Local Notation eq_arg_min := (eq_arg_min _ (frefl _) cardwset1).
Local Notation eq_arg_max := (eq_arg_max _ (frefl _) cardwset1).

Definition of unweighted parameters and its conversion to weighted ones.

Definition ir : nat := #|arg_min inhb_max_irr max_irr W1|.

Fact eq_ir_ir1 : ir = ir_w ones.
Proof. by rewrite /ir /ir_w -cardwset1 eq_arg_min. Qed.

Definition gamma : nat := #|arg_min setT dominating W1|.

Fact eq_gamma_gamma1 : gamma = gamma_w ones.
Proof. by rewrite /gamma /gamma_w -cardwset1 eq_arg_min. Qed.

Definition ii : nat := #|arg_min inhb_max_st max_st W1|.

Fact eq_ii_ii1 : ii = ii_w ones.
Proof. by rewrite /ii /ii_w -cardwset1 eq_arg_min. Qed.

Definition alpha : nat := #|arg_max set0 stable W1|.

Fact eq_alpha_alpha1 : alpha = alpha_w ones.
Proof. by rewrite /alpha /alpha_w -cardwset1 eq_arg_max. Qed.

Definition Gamma : nat := #|arg_max inhb_min_dom min_dom W1|.

Fact eq_Gamma_Gamma1 : Gamma = Gamma_w ones.
Proof. by rewrite /Gamma /Gamma_w -cardwset1 eq_arg_max. Qed.

Definition IR : nat := #|arg_max set0 irredundant W1|.

Fact eq_IR_IR1 : IR = IR_w ones.
Proof. by rewrite /IR /IR_w -cardwset1 eq_arg_max. Qed.

Classic Cockayne-Hedetniemi domination chain.

Corollary ir_leq_gamma : ir gamma.
Proof. by rewrite eq_ir_ir1 eq_gamma_gamma1 ir_w_leq_gamma_w. Qed.

Corollary gamma_leq_ii : gamma ii.
Proof. by rewrite eq_gamma_gamma1 eq_ii_ii1 gamma_w_leq_ii_w. Qed.

Corollary ii_leq_alpha : ii alpha.
Proof. by rewrite eq_ii_ii1 eq_alpha_alpha1 ii_w_leq_alpha_w. Qed.

Corollary alpha_leq_Gamma : alpha Gamma.
Proof. by rewrite eq_alpha_alpha1 eq_Gamma_Gamma1 alpha_w_leq_Gamma_w. Qed.

Corollary Gamma_leq_IR : Gamma IR.
Proof. by rewrite eq_Gamma_Gamma1 eq_IR_IR1 Gamma_w_leq_IR_w. Qed.

Corollary Cockayne_Hedetniemi_chain:
  sorted leq [:: ir; gamma; ii; alpha; Gamma; IR].
rewrite /sorted /= ir_leq_gamma gamma_leq_ii ii_leq_alpha.
by rewrite alpha_leq_Gamma Gamma_leq_IR.

Notation Cockayne_Hedetniemi i j :=
  (@sorted_leq_nth _ Cockayne_Hedetniemi_chain i j erefl erefl erefl).

End Classic_domination_parameters.

End Domination_Theory.

Arguments ir_w : clear implicits.
Arguments gamma_w : clear implicits.
Arguments ii_w : clear implicits.
Arguments alpha_w : clear implicits.
Arguments Gamma_w : clear implicits.
Arguments IR_w : clear implicits.
Arguments ir : clear implicits.
Arguments gamma : clear implicits.
Arguments ii : clear implicits.
Arguments alpha : clear implicits.
Arguments Gamma : clear implicits.
Arguments IR : clear implicits.