Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import TruncType HProp.Require Import Truncations.Core Modalities.ReflectiveSubuniverse.LocalOpen Scope path_scope.(** ** Definitions *)(** A decidable proposition is, morally speaking, an HProp that is decidable. However, we only require that it be an HProp under the additional assumption of [Funext]; this enables decidable propositions to usually be used without [Funext] hypotheses. *)RecordDProp := {
dprop_type : Type ;
ishprop_dprop : Funext -> IsHProp dprop_type ;
dec_dprop : Decidable dprop_type
}.(** A fancier definition, which would have the property that negation is judgmentally involutive, would be<<Record DProp := { dprop_holds : Type ; ishprop_holds : Funext -> IsHProp dprop_holds ; dprop_denies : Type ; ishprop_denies : Funext -> IsHProp dprop_denies ; holds_or_denies : dprop_holds + dprop_denies ; denies_or_holds : dprop_denies + dprop_holds ; not_holds_and_denies : dprop_holds -> dprop_denies -> Empty }.>>At some point we may want to go that route, but it would be more work. In particualar, [Instance]s of [Decidable] wouldn't be automatically computed for us, and the characterization of the homotopy type of [DProp] itself would be a lot harder. *)Coerciondprop_type : DProp >-> Sortclass.Global Existing Instanceishprop_dprop.Global Existing Instancedec_dprop.(** Sometimes, however, we have decidable props that are hprops without funext, and we want to remember that. *)RecordDHProp :=
{ dhprop_hprop : HProp ;
dec_dhprop : Decidable dhprop_hprop
}.Coerciondhprop_hprop : DHProp >-> HProp.Global Existing Instancedec_dhprop.Definitiondhprop_to_dprop : DHProp -> DProp
:= funP => Build_DProp P (fun_ => _) _.Coerciondhprop_to_dprop : DHProp >-> DProp.(** In particular, [True] and [False] are always hprops. *)DefinitionTrue : DHProp
:= Build_DHProp Unit_hp (inl tt).DefinitionFalse : DHProp
:= Build_DHProp False_hp (inr idmap).(** Decidable props can be coerced to [Bool]. *)Definitiondprop_to_bool (P : DProp) : Bool
:= if dec P then true else false.Coerciondprop_to_bool : DProp >-> Bool.(** And back again, but we don't declare that as a coercion. *)Definitionbool_to_dhprop (b : Bool) : DHProp
:= if b thenTrueelseFalse.(** ** The type of decidable props *)
{X : Type & {_ : Funext -> IsHProp X & Decidable X}} <~>
DProp
{X : Type & {_ : Funext -> IsHProp X & Decidable X}} <~>
DProp
issig.Defined.
H: Funext P, Q: DProp
P = Q <~> P = Q
H: Funext P, Q: DProp
P = Q <~> P = Q
H: Funext P: Type hP: Funext -> IsHProp P dP: Decidable P Q: DProp
apply if_not_hprop_then_equiv_Empty; [ exact _ | assumption ].Defined.Definitionequiv_dprop_to_bool `{Univalence}
: DProp <~> Bool
:= Build_Equiv _ _ dprop_to_bool _.(** ** Operations *)(** We define the logical operations on decidable hprops to be the operations on ordinary hprops, with decidability carrying over. For the operations which preserve hprops without funext, we define separate versions that act on [DHProp]. *)Definitiondand (b1b2 : DProp) : DProp
:= Build_DProp (b1 * b2) _ _.Definitiondhand (b1b2 : DHProp) : DHProp
:= Build_DHProp (Build_HProp (b1 * b2)) _.Definitiondor (b1b2 : DProp) : DProp
:= Build_DProp (hor b1 b2) _ _.Definitiondhor (b1b2 : DHProp) : DHProp
:= Build_DHProp (Build_HProp (hor b1 b2)) _.Definitiondneg (b : DProp) : DProp
:= Build_DProp (~b) _ _.Definitiondimpl (b1b2 : DProp) : DProp
:= Build_DProp (b1 -> b2) _ _.Declare Scope dprop_scope.Delimit Scope dprop_scope with dprop.Bind Scope dprop_scope with DProp.Declare Scope dhprop_scope.Delimit Scope dhprop_scope with dhprop.Bind Scope dhprop_scope with DHProp.Infix"&&" := dand : dprop_scope.Infix"&&" := dhand : dhprop_scope.Infix"||" := dor : dprop_scope.Infix"||" := dhor : dhprop_scope.Infix"->" := dimpl : dprop_scope.Notation"!! P" := (dneg P) : dprop_scope.LocalOpen Scope dprop_scope.(** ** Computation *)(** In order to be able to "compute" with [DProp]s like booleans, we define a couple of typeclasses. *)ClassIsTrue (P : DProp) :=
dprop_istrue : P.ClassIsFalse (P : DProp) :=
dprop_isfalse : ~ P.(** Note that we are not using [Typeclasses Strict Resolution] for [IsTrue] and [IsFalse]; this enables us to write simply [dprop_istrue] as a proof of some true dprop, and Coq will infer from context what the dprop is that we're proving. *)Global Instancetrue_istrue : IsTrue True := tt.Global Instancefalse_isfalse : IsFalse False := idmap.
P, Q: DProp H: IsTrue P H0: IsTrue Q
IsTrue (P && Q)
P, Q: DProp H: IsTrue P H0: IsTrue Q
IsTrue (P && Q)
exact (dprop_istrue, dprop_istrue).Defined.
P, Q: DProp H: IsFalse P
IsFalse (P && Q)
P, Q: DProp H: IsFalse P
IsFalse (P && Q)
P, Q: DProp H: IsFalse P p: P q: Q
Empty
exact (dprop_isfalse p).Defined.
P, Q: DProp H: IsFalse Q
IsFalse (P && Q)
P, Q: DProp H: IsFalse Q
IsFalse (P && Q)
P, Q: DProp H: IsFalse Q p: P q: Q
Empty
exact (dprop_isfalse q).Defined.
P, Q: DHProp H: IsTrue P H0: IsTrue Q
IsTrue (P && Q)%dhprop
P, Q: DHProp H: IsTrue P H0: IsTrue Q
IsTrue (P && Q)%dhprop
(** We have to give [P] as an explicit argument here. This is apparently because with two [IsTrue] instances in the context, when we write simply [dprop_istrue], Coq guesses one of them during typeclass resolution, and isn't willing to backtrack once it realizes that that choice fails to be what's needed to solve the goal. Coq currently seems to consistently guess [Q] rather than [P], so that we don't have to give the argument [Q] to the second call to [dprop_istrue]; but rather than depend on such behavior, we give both arguments explicitly. (The problem doesn't arise with [dand_true_true] because in that case, unification, which fires before typeclass search, is able to guess that the argument must be [P].) *)exact (@dprop_istrue P _, @dprop_istrue Q _).Defined.