Module mathcomp.classical.boolp

From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import mathcomp_extra.

# Classical Logic This file provides the axioms of classical logic and tools to perform classical reasoning in the Mathematical Compnent framework. The three axioms are taken from the standard library of Coq, more details can be found in Section 5 of - R. Affeldt, C. Cohen, D. Rouhling. Formalization Techniques for Asymptotic Reasoning in Classical Analysis. JFR 2018 ## Axioms ``` functional_extensionality_dep == functional extensionality (on dependently typed functions), i.e., functions that are pointwise equal are equal propositional_extensionality == propositional extensionality, i.e., iff and equality are the same on Prop constructive_indefinite_description == existential in Prop (ex) implies existential in Type (sig) cid := constructive_indefinite_description (shortcut) ``` A number of properties are derived below from these axioms and are often more pratical to use than directly using the axioms. For instance propext, funext, the excluded middle (EM),... ## Boolean View of Prop ``` `[] == boolean view of P : Prop, see all lemmas about asbool ``` ## Mathematical Components Structures ``` {classic T} == Endow T : Type with a canonical eqType/choiceType. This is intended for local use. E.g., T : Type |- A : {fset {classic T}} Alternatively one may use elim/Pchoice: T => T in H *. to substitute T with T : choiceType once and for all. {eclassic T} == Endow T : eqType with a canonical choiceType. On the model of {classic _}. See also the lemmas Peq and eqPchoice. ``` Functions onto a porderType (resp. latticeType) are equipped with a porderType (resp. latticeType), so that the generic notation (_ <= _)%O (resp. `&`, `|`) from `order.v` can be used. ``` FunOrder.lef f g == pointwise large inequality between two functions FunOrder.ltf f g == pointwise strict inequality between two functions FunLattice.meetf f g == pointwise meet between two functions FunLattice.joinf f g == pointwise join between two functions ```

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

Declare Scope box_scope.
Declare Scope quant_scope.

Axiom functional_extensionality_dep :
 forall (A : Type) (B : A -> Type) (f g : forall x : A, B x),
 (forall x : A, f x = g x) -> f = g.
Axiom propositional_extensionality :
 forall P Q : Prop, P <-> Q -> P = Q.

Axiom constructive_indefinite_description :
 forall (A : Type) (P : A -> Prop),
 (exists x : A, P x) -> {x : A | P x}.
Notation cid := constructive_indefinite_description.

Lemma cid2 (A : Type) (P Q : A -> Prop) :
 (exists2 x : A, P x & Q x) -> {x : A | P x & Q x}.

Proof.

move=> PQA; suff: {x | P x /\ Q x} by move=> [a [*]]; exists a.
by apply: cid; case: PQA => x; exists x.
Qed.

Lemma existT_inj1 (T : Type) (P : T -> Type) (x y : T) (Px : P x) (Py : P y) :
existT P x Px = existT P y Py -> x = y.

Proof.

by case. Qed.

Lemma existT_inj2 (T : eqType) (P : T -> Type) (x : T) (Px1 Px2 : P x) :
existT P x Px1 = existT P x Px2 -> Px1 = Px2.

Proof.

apply: Eqdep_dec.inj_pair2_eq_dec => y z.
by have [|/eqP] := eqVneq y z; [left|right].
Qed.

Lemma surjective_existT (T : Type) (P : T -> Type) (p : {x : T & P x}):
existT [eta P] (projT1 p) (projT2 p) = p.

Proof.

by case: p. Qed.

Record mextensionality := {
 _ : forall (P Q : Prop), (P <-> Q) -> (P = Q);
 _ : forall {T U : Type} (f g : T -> U),
 (forall x, f x = g x) -> f = g;
}.

Fact extensionality : mextensionality.

Proof.

split.
- exact: propositional_extensionality.
- by move=> T U f g; apply: functional_extensionality_dep.
Qed.

Lemma propext (P Q : Prop) : (P <-> Q) -> (P = Q).

Proof.

by have [propext _] := extensionality; apply: propext. Qed.

Ltac eqProp := apply: propext; split.

Lemma funext {T U : Type} (f g : T -> U) : (f =1 g) -> f = g.

Proof.

by case: extensionality=> _; apply. Qed.

Lemma propeqE (P Q : Prop) : (P = Q) = (P <-> Q).

Proof.

by apply: propext; split=> [->|/propext]. Qed.

Lemma propeqP (P Q : Prop) : (P = Q) <-> (P <-> Q).

Proof.

by rewrite propeqE. Qed.

Lemma funeqE {T U : Type} (f g : T -> U) : (f = g) = (f =1 g).

Proof.

by rewrite propeqE; split=> [->//|/funext]. Qed.

Lemma funeq2E {T U V : Type} (f g : T -> U -> V) : (f = g) = (f =2 g).

Proof.

by rewrite propeqE; split=> [->//|?]; rewrite funeqE=> x; rewrite funeqE.
Qed.

Lemma funeq3E {T U V W : Type} (f g : T -> U -> V -> W) :
(f = g) = (forall x y z, f x y z = g x y z).

Proof.

by rewrite propeqE; split=> [->//|?]; rewrite funeq2E=> x y; rewrite funeqE.
Qed.

Lemma funeqP {T U : Type} (f g : T -> U) : (f = g) <-> (f =1 g).

Proof.

by rewrite funeqE. Qed.

Lemma funeq2P {T U V : Type} (f g : T -> U -> V) : (f = g) <-> (f =2 g).

Proof.

by rewrite funeq2E. Qed.

Lemma funeq3P {T U V W : Type} (f g : T -> U -> V -> W) :
(f = g) <-> (forall x y z, f x y z = g x y z).

Proof.

by rewrite funeq3E. Qed.

Lemma predeqE {T} (P Q : T -> Prop) : (P = Q) = (forall x, P x <-> Q x).

Proof.

by rewrite propeqE; split=> [->//|?]; rewrite funeqE=> x; rewrite propeqE.
Qed.

Lemma predeq2E {T U} (P Q : T -> U -> Prop) :
(P = Q) = (forall x y, P x y <-> Q x y).

Proof.

by rewrite propeqE; split=> [->//|?]; rewrite funeq2E=> ??; rewrite propeqE.
Qed.

Lemma predeq3E {T U V} (P Q : T -> U -> V -> Prop) :
(P = Q) = (forall x y z, P x y z <-> Q x y z).

Proof.

by rewrite propeqE; split=> [->//|?]; rewrite funeq3E=> ???; rewrite propeqE.
Qed.

Lemma predeqP {T} (A B : T -> Prop) : (A = B) <-> (forall x, A x <-> B x).

Proof.

by rewrite predeqE. Qed.

Lemma predeq2P {T U} (P Q : T -> U -> Prop) :
(P = Q) <-> (forall x y, P x y <-> Q x y).

Proof.

by rewrite predeq2E. Qed.

Lemma predeq3P {T U V} (P Q : T -> U -> V -> Prop) :
(P = Q) <-> (forall x y z, P x y z <-> Q x y z).

Proof.

by rewrite predeq3E. Qed.

Lemma propT {P : Prop} : P -> P = True.

Proof.

by move=> p; rewrite propeqE. Qed.

Lemma Prop_irrelevance (P : Prop) (x y : P) : x = y.

Proof.

by move: x (x) y => /propT-> [] []. Qed.

#[global] Hint Resolve Prop_irrelevance : core.

Record mclassic := {
  _ : forall (P : Prop), {P} + {~P};
  _ : forall T, hasChoice T
}.

Lemma choice X Y (P : X -> Y -> Prop) :
  (forall x, exists y, P x y) -> {f & forall x, P x (f x)}.

Proof.

by move=> /(_ _)/constructive_indefinite_description -/all_tag. Qed.

Theorem EM P : P \/ ~ P.

Proof.

pose U val := fun Q : bool => Q = val \/ P.
have Uex val : exists b, U val b by exists val; left.
pose f val := projT1 (cid (Uex val)).
pose Uf val : U val (f val) := projT2 (cid (Uex val)).
have : f true != f false \/ P.
have [] := (Uf true, Uf false); rewrite /U.
by move=> [->|?] [->|?] ; do ?[by right]; left.
move=> [/eqP fTFN|]; [right=> p|by left]; apply: fTFN.
have UTF : U true = U false by rewrite predeqE /U => b; split=> _; right.
rewrite /f; move: (Uex true) (Uex false); rewrite UTF => p1 p2.
by congr (projT1 (cid _)).
Qed.

Lemma pselect (P : Prop): {P} + {~P}.

Proof.

have : exists b, if b then P else ~ P.
by case: (EM P); [exists true|exists false].
by move=> /cid [[]]; [left|right].
Qed.

Lemma pselectT T : (T -> False) + T.

Proof.

have [/cid[]//|NT] := pselect (exists t : T, True); first by right.
by left=> t; case: NT; exists t.
Qed.

Lemma classic : mclassic.

Proof.

split=> [|T]; first exact: pselect.
exists (fun (P : pred T) (n : nat) =>
 if pselect (exists x, P x) isn't left ex then None
 else Some (projT1 (cid ex)))
 => [P n x|P [x Px]|P Q /funext -> //].
 by case: pselect => // ex [<- ]; case: cid.
by exists 0; case: pselect => // -[]; exists x.
Qed.

Lemma gen_choiceMixin (T : Type) : hasChoice T.

Proof.

by case: classic. Qed.

Lemma lem (P : Prop): P \/ ~P.

Proof.

by case: (pselect P); tauto. Qed.

Lemma trueE : true = True :> Prop.

Proof.

by rewrite propeqE; split. Qed.

Lemma falseE : false = False :> Prop.

Proof.

by rewrite propeqE; split. Qed.

Lemma propF (P : Prop) : ~ P -> P = False.

Proof.

by move=> p; rewrite propeqE; tauto. Qed.

Lemma eq_fun T rT (U V : T -> rT) :
(forall x : T, U x = V x) -> (fun x => U x) = (fun x => V x).

Proof.

by move=> /funext->. Qed.

Lemma eq_fun2 T1 T2 rT (U V : T1 -> T2 -> rT) :
(forall x y, U x y = V x y) -> (fun x y => U x y) = (fun x y => V x y).

Proof.

by move=> UV; rewrite funeq2E => x y; rewrite UV. Qed.

Lemma eq_fun3 T1 T2 T3 rT (U V : T1 -> T2 -> T3 -> rT) :
(forall x y z, U x y z = V x y z) ->
(fun x y z => U x y z) = (fun x y z => V x y z).

Proof.

by move=> UV; rewrite funeq3E => x y z; rewrite UV. Qed.

Lemma eq_forall T (U V : T -> Prop) :
(forall x : T, U x = V x) -> (forall x, U x) = (forall x, V x).

Proof.

by move=> e; rewrite propeqE; split=> ??; rewrite (e,=^~e). Qed.

Lemma eq_forall2 T S (U V : forall x : T, S x -> Prop) :
(forall x y, U x y = V x y) -> (forall x y, U x y) = (forall x y, V x y).

Proof.

by move=> UV; apply/eq_forall => x; apply/eq_forall. Qed.

Lemma eq_forall3 T S R (U V : forall (x : T) (y : S x), R x y -> Prop) :
(forall x y z, U x y z = V x y z) ->
(forall x y z, U x y z) = (forall x y z, V x y z).

Proof.

by move=> UV; apply/eq_forall2 => x y; apply/eq_forall. Qed.

Lemma eq_exists T (U V : T -> Prop) :
(forall x : T, U x = V x) -> (exists x, U x) = (exists x, V x).

Proof.

by move=> e; rewrite propeqE; split=> - [] x ?; exists x; rewrite (e,=^~e).
Qed.

Lemma eq_exists2 T S (U V : forall x : T, S x -> Prop) :
(forall x y, U x y = V x y) -> (exists x y, U x y) = (exists x y, V x y).

Proof.

by move=> UV; apply/eq_exists => x; apply/eq_exists. Qed.

Lemma eq_exists3 T S R (U V : forall (x : T) (y : S x), R x y -> Prop) :
(forall x y z, U x y z = V x y z) ->
(exists x y z, U x y z) = (exists x y z, V x y z).

Proof.

by move=> UV; apply/eq_exists2 => x y; apply/eq_exists. Qed.

Lemma eq_exist T (P : T -> Prop) (s t : T) (p : P s) (q : P t) :
s = t -> exist P s p = exist P t q.

Proof.

by move=> st; case: _ / st in q *; apply/congr1. Qed.

Lemma forall_swap T S (U : forall (x : T) (y : S), Prop) :
(forall x y, U x y) = (forall y x, U x y).

Proof.

by rewrite propeqE; split. Qed.

Lemma exists_swap T S (U : forall (x : T) (y : S), Prop) :
(exists x y, U x y) = (exists y x, U x y).

Proof.

by rewrite propeqE; split => -[x [y]]; exists y, x. Qed.

Lemma reflect_eq (P : Prop) (b : bool) : reflect P b -> P = b.

Proof.

by rewrite propeqE; exact: rwP. Qed.

Definition asbool (P : Prop) := if pselect P then true else false.

Notation "`[]" := (asbool P) : bool_scope.

Lemma asboolE (P : Prop) : `[] = P :> Prop.

Proof.

by rewrite propeqE /asbool; case: pselect; split. Qed.

Lemma asboolP (P : Prop) : reflect P `[].

Proof.

by apply: (equivP idP); rewrite asboolE. Qed.

Lemma asboolb (b : bool) : `[] = b.

Proof.

by apply/asboolP/idP. Qed.

Lemma asboolPn (P : Prop) : reflect (~ P) (~~ `[]).

Proof.

by rewrite /asbool; case: pselect=> h; constructor. Qed.

Lemma asboolW (P : Prop) : `[] -> P.

Proof.

by case: asboolP. Qed.

Lemma asboolT (P : Prop) : P -> `[].

Proof.

by case: asboolP. Qed.

Lemma asboolF (P : Prop) : ~ P -> `[] = false.

Proof.

by apply/introF/asboolP. Qed.

Lemma eq_opE (T : eqType) (x y : T) : (x == y : Prop) = (x = y).

Proof.

by apply/propext; split=> /eqP. Qed.

Lemma is_true_inj : injective is_true.

Proof.

by move=> [] []; rewrite ?(trueE, falseE) ?propeqE; tauto. Qed.

Definition gen_eq (T : Type) (u v : T) := `[].
Lemma gen_eqP (T : Type) : Equality.axiom (@gen_eq T).

Proof.

by move=> x y; apply: (iffP (asboolP _)). Qed.

Definition gen_eqMixin (T : Type) : hasDecEq T :=
  hasDecEq.Build T (@gen_eqP T).

HB.instance Definition _ (T : Type) (T' : T -> eqType) :=
  gen_eqMixin (forall t : T, T' t).

HB.instance Definition _ (T : Type) (T' : T -> choiceType) :=
  gen_choiceMixin (forall t : T, T' t).

HB.instance Definition _ := gen_eqMixin Prop.
HB.instance Definition _ := gen_choiceMixin Prop.

Section classicType.
Variable T : Type.
Definition classicType := T.
HB.instance Definition _ := gen_eqMixin classicType.
HB.instance Definition _ := gen_choiceMixin classicType.
End classicType.
Notation "'{classic' T }" := (classicType T)
(format "'{classic' T }") : type_scope.

Section eclassicType.
Variable T : eqType.
Definition eclassicType : Type := T.
HB.instance Definition _ := Equality.copy eclassicType T.
HB.instance Definition _ := gen_choiceMixin eclassicType.
End eclassicType.
Notation "'{eclassic' T }" := (eclassicType T)
(format "'{eclassic' T }") : type_scope.

Definition canonical_of T U (sort : U -> T) := forall (G : T -> Type),
  (forall x', G (sort x')) -> forall x, G x.
Notation canonical_ sort := (@canonical_of _ _ sort).
Notation canonical T E := (@canonical_of T E id).

Lemma canon T U (sort : U -> T) :
  (forall x, exists y, sort y = x) -> canonical_ sort.

Proof.

by move=> + G Gs x => /(_ x)/cid[x' <-]. Qed.

Arguments canon {T U sort} x.

Lemma Peq : canonical Type eqType.

Proof.

by apply: canon => T; exists {classic T}. Qed.

Lemma Pchoice : canonical Type choiceType.

Proof.

by apply: canon => T; exists {classic T}. Qed.

Lemma eqPchoice : canonical eqType choiceType.

Proof.

by apply: canon => T; exists {eclassic T}; case: T => //= T [?]//. Qed.

Lemma not_True : (~ True) = False

Proof.

exact/propext. Qed.

Lemma not_False : (~ False) = True

Proof.

by apply/propext; split=> _. Qed.

Lemma asbool_equiv_eq {P Q : Prop} : (P <-> Q) -> `[] = `[<Q>].

Proof.

by rewrite -propeqE => ->. Qed.

Lemma asbool_equiv_eqP {P Q : Prop} b : reflect Q b -> (P <-> Q) -> `[] = b.

Proof.

by move=> Q_b [PQ QP]; apply/asboolP/Q_b. Qed.

Lemma asbool_equiv {P Q : Prop} : (P <-> Q) -> (`[] <-> `[<Q>]).

Proof.

by move/asbool_equiv_eq->. Qed.

Lemma asbool_eq_equiv {P Q : Prop} : `[] = `[<Q>] -> (P <-> Q).

Proof.

by move=> eq; split=> /asboolP; rewrite (eq, =^~ eq) => /asboolP. Qed.

Lemma and_asboolP (P Q : Prop) : reflect (P /\ Q) (`[] && `[< Q >]).

Proof.

apply: (iffP idP); first by case/andP => /asboolP p /asboolP q.
by case=> /asboolP-> /asboolP->.
Qed.

Lemma and3_asboolP (P Q R : Prop) :
reflect [/\ P, Q & R] [&& `[], `[< Q >] & `[< R >]].

Proof.

apply: (iffP idP); first by case/and3P => /asboolP p /asboolP q /asboolP r.
by case => /asboolP -> /asboolP -> /asboolP ->.
Qed.

Lemma or_asboolP (P Q : Prop) : reflect (P \/ Q) (`[] || `[< Q >]).

Proof.

apply: (iffP idP); first by case/orP=> /asboolP; [left | right].
by case=> /asboolP-> //=; rewrite orbT.
Qed.

Lemma or3_asboolP (P Q R : Prop) :
reflect [\/ P, Q | R] [|| `[], `[< Q >] | `[< R >]].

Proof.

Lemma asbool_neg {P : Prop} : `[<~ P>] = ~~ `[].

Proof.

by apply/idP/asboolPn=> [/asboolP|/asboolT]. Qed.

Lemma asbool_or {P Q : Prop} : `[] = `[] || `[<Q>].

Proof.

exact: (asbool_equiv_eqP (or_asboolP _ _)). Qed.

Lemma asbool_and {P Q : Prop} : `[] = `[] && `[<Q>].

Proof.

exact: (asbool_equiv_eqP (and_asboolP _ _)). Qed.

Lemma imply_asboolP {P Q : Prop} : reflect (P -> Q) (`[] ==> `[<Q>]).

Proof.

apply: (iffP implyP)=> [PQb /asboolP/PQb/asboolW //|].
by move=> PQ /asboolP/PQ/asboolT.
Qed.

Lemma asbool_imply {P Q : Prop} : `[ Q>] = `[] ==> `[<Q>].

Proof.

exact: (asbool_equiv_eqP imply_asboolP). Qed.

Lemma imply_asboolPn (P Q : Prop) : reflect (P /\ ~ Q) (~~ `[ Q>]).

Proof.

apply: (iffP idP).
by rewrite asbool_imply negb_imply -asbool_neg => /and_asboolP.
by move/and_asboolP; rewrite asbool_neg -negb_imply asbool_imply.
Qed.

Lemma forall_asboolP {T : Type} (P : T -> Prop) :
reflect (forall x, `[]) (`[<forall x, P x>]).

Proof.

apply: (iffP idP); first by move/asboolP=> Px x; apply/asboolP.
by move=> Px; apply/asboolP=> x; apply/asboolP.
Qed.

Lemma exists_asboolP {T : Type} (P : T -> Prop) :
reflect (exists x, `[]) (`[<exists x, P x>]).

Proof.

apply: (iffP idP); first by case/asboolP=> x Px; exists x; apply/asboolP.
by case=> x bPx; apply/asboolP; exists x; apply/asboolP.
Qed.

Variant BoolProp : Prop -> Type :=
| TrueProp : BoolProp True
| FalseProp : BoolProp False.

Lemma PropB P : BoolProp P.

Proof.

by case: (asboolP P) => [/propT-> | /propF->]; [left | right]. Qed.

Lemma notB : ((~ True) = False) * ((~ False) = True).

Proof.

by rewrite /not; split; eqProp. Qed.

Lemma andB : left_id True and * right_id True and
* (left_zero False and * right_zero False and * idempotent and).

Proof.

by do ![split] => /PropB[]; eqProp=> // -[]. Qed.

Lemma orB : left_id False or * right_id False or
* (left_zero True or * right_zero True or * idempotent or).

Proof.

do ![split] => /PropB[]; eqProp=> -[] //; by [left | right]. Qed.

Lemma implyB : let imply (P Q : Prop) := P -> Q in
(imply False =1 fun=> True) * (imply^~ False =1 not)
* (left_id True imply * right_zero True imply * self_inverse True imply).

Proof.

by do ![split] => /PropB[]; eqProp=> //; apply. Qed.

Lemma decide_or P Q : P \/ Q -> {P} + {Q}.

Proof.

by case/PropB: P; [left | rewrite orB; right]. Qed.

Lemma notT (P : Prop) : P = False -> ~ P.

Proof.

by move->. Qed.

Lemma contrapT P : ~ ~ P -> P.

Proof.

by case: (PropB P) => //; rewrite not_False. Qed.

Lemma notTE (P : Prop) : (~ P) -> P = False

Proof.

by case: (PropB P). Qed.

Lemma notFE (P : Prop) : (~ P) = False -> P.

Proof.

by move/notT; exact: contrapT. Qed.

Lemma notK : involutive not.

Proof.

by case/PropB; rewrite !(not_False,not_True). Qed.

Lemma contra_notP (Q P : Prop) : (~ Q -> P) -> ~ P -> Q.

Proof.

by move: Q P => /PropB[] /PropB[]. Qed.

Lemma contraPP (Q P : Prop) : (~ Q -> ~ P) -> P -> Q.

Proof.

by move: Q P => /PropB[] /PropB[]//; rewrite not_False not_True. Qed.

Lemma contra_notT b (P : Prop) : (~~ b -> P) -> ~ P -> b.

Proof.

by move=> bP; apply: contra_notP => /negP. Qed.

Lemma contraPT (P : Prop) b : (~~ b -> ~ P) -> P -> b.

Proof.

by move=> /contra_notT; rewrite notK. Qed.

Lemma contraTP b (Q : Prop) : (~ Q -> ~~ b) -> b -> Q.

Proof.

by move=> QB; apply: contraPP => /QB/negP. Qed.

Lemma contraNP (P : Prop) (b : bool) : (~ P -> b) -> ~~ b -> P.

Proof.

by move=> /contra_notP + /negP => /[apply]. Qed.

Lemma contra_neqP (T : eqType) (x y : T) P : (~ P -> x = y) -> x != y -> P.

Proof.

by move=> Pxy; apply: contraNP => /Pxy/eqP. Qed.

Lemma contra_eqP (T : eqType) (x y : T) Q : (~ Q -> x != y) -> x = y -> Q.

Proof.

by move=> Qxy /eqP; apply: contraTP. Qed.

Lemma contra_leP {disp1} {T1 : porderType disp1} [P : Prop] [x y : T1] :
(~ P -> (x < y)%O) -> (y <= x)%O -> P.

Proof.

move=> Pxy yx; apply/asboolP.
by apply: Order.POrderTheory.contra_leT yx => /asboolPn.
Qed.

Lemma contra_ltP {disp1} {T1 : porderType disp1} [P : Prop] [x y : T1] :
(~ P -> (x <= y)%O) -> (y < x)%O -> P.

Proof.

move=> Pxy yx; apply/asboolP.
by apply: Order.POrderTheory.contra_ltT yx => /asboolPn.
Qed.

Lemma wlog_neg P : (~ P -> P) -> P.

Proof.

by case: (PropB P); exact. Qed.

Lemma not_inj : injective not

Proof.

exact: can_inj notK. Qed.

Lemma notLR P Q : (P = ~ Q) -> (~ P) = Q

Proof.

exact: canLR notK. Qed.

Lemma notRL P Q : (~ P) = Q -> P = ~ Q

Proof.

exact: canRL notK. Qed.

Lemma iff_notr (P Q : Prop) : (P <-> ~ Q) <-> (~ P <-> Q).

Proof.

by split=> [/propext ->|/propext <-]; rewrite notK. Qed.

Lemma iff_not2 (P Q : Prop) : (~ P <-> ~ Q) <-> (P <-> Q).

Proof.

by split=> [/iff_notr|PQ]; [|apply/iff_notr]; rewrite notK. Qed.

Definition predp T := T -> Prop.

Identity Coercion fun_of_pred : predp >-> Funclass.

Definition relp T := T -> predp T.

Identity Coercion fun_of_rel : rel >-> Funclass.

Notation xpredp0 := (fun _ => False).
Notation xpredpT := (fun _ => True).
Notation xpredpI := (fun (p1 p2 : predp _) x => p1 x /\ p2 x).
Notation xpredpU := (fun (p1 p2 : predp _) x => p1 x \/ p2 x).
Notation xpredpC := (fun (p : predp _) x => ~ p x).
Notation xpredpD := (fun (p1 p2 : predp _) x => ~ p2 x /\ p1 x).
Notation xpreimp := (fun f (p : predp _) x => p (f x)).
Notation xrelpU := (fun (r1 r2 : relp _) x y => r1 x y \/ r2 x y).

Definition pred0p (T : Type) (P : predp T) : bool := `[].
Prenex Implicits pred0p.

Lemma pred0pP (T : Type) (P : predp T) : reflect (P =1 xpredp0) (pred0p P).

Proof.

by apply: (iffP (asboolP _)). Qed.

Lemma forallp_asboolPn {T} {P : T -> Prop} :
reflect (forall x : T, ~ P x) (~~ `[<exists x : T, P x>]).

Proof.

apply: (iffP idP)=> [/asboolPn NP x Px|NP].
by apply/NP; exists x. by apply/asboolP=> -[x]; apply/NP.
Qed.

Lemma existsp_asboolPn {T} {P : T -> Prop} :
reflect (exists x : T, ~ P x) (~~ `[<forall x : T, P x>]).

Proof.

apply: (iffP idP); last by case=> x NPx; apply/asboolPn=> /(_ x).
move/asboolPn=> NP; apply/asboolP/negbNE/asboolPn=> h.
by apply/NP=> x; apply/asboolP/negbNE/asboolPn=> NPx; apply/h; exists x.
Qed.

Lemma asbool_forallNb {T : Type} (P : pred T) :
`[< forall x : T, ~~ (P x) >] = ~~ `[< exists x : T, P x >].

Proof.

apply: (asbool_equiv_eqP forallp_asboolPn);
by split=> h x; apply/negP/h.
Qed.

Lemma asbool_existsNb {T : Type} (P : pred T) :
`[< exists x : T, ~~ (P x) >] = ~~ `[< forall x : T, P x >].

Proof.

apply: (asbool_equiv_eqP existsp_asboolPn);
by split=> -[x h]; exists x; apply/negP.
Qed.

Lemma not_implyP (P Q : Prop) : ~ (P -> Q) <-> P /\ ~ Q.

Proof.

split=> [/asboolP|[p nq pq]]; [|exact/nq/pq].
by rewrite asbool_neg => /imply_asboolPn.
Qed.

Lemma not_andE (P Q : Prop) : (~ (P /\ Q)) = ~ P \/ ~ Q.

Proof.

eqProp=> [/asboolPn|[|]]; try by apply: contra_not => -[].
by rewrite asbool_and negb_and => /orP[]/asboolPn; [left|right].
Qed.

Lemma not_andP (P Q : Prop) : ~ (P /\ Q) <-> ~ P \/ ~ Q.

Proof.

by rewrite not_andE. Qed.

Lemma not_and3P (P Q R : Prop) : ~ [/\ P, Q & R] <-> [\/ ~ P, ~ Q | ~ R].

Proof.

split=> [/and3_asboolP|/or3_asboolP].
by rewrite 2!negb_and -3!asbool_neg => /or3_asboolP.
by rewrite 3!asbool_neg -2!negb_and => /and3_asboolP.
Qed.

Lemma notP (P : Prop) : ~ ~ P <-> P.

Proof.

by split => [|p]; [exact: contrapT|exact]. Qed.

Lemma notE (P : Prop) : (~ ~ P) = P

Proof.

by rewrite propeqE notP. Qed.

Lemma not_orE (P Q : Prop) : (~ (P \/ Q)) = ~ P /\ ~ Q.

Proof.

by rewrite -[_ /\ _]notE not_andE 2!notE. Qed.

Lemma not_orP (P Q : Prop) : ~ (P \/ Q) <-> ~ P /\ ~ Q.

Proof.

by rewrite not_orE. Qed.

Lemma not_implyE (P Q : Prop) : (~ (P -> Q)) = (P /\ ~ Q).

Proof.

by rewrite propeqE not_implyP. Qed.

Lemma implyE (P Q : Prop) : (P -> Q) = (~ P \/ Q).

Proof.

by rewrite -[LHS]notE not_implyE propeqE not_andP notE. Qed.

Lemma orC : commutative or.

Proof.

by move=> /PropB[] /PropB[] => //; rewrite !orB. Qed.

Lemma orA : associative or.

Proof.

by move=> P Q R; rewrite propeqE; split=> [|]; tauto. Qed.

Lemma orCA : left_commutative or.

Proof.

by move=> P Q R; rewrite !orA (orC P). Qed.

Lemma orAC : right_commutative or.

Proof.

by move=> P Q R; rewrite -!orA (orC Q). Qed.

Lemma orACA : interchange or or.

Proof.

by move=> P Q R S; rewrite !orA (orAC P). Qed.

Lemma orNp P Q : (~ P \/ Q) = (P -> Q).

Proof.

by case/PropB: P; rewrite notB orB implyB. Qed.

Lemma orpN P Q : (P \/ ~ Q) = (Q -> P)

Proof.

by rewrite orC orNp. Qed.

Lemma or3E P Q R : [\/ P, Q | R] = (P \/ Q \/ R).

Proof.

rewrite -(asboolE P) -(asboolE Q) -(asboolE R) (reflect_eq or3P).
by rewrite -2!(reflect_eq orP).
Qed.

Lemma or4E P Q R S : [\/ P, Q, R | S] = (P \/ Q \/ R \/ S).

Proof.

rewrite -(asboolE P) -(asboolE Q) -(asboolE R) -(asboolE S) (reflect_eq or4P).
by rewrite -3!(reflect_eq orP).
Qed.

Lemma andC : commutative and.

Proof.

by move=> /PropB[] /PropB[]; rewrite !andB. Qed.

Lemma andA : associative and.

Proof.

by move=> P Q R; rewrite propeqE; split=> [|]; tauto. Qed.

Lemma andCA : left_commutative and.

Proof.

by move=> P Q R; rewrite !andA (andC P). Qed.

Lemma andAC : right_commutative and.

Proof.

by move=> P Q R; rewrite -!andA (andC Q). Qed.

Lemma andACA : interchange and and.

Proof.

by move=> P Q R S; rewrite !andA (andAC P). Qed.

Lemma and3E P Q R : [/\ P, Q & R] = (P /\ Q /\ R).

Proof.

by eqProp=> [[] | [? []]]. Qed.

Lemma and4E P Q R S : [/\ P, Q, R & S] = (P /\ Q /\ R /\ S).

Proof.

by eqProp=> [[] | [? [? []]]]. Qed.

Lemma and5E P Q R S T : [/\ P, Q, R, S & T] = (P /\ Q /\ R /\ S /\ T).

Proof.

by eqProp=> [[] | [? [? [? []]]]]. Qed.

Lemma implyNp P Q : (~ P -> Q : Prop) = (P \/ Q).

Proof.

by rewrite -orNp notK. Qed.

Lemma implypN (P Q : Prop) : (P -> ~ Q) = ~ (P /\ Q).

Proof.

by case/PropB: P; rewrite implyB andB ?notB. Qed.

Lemma implyNN P Q : (~ P -> ~ Q) = (Q -> P).

Proof.

by rewrite implyNp orpN. Qed.

Lemma or_andr : right_distributive or and.

Proof.

by case/PropB=> Q R; rewrite !orB ?andB. Qed.

Lemma or_andl : left_distributive or and.

Proof.

by move=> P Q R; rewrite -!(orC R) or_andr. Qed.

Lemma and_orr : right_distributive and or.

Proof.

by move=> P Q R; apply/not_inj; rewrite !(not_andE, not_orE) or_andr. Qed.

Lemma and_orl : left_distributive and or.

Proof.

by move=> P Q R; apply/not_inj; rewrite !(not_andE, not_orE) or_andl. Qed.

Lemma forallNE {T} (P : T -> Prop) : (forall x, ~ P x) = ~ exists x, P x.

Proof.

by rewrite propeqE; split => [fP [x /fP]//|nexP x Px]; apply: nexP; exists x.
Qed.

Lemma existsNE {T} (P : T -> Prop) : (exists x, ~ P x) = ~ forall x, P x.

Proof.

rewrite propeqE; split=> [[x Px] aP //|NaP].
by apply: contrapT; rewrite -forallNE => aP; apply: NaP => x; apply: contrapT.
Qed.

Lemma existsNP T (P : T -> Prop) : (exists x, ~ P x) <-> ~ forall x, P x.

Proof.

by rewrite existsNE. Qed.

Lemma not_existsP T (P : T -> Prop) : (exists x, P x) <-> ~ forall x, ~ P x.

Proof.

by rewrite forallNE notK. Qed.

Lemma forallNP T (P : T -> Prop) : (forall x, ~ P x) <-> ~ exists x, P x.

Proof.

by rewrite forallNE. Qed.

Lemma not_forallP T (P : T -> Prop) : (forall x, P x) <-> ~ exists x, ~ P x.

Proof.

by rewrite existsNE notK. Qed.

Lemma exists2E A P Q : (exists2 x : A, P x & Q x) = (exists x, P x /\ Q x).

Proof.

by eqProp=> -[x]; last case; exists x. Qed.

Lemma exists2P T (P Q : T -> Prop) :
(exists2 x, P x & Q x) <-> exists x, P x /\ Q x.

Proof.

by rewrite exists2E. Qed.

Lemma not_exists2P T (P Q : T -> Prop) :
(exists2 x, P x & Q x) <-> ~ forall x, ~ P x \/ ~ Q x.

Proof.

rewrite exists2P not_existsP.
by split; apply: contra_not => PQx x; apply/not_andP; apply: PQx.
Qed.

Lemma forall2NP T (P Q : T -> Prop) :
(forall x, ~ P x \/ ~ Q x) <-> ~ (exists2 x, P x & Q x).

Proof.

split=> [PQ [t Pt Qt]|PQ t]; first by have [] := PQ t.
by rewrite -not_andP => -[Pt Qt]; apply PQ; exists t.
Qed.

Lemma forallPNP T (P Q : T -> Prop) :
(forall x, P x -> ~ Q x) <-> ~ (exists2 x, P x & Q x).

Proof.

split=> [PQ [t Pt Qt]|PQ t]; first by have [] := PQ t.
by move=> Pt Qt; apply: PQ; exists t.
Qed.

Lemma existsPNP T (P Q : T -> Prop) :
(exists2 x, P x & ~ Q x) <-> ~ (forall x, P x -> Q x).

Proof.

split=> [[x Px NQx] /(_ x Px)//|]; apply: contra_notP => + x Px.
by apply: contra_notP => NQx; exists x.
Qed.

Lemma forallp_asboolPn2 {T} {P Q : T -> Prop} :
reflect (forall x : T, ~ P x \/ ~ Q x) (~~ `[<exists2 x : T, P x & Q x>]).

Proof.

apply: (iffP idP)=> [/asboolPn NP x|NP].
by move/forallPNP : NP => /(_ x)/and_rec/not_andP.
by apply/asboolP=> -[x Px Qx]; have /not_andP := NP x; exact.
Qed.

Section bigmaxmin.
Local Notation max := Order.max.
Local Notation min := Order.min.
Local Open Scope order_scope.
Variables (d : Order.disp_t) (T : orderType d).
Variables (x : T) (I : finType) (P : pred I) (m : T) (F : I -> T).

Import Order.TTheory.

Lemma bigmax_geP : reflect (m <= x \/ exists2 i, P i & m <= F i)
(m <= \big[max/x]_(i | P i) F i).

Proof.

apply: (iffP idP) => [|[mx|[i Pi mFi]]].
- rewrite leNgt => /bigmax_ltP /not_andP[/negP|]; first by rewrite -leNgt; left.
by move=> /existsNP[i /not_implyP[Pi /negP]]; rewrite -leNgt; right; exists i.
- by rewrite bigmax_idl le_max mx.
- by rewrite (bigmaxD1 i)// le_max mFi.
Qed.

Lemma bigmax_gtP : reflect (m < x \/ exists2 i, P i & m < F i)
(m < \big[max/x]_(i | P i) F i).

Proof.

apply: (iffP idP) => [|[mx|[i Pi mFi]]].
- rewrite ltNge => /bigmax_leP /not_andP[/negP|]; first by rewrite -ltNge; left.
by move=> /existsNP[i /not_implyP[Pi /negP]]; rewrite -ltNge; right; exists i.
- by rewrite bigmax_idl lt_max mx.
- by rewrite (bigmaxD1 i)// lt_max mFi.
Qed.

Lemma bigmin_leP : reflect (x <= m \/ exists2 i, P i & F i <= m)
(\big[min/x]_(i | P i) F i <= m).

Proof.

apply: (iffP idP) => [|[xm|[i Pi Fim]]].
- rewrite leNgt => /bigmin_gtP /not_andP[/negP|]; first by rewrite -leNgt; left.
by move=> /existsNP[i /not_implyP[Pi /negP]]; rewrite -leNgt; right; exists i.
- by rewrite bigmin_idl ge_min xm.
- by rewrite (bigminD1 i)// ge_min Fim.
Qed.

Lemma bigmin_ltP : reflect (x < m \/ exists2 i, P i & F i < m)
(\big[min/x]_(i | P i) F i < m).

Proof.

apply: (iffP idP) => [|[xm|[i Pi Fim]]].
- rewrite ltNge => /bigmin_geP /not_andP[/negP|]; first by rewrite -ltNge; left.
by move=> /existsNP[i /not_implyP[Pi /negP]]; rewrite -ltNge; right; exists i.
- by rewrite bigmin_idl gt_min xm.
- by rewrite (bigminD1 _ _ _ Pi) gt_min Fim.
Qed.

End bigmaxmin.

Module FunOrder.
Section FunOrder.
Import Order.TTheory.
Variables (aT : Type) (d : Order.disp_t) (T : porderType d).
Implicit Types f g h : aT -> T.

Lemma fun_display : Order.disp_t

Proof.

exact: Order.default_display. Qed.

Definition lef f g := `[< forall x, (f x <= g x)%O >].
Local Notation "f <= g" := (lef f g).

Definition ltf f g := `[< (forall x, (f x <= g x)%O) /\ exists x, f x != g x >].
Local Notation "f < g" := (ltf f g).

Lemma ltf_def f g : (f < g) = (g != f) && (f <= g).

Proof.

apply/idP/andP => [fg|[gf fg]]; [split|apply/asboolP; split; [exact/asboolP|]].
- by apply/eqP => gf; move: fg => /asboolP[fg] [x /eqP]; apply; rewrite gf.
- apply/asboolP => x; rewrite le_eqVlt; move/asboolP : fg => [fg [y gfy]].
  by have [//|gfx /=] := boolP (f x == g x); rewrite lt_neqAle gfx /= fg.
- apply/not_existsP => h.
  have : f =1 g by move=> x; have /negP/negPn/eqP := h x.
  by rewrite -funeqE; apply/nesym/eqP.
Qed.

Fact lef_refl : reflexive lef

Proof.

by move=> f; apply/asboolP => x. Qed.

Fact lef_anti : antisymmetric lef.

Proof.