Module mathcomp.classical.boolp

From HB Require Import structures.
From mathcomp Require Import boot order.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require internal_Eqdep_dec.

# Classical Logic This file provides the axioms of classical logic and tools to perform classical reasoning in the Mathematical Component 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 - A decidable equality is defined for any type. It is thus possible to define an eqType structure for any type using the mixin `gen_eqMixin`. - This file adds the possibility to define a choiceType structure for any type thanks to an axiom `gen_choiceMixin` giving a choice mixin. - We chose to have generic mixins and no global instances of the eqType and choiceType structures to let the user choose which definition of equality to use and to avoid conflict with already declared instances. ``` {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 ```

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

Declare Scope box_scope.
Declare Scope quant_scope.

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

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

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

Proof.

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

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

Proof.

by case. Qed.

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

Proof.

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

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

Proof.

by case: p. Qed.

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

Fact : mextensionality.

Proof.

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

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

Proof.

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

Ltac eqProp := apply: propext; split.

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

Proof.

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

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

Proof.

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

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

Proof.

by rewrite propeqE. Qed.

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

by rewrite funeqE. Qed.

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

Proof.

by rewrite funeq2E. Qed.

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

Proof.

by rewrite funeq3E. Qed.

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

by rewrite predeqE. Qed.

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

Proof.

by rewrite predeq2E. Qed.

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

Proof.

by rewrite predeq3E. Qed.

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

Proof.

by move=> p; rewrite propeqE. Qed.

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

Proof.

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

#[global] Hint Resolve Prop_irrelevance : core.

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

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

Proof.

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

Theorem : P \/ ~ P.

Proof.

pose U := fun : bool => Q = val \/ P.
have Uex val : exists , U val b by exists val; left.
pose f := projT1 (cid (Uex val)).
pose Uf : 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 ( : Prop): {P} + {~P}.

Proof.

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

Lemma : (T -> False) + T.

Proof.

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

Lemma : mclassic.

Proof.

