decidable

decToBoolYes

theorem decToBoolYes {P : Type} (p : P) : decToBool (yes p) = true

A positive decision yes p converts to the boolean true.

decToBoolNo

theorem decToBoolNo {P : Type} (f : P -> Empty) : decToBool (no f) = false

A negative decision no f converts to the boolean false.

decMap

def decMap {P Q : Type} (f : P -> Q) (g : Q -> P) (d : Dec P) : Dec Q

Transports a decision for P to a decision for Q along maps in both directions.

decMapYes

theorem decMapYes {P Q : Type} (f : P -> Q) (g : Q -> P) (p : P) : decMap f g (yes p) = yes (f p)

Mapping a positive decision gives yes of the mapped witness.

decMapNo

theorem decMapNo {P Q : Type} (f : P -> Q) (g : Q -> P) (np : P -> Empty) : decMap f g (no np) = no (fun (q : Q) => np (g q))

Mapping a negative decision gives no with the refutation precomposed by the backward map.

decNot

def decNot {P : Type} (d : Dec P) : Dec (P -> Empty)

Decides the negation of P from a decision for P.

decAnd

def decAnd {P Q : Type} (dp : Dec P) (dq : Dec Q) : Dec (P × Q)

Decides the conjunction (product) of two decidable propositions.

decOr

def decOr {P Q : Type} (dp : Dec P) (dq : Dec Q) : Dec (Either P Q)

Decides the disjunction (Either) of two decidable propositions, preferring the left one.

decImpl

def decImpl {P Q : Type} (dp : Dec P) (dq : Dec Q) : Dec (P -> Q)

Decides the implication P -> Q from decisions for P and Q.

decEquiv

def decEquiv {P Q : Type} (f : P -> Q) (g : Q -> P) (d : Dec P) : Dec Q

Transports a decision across a logical equivalence given by maps both ways; an alias of decMap.

decRefl

def decRefl {A : Type} (a : A) : Dec (a = a)

Decides a = a positively by reflexivity.

decUnit

def decUnit : Dec Unit

The decision that Unit holds.

decEmpty

def decEmpty : Dec Empty

The decision that Empty does not hold.

decNotYes

theorem decNotYes {P : Type} (p : P) : decToBool (decNot (yes p)) = false

Negating a positive decision yields boolean false.

decNotNo

theorem decNotNo {P : Type} (np : P -> Empty) : decToBool (decNot (no np)) = true

Negating a negative decision yields boolean true.

decNotNot

theorem decNotNot {P : Type} (d : Dec P) : decToBool (decNot (decNot d)) = decToBool d

Double negation of a decision has the same boolean value as the original.

decAndYesYes

theorem decAndYesYes {P Q : Type} (p : P) (q : Q) : decToBool (decAnd (yes p) (yes q)) = true

The conjunction of two positive decisions is true.

decAndYesNo

theorem decAndYesNo {P Q : Type} (p : P) (nq : Q -> Empty) : decToBool (decAnd (yes p) (no nq)) = false

The conjunction of a positive and a negative decision is false.

decAndNoYes

theorem decAndNoYes {P Q : Type} (np : P -> Empty) (q : Q) : decToBool (decAnd (no np) (yes q)) = false

The conjunction of a negative and a positive decision is false.

decAndNoNo

theorem decAndNoNo {P Q : Type} (np : P -> Empty) (nq : Q -> Empty) : decToBool (decAnd (no np) (no nq)) = false

The conjunction of two negative decisions is false.

decAndBool

theorem decAndBool {P Q : Type} (dp : Dec P) (dq : Dec Q) : decToBool (decAnd dp dq) = and (decToBool dp) (decToBool dq)

The boolean value of decAnd is the boolean and of the two decisions’ values.

decOrYesYes

theorem decOrYesYes {P Q : Type} (p : P) (q : Q) : decToBool (decOr (yes p) (yes q)) = true

The disjunction of two positive decisions is true.

decOrYesNo

theorem decOrYesNo {P Q : Type} (p : P) (nq : Q -> Empty) : decToBool (decOr (yes p) (no nq)) = true

