phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/base.v *)
(* This notation is necessary to prevent [length] from being printed
as [strings.length] if strings.v is imported and later base.v. See
also strings.v and
https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/144 and
https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/129. *)
Notation length
:= Datatypes.length.
(* stdpp/base.v *)
(* * Sealing off definitions *)
Record seal {A} (f : A)
:= { unseal : A; seal_eq : unseal = f }.
(* stdpp/base.v *)
(* The tactic [tc_solve] is used to solve type class goals by invoking type
class search. It is similar to [apply _], but it is more robust since it does
not affect unrelated goals/evars due to https://github.com/coq/coq/issues/6583.

The tactic [tc_solve] is particularly useful when building custom tactics that
need tight control over when type class search is invoked. In Iris, many of the
proof mode tactics make use of [notypeclasses refine] and use [tc_solve] to
manually invoke type class search.

Note that [typeclasses eauto] is multi-success. That means, whenever subsequent
tactics fail, it will backtrack to [typeclasses eauto] to try the next type
class instance. This is almost always undesired and can lead to poor performance
and horrible error messages. Hence, we wrap it in a [once]. *)
Ltac tc_solve
:=
  solve [once (typeclasses eauto)].
(* stdpp/base.v *)
(* The type class [TCNoBackTrack P] can be used to establish [P] without ever
backtracking on the instance of [P] that has been found. Backtracking may
normally happen when [P] contains evars that could be instanciated in different
ways depending on which instance is picked, and type class search somewhere else
depends on this evar.

The proper way of handling this would be by setting Coq's option
`Typeclasses Unique Instances`. However, this option seems to be broken, see Coq
issue #6714.

See https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/112 for a rationale
of this type class. *)
Class TCNoBackTrack (P : Prop)
:= TCNoBackTrack_intro { tc_no_backtrack : P }.
(* stdpp/base.v *)
(* A conditional at the type class level. Note that [TCIf P Q R] is not the same
as [TCOr (TCAnd P Q) R]: the latter will backtrack to [R] if it fails to
establish [Q], i.e. does not have the behavior of a conditional. Furthermore,
note that [TCOr (TCAnd P Q) (TCAnd (TCNot P) R)] would not work; we generally
would not be able to prove the negation of [P]. *)
Inductive TCIf (P Q R : Prop) : Prop
:=
  | TCIf_true : P → Q → TCIf P Q R
  | TCIf_false : R → TCIf P Q R.
(* stdpp/base.v *)
(* The constant [tc_opaque] is used to make definitions opaque for just type
class search. Note that [simpl] is set up to always unfold [tc_opaque]. *)
Definition tc_opaque {A} (x : A) : A
:= x.
(* stdpp/base.v *)
(* Below we define type class versions of the common logical operators. It is
important to note that we duplicate the definitions, and do not declare the
existing logical operators as type classes. That is, we do not say:

  Existing Class or.
  Existing Class and.

If we could define the existing logical operators as classes, there is no way
of disambiguating whether a premise of a lemma should be solved by type class
resolution or not.

These classes are useful for two purposes: writing complicated type class
premises in a more concise way, and for efficiency. For example, using the [Or]
class, instead of defining two instances [P → Q1 → R] and [P → Q2 → R] we could
have one instance [P → Or Q1 Q2 → R]. When we declare the instance that way, we
avoid the need to derive [P] twice. *)
Inductive TCOr (P1 P2 : Prop) : Prop
:=
  | TCOr_l : P1 → TCOr P1 P2
  | TCOr_r : P2 → TCOr P1 P2.
(* stdpp/base.v *)
Inductive TCAnd (P1 P2 : Prop) : Prop
:= TCAnd_intro : P1 → P2 → TCAnd P1 P2.
(* stdpp/base.v *)
Inductive TCTrue : Prop
:= TCTrue_intro : TCTrue.
(* stdpp/base.v *)
(* The class [TCFalse] is not stricly necessary as one could also use
[False]. However, users might expect that TCFalse exists and if it
does not, it can cause hard to diagnose bugs due to automatic
generalization. *)
Inductive TCFalse : Prop
:=.
(* stdpp/base.v *)
(* The class [TCUnless] can be used to check that search for [P]
fails. This is useful as a guard for certain instances together with
classes like [TCFastDone] (see [tactics.v]) to prevent infinite loops
(e.g. when saturating the context). *)
Notation TCUnless P
:= (TCIf P TCFalse TCTrue).
(* stdpp/base.v *)
Inductive TCForall {A} (P : A → Prop) : list A → Prop
:=
  | TCForall_nil : TCForall P []
  | TCForall_cons x xs : P x → TCForall P xs → TCForall P (x :: xs).
