Merge pull request #519 from CohenCyril/homomono_in

Missing homo/mono lemmas in the presence of cancellation

1 files changed, 117 insertions, 0 deletions

diff --git a/mathcomp/ssreflect/ssrbool.v b/mathcomp/ssreflect/ssrbool.v
index 80dea3b..b1498cd 100644
--- a/mathcomp/ssreflect/ssrbool.v
+++ b/mathcomp/ssreflect/ssrbool.v
@@ -11,8 +11,16 @@ From Coq Require Export ssrbool.
 (* This file also anticipates a v8.11 change in the definition of simpl_pred  *)
 (* to T -> simpl_pred T. This change ensures that inE expands the definition  *)
 (* of r : simpl_rel along with the \in, when rewriting in y \in r x.          *)
+(*                                                                            *)
+(* This file also anticipates v8.13 additions as well as a generalization in  *)
+(* the statments of `homoRL_in`, `homoLR_in`, `homo_mono_in`, `monoLR_in`,    *)
+(* monoRL_in, and can_mono_in.                                                *)
 (******************************************************************************)
 
+(******************)
+(* v8.11 addtions *)
+(******************)
+
 Notation "{ 'pred' T }" := (pred_sort (predPredType T)) (at level 0,
   format "{ 'pred'  T }") : type_scope.
 
@@ -50,6 +58,10 @@ Notation xrelpre := (fun f (r : rel _) x y => r (f x) (f y)).
 Definition relpre {T rT} (f : T -> rT)  (r : rel rT) :=
   [rel x y | r (f x) (f y)].
 