The disjunction of a positive and a negative decision is true.

decOrNoYes

theorem decOrNoYes {P Q : Type} (np : P -> Empty) (q : Q) : decToBool (decOr (no np) (yes q)) = true

The disjunction of a negative and a positive decision is true.

decOrNoNo

theorem decOrNoNo {P Q : Type} (np : P -> Empty) (nq : Q -> Empty) : decToBool (decOr (no np) (no nq)) = false

The disjunction of two negative decisions is false.

decOrBool

theorem decOrBool {P Q : Type} (dp : Dec P) (dq : Dec Q) : decToBool (decOr dp dq) = or (decToBool dp) (decToBool dq)

The boolean value of decOr is the boolean or of the two decisions’ values.

decImplNoAny

theorem decImplNoAny {P Q : Type} (np : P -> Empty) (dq : Dec Q) : decToBool (decImpl (no np) dq) = true

An implication with a refuted premise is decided true, whatever the conclusion.

decImplYesYes

theorem decImplYesYes {P Q : Type} (p : P) (q : Q) : decToBool (decImpl (yes p) (yes q)) = true

An implication between two positive decisions is true.

decImplYesNo

theorem decImplYesNo {P Q : Type} (p : P) (nq : Q -> Empty) : decToBool (decImpl (yes p) (no nq)) = false

An implication from a positive to a negative decision is false.

decEquivYes

theorem decEquivYes {P Q : Type} (f : P -> Q) (g : Q -> P) (p : P) : decToBool (decEquiv f g (yes p)) = true

Transporting a positive decision with decEquiv stays true.

decEquivNo

theorem decEquivNo {P Q : Type} (f : P -> Q) (g : Q -> P) (np : P -> Empty) : decToBool (decEquiv f g (no np)) = false

Transporting a negative decision with decEquiv stays false.

decReflBool

theorem decReflBool {A : Type} (a : A) : decToBool (decRefl a) = true

The reflexivity decision decRefl a is true.

decAndDecNotYes

theorem decAndDecNotYes {P : Type} (p : P) : decToBool (decAnd (yes p) (decNot (yes p))) = false

A positive decision conjoined with its own negation is false.

decAndDecNotNo

theorem decAndDecNotNo {P : Type} (np : P -> Empty) : decToBool (decAnd (no np) (decNot (no np))) = false

A negative decision conjoined with its own negation is false.

decOrDecNotYes

theorem decOrDecNotYes {P : Type} (p : P) : decToBool (decOr (yes p) (decNot (yes p))) = true

A positive decision disjoined with its own negation is true.

decOrDecNotNo

theorem decOrDecNotNo {P : Type} (np : P -> Empty) : decToBool (decOr (no np) (decNot (no np))) = true

A negative decision disjoined with its own negation is true.

decExcludedMiddle

theorem decExcludedMiddle {P : Type} (d : Dec P) : decToBool (decOr d (decNot d)) = true

Excluded middle for decisions: a decision or its negation is always true.

decAndCommBool

theorem decAndCommBool {P Q : Type} (dp : Dec P) (dq : Dec Q) : decToBool (decAnd dp dq) = decToBool (decAnd dq dp)

Conjunction of decisions is commutative at the boolean level.

decOrCommBool

theorem decOrCommBool {P Q : Type} (dp : Dec P) (dq : Dec Q) : decToBool (decOr dp dq) = decToBool (decOr dq dp)

Disjunction of decisions is commutative at the boolean level.

decContra

def decContra {P : Type} (d : Dec P) : Dec (P -> Empty)

Decides the negation of P (contrapositive form); the same as decNot.

decId

def decId {P : Type} (d : Dec P) : Dec P

The identity on decisions.

decConstYes

def decConstYes {P : Type} (p : P) : Dec P

The constant positive decision built from a witness.

decConstNo

def decConstNo {P : Type} (np : P -> Empty) : Dec P

The constant negative decision built from a refutation.

decAndAssocBool

