Library mathcomp.ssreflect.ssrbool

From mathcomp Require Import ssreflect ssrfun.
From Coq Require Export ssrbool.

Local additions: {pred T} == a type convertible to pred T but that presents the pred_sort coercion class. PredType toP == the predType structure for toP : A -> pred T. relpre f r == the preimage of r by f, simplifying to r (f x) (f y). > These will become part of the core SSReflect library with Coq 8.11. 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.

Lemma simpl_pred_sortE T (p : pred T) : (SimplPred p : {pred T }) =1 p.
Definition inE := (inE , simpl_pred_sortE ).

Definition PredType : ∀ T pT, (pT → pred T ) → predType T.
Defined.

Definition simpl_rel T := T → simpl_pred T.
Definition SimplRel {T} (r : rel T) : simpl_rel T := fun x ⇒ SimplPred (r x).
Coercion rel_of_simpl_rel T (sr : simpl_rel T) : rel T := sr.

Notation "[ 'rel' x y | E ]" := (SimplRel (fun x y ⇒ E%B)) (at level 0,
  x ident, y ident, format "'[hv' [ 'rel' x y | '/ ' E ] ']'") : fun_scope.
Notation "[ 'rel' x y : T | E ]" := (SimplRel (fun x y : T ⇒ E%B)) (at level 0,
  x ident, y ident, only parsing) : fun_scope.
Notation "[ 'rel' x y 'in' A & B | E ]" :=
  [rel x y | (x \in A) && (y \in B) && E] (at level 0, x ident, y ident,
  format "'[hv' [ 'rel' x y 'in' A & B | '/ ' E ] ']'") : fun_scope.
Notation "[ 'rel' x y 'in' A & B ]" := [rel x y | (x \in A) && (y \in B)]
  (at level 0, x ident, y ident,
  format "'[hv' [ 'rel' x y 'in' A & B ] ']'") : fun_scope.
Notation "[ 'rel' x y 'in' A | E ]" := [rel x y in A & A | E]
  (at level 0, x ident, y ident,
  format "'[hv' [ 'rel' x y 'in' A | '/ ' E ] ']'") : fun_scope.
Notation "[ 'rel' x y 'in' A ]" := [rel x y in A & A] (at level 0,
  x ident, y ident, format "'[hv' [ 'rel' x y 'in' A ] ']'") : fun_scope.

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 }).

Lemma homo_sym : {homo f : x y / aR x y >-> rR x y } →
  {homo f : y x / aR x y >-> rR x y }.

Lemma mono_sym : {mono f : x y / aR x y >-> rR x y } →
  {mono f : y x / aR x y >-> rR x y }.

Lemma homo_sym_in : {in aD &, {homo f : x y / aR x y >-> rR x y }} →
  {in aD &, {homo f : y x / aR x y >-> rR x y }}.

Lemma mono_sym_in : {in aD &, {mono f : x y / aR x y >-> rR x y }} →
  {in aD &, {mono f : y x / aR x y >-> rR x y }}.

Lemma homo_sym_in11 : {in aD & aD', {homo f : x y / aR x y >-> rR x y }} →
  {in aD' & aD , {homo f : y x / aR x y >-> rR x y }}.

Lemma mono_sym_in11 : {in aD & aD', {mono f : x y / aR x y >-> rR x y }} →
  {in aD' & aD , {mono f : y x / aR x y >-> rR x y }}.

End HomoMonoMorphismFlip.

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

Lemma onW_can_in : {in rD , cancel g f } → {in rD , {on aD , cancel g & f }}.

Lemma in_onW_can : cancel g f → {in rD , {on aD , cancel g & f }}.

Lemma onS_can : (∀ x, g x \in aD ) → {on aD , cancel g & f } → cancel g f.

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

Lemma in_onS_can : (∀ x, g x \in aD ) →
  {in rT , {on aD , cancel g & f }} → cancel g f.

End CancelOn.

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 , ∀ x y, aR (g x) y → rR x (f y)}.

Lemma homoLR_in :
    {in aD &, {homo f : x y / aR x y >-> rR x y }} →
  {in aD & rD , ∀ x y, aR x (g y) → rR (f x) y }.

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

Lemma monoLR_in :
    {in aD &, {mono f : x y / aR x y >-> rR x y }} →
  {in aD & rD , ∀ x y, rR (f x) y = aR x (g y)}.

Lemma monoRL_in :
    {in aD &, {mono f : x y / aR x y >-> rR x y }} →
  {in rD & aD , ∀ x y, rR x (f y) = aR (g x) y }.

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

End MonoHomoMorphismTheory_in.

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

Lemma inj_can_sym_on : {in aD , cancel f g } →
  {on aD &, injective g } → {on aD , cancel g & f }.

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

End inj_can_sym_in_on.