diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-05-05 15:40:04 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-05 15:40:04 +0200 |
commit | 6ae72542dd5ec63775e75a3459c5064292b64e32 (patch) | |
tree | a0ac2732e9f7cd1cbfc5ed6c8d35ecdf537d9693 /theories/Init | |
parent | 5548e5f6bc5446f7541cfc7d93b0b47e4b751e86 (diff) | |
parent | 8adfa0e5290056b7683a3a8b778ca16182a1eb3d (diff) |
Merge PR#593: Functional choice <-> [inhabited] and [forall] commute
Diffstat (limited to 'theories/Init')
-rw-r--r-- | theories/Init/Logic.v | 5 | ||||
-rw-r--r-- | theories/Init/Specif.v | 11 |
2 files changed, 16 insertions, 0 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 9ae9dde28..3eefe9a84 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -609,6 +609,11 @@ Proof. destruct 1; auto. Qed. +Lemma inhabited_covariant (A B : Type) : (A -> B) -> inhabited A -> inhabited B. +Proof. + intros f [x];exact (inhabits (f x)). +Qed. + (** Declaration of stepl and stepr for eq and iff *) Lemma eq_stepl : forall (A : Type) (x y z : A), x = y -> x = z -> z = y. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 2cc2ecbc2..43a441fc5 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -207,6 +207,17 @@ Definition sig2_eta {A P Q} (p : { a : A | P a & Q a }) : p = exist2 _ _ (proj1_sig (sig_of_sig2 p)) (proj2_sig (sig_of_sig2 p)) (proj3_sig p). Proof. destruct p; reflexivity. Defined. +(** [exists x : A, B] is equivalent to [inhabited {x : A | B}] *) +Lemma exists_to_inhabited_sig {A P} : (exists x : A, P x) -> inhabited {x : A | P x}. +Proof. + intros [x y]. exact (inhabits (exist _ x y)). +Qed. + +Lemma inhabited_sig_to_exists {A P} : inhabited {x : A | P x} -> exists x : A, P x. +Proof. + intros [[x y]];exists x;exact y. +Qed. + (** [sumbool] is a boolean type equipped with the justification of their value *) |