theorem decAndAssocBool {P Q R : Type} (dp : Dec P) (dq : Dec Q) (dr : Dec R) : decToBool (decAnd (decAnd dp dq) dr) = decToBool (decAnd dp (decAnd dq dr))

Conjunction of decisions is associative at the boolean level.

decOrAssocBool

theorem decOrAssocBool {P Q R : Type} (dp : Dec P) (dq : Dec Q) (dr : Dec R) : decToBool (decOr (decOr dp dq) dr) = decToBool (decOr dp (decOr dq dr))

Disjunction of decisions is associative at the boolean level.

decAndUnitL

theorem decAndUnitL {P : Type} (d : Dec P) : decToBool (decAnd decUnit d) = decToBool d

decUnit is a left unit for decAnd at the boolean level.

decAndUnitR

theorem decAndUnitR {P : Type} (d : Dec P) : decToBool (decAnd d decUnit) = decToBool d

decUnit is a right unit for decAnd at the boolean level.

decOrEmptyL

theorem decOrEmptyL {P : Type} (d : Dec P) : decToBool (decOr decEmpty d) = decToBool d

decEmpty is a left unit for decOr at the boolean level.

decOrEmptyR

theorem decOrEmptyR {P : Type} (d : Dec P) : decToBool (decOr d decEmpty) = decToBool d

decEmpty is a right unit for decOr at the boolean level.

decAndEmptyL

theorem decAndEmptyL {P : Type} (d : Dec P) : decToBool (decAnd decEmpty d) = false

decEmpty annihilates decAnd on the left: the result is false.

decOrUnitL

theorem decOrUnitL {P : Type} (d : Dec P) : decToBool (decOr decUnit d) = true

decUnit annihilates decOr on the left: the result is true.

decDeMorganAndBool

theorem decDeMorganAndBool {P Q : Type} (dp : Dec P) (dq : Dec Q) : decToBool (decNot (decAnd dp dq)) = or (decToBool (decNot dp)) (decToBool (decNot dq))

De Morgan at the boolean level: the negation of a conjunction is the disjunction of the negations.

decDeMorganOrBool

theorem decDeMorganOrBool {P Q : Type} (dp : Dec P) (dq : Dec Q) : decToBool (decNot (decOr dp dq)) = and (decToBool (decNot dp)) (decToBool (decNot dq))

De Morgan at the boolean level: the negation of a disjunction is the conjunction of the negations.

decIdBool

theorem decIdBool {P : Type} (d : Dec P) : decToBool (decId d) = decToBool d

decId leaves the boolean value of a decision unchanged.

decContraBool

theorem decContraBool {P : Type} (d : Dec P) : decToBool (decContra d) = decToBool (decNot d)

decContra has the same boolean value as decNot.

decConstYesBool

theorem decConstYesBool {P : Type} (p : P) : decToBool (decConstYes p) = true

decConstYes is always true.

decConstNoBool

theorem decConstNoBool {P : Type} (np : P -> Empty) : decToBool (decConstNo np) = false

decConstNo is always false.

decAndOrDistribBool

theorem decAndOrDistribBool {P Q R : Type} (dp : Dec P) (dq : Dec Q) (dr : Dec R) : decToBool (decAnd dp (decOr dq dr)) = or (decToBool (decAnd dp dq)) (decToBool (decAnd dp dr))

Conjunction distributes over disjunction of decisions at the boolean level.

decAndIdempotent

theorem decAndIdempotent {P : Type} (d : Dec P) : decToBool (decAnd d d) = decToBool d

Conjunction of a decision with itself has the same boolean value as the decision.

decOrIdempotent

theorem decOrIdempotent {P : Type} (d : Dec P) : decToBool (decOr d d) = decToBool d

Disjunction of a decision with itself has the same boolean value as the decision.

decAndAbsorb

theorem decAndAbsorb {P Q : Type} (dp : Dec P) (dq : Dec Q) : decToBool (decAnd dp (decOr dp dq)) = decToBool dp

Absorption: dp conjoined with dp or dq has the boolean value of dp.