(* stdpp/base.v *)
(* The class [TCForall2 P l k] is commonly used to transform an input list [l]
into an output list [k], or the converse. Therefore there are two modes, either
[l] input and [k] output, or [k] input and [l] input. *)
Inductive TCForall2 {A B} (P : A → B → Prop) : list A → list B → Prop
:=
  | TCForall2_nil : TCForall2 P [] []
  | TCForall2_cons x y xs ys :
     P x y → TCForall2 P xs ys → TCForall2 P (x :: xs) (y :: ys).
(* stdpp/base.v *)
Inductive TCExists {A} (P : A → Prop) : list A → Prop
:=
  | TCExists_cons_hd x l : P x → TCExists P (x :: l)
  | TCExists_cons_tl x l: TCExists P l → TCExists P (x :: l).
(* stdpp/base.v *)
Inductive TCElemOf {A} (x : A) : list A → Prop
:=
  | TCElemOf_here xs : TCElemOf x (x :: xs)
  | TCElemOf_further y xs : TCElemOf x xs → TCElemOf x (y :: xs).
(* stdpp/base.v *)
(* The intended use of [TCEq x y] is to use [x] as input and [y] as output, but
this is not enforced. We use output mode [-] (instead of [!]) for [x] to ensure
that type class search succeed on goals like [TCEq (if ? then e1 else e2) ?y],
see https://gitlab.mpi-sws.org/iris/iris/merge_requests/391 for a use case.
Mode [-] is harmless, the only instance of [TCEq] is [TCEq_refl] below, so we
cannot create loops. *)
Inductive TCEq {A} (x : A) : A → Prop
:= TCEq_refl : TCEq x x.
(* stdpp/base.v *)
Lemma TCEq_eq {A} (x1 x2 : A) : TCEq x1 x2 ↔ x1 = x2.
Proof. split; destruct 1; reflexivity. Qed.
(* stdpp/base.v *)
(* The [TCSimpl x y] type class is similar to [TCEq] but performs [simpl]
before proving the goal by reflexivity. Similar to [TCEq], the argument [x]
is the input and [y] the output. When solving [TCEq x y], the argument [x]
should be a concrete term and [y] an evar for the [simpl]ed result. *)
Class TCSimpl {A} (x x' : A)
:= TCSimpl_TCEq : TCEq x x'.
(* stdpp/base.v *)
Lemma TCSimpl_eq {A} (x1 x2 : A) : TCSimpl x1 x2 ↔ x1 = x2.
Proof. apply TCEq_eq. Qed.
(* stdpp/base.v *)
Inductive TCDiag {A} (C : A → Prop) : A → A → Prop
:=
  | TCDiag_diag x : C x → TCDiag C x x.
(* stdpp/base.v *)
(* Given a proposition [P] that is a type class, [tc_to_bool P] will return
[true] iff there is an instance of [P]. It is often useful in Ltac programming,
where one can do [lazymatch tc_to_bool P with true => .. | false => .. end]. *)
Definition tc_to_bool (P : Prop)
  {p : bool} `{TCIf P (TCEq p true) (TCEq p false)} : bool
:= p.
(* stdpp/base.v *)
(* Change [True] and [False] into notations in order to enable overloading.
We will use this to give [True] and [False] a different interpretation for
embedded logics. *)
Notation "'True'"
:= True (format "True") : type_scope.
(* stdpp/base.v *)
Notation "'False'"
:= False (format "False") : type_scope.
(* stdpp/base.v *)
(* Change [forall] into a notation in order to enable overloading. *)
Notation "'forall' x .. y , P"
:= (forall x, .. (forall y, P) ..)
  (at level 200, x binder, y binder, right associativity,
   only parsing) : type_scope.
(* stdpp/base.v *)
(* Introduce some Haskell style like notations. *)
Notation "(=)"
:= eq (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "( x =.)"
:= (eq x) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.= x )"
:= (λ y, eq y x) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(≠)"
:= (λ x y, x ≠ y) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "( x ≠.)"
:= (λ y, x ≠ y) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.≠ x )"
:= (λ y, y ≠ x) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(=@{ A } )"
:= (@eq A) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(≠@{ A } )"
:= (λ X Y, ¬X =@{A} Y) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "X ≠@{ A } Y"
:= (¬X =@{ A } Y)
  (at level 70, only parsing, no associativity) : stdpp_scope.
(* stdpp/base.v *)
Instance : ∀ A, PreOrder (=@{A}).
Proof. split; repeat intro; congruence. Qed.
(* stdpp/base.v *)
(* We define an operational type class for setoid equality, i.e., the
"canonical" equivalence for a type. The typeclass is tied to the \equiv
symbol. This is based on (Spitters/van der Weegen, 2011). *)
Class Equiv A
:= equiv: relation A.
(* stdpp/base.v *)
(* We instruct setoid rewriting to infer [equiv] as a relation on
type [A] when needed. This allows setoid_rewrite to solve constraints
of shape [Proper (eq ==> ?R) f] using [Proper (eq ==> (equiv (A:=A))) f]
when an equivalence relation is available on type [A]. We put this instance
at level 150 so it does not take precedence over Coq's stdlib instances,
favoring inference of [eq] (all Coq functions are automatically morphisms
for [eq]). We have [eq] (at 100) < [≡] (at 150) < [⊑] (at 200). *)
Instance equiv_rewrite_relation `{Equiv A} :
  RewriteRelation (@equiv A _) | 150
:= {}.
(* stdpp/base.v *)
Notation "(≡)"
:= equiv (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "( X ≡.)"
:= (equiv X) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.≡ X )"
:= (λ Y, Y ≡ X) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(≢)"
:= (λ X Y, ¬X ≡ Y) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "X ≢ Y"
:= (¬X ≡ Y) (at level 70, no associativity) : stdpp_scope.
(* stdpp/base.v *)
Notation "( X ≢.)"
:= (λ Y, X ≢ Y) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.≢ X )"
:= (λ Y, Y ≢ X) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(≡@{ A } )"
:= (@equiv A _) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(≢@{ A } )"
:= (λ X Y, ¬X ≡@{A} Y) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "X ≢@{ A } Y"
:= (¬X ≡@{ A } Y)
  (at level 70, only parsing, no associativity) : stdpp_scope.
