Library MetaCoq.Template.utils.MCPred

From Coq Require Import List Bool Arith ssreflect ssrbool Morphisms Lia.
From MetaCoq.Template Require Import MCPrelude MCReflect MCList MCRelations MCProd MCOption.
From Equations Require Import Equations.

Definition predA {A} (p q : pred A) : pred A := (fun i ⇒ p i ==> q i).


#[global] Instance orP_Proper {A} : Proper (`=1` ==> `=1` ==> `=1`) (@predU A).
Proof.
  intros f g Hfg f' g' Hfg' i; rewrite /predU /=.
  now rewrite Hfg Hfg'.
Qed.

#[global] Instance andP_Proper A : Proper (`=1` ==> `=1` ==> `=1`) (@predI A).
Proof.
  intros f g Hfg f' g' Hfg' i; rewrite /predI /=.
  now rewrite Hfg Hfg'.
Qed.

#[global] Instance implP_Proper {A} : Proper (`=1` ==> `=1` ==> `=1`) (@predA A).
Proof.
  intros f g Hfg f' g' Hfg' i; rewrite /predA /=.
  now rewrite Hfg Hfg'.
Qed.

Lemma orPL (p q : nat → bool) : predA p (predU p q) =1 xpredT.
Proof.
  intros i. rewrite /predA /predU /=.
  rewrite (ssrbool.implybE (p i)).
  destruct (p i) ⇒ //.
Qed.

Lemma orPR (p q : nat → bool) i : q i → (predU p q) i.
Proof.
  rewrite /predU /= ⇒ ->; rewrite orb_true_r //.
Qed.