decOrAbsorb

theorem decOrAbsorb {P Q : Type} (dp : Dec P) (dq : Dec Q) : decToBool (decOr dp (decAnd dp dq)) = decToBool dp

Absorption: dp disjoined with dp and dq has the boolean value of dp.

decAndComplement

theorem decAndComplement {P : Type} (d : Dec P) : decToBool (decAnd d (decNot d)) = false

A decision conjoined with its negation is always false.

decIff

def decIff {P Q : Type} (dp : Dec P) (dq : Dec Q) : Dec ((P -> Q) × (Q -> P))

Decides the biconditional (maps both ways) of two decidable propositions.

decXorBool

def decXorBool {P Q : Type} (dp : Dec P) (dq : Dec Q) : Bool

Boolean exclusive or of two decisions.

decNandBool

def decNandBool {P Q : Type} (dp : Dec P) (dq : Dec Q) : Bool

Boolean not-and of two decisions.

decNorBool

def decNorBool {P Q : Type} (dp : Dec P) (dq : Dec Q) : Bool

Boolean not-or of two decisions.

decIffYesYes

theorem decIffYesYes {P Q : Type} (p : P) (q : Q) : decToBool (decIff (yes p) (yes q)) = true

The biconditional of two positive decisions is true.

decIffNoNo

theorem decIffNoNo {P Q : Type} (np : P -> Empty) (nq : Q -> Empty) : decToBool (decIff (no np) (no nq)) = true

The biconditional of two negative decisions is true.

decIffYesNo

theorem decIffYesNo {P Q : Type} (p : P) (nq : Q -> Empty) : decToBool (decIff (yes p) (no nq)) = false

The biconditional of a positive and a negative decision is false.

decIffNoYes

theorem decIffNoYes {P Q : Type} (np : P -> Empty) (q : Q) : decToBool (decIff (no np) (yes q)) = false

The biconditional of a negative and a positive decision is false.

decIffRefl

theorem decIffRefl {P : Type} (d : Dec P) : decToBool (decIff d d) = true

The biconditional of a decision with itself is true.

decIffSymm

theorem decIffSymm {P Q : Type} (dp : Dec P) (dq : Dec Q) : decToBool (decIff dp dq) = decToBool (decIff dq dp)

The biconditional of decisions is symmetric at the boolean level.

decXorBoolYesYes

theorem decXorBoolYesYes {P Q : Type} (p : P) (q : Q) : decXorBool (yes p) (yes q) = false

Exclusive or of two positive decisions is false.

decXorBoolYesNo

theorem decXorBoolYesNo {P Q : Type} (p : P) (nq : Q -> Empty) : decXorBool (yes p) (no nq) = true

Exclusive or of a positive and a negative decision is true.

decXorBoolNoYes

theorem decXorBoolNoYes {P Q : Type} (np : P -> Empty) (q : Q) : decXorBool (no np) (yes q) = true

Exclusive or of a negative and a positive decision is true.

decXorBoolNoNo

theorem decXorBoolNoNo {P Q : Type} (np : P -> Empty) (nq : Q -> Empty) : decXorBool (no np) (no nq) = false

Exclusive or of two negative decisions is false.

decXorComm

theorem decXorComm {P Q : Type} (dp : Dec P) (dq : Dec Q) : decXorBool dp dq = decXorBool dq dp

Exclusive or of decisions is commutative.

decNandBoolYesYes

theorem decNandBoolYesYes {P Q : Type} (p : P) (q : Q) : decNandBool (yes p) (yes q) = false

Not-and of two positive decisions is false.

decNandBoolYesNo

theorem decNandBoolYesNo {P Q : Type} (p : P) (nq : Q -> Empty) : decNandBool (yes p) (no nq) = true

Not-and of a positive and a negative decision is true.

decNandBoolNoYes

theorem decNandBoolNoYes {P Q : Type} (np : P -> Empty) (q : Q) : decNandBool (no np) (yes q) = true

Not-and of a negative and a positive decision is true.

decNandBoolNoNo