(* stdpp/base.v *)
(* The type class [LeibnizEquiv] collects setoid equalities that coincide
with Leibniz equality. We provide the tactic [fold_leibniz] to transform such
setoid equalities into Leibniz equalities, and [unfold_leibniz] for the
reverse.

Various std++ tactics assume that this class is only instantiated if [≡]
is an equivalence relation. *)
Class LeibnizEquiv A `{Equiv A}
:=
  leibniz_equiv (x y : A) : x ≡ y → x = y.
(* stdpp/base.v *)
Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (≡@{A})} (x y : A) :
  x ≡ y ↔ x = y.
Proof. split; [apply leibniz_equiv|]. intros ->; reflexivity. Qed.
(* stdpp/base.v *)
Ltac fold_leibniz
:= repeat
  match goal with
  | H : context [ _ ≡@{?A} _ ] |- _ =>
    setoid_rewrite (leibniz_equiv_iff (A:=A)) in H
  | |- context [ _ ≡@{?A} _ ] =>
    setoid_rewrite (leibniz_equiv_iff (A:=A))
  end.
(* stdpp/base.v *)
Ltac unfold_leibniz
:= repeat
  match goal with
  | H : context [ _ =@{?A} _ ] |- _ =>
    setoid_rewrite <-(leibniz_equiv_iff (A:=A)) in H
  | |- context [ _ =@{?A} _ ] =>
    setoid_rewrite <-(leibniz_equiv_iff (A:=A))
  end.
(* stdpp/base.v *)
Definition equivL {A} : Equiv A
:= (=).
(* stdpp/base.v *)
(* A [Params f n] instance forces the setoid rewriting mechanism not to
rewrite in the first [n] arguments of the function [f]. We will declare such
instances for all operational type classes in this development. *)
Instance : Params (@equiv) 2
:= {}.
(* stdpp/base.v *)
(* The following instance forces [setoid_replace] to use setoid equality
(for types that have an [Equiv] instance) rather than the standard Leibniz
equality. *)
Instance equiv_default_relation `{Equiv A} :
  DefaultRelation (≡@{A}) | 3
