Split `Inhabited` between `Prop` and `Type` version
Suggested in #116 (comment 71501), but worth a separate issue.
@robbertkrebbers writes:
Maybe we should have two versions of Inhabited: one in
Prop
and one inType
, and only have the default instance for theProp
-based one?
Since I have misgivings about Inhabited
being in Type
, I would propose:
Class Inhabited (A : Type) : Prop := populate { inhabitant : A }.
Class InhabitedT (A : Type) : Type := populateT { inhabitantT : A }.
#[global] Instance inhabitedT_inhabited {A} : InhabitedT A -> Inhabited A.
Since later_exist
only needs the Prop
version (I confirmed via later_exist_prop
below), most code could remain unchanged.
While this is more invasive than adding InhabitedP
in Prop
, it seems better: InhabitantT
seems only appropriate for types with a canonical sentinel value (say, the empty collection for option A
, list A
etc.); but many types lack such inhabitants, so InhabitedT
might hide bugs in specs; as a compromise, we're currently Qed
ing all our Inhabited
instances.
Minimized from derived_laws_later.v
:
Local Hint Resolve False_elim later_mono : core.
Lemma later_exist {PROP : bi} `(H : exists a : A, True) (Φ : A → PROP) : ▷ (∃ a, Φ a) ⊣⊢ (∃ a, ▷ Φ a).
Proof.
apply: anti_symm; [|apply later_exist_2].
rewrite later_exist_false. apply or_elim; last done.
destruct H as [inhabitant _].
rewrite -(exist_intro inhabitant); auto.
Qed.