theorem decNandBoolNoNo {P Q : Type} (np : P -> Empty) (nq : Q -> Empty) : decNandBool (no np) (no nq) = true

Not-and of two negative decisions is true.

decNorBoolYesYes

theorem decNorBoolYesYes {P Q : Type} (p : P) (q : Q) : decNorBool (yes p) (yes q) = false

Not-or of two positive decisions is false.

decNorBoolYesNo

theorem decNorBoolYesNo {P Q : Type} (p : P) (nq : Q -> Empty) : decNorBool (yes p) (no nq) = false

Not-or of a positive and a negative decision is false.

decNorBoolNoYes

theorem decNorBoolNoYes {P Q : Type} (np : P -> Empty) (q : Q) : decNorBool (no np) (yes q) = false

Not-or of a negative and a positive decision is false.

decNorBoolNoNo

theorem decNorBoolNoNo {P Q : Type} (np : P -> Empty) (nq : Q -> Empty) : decNorBool (no np) (no nq) = true

Not-or of two negative decisions is true.

decJoin

def decJoin {P : Type} (d : Dec (Dec P)) : Dec P

Flattens a decision about a decision into a decision about P.

decJoinYesYes

theorem decJoinYesYes {P : Type} (p : P) : decJoin (yes (yes p)) = yes p

Joining yes (yes p) gives yes p.

decJoinYesNo

theorem decJoinYesNo {P : Type} (np : P -> Empty) : decJoin (yes (no np)) = no np

Joining yes (no f) gives no f.

decDNE

def decDNE {P : Type} (d : Dec P) (dnn : (P -> Empty) -> Empty) : P

Double negation elimination for a decidable proposition.

decEqProd

def decEqProd {A B : Type} (da : Dec A) (db : Dec B) : Dec (A × B)

Decides a product from decisions for its components; an alias of decAnd.

decEqProdYY

theorem decEqProdYY {A B : Type} (a : A) (b : B) : decToBool (decEqProd (yes a) (yes b)) = true

decEqProd of two positive decisions is true.

decEqProdYN

theorem decEqProdYN {A B : Type} (a : A) (nb : B -> Empty) : decToBool (decEqProd (yes a) (no nb)) = false

decEqProd of a positive and a negative decision is false.

decEqProdNY

theorem decEqProdNY {A B : Type} (na : A -> Empty) (b : B) : decToBool (decEqProd (no na) (yes b)) = false

decEqProd of a negative and a positive decision is false.

decEqProdNN

theorem decEqProdNN {A B : Type} (na : A -> Empty) (nb : B -> Empty) : decToBool (decEqProd (no na) (no nb)) = false

decEqProd of two negative decisions is false.

decEqSum

def decEqSum {A B : Type} (da : Dec A) (db : Dec B) : Dec (Either A B)

Decides a sum (Either) from decisions for its components; an alias of decOr.

decEqSumYY

theorem decEqSumYY {A B : Type} (a : A) (b : B) : decToBool (decEqSum (yes a) (yes b)) = true

decEqSum of two positive decisions is true.

decEqSumYN

theorem decEqSumYN {A B : Type} (a : A) (nb : B -> Empty) : decToBool (decEqSum (yes a) (no nb)) = true

decEqSum of a positive and a negative decision is true.

decEqSumNY

theorem decEqSumNY {A B : Type} (na : A -> Empty) (b : B) : decToBool (decEqSum (no na) (yes b)) = true

decEqSum of a negative and a positive decision is true.

decEqSumNN

theorem decEqSumNN {A B : Type} (na : A -> Empty) (nb : B -> Empty) : decToBool (decEqSum (no na) (no nb)) = false

decEqSum of two negative decisions is false.

decTrue

def decTrue : Dec (true = true)

Decides true = true positively by reflexivity.

decElim

def decElim {P A : Type} (ifYes : P -> A) (ifNo : (P -> Empty) -> A) (d : Dec P) : A

Eliminates a decision into any type by handling the positive and negative cases.

decElimYes

theorem decElimYes {P A : Type} (ifYes : P -> A) (ifNo : (P -> Empty) -> A) (p : P) : decElim ifYes ifNo (yes p) = ifYes p

Eliminating a positive decision runs the yes branch on the witness.

decElimNo

theorem decElimNo {P A : Type} (ifYes : P -> A) (ifNo : (P -> Empty) -> A) (np : P -> Empty) : decElim ifYes ifNo (no np) = ifNo np

Eliminating a negative decision runs the no branch on the refutation.

decOrAndDistribBool

theorem decOrAndDistribBool {P Q R : Type} (dp : Dec P) (dq : Dec Q) (dr : Dec R) : decToBool (decOr dp (decAnd dq dr)) = and (decToBool (decOr dp dq)) (decToBool (decOr dp dr))

Disjunction distributes over conjunction of decisions at the boolean level.

decImplRefl

theorem decImplRefl {P : Type} (d : Dec P) : decToBool (decImpl d d) = true

The implication from a decision to itself is true.

decTripleNot

theorem decTripleNot {P : Type} (d : Dec P) : decToBool (decNot (decNot (decNot d))) = decToBool (decNot d)

Triple negation of a decision has the same boolean value as single negation.

decXorSelf

theorem decXorSelf {P : Type} (d : Dec P) : decXorBool d d = false

Exclusive or of a decision with itself is false.

decNandSelf

theorem decNandSelf {P : Type} (d : Dec P) : decNandBool d d = not (decToBool d)

Not-and of a decision with itself is the boolean negation of the decision.

decNorSelf

theorem decNorSelf {P : Type} (d : Dec P) : decNorBool d d = not (decToBool d)

Not-or of a decision with itself is the boolean negation of the decision.

decWhen

def decWhen {P A : Type} (d : Dec P) (f : P -> A) (default : A) : A

Applies a function to the witness of a positive decision, or returns a default when it is negative.

decWhenYes

theorem decWhenYes {P A : Type} (p : P) (f : P -> A) (default : A) : decWhen (yes p) f default = f p

decWhen on a positive decision applies the function to the witness.

decWhenNo

theorem decWhenNo {P A : Type} (np : P -> Empty) (f : P -> A) (default : A) : decWhen (no np) f default = default

decWhen on a negative decision returns the default.

Decidable

class Decidable (P : Type)

The class of decidable propositions, carrying a decision dec; instances drive the decide tactic.

ofDecideTrue

def ofDecideTrue {P : Type} (d : Dec P) (h : decToBool d = true) : P

Extracts a proof of P from a decision whose boolean value computes to true.

ofDecide

def ofDecide {P : Type} {{d : Decidable P}} (h : decToBool d.dec = true) : P

Proof produced by decide: a proof of P from the instance’s decision computing to true.

decEqBool

instance decEqBool (a : Bool) (b : Bool) : Decidable (a = b)

a = b on booleans is decidable (used by decide).

zeroNeqSuccD

def zeroNeqSuccD (n : Nat) (h : zero = succ n) : Empty

Zero is not the successor of any natural number.

succNeqZeroD

def succNeqZeroD (n : Nat) (h : succ n = zero) : Empty

A successor is never zero.

natDecEq

def natDecEq (m : Nat) (n : Nat) : Dec (m = n)

Decidable equality of natural numbers.

decEqNat

instance decEqNat (m : Nat) (n : Nat) : Decidable (m = n)

m = n on naturals is decidable (used by decide).

decide

def decide (P : Type) {{d : Decidable P}} : Dec P

The decision of P: match decide(a == b) branches with the proof either way.

decPath

def decPath {A : Type} {a : A} {b : A} (d : Dec (a = b)) : Dec (a ≡ b)

A path is decided as its identity is. The identity is decided by d.

decPathBool

instance decPathBool (a : Bool) (b : Bool) : Decidable (a ≡ b)

a == b on booleans is decidable.

decPathNat

instance decPathNat (m : Nat) (n : Nat) : Decidable (m ≡ n)

m == n on naturals is decidable.