Library UniMath.MoreFoundations.DecidablePropositions
Require Export UniMath.MoreFoundations.Notations.
Require Import UniMath.MoreFoundations.Tactics.
Lemma retract_dec {X Y} (f : X -> Y) (g : Y -> X) (h : f ∘ g ~ idfun Y) : isdeceq X -> isdeceq Y.
Show proof.
Lemma logeq_dec {X Y} : (X <-> Y) -> decidable X -> decidable Y.
Show proof.
Definition decidable_prop (X:hProp) := make_hProp (decidable X) (isapropdec X (pr2 X)).
Definition LEM : hProp := ∀ P : hProp, decidable_prop P.
Require Import UniMath.MoreFoundations.Tactics.
Lemma retract_dec {X Y} (f : X -> Y) (g : Y -> X) (h : f ∘ g ~ idfun Y) : isdeceq X -> isdeceq Y.
Show proof.
intros i y y'. induction (i (g y) (g y')) as [eq|ne].
- apply ii1. exact (! h y @ maponpaths f eq @ h y').
- apply ii2. intro p. apply ne. exact (maponpaths g p).
- apply ii1. exact (! h y @ maponpaths f eq @ h y').
- apply ii2. intro p. apply ne. exact (maponpaths g p).
Lemma logeq_dec {X Y} : (X <-> Y) -> decidable X -> decidable Y.
Show proof.
intros iff decX. induction iff as [XtoY YtoX].
induction decX as [x|nx].
- now apply ii1, XtoY.
- now apply ii2, (negf YtoX).
induction decX as [x|nx].
- now apply ii1, XtoY.
- now apply ii2, (negf YtoX).
Definition decidable_prop (X:hProp) := make_hProp (decidable X) (isapropdec X (pr2 X)).
Definition LEM : hProp := ∀ P : hProp, decidable_prop P.
Definition ComplementaryPair : UU := ∑ (P Q : UU), complementary P Q.
Definition Part1 (C : ComplementaryPair) : UU := pr1 C.
Definition Part2 (C : ComplementaryPair) : UU := pr1 (pr2 C).
Definition pair_contradiction (C : ComplementaryPair) : Part1 C -> Part2 C -> ∅
:= pr1 (pr2 (pr2 C)).
Definition chooser (C : ComplementaryPair) : Part1 C ⨿ Part2 C
:= pr2 (pr2 (pr2 C)).
Definition isTrue (C : ComplementaryPair)
:= hfiber (@ii1 (Part1 C) (Part2 C)) (chooser C).
Definition isFalse (C : ComplementaryPair)
:= hfiber (@ii2 (Part1 C) (Part2 C)) (chooser C).
Definition trueWitness {C : ComplementaryPair} : isTrue C -> Part1 C := pr1.
Definition falseWitness {C : ComplementaryPair} : isFalse C -> Part2 C := pr1.
Coercion trueWitness : isTrue >-> Part1.
Coercion falseWitness : isFalse >-> Part2.
Lemma complementaryDecisions (C : ComplementaryPair) :
iscontr (isTrue C ⨿ isFalse C).
Show proof.
intros.
apply iscontrifweqtounit. assert (w := weqcoprodsplit (λ _:unit, chooser C)).
apply invweq. apply (weqcomp w). apply weqcoprodf; apply weqhfiberunit.
apply iscontrifweqtounit. assert (w := weqcoprodsplit (λ _:unit, chooser C)).
apply invweq. apply (weqcomp w). apply weqcoprodf; apply weqhfiberunit.
Lemma isaprop_isTrue (C : ComplementaryPair) : isaprop (isTrue C).
Show proof.
intros.
apply (isapropcomponent1 (isTrue C) (isFalse C)).
apply isapropifcontr.
apply complementaryDecisions.
apply (isapropcomponent1 (isTrue C) (isFalse C)).
apply isapropifcontr.
apply complementaryDecisions.
Lemma isaprop_isFalse (C : ComplementaryPair) : isaprop (isFalse C).
Show proof.
intros.
apply (isapropcomponent2 (isTrue C) (isFalse C)).
apply isapropifcontr.
apply complementaryDecisions.
apply (isapropcomponent2 (isTrue C) (isFalse C)).
apply isapropifcontr.
apply complementaryDecisions.
Ltac unpack_pair C P Q con c := induction C as [P Qc]; induction Qc as [Q c];
induction c as [con c]; simpl in c, P, Q.
Lemma pair_truth (C : ComplementaryPair) : Part1 C -> isTrue C.
Show proof.
intros p.
unpack_pair C P Q con c;
unfold isTrue, hfiber, Part1, Part2, chooser in *; simpl in *.
induction c as [p'|q].
- now exists p'.
- apply fromempty. contradicts (con p) q.
unpack_pair C P Q con c;
unfold isTrue, hfiber, Part1, Part2, chooser in *; simpl in *.
induction c as [p'|q].
- now exists p'.
- apply fromempty. contradicts (con p) q.
Lemma pair_falsehood (C : ComplementaryPair) : Part2 C -> isFalse C.
Show proof.
intros q.
unpack_pair C P Q con c;
unfold isFalse, hfiber, Part1, Part2, chooser in *; simpl in *.
induction c as [p|q'].
- apply fromempty. contradicts (con p) q.
- now exists q'.
unpack_pair C P Q con c;
unfold isFalse, hfiber, Part1, Part2, chooser in *; simpl in *.
induction c as [p|q'].
- apply fromempty. contradicts (con p) q.
- now exists q'.
Definition to_ComplementaryPair {P : UU} (c : P ⨿ neg P) : ComplementaryPair
:= (P,,neg P,,(λ p n, n p),,c).
Definition isolation {X : UU} (x : X) (is : isisolated X x) (y : X) : UU
:= isFalse (to_ComplementaryPair (is y)).
Definition isaprop_isolation {X : UU} (x : X) (is : isisolated X x) (y : X) :
isaprop (isolation x is y) := isaprop_isFalse _.
Definition isolation_to_inequality {X : UU} (x : X) (is : isisolated X x)
(y : X) :
isolation x is y -> x != y := falseWitness.
Definition inequality_to_isolation {X : UU} (x : X) (i : isisolated X x)
(y : X) :
x != y -> isolation x i y := pair_falsehood (to_ComplementaryPair (i y)).
Definition pairNegation (C : ComplementaryPair) : ComplementaryPair
:= Part2 C,, Part1 C ,, (λ q p, pair_contradiction C p q),,
coprodcomm _ _ (chooser C).
Definition pairConjunction (C C' : ComplementaryPair) : ComplementaryPair.
Show proof.
unpack_pair C P Q con c; unpack_pair C' P' Q' con' c'; simpl in *.
unfold ComplementaryPair. exists (P × P'); exists (Q ⨿ Q'). split.
- simpl. intros a b. induction a as [p p']. induction b as [b|b].
+ induction c' as [_|q'].
* contradicts (con p) b.
* contradicts (con p) b.
+ contradicts (con' p') b.
- simpl. induction c as [p|q].
+ induction c' as [p'|q'].
* apply ii1. exact (p,,p').
* apply ii2, ii2. exact q'.
+ induction c' as [p'|q'].
* apply ii2, ii1. exact q.
* apply ii2, ii2. exact q'.
unfold ComplementaryPair. exists (P × P'); exists (Q ⨿ Q'). split.
- simpl. intros a b. induction a as [p p']. induction b as [b|b].
+ induction c' as [_|q'].
* contradicts (con p) b.
* contradicts (con p) b.
+ contradicts (con' p') b.
- simpl. induction c as [p|q].
+ induction c' as [p'|q'].
* apply ii1. exact (p,,p').
* apply ii2, ii2. exact q'.
+ induction c' as [p'|q'].
* apply ii2, ii1. exact q.
* apply ii2, ii2. exact q'.
Definition pairDisjunction (C C' : ComplementaryPair) : ComplementaryPair.
Show proof.
Definition dnegelim {P Q : UU} : complementary P Q -> ¬¬ P -> P.
Show proof.
intros c nnp. induction c as [n c].
induction c as [p|q].
- assumption.
- contradicts nnp (λ p, n p q).
induction c as [p|q].
- assumption.
- contradicts nnp (λ p, n p q).
Lemma LEM_for_sets (X : UU) : LEM -> isaset X -> isdeceq X.
Show proof.
Lemma isaprop_LEM : isaprop LEM.
Show proof.
Lemma dneg_LEM (P : hProp) : LEM -> ¬¬ P -> P.
Show proof.
Corollary reversal_LEM (P Q : hProp) : LEM -> (¬ P -> Q) -> (¬ Q -> P).
Show proof.
intros lem f n.
assert (g := negf f); clear f.
assert (h := g n); clear g n.
apply (dneg_LEM _ lem).
exact h.
assert (g := negf f); clear f.
assert (h := g n); clear g n.
apply (dneg_LEM _ lem).
exact h.
Definition DecidableProposition : UU := ∑ X : UU, isdecprop X.
Definition isdecprop_to_DecidableProposition {X : UU} (i : isdecprop X) :
DecidableProposition := X,,i.
Definition decidable_to_isdecprop {X : hProp} : decidable X -> isdecprop X.
Show proof.
Definition decidable_to_isdecprop_2 {X : UU} :
isaprop X -> X ⨿ ¬ X -> isdecprop X.
Show proof.
Definition decidable_to_DecidableProposition {X : hProp} :
decidable X -> DecidableProposition.
Show proof.
Definition DecidableProposition_to_isdecprop (X : DecidableProposition) :
isdecprop (pr1 X).
Show proof.
apply pr2.
Definition DecidableProposition_to_hProp : DecidableProposition -> hProp.
Show proof.
Coercion DecidableProposition_to_hProp : DecidableProposition >-> hProp.
Definition decidabilityProperty (X : DecidableProposition) :
isdecprop X := pr2 X.
Definition DecidableSubtype (X : UU) : UU := X -> DecidableProposition.
Definition DecidableRelation (X : UU) : UU := X -> X -> DecidableProposition.
Definition decrel_to_DecidableRelation {X : UU} :
decrel X -> DecidableRelation X.
Show proof.
intros R x y. induction R as [R is]. exists (R x y).
apply isdecpropif. { apply propproperty. } apply is.
apply isdecpropif. { apply propproperty. } apply is.
Definition decidableAnd (P Q : DecidableProposition) : DecidableProposition.
Show proof.
Definition decidableOr (P Q : DecidableProposition) : DecidableProposition.
Show proof.
Lemma neg_isdecprop {X : UU} : isdecprop X -> isdecprop (¬ X).
Show proof.
intros i.
set (j := isdecproptoisaprop X i).
apply isdecpropif.
- apply isapropneg.
- unfold isdecprop in i.
set (k := pr1 i).
induction k as [k|k].
+ apply ii2. now apply todneg.
+ now apply ii1.
set (j := isdecproptoisaprop X i).
apply isdecpropif.
- apply isapropneg.
- unfold isdecprop in i.
set (k := pr1 i).
induction k as [k|k].
+ apply ii2. now apply todneg.
+ now apply ii1.
Definition decidableNot (P : DecidableProposition) : DecidableProposition.
Show proof.
Declare Scope decidable_logic.
Notation "X ∨ Y" := (decidableOr X Y) (at level 85, right associativity) :
decidable_logic.
Notation "A ∧ B" := (decidableAnd A B) (at level 80, right associativity) :
decidable_logic.
Notation "'¬' X" := (decidableNot X) (at level 35, right associativity) :
decidable_logic.
Delimit Scope decidable_logic with declog.
Ltac choose P yes no := induction (pr1 (decidabilityProperty P)) as [yes|no].
Definition choice {W : UU} : DecidableProposition -> W -> W -> W.
Show proof.
intros P yes no.
choose P p q.
- exact yes.
- exact no.
choose P p q.
- exact yes.
- exact no.
Definition dependent_choice {W : UU} (P : DecidableProposition) :
(P -> W) -> (¬ P -> W) -> W.
Show proof.
intros yes no.
choose P p q.
- exact (yes p).
- exact (no q).
choose P p q.
- exact (yes p).
- exact (no q).
Definition choice_compute_yes {W : UU} (P : DecidableProposition) (p : P)
(yes no : W) :
choice P yes no = yes.
Show proof.
Definition choice_compute_no {W : UU} (P : DecidableProposition) (p : ¬ P)
(yes no : W) :
choice P yes no = no.
Show proof.
Definition decidableSubtypeCarrier {X : UU} : DecidableSubtype X -> UU.
Show proof.
Definition decidableSubtypeCarrier' {X : UU} : DecidableSubtype X -> UU.
Show proof.
Definition decidableSubtypeCarrier_weq {X : UU} (P : DecidableSubtype X) :
decidableSubtypeCarrier' P ≃ decidableSubtypeCarrier P.
Show proof.
intros.
apply weqfibtototal.
intros x.
unfold choice.
simpl.
change (pr1 (decidabilityProperty (P x)))
with (pr1 (decidabilityProperty (P x))).
choose (P x) p q.
- simpl. apply weqiff.
+ apply logeq_both_true.
* reflexivity.
* assumption.
+ apply isasetbool.
+ apply (propproperty (DecidableProposition_to_hProp _)).
- simpl. apply weqiff.
+ apply logeq_both_false.
* exact nopathsfalsetotrue.
* assumption.
+ apply isasetbool.
+ apply (propproperty (DecidableProposition_to_hProp _)).
apply weqfibtototal.
intros x.
unfold choice.
simpl.
change (pr1 (decidabilityProperty (P x)))
with (pr1 (decidabilityProperty (P x))).
choose (P x) p q.
- simpl. apply weqiff.
+ apply logeq_both_true.
* reflexivity.
* assumption.
+ apply isasetbool.
+ apply (propproperty (DecidableProposition_to_hProp _)).
- simpl. apply weqiff.
+ apply logeq_both_false.
* exact nopathsfalsetotrue.
* assumption.
+ apply isasetbool.
+ apply (propproperty (DecidableProposition_to_hProp _)).
Definition DecidableSubtype_to_hsubtype {X : UU} (P : DecidableSubtype X) :
hsubtype X
:= λ x, DecidableProposition_to_hProp (P x).
Coercion DecidableSubtype_to_hsubtype : DecidableSubtype >-> hsubtype.
Definition DecidableRelation_to_hrel {X : UU} (P : DecidableRelation X) : hrel X
:= λ x y, DecidableProposition_to_hProp(P x y).
Coercion DecidableRelation_to_hrel : DecidableRelation >-> hrel.
Definition natlth_DecidableProposition : DecidableRelation nat :=
decrel_to_DecidableRelation natlthdec.
Definition natleh_DecidableProposition : DecidableRelation nat :=
decrel_to_DecidableRelation natlehdec.
Definition natgth_DecidableProposition : DecidableRelation nat :=
decrel_to_DecidableRelation natgthdec.
Definition natgeh_DecidableProposition : DecidableRelation nat :=
decrel_to_DecidableRelation natgehdec.
Definition nateq_DecidableProposition : DecidableRelation nat :=
decrel_to_DecidableRelation natdeceq.
Definition natneq_DecidableProposition : DecidableRelation nat :=
decrel_to_DecidableRelation natdecneq.
Declare Scope decidable_nat.
Notation " x < y " := (natlth_DecidableProposition x y) (at level 70, no associativity) :
decidable_nat.
Notation " x <= y " := (natleh_DecidableProposition x y) (at level 70, no associativity) :
decidable_nat.
Notation " x ≤ y " := (natleh_DecidableProposition x y) (at level 70, no associativity) :
decidable_nat.
Notation " x ≥ y " := (natgeh_DecidableProposition x y) (at level 70, no associativity) :
decidable_nat.
Notation " x ≥ y " := (natgeh_DecidableProposition x y) (at level 70, no associativity) :
decidable_nat.
Notation " x > y " := (natgth_DecidableProposition x y) (at level 70, no associativity) :
decidable_nat.
Notation " x =? y " := (nateq_DecidableProposition x y) (at level 70, no associativity) :
decidable_nat.
Notation " x ≠ y " := (natneq_DecidableProposition x y) (at level 70, no associativity) :
decidable_nat.
Delimit Scope decidable_nat with dnat.