+(******************)
+(* v8.13 addtions *)
+(******************)
+
 Section HomoMonoMorphismFlip.
 Variables (aT rT : Type) (aR : rel aT) (rR : rel rT) (f : aT -> rT).
 Variable (aD aD' : {pred aT}).
@@ -85,3 +97,108 @@ Arguments homo_sym_in {aT rT} [aR rR f aD].
 Arguments mono_sym_in {aT rT} [aR rR f aD].
 Arguments homo_sym_in11 {aT rT} [aR rR f aD aD'].
 Arguments mono_sym_in11 {aT rT} [aR rR f aD aD'].
+
+Section CancelOn.
+
+Variables (aT rT : predArgType) (aD : {pred aT}) (rD : {pred rT}).
+Variables (f : aT -> rT) (g : rT -> aT).
+
+Lemma onW_can : cancel g f -> {on aD, cancel g & f}.
+Proof. by move=> fgK x xaD; apply: fgK. Qed.
+
+Lemma onW_can_in : {in rD, cancel g f} -> {in rD, {on aD, cancel g & f}}.
+Proof. by move=> fgK x xrD xaD; apply: fgK. Qed.
+
+Lemma in_onW_can : cancel g f -> {in rD, {on aD, cancel g & f}}.
+Proof. by move=> fgK x xrD xaD; apply: fgK. Qed.
+
+Lemma onS_can : (forall x, g x \in aD) -> {on aD, cancel g & f} -> cancel g f.
+Proof. by move=> mem_g fgK x; apply: fgK. Qed.
+
+Lemma onS_can_in : {homo g : x / x \in rD >-> x \in aD} ->
+  {in rD, {on aD, cancel g & f}} -> {in rD, cancel g f}.
+Proof. by move=> mem_g fgK x x_rD; apply/fgK/mem_g. Qed.
+
+Lemma in_onS_can : (forall x, g x \in aD) ->
+  {in rT, {on aD, cancel g & f}} -> cancel g f.
+Proof. by move=> mem_g fgK x; apply/fgK. Qed.
+
+End CancelOn.
+Arguments onW_can {aT rT} aD {f g}.
+Arguments onW_can_in {aT rT} aD {rD f g}.
+Arguments in_onW_can {aT rT} aD rD {f g}.
+Arguments onS_can {aT rT} aD {f g}.
+Arguments onS_can_in {aT rT} aD {rD f g}.
+Arguments in_onS_can {aT rT} aD {f g}.
+
+Section MonoHomoMorphismTheory_in.
+
+Variables (aT rT : predArgType) (aD : {pred aT}) (rD : {pred rT}).
+Variables (f : aT -> rT) (g : rT -> aT) (aR : rel aT) (rR : rel rT).
+
+Hypothesis fgK : {in rD, {on aD, cancel g & f}}.
+Hypothesis mem_g : {homo g : x / x \in rD >-> x \in aD}.
+
+Lemma homoRL_in :
+    {in aD &, {homo f : x y / aR x y >-> rR x y}} ->
+  {in rD & aD, forall x y, aR (g x) y -> rR x (f y)}.
+Proof. by move=> Hf x y hx hy /Hf; rewrite fgK ?mem_g// ?inE; apply. Qed.
+
+Lemma homoLR_in :
+    {in aD &, {homo f : x y / aR x y >-> rR x y}} ->
+  {in aD & rD, forall x y, aR x (g y) -> rR (f x) y}.
+Proof. by move=> Hf x y hx hy /Hf; rewrite fgK ?mem_g// ?inE; apply. Qed.
+
+Lemma homo_mono_in :
+    {in aD &, {homo f : x y / aR x y >-> rR x y}} ->
+    {in rD &, {homo g : x y / rR x y >-> aR x y}} ->
+  {in rD &, {mono g : x y / rR x y >-> aR x y}}.
+Proof.
+move=> mf mg x y hx hy; case: (boolP (rR _ _))=> [/mg //|]; first exact.
+by apply: contraNF=> /mf; rewrite !fgK ?mem_g//; apply.
+Qed.
+
+Lemma monoLR_in :
+    {in aD &, {mono f : x y / aR x y >-> rR x y}} ->
+  {in aD & rD, forall x y, rR (f x) y = aR x (g y)}.
+Proof. by move=> mf x y hx hy; rewrite -{1}[y]fgK ?mem_g// mf ?mem_g. Qed.
+
+Lemma monoRL_in :
+    {in aD &, {mono f : x y / aR x y >-> rR x y}} ->
+  {in rD & aD, forall x y, rR x (f y) = aR (g x) y}.
+Proof. by move=> mf x y hx hy; rewrite -{1}[x]fgK ?mem_g// mf ?mem_g. Qed.
+
+Lemma can_mono_in :
+    {in aD &, {mono f : x y / aR x y >-> rR x y}} ->
+  {in rD &, {mono g : x y / rR x y >-> aR x y}}.
+Proof. by move=> mf x y hx hy; rewrite -mf ?mem_g// !fgK ?mem_g. Qed.
+
+End MonoHomoMorphismTheory_in.
+Arguments homoRL_in {aT rT aD rD f g aR rR}.
+Arguments homoLR_in {aT rT aD rD f g aR rR}.
+Arguments homo_mono_in {aT rT aD rD f g aR rR}.
+Arguments monoLR_in {aT rT aD rD f g aR rR}.
+Arguments monoRL_in {aT rT aD rD f g aR rR}.
+Arguments can_mono_in {aT rT aD rD f g aR rR}.
+
+Section inj_can_sym_in_on.
+Variables (aT rT : predArgType) (aD : {pred aT}) (rD : {pred rT}).
+Variables (f : aT -> rT) (g : rT -> aT).
+
+Lemma inj_can_sym_in_on :
+    {homo f : x / x \in aD >-> x \in rD} -> {in aD, {on rD, cancel f & g}} ->
+  {in rD &, {on aD &, injective g}} -> {in rD, {on aD, cancel g & f}}.
+Proof. by move=> fD fK gI x x_rD gx_aD; apply: gI; rewrite ?inE ?fK ?fD. Qed.
+
+Lemma inj_can_sym_on : {in aD, cancel f g} ->
+  {on aD &, injective g} -> {on aD, cancel g & f}.
+Proof. by move=> fK gI x gx_aD; apply: gI; rewrite ?inE ?fK. Qed.
+
+Lemma inj_can_sym_in : {homo f \o g : x / x \in rD} -> {on rD, cancel f & g} ->
+  {in rD &, injective g} ->  {in rD, cancel g f}.
+Proof. by move=> fgD fK gI x x_rD; apply: gI; rewrite ?fK ?fgD. Qed.
+
+End inj_can_sym_in_on.
+Arguments inj_can_sym_in_on {aT rT aD rD f g}.
+Arguments inj_can_sym_on {aT rT aD f g}.
+Arguments inj_can_sym_in {aT rT rD f g}.