:= {}.
(* stdpp/base.v *)
(* This type class by (Spitters/van der Weegen, 2011) collects decidable
propositions. *)
Class Decision (P : Prop)
:= decide : {P} + {¬P}.
(* stdpp/base.v *)
(* Although [RelDecision R] is just [∀ x y, Decision (R x y)], we make this
an explicit class instead of a notation for two reasons:

- It allows us to control [Hint Mode] more precisely. In particular, if it were
  defined as a notation, the above [Hint Mode] for [Decision] would not prevent
  diverging instance search when looking for [RelDecision (@eq ?A)], which would
  result in it looking for [Decision (@eq ?A x y)], i.e. an instance where the
  head position of [Decision] is not en evar.
- We use it to avoid inefficient computation due to eager evaluation of
  propositions by [vm_compute]. This inefficiency arises for example if
  [(x = y) := (f x = f y)]. Since [decide (x = y)] evaluates to
  [decide (f x = f y)], this would then lead to evaluation of [f x] and [f y].
  Using the [RelDecision], the [f] is hidden under a lambda, which prevents
  unnecessary evaluation. *)
Class RelDecision {A B} (R : A → B → Prop)
:=
  decide_rel x y :: Decision (R x y).
(* stdpp/base.v *)
Notation EqDecision A
:= (RelDecision (=@{A})).
(* stdpp/base.v *)
(* This type class collects types that are inhabited. *)
Class Inhabited (A : Type) : Type
:= populate { inhabitant : A }.
(* stdpp/base.v *)
(* This type class collects types that are proof irrelevant. That means, all
elements of the type are equal. We use this notion only used for propositions,
but by universe polymorphism we can generalize it. *)
Class ProofIrrel (A : Type) : Prop
:= proof_irrel (x y : A) : x = y.
(* stdpp/base.v *)
(* These operational type classes allow us to refer to common mathematical
properties in a generic way. For example, for injectivity of [(k ++.)] it
allows us to write [inj (k ++.)] instead of [app_inv_head k]. *)
Class Inj {A B} (R : relation A) (S : relation B) (f : A → B) : Prop
:=
  inj x y : S (f x) (f y) → R x y.
(* stdpp/base.v *)
Class Inj2 {A B C} (R1 : relation A) (R2 : relation B)
    (S : relation C) (f : A → B → C) : Prop
:=
  inj2 x1 x2 y1 y2 : S (f x1 x2) (f y1 y2) → R1 x1 y1 ∧ R2 x2 y2.
(* stdpp/base.v *)
Class Cancel {A B} (S : relation B) (f : A → B) (g : B → A) : Prop
:=
  cancel x : S (f (g x)) x.
(* stdpp/base.v *)
Class Surj {A B} (R : relation B) (f : A → B)
:=
  surj y : ∃ x, R (f x) y.
(* stdpp/base.v *)
Class IdemP {A} (R : relation A) (f : A → A → A) : Prop
:=
  idemp x : R (f x x) x.
(* stdpp/base.v *)
Class Comm {A B} (R : relation A) (f : B → B → A) : Prop
:=
  comm x y : R (f x y) (f y x).
(* stdpp/base.v *)
Class LeftId {A} (R : relation A) (i : A) (f : A → A → A) : Prop
:=
  left_id x : R (f i x) x.
(* stdpp/base.v *)
Class RightId {A} (R : relation A) (i : A) (f : A → A → A) : Prop
:=
  right_id x : R (f x i) x.
(* stdpp/base.v *)
Class Assoc {A} (R : relation A) (f : A → A → A) : Prop
:=
  assoc x y z : R (f x (f y z)) (f (f x y) z).
(* stdpp/base.v *)
Class LeftAbsorb {A} (R : relation A) (i : A) (f : A → A → A) : Prop
:=
  left_absorb x : R (f i x) i.
(* stdpp/base.v *)
Class RightAbsorb {A} (R : relation A) (i : A) (f : A → A → A) : Prop
:=
  right_absorb x : R (f x i) i.
(* stdpp/base.v *)
Class AntiSymm {A} (R S : relation A) : Prop
:=
  anti_symm x y : S x y → S y x → R x y.
(* stdpp/base.v *)
Class Total {A} (R : relation A)
:= total x y : R x y ∨ R y x.
(* stdpp/base.v *)
Class Trichotomy {A} (R : relation A)
:=
  trichotomy x y : R x y ∨ x = y ∨ R y x.
(* stdpp/base.v *)
Class TrichotomyT {A} (R : relation A)
:=
  trichotomyT x y : {R x y} + {x = y} + {R y x}.
(* stdpp/base.v *)
Notation Involutive R f
:= (Cancel R f f).
(* stdpp/base.v *)
Lemma involutive {A} {R : relation A} (f : A → A) `{Involutive R f} x :
  R (f (f x)) x.
Proof. auto. Qed.
(* stdpp/base.v *)
Lemma not_symmetry `{R : relation A, !Symmetric R} x y : ¬R x y → ¬R y x.
Proof. intuition. Qed.
(* stdpp/base.v *)
Lemma symmetry_iff `(R : relation A) `{!Symmetric R} x y : R x y ↔ R y x.
Proof. intuition. Qed.
(* stdpp/base.v *)
Lemma not_inj `{Inj A B R R' f} x y : ¬R x y → ¬R' (f x) (f y).
Proof. intuition. Qed.
(* stdpp/base.v *)
Lemma not_inj2_1 `{Inj2 A B C R R' R'' f} x1 x2 y1 y2 :
  ¬R x1 x2 → ¬R'' (f x1 y1) (f x2 y2).
Proof. intros HR HR''. destruct (inj2 f x1 y1 x2 y2); auto. Qed.
(* stdpp/base.v *)
Lemma not_inj2_2 `{Inj2 A B C R R' R'' f} x1 x2 y1 y2 :
  ¬R' y1 y2 → ¬R'' (f x1 y1) (f x2 y2).
Proof. intros HR' HR''. destruct (inj2 f x1 y1 x2 y2); auto. Qed.
(* stdpp/base.v *)
Lemma inj_iff {A B} {R : relation A} {S : relation B} (f : A → B)
  `{!Inj R S f} `{!Proper (R ==> S) f} x y : S (f x) (f y) ↔ R x y.
Proof. firstorder. Qed.
(* stdpp/base.v *)
Instance inj2_inj_1 `{Inj2 A B C R1 R2 R3 f} y : Inj R1 R3 (λ x, f x y).
Proof. repeat intro; edestruct (inj2 f); eauto. Qed.
(* stdpp/base.v *)
Instance inj2_inj_2 `{Inj2 A B C R1 R2 R3 f} x : Inj R2 R3 (f x).
Proof. repeat intro; edestruct (inj2 f); eauto. Qed.
(* stdpp/base.v *)
(* Smart constructors for [Inj] and [Surj] based on [Cancel]. These are not
instances because they will blow-up the search space due to diamonds: in every
node of the search tree for [Inj] or [Surj] of composed functions these
instances could be applied. Note that [f] and [g] do not need to be given,
these are infered using [Cancel]. *)
Lemma cancel_inj `{Cancel A B R1 f g, !Equivalence R1, !Proper (R2 ==> R1) f} :
  Inj R1 R2 g.
Proof.
  intros x y E. rewrite <-(cancel f g x), <-(cancel f g y), E. reflexivity.
Qed.
(* stdpp/base.v *)
Lemma cancel_surj `{Cancel A B R1 f g} : Surj R1 f.
Proof. intros y. exists (g y). auto. Qed.
(* stdpp/base.v *)
(* The following lemmas are specific versions of the projections of the above
type classes for Leibniz equality. These lemmas allow us to enforce Coq not to
use the setoid rewriting mechanism. *)
Lemma idemp_L {A} f `{!@IdemP A (=) f} x : f x x = x.
Proof. auto. Qed.
(* stdpp/base.v *)
Lemma comm_L {A B} f `{!@Comm A B (=) f} x y : f x y = f y x.
Proof. auto. Qed.
(* stdpp/base.v *)
Lemma left_id_L {A} i f `{!@LeftId A (=) i f} x : f i x = x.
Proof. auto. Qed.
(* stdpp/base.v *)
Lemma right_id_L {A} i f `{!@RightId A (=) i f} x : f x i = x.
Proof. auto. Qed.
(* stdpp/base.v *)
Lemma assoc_L {A} f `{!@Assoc A (=) f} x y z : f x (f y z) = f (f x y) z.
Proof. auto. Qed.
(* stdpp/base.v *)
Lemma left_absorb_L {A} i f `{!@LeftAbsorb A (=) i f} x : f i x = i.
Proof. auto. Qed.
(* stdpp/base.v *)
Lemma right_absorb_L {A} i f `{!@RightAbsorb A (=) i f} x : f x i = i.
Proof. auto. Qed.
(* stdpp/base.v *)
(* The classes [PreOrder], [PartialOrder], and [TotalOrder] use an arbitrary
relation [R] instead of [⊆] to support multiple orders on the same type. *)
Definition strict {A} (R : relation A) : relation A
:= λ X Y, R X Y ∧ ¬R Y X.
(* stdpp/base.v *)
Instance : Params (@strict) 2
:= {}.
(* stdpp/base.v *)
Class PartialOrder {A} (R : relation A) : Prop
:= {
  partial_order_pre :: PreOrder R;
  partial_order_anti_symm :: AntiSymm (=) R
}.
(* stdpp/base.v *)
Class TotalOrder {A} (R : relation A) : Prop
:= {
  total_order_partial :: PartialOrder R;
  total_order_trichotomy :: Trichotomy (strict R)
}.
(* stdpp/base.v *)
(* * Logic *)
Instance prop_inhabited : Inhabited Prop
:= populate True.
(* stdpp/base.v *)
Notation "(∧)"
:= and (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "( A ∧.)"
:= (and A) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.∧ B )"
:= (λ A, A ∧ B) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(∨)"
:= or (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "( A ∨.)"
:= (or A) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.∨ B )"
:= (λ A, A ∨ B) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(↔)"
:= iff (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "( A ↔.)"
:= (iff A) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.↔ B )"
:= (λ A, A ↔ B) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Lemma or_l P Q : ¬Q → P ∨ Q ↔ P.
Proof. tauto. Qed.
(* stdpp/base.v *)
Lemma or_r P Q : ¬P → P ∨ Q ↔ Q.
Proof. tauto. Qed.
(* stdpp/base.v *)
Lemma and_wlog_l (P Q : Prop) : (Q → P) → Q → (P ∧ Q).
Proof. tauto. Qed.
(* stdpp/base.v *)
Lemma and_wlog_r (P Q : Prop) : P → (P → Q) → (P ∧ Q).
Proof. tauto. Qed.
(* stdpp/base.v *)
Lemma impl_trans (P Q R : Prop) : (P → Q) → (Q → R) → (P → R).
Proof. tauto. Qed.
(* stdpp/base.v *)
Lemma forall_proper {A} (P Q : A → Prop) :
  (∀ x, P x ↔ Q x) → (∀ x, P x) ↔ (∀ x, Q x).
Proof. firstorder. Qed.
(* stdpp/base.v *)
Lemma exist_proper {A} (P Q : A → Prop) :
  (∀ x, P x ↔ Q x) → (∃ x, P x) ↔ (∃ x, Q x).
Proof. firstorder. Qed.
(* stdpp/base.v *)
Instance eq_comm {A} : Comm (↔) (=@{A}).
Proof. red; intuition. Qed.
(* stdpp/base.v *)
Instance flip_eq_comm {A} : Comm (↔) (λ x y, y =@{A} x).
Proof. red; intuition. Qed.
(* stdpp/base.v *)
Instance iff_comm : Comm (↔) (↔).
Proof. red; intuition. Qed.
(* stdpp/base.v *)
Instance and_comm : Comm (↔) (∧).
Proof. red; intuition. Qed.
(* stdpp/base.v *)
Instance and_assoc : Assoc (↔) (∧).
Proof. red; intuition. Qed.
(* stdpp/base.v *)
Instance and_idemp : IdemP (↔) (∧).
Proof. red; intuition. Qed.
(* stdpp/base.v *)
Instance or_comm : Comm (↔) (∨).
Proof. red; intuition. Qed.
(* stdpp/base.v *)
Instance or_assoc : Assoc (↔) (∨).
Proof. red; intuition. Qed.
(* stdpp/base.v *)
Instance or_idemp : IdemP (↔) (∨).
Proof. red; intuition. Qed.
(* stdpp/base.v *)
Instance True_and : LeftId (↔) True (∧).
Proof. red; intuition. Qed.
(* stdpp/base.v *)
Instance and_True : RightId (↔) True (∧).
Proof. red; intuition. Qed.
(* stdpp/base.v *)
Instance False_and : LeftAbsorb (↔) False (∧).
Proof. red; intuition. Qed.
(* stdpp/base.v *)
Instance and_False : RightAbsorb (↔) False (∧).
Proof. red; intuition. Qed.
(* stdpp/base.v *)
Instance False_or : LeftId (↔) False (∨).
Proof. red; intuition. Qed.
(* stdpp/base.v *)
Instance or_False : RightId (↔) False (∨).
Proof. red; intuition. Qed.
(* stdpp/base.v *)
Instance True_or : LeftAbsorb (↔) True (∨).
Proof. red; intuition. Qed.
(* stdpp/base.v *)
Instance or_True : RightAbsorb (↔) True (∨).
Proof. red; intuition. Qed.
(* stdpp/base.v *)
Instance True_impl : LeftId (↔) True impl.
Proof. unfold impl. red; intuition. Qed.
(* stdpp/base.v *)
Instance impl_True : RightAbsorb (↔) True impl.
Proof. unfold impl. red; intuition. Qed.
(* stdpp/base.v *)
(* ** Functions *)
Notation "(→)"
:= (λ A B, A → B) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "( A →.)"
:= (λ B, A → B) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.→ B )"
:= (λ A, A → B) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "t $ r"
:= (t r)
  (at level 65, right associativity, only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "($)"
:= (λ f x, f x) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.$ x )"
:= (λ f, f x) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(∘)"
:= compose (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "( f ∘.)"
:= (compose f) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Notation "(.∘ f )"
:= (λ g, compose g f) (only parsing) : stdpp_scope.
(* stdpp/base.v *)
Instance forall_inhabited {A} {B : A → Type} `{!∀ x, Inhabited (B x)} :
    Inhabited (∀ x, B x)
:=
  populate (λ _, inhabitant).
(* stdpp/base.v *)
Definition fun_map {A A' B B'} (f: A' → A) (g: B → B') (h : A → B) : A' → B'
:=
  g ∘ h ∘ f.
(* stdpp/base.v *)
Instance const_proper `{R1 : relation A, R2 : relation B} (x : B) :
  Reflexive R2 → Proper (R1 ==> R2) (λ _, x).
Proof. intros ? y1 y2; reflexivity. Qed.
(* stdpp/base.v *)
Instance id_inj {A} : Inj (=) (=) (@id A).
Proof. intros ??; auto. Qed.
(* stdpp/base.v *)
Instance compose_inj {A B C} R1 R2 R3 (f : A → B) (g : B → C) :
  Inj R1 R2 f → Inj R2 R3 g → Inj R1 R3 (g ∘ f).
Proof. red; intuition. Qed.
(* stdpp/base.v *)
Instance id_surj {A} : Surj (=) (@id A).
Proof. intros y; exists y; reflexivity. Qed.
(* stdpp/base.v *)
Instance compose_surj {A B C} R (f : A → B) (g : B → C) :
  Surj (=) f → Surj R g → Surj R (g ∘ f).
Proof.
  intros ?? x. unfold compose. destruct (surj g x) as [y ?].
  destruct (surj f y) as [z ?]. exists z. congruence.
Qed.
(* stdpp/base.v *)
Instance const2_comm {A B} (x : B) : Comm (=) (λ _ _ : A, x).
Proof. intros ?; reflexivity. Qed.
(* stdpp/base.v *)
Instance const2_assoc {A} (x : A) : Assoc (=) (λ _ _ : A, x).
Proof. intros ???; reflexivity. Qed.
(* stdpp/base.v *)
Instance id1_assoc {A} : Assoc (=) (λ x _ : A, x).
Proof. intros ???; reflexivity. Qed.