split=> [|T]; first exact: pselect.
exists (fun ( : pred T) ( : nat) =>
 if pselect (exists , 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 ( : Type) : hasChoice T.

Proof.

by case: classic. Qed.

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

Proof.

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

Lemma : true = True :> Prop.

Proof.

by rewrite propeqE; split. Qed.

Lemma : false = False :> Prop.

Proof.

by rewrite propeqE; split. Qed.

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

Proof.

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

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

Proof.

by move=> /funext->. Qed.

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

Lemma ( : T -> Prop) ( : T) ( : P s) ( : 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 ( : T) ( : S), Prop) :
(forall , U x y) = (forall , U x y).

Proof.

by rewrite propeqE; split. Qed.

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

Proof.

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

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

Proof.

by rewrite propeqE; exact: rwP. Qed.

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

Notation := (asbool P) : bool_scope.

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

Proof.

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

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

Proof.

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

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

Proof.

by apply/asboolP/idP. Qed.

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

Proof.

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

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

Proof.

by case: asboolP. Qed.

Lemma : A \/ B -> A + B.

Proof.

have [|NA] := asboolP A; first by left.
have [|NB] := asboolP B; first by right.
by move=> AB; exfalso; case: AB.
Qed.

Lemma : [\/ A, B | C] -> A + B + C.

Proof.

have [|NA] := asboolP A; first by left; left.
have [|NB] := asboolP B; first by left; right.
have [|NC] := asboolP C; first by right.
by move=> ABC; exfalso; case: ABC.
Qed.

Lemma : [\/ A, B, C | D] -> A + B + C + D.

Proof.

have [|NA] := asboolP A; first by left; left; left.
have [|NB] := asboolP B; first by left; left; right.
have [|NC] := asboolP C; first by left; right.
have [|ND] := asboolP D; first by right.
by move=> ABCD; exfalso; case: ABCD.
Qed.

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

Proof.

by case: asboolP. Qed.

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

Proof.

by apply/introF/asboolP. Qed.

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

Proof.

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

Lemma : injective is_true.

Proof.

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

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

Proof.

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

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

. () ( -> eqType) :=
  gen_eqMixin (forall : T, T' t).

. () ( -> choiceType) :=
  gen_choiceMixin (forall : T, T' t).

. Prop.
. Prop.

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

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

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

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

Proof.

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

Arguments canon {T U sort} x.

Lemma : canonical Type eqType.

Proof.

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

Lemma : canonical Type choiceType.

Proof.

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

Lemma : canonical eqType choiceType.

Proof.

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

Lemma : (~ True) = False

Proof.

exact/propext. Qed.

Lemma : (~ False) = True

Proof.

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

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

Proof.

by rewrite -propeqE => ->. Qed.

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

Proof.

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

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

Proof.

by move/asbool_equiv_eq->. Qed.

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

Proof.

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

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

Proof.

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

Lemma ( : 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 ( : Prop) : reflect (P \/ Q) (`[] || `[< Q >]).

Proof.

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

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

Proof.

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

exact: (asbool_equiv_eqP imply_asboolP). Qed.

Lemma ( : 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 { : Type} ( : T -> Prop) :
reflect (forall , `[]) (`[<forall , P x>]).

Proof.

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

Lemma { : Type} ( : T -> Prop) :
reflect (exists , `[]) (`[<exists , 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 : Prop -> Type :=
| : BoolProp True
| : BoolProp False.

Lemma : BoolProp P.

Proof.

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

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

Proof.

by rewrite /not; split; eqProp. Qed.

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

Proof.

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

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

Proof.

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

Lemma : let ( : 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 : P \/ Q -> {P} + {Q}.

Proof.

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

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

Proof.

by move->. Qed.

Lemma : ~ ~ P -> P.

Proof.

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

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

Proof.

by case: (PropB P). Qed.

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

Proof.

by move/notT; exact: contrapT. Qed.

Lemma : involutive not.

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

Lemma {} { : porderType disp1} [ : Prop] [ : 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 {} { : porderType disp1} [ : Prop] [ : 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 : (~ P -> P) -> P.

Proof.

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

Lemma : injective not

Proof.

exact: can_inj notK. Qed.

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

Proof.

exact: canLR notK. Qed.

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

Proof.

exact: canRL notK. Qed.

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

Proof.

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

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

Proof.

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

Definition := T -> Prop.

Identity Coercion fun_of_pred : predp >-> Funclass.

Definition := T -> predp T.

Identity Coercion fun_of_rel : rel >-> Funclass.

Notation := (fun _ => False).
Notation := (fun _ => True).
Notation := (fun ( : predp _) => p1 x /\ p2 x).
Notation := (fun ( : predp _) => p1 x \/ p2 x).
Notation := (fun ( : predp _) => ~ p x).
Notation := (fun ( : predp _) => ~ p2 x /\ p1 x).
Notation := (fun ( : predp _) => p (f x)).
Notation := (fun ( : relp _) => r1 x y \/ r2 x y).

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

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

Proof.

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

Lemma {} { : T -> Prop} :
reflect (forall : T, ~ P x) (~~ `[<exists : 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 {} { : T -> Prop} :
reflect (exists : T, ~ P x) (~~ `[<forall : 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 { : Type} ( : pred T) :
`[< forall : T, ~~ (P x) >] = ~~ `[< exists : T, P x >].

Proof.

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

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

Proof.

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

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

Proof.

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

Lemma ( : 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 ( : Prop) : ~ (P /\ Q) <-> ~ P \/ ~ Q.

Proof.

by rewrite not_andE. Qed.

Lemma ( : 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 ( : Prop) : ~ ~ P <-> P.

Proof.

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

#[deprecated(since="mathcomp-analysis 1.15.0", note="Renamed to `not_notP`. Warning: a different `notP` is provided by `contra.v`.")]
Notation := not_notP (only parsing).

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

Proof.

by rewrite propeqE not_notP. Qed.

#[deprecated(since="mathcomp-analysis 1.15.0", note="Renamed to `not_notE`. Warning: a different `notE` is provided by `contra.v`.")]
Notation := not_notE (only parsing).

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

Proof.

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

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

Proof.

by rewrite not_orE. Qed.

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

Proof.

by rewrite propeqE not_implyP. Qed.

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

Proof.

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

Lemma : commutative or.

Proof.

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

Lemma : associative or.

Proof.

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

Lemma : left_commutative or.

Proof.

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

Lemma : right_commutative or.

Proof.

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

Lemma : interchange or or.

Proof.

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

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

Proof.

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

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

Proof.

by rewrite orC orNp. Qed.

Lemma : [\/ 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 : [\/ 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 : commutative and.

Proof.

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

Lemma : associative and.

Proof.

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

Lemma : left_commutative and.

Proof.

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

Lemma : right_commutative and.

Proof.

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

Lemma : interchange and and.

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

by rewrite -orNp notK. Qed.

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

Proof.

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

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

Proof.

by rewrite implyNp orpN. Qed.

Lemma : right_distributive or and.

Proof.

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

Lemma : left_distributive or and.

Proof.

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

Lemma : right_distributive and or.

Proof.

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

Lemma : left_distributive and or.

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

by rewrite existsNE. Qed.

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

Proof.

by rewrite forallNE notK. Qed.

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

Proof.

by rewrite forallNE. Qed.

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

Proof.

by rewrite existsNE notK. Qed.

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

Proof.

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

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

Proof.

by rewrite exists2E. Qed.

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

Proof.

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

Lemma ( : T -> Prop) :
(forall , ~ P x \/ ~ Q x) <-> ~ (exists2 , 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 ( : T -> Prop) :
(forall , P x -> ~ Q x) <-> ~ (exists2 , 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 ( : T -> Prop) :
(exists2 , P x & ~ Q x) <-> ~ (forall , 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 {} { : T -> Prop} :
reflect (forall : T, ~ P x \/ ~ Q x) (~~ `[<exists2 : 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 := Order.max.
Local Notation := Order.min.
Local Open Scope order_scope.
Context {} { : orderType d} ( : T)
{ : finType} ( : pred I) ( : T) ( : I -> T).

Import Order.TTheory.

Lemma : reflect (m <= x \/ exists2 , P i & m <= F i)
(m <= \big[max/x]_( | 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 : reflect (m < x \/ exists2 , P i & m < F i)
(m < \big[max/x]_( | 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 : reflect (x <= m \/ exists2 , P i & F i <= m)
(\big[min/x]_( | 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 : reflect (x < m \/ exists2 , P i & F i < m)
(\big[min/x]_( | 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 .
Section FunOrder.
Import Order.TTheory.
Context { : Type} {} { : porderType d}.
Implicit Types f g h : aT -> T.

Lemma : Order.disp_t

Proof.

exact: Order.default_display. Qed.

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

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

Lemma : (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 : reflexive lef

Proof.

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

Fact : antisymmetric lef.

Proof.

move=> f g => /andP[/asboolP fg /asboolP gf]; rewrite funeqE => x.
by apply/eqP; rewrite eq_le fg gf.
Qed.

Fact : transitive lef.

Proof.

move=> g f h /asboolP fg /asboolP gh; apply/asboolP => x.
by rewrite (le_trans (fg x)).
Qed.

..isPOrder.Build
fun_display (aT -> T) lef ltf ltf_def lef_refl lef_anti lef_trans.

End FunOrder.

Section FunLattice.
Import Order.TTheory.
Context { : Type} {} { : latticeType d}.
Implicit Types f g h : aT -> T.

Definition := fun => Order.meet (f x) (g x).
Definition := fun => Order.join (f x) (g x).

Lemma : commutative meetf.

Proof.

move=> f g; apply/funext => x; exact: meetC. Qed.

Lemma : commutative joinf.

Proof.

move=> f g; apply/funext => x; exact: joinC. Qed.

Lemma : associative meetf.

Proof.

move=> f g h; apply/funext => x; exact: meetA. Qed.

Lemma : associative joinf.

Proof.

move=> f g h; apply/funext => x; exact: joinA. Qed.

Lemma : meetf f (joinf f g) = f.

Proof.

apply/funext => x; exact: joinKI. Qed.

Lemma : joinf f (meetf f g) = f.

Proof.

apply/funext => x; exact: meetKU. Qed.

Lemma : (f <= g)%O = (meetf f g == f).

Proof.

apply/idP/idP => [/asboolP f_le_g|/eqP <-].
- apply/eqP/funext => x; exact/meet_l/f_le_g.
- apply/asboolP => x; exact: leIr.
Qed.

..POrder_isLattice.Build _ (aT -> T)
meetfC joinfC meetfA joinfA joinfKI meetfKU lef_meet.

End FunLattice.
Module .
HB.reexport.
End Exports.
End FunOrder.
Export FunOrder.Exports.

Lemma ( : Type) ( : porderType d) ( : aT -> T) :
reflect (forall , (f x <= g x)%O) (f <= g)%O.

Proof.

by apply: (iffP idP) => [fg|fg]; [exact/asboolP | exact/asboolP]. Qed.

Lemma ( : Type) ( : latticeType d) ( : aT -> T) :
((f `&` g) x = f x `&` g x)%O.

Proof.

by []. Qed.

Lemma ( : Type) ( : latticeType d) ( : aT -> T) :
((f `|` g) x = f x `|` g x)%O.

Proof.

by []. Qed.

Lemma {} ( : T -> T) : iter n.+1 f = f \o iter n f.

Proof.

by []. Qed.

Lemma {} ( : T -> T) : iter n.+1 f = iter n f \o f.

Proof.

by apply/funeqP => ?; rewrite iterSr. Qed.

Lemma {} ( : T -> T) : iter 0 f = id.

Proof.

by []. Qed.

Section Inhabited.
Context ( : Type).

Lemma : inhabited T = exists : T, True.

Proof.

by eqProp; case. Qed.

Lemma : inhabited T -> T.

Proof.

by rewrite inhabitedE => /cid[]. Qed.

End Inhabited.

Lemma { : Type} : cancel (@uncurry X Y Z) curry.

Proof.

by move=> f; rewrite funeq2E. Qed.

Lemma { : Type} : cancel curry (@uncurry X Y Z).

Proof.

by move=> f; rewrite funeqE=> -[]. Qed.

Files

Module mathcomp.classical.boolp