Library hlemmas
Require Import prelude.
Require Import FunctionalExtensionality.
Require Import Arith.
Scheme J := Induction for eq Sort Type.
Lemma hedberg : forall T, (forall x y : T, decidable (x = y)) -> hset T.
intros ? ?.
pose (fun (x y : T) (e : x = y) => match X x y with inl e' => e' | inr p => match (p e) with end end).
assert (forall x y p q, e x y p = e x y q).
{
intros; subst e; simpl; destruct (X x y);[reflexivity|].
destruct (f p).
}
pose (s := @eq_sym T).
pose (t := @eq_trans T).
intros x y.
assert (forall p : x = y, p = t _ _ _ (s _ _ (e _ _ eq_refl)) (e _ _ p)).
{
intro p; subst t s; unfold eq_sym, eq_trans.
destruct p.
subst e; simpl.
destruct (X x x).
- destruct e; reflexivity.
- destruct (f eq_refl).
}
intros p q.
rewrite (H0 p), (H0 q), (H _ _ p q); reflexivity.
Defined.
Lemma nat_hset : hset nat.
apply hedberg; intros x y; assert ({ x = y } + { x <> y}) by decide equality.
unfold decidable; destruct H; eauto.
Qed.
Lemma bool_hset : hset bool.
apply hedberg; intros x y; assert ({ x = y } + { x <> y}) by decide equality.
unfold decidable; destruct H; eauto.
Qed.
Lemma hprop_implies_hset : forall A : Type, hprop A -> hset A.
intros.
assert (forall x y p, p = eq_trans (eq_sym (H x x)) (H x y)) as C by
(intros x ? p; induction p using J; induction (H x x) using J; reflexivity).
intros ? ? ? ?; etransitivity; [| symmetry]; eapply C.
Qed.
Lemma neg_hprop : forall A : Type, hprop (¬ A).
intros ? ? ?.
extensionality x.
destruct (a x).
Qed.
Definition topluseqleft {A : Type} {B : Type} {x y : A} : x = y -> @inl A B x = inl y :=
fun e => match e with
eq_refl => eq_refl
end.
Definition frompluseqleft {A : Type} {B : Type} {x y : A} : @inl A B x = inl y -> x = y.
intros e; inversion e; auto.
Defined.
Definition topluseqright {A : Type} {B : Type} {x y : B} : x = y -> @inr A B x = inr y :=
fun e => match e with
eq_refl => eq_refl
end.
Definition frompluseqright {A : Type} {B : Type} {x y : B} : @inr A B x = inr y -> x = y.
intros e; inversion e; auto.
Defined.
Lemma tofrompluseqleft {A B : Type} {x y : A} : forall p : @inl A B x = inl y, p = topluseqleft (frompluseqleft p).
exact (fun p => J (A + B)%type (inl x) (fun y => match y with
inl y => fun p => p = topluseqleft (frompluseqleft p)
| inr y => fun p => False end) (eq_refl) (inl y) p).
Qed.
Lemma tofrompluseqright {A B : Type} {x y : B} : forall p : @inr A B x = inr y, p = topluseqright (frompluseqright p).
exact (fun p => J (A + B)%type (inr x) (fun y => match y with
inr y => fun p => p = topluseqright (frompluseqright p)
| inl y => fun p => False end) (eq_refl) (inr y) p).
Qed.
Lemma plus_hset : forall (A B : Type), hset A -> hset B -> hset (A + B)%type.
intros ? ? ? ? x y ?.
destruct x, y; try congruence; intro.
+ assert (frompluseqleft a = frompluseqleft b) by apply H.
rewrite tofrompluseqleft.
rewrite <-H1; apply tofrompluseqleft.
+ rewrite tofrompluseqright.
assert (frompluseqright b1 = frompluseqright a) by apply H0.
rewrite H1; apply tofrompluseqright.
Qed.
Lemma forall_hprop : forall (A : Type) (B : A -> Type), (forall x, hprop (B x)) -> hprop (forall x, B x).
intros.
intros ? ?.
extensionality z.
apply H.
Qed.
Lemma forall_hset : forall (A : Type) (B : A -> Type), (forall x, hset (B x)) -> hset (forall x, B x).
Admitted.
Definition τ {A : Type} (P : A -> Type) {x : A} (t : P x) {y : A} (p : x = y) : P y :=
J A x (fun z _ => P z) t y p.
Lemma Sigma_eq : forall (A : Type) (B : A -> Type), forall x y : Σ z : A, B z, forall p : π₁ x = π₁ y, τ _ (π₂ x) p = π₂ y -> x = y.
intros ? ? [? ?] [? ?] p q.
simpl in *.
revert b0 q.
destruct p; intros ? []; reflexivity.
Defined.
Lemma Sigma_eq_uncurried : forall (A : Type) (B : A -> Type), forall x y : Σ z : A, B z, (Σ p : π₁ x = π₁ y, τ _ (π₂ x) p = π₂ y) -> x = y.
intros.
destruct H; eapply Sigma_eq; eassumption.
Defined.
Definition Sigma_eq_inv1 : forall (A : Type) (B : A -> Type), forall x y : Σ z : A, B z, x = y -> π₁ x = π₁ y := fun _ _ x y p => f_equal (fun x => π₁ x) p.
Definition Sigma_eq_inv2 : forall (A : Type) (B : A -> Type), forall x y (p : x = y), τ _ (π₂ x) (Sigma_eq_inv1 _ B _ _ p) = π₂ y.
intros; destruct p; reflexivity.
Defined.
Lemma Sigma_eq_uncurried_inv : forall (A : Type) (B : A -> Type), forall x y : Σ z : A, B z, x = y -> (Σ p : π₁ x = π₁ y, τ _ (π₂ x) p = π₂ y).
intros. exists (Sigma_eq_inv1 _ _ _ _ H).
apply Sigma_eq_inv2.
Defined.
Lemma Sigma_eq_equiv : forall (A : Type) (B : A -> Type), forall x y : Σ z : A, B z, forall p : x = y, Sigma_eq_uncurried _ _ _ _ (Sigma_eq_uncurried_inv _ _ _ _ p) = p.
intros; destruct p, x; reflexivity.
Qed.
Lemma range_hprop : forall {A B : Type} (b : B) (f : A -> B), hset B -> injective f -> hprop (range f b).
intros.
intros [? ?] [? ?].
unshelve eapply Sigma_eq.
- simpl; apply H0; congruence.
- apply H.
Qed.
Lemma Sigma_hprop : forall {A : Type} (B : A -> Type), (forall a a', B a -> B a' -> a = a') -> (forall a, hprop (B a)) -> hprop (Σ a, B a).
intros.
intros [? ?] [? ?].
unshelve eapply Sigma_eq.
- apply H; assumption.
- apply H0.
Qed.
Lemma Sigma_hset : forall {A : Type} (B : A -> Type), hset A -> (forall a, hset (B a)) -> hset (Σ a, B a).
intros.
intros ? ? ? ?.
rewrite <-(Sigma_eq_equiv _ _ _ _ a0); rewrite <-(Sigma_eq_equiv _ _ _ _ b0).
apply (f_equal (Sigma_eq_uncurried _ _ _ _)).
unfold Sigma_eq_uncurried_inv; simpl.
apply Sigma_eq_uncurried; simpl.
unshelve eexists.
- apply H.
- apply H0.
Qed.
Lemma prod_hprop : forall A B : Type, hprop A -> hprop B -> hprop (A × B).
intros ? ? ? ? [? ?] [? ?].
erewrite (H a), (H0 b); reflexivity.
Qed.
Lemma plus_hprop : forall A B : Type, (A -> ¬ B) -> (B -> ¬ A) -> hprop A -> hprop B -> hprop (A + B).
intros; intros [?|?] [?|?]; try (exfalso; auto; fail).
+ specialize (H1 a0 a). rewrite H1. reflexivity.
+ specialize (H2 b0 b). rewrite H2. reflexivity.
Qed.
Lemma hpropEM_hprop : forall A : Type, hprop A -> hprop (A + ¬ A).
intros; apply plus_hprop; auto.
apply neg_hprop.
Qed.
Require Import FunctionalExtensionality.
Require Import Arith.
Scheme J := Induction for eq Sort Type.
Lemma hedberg : forall T, (forall x y : T, decidable (x = y)) -> hset T.
intros ? ?.
pose (fun (x y : T) (e : x = y) => match X x y with inl e' => e' | inr p => match (p e) with end end).
assert (forall x y p q, e x y p = e x y q).
{
intros; subst e; simpl; destruct (X x y);[reflexivity|].
destruct (f p).
}
pose (s := @eq_sym T).
pose (t := @eq_trans T).
intros x y.
assert (forall p : x = y, p = t _ _ _ (s _ _ (e _ _ eq_refl)) (e _ _ p)).
{
intro p; subst t s; unfold eq_sym, eq_trans.
destruct p.
subst e; simpl.
destruct (X x x).
- destruct e; reflexivity.
- destruct (f eq_refl).
}
intros p q.
rewrite (H0 p), (H0 q), (H _ _ p q); reflexivity.
Defined.
Lemma nat_hset : hset nat.
apply hedberg; intros x y; assert ({ x = y } + { x <> y}) by decide equality.
unfold decidable; destruct H; eauto.
Qed.
Lemma bool_hset : hset bool.
apply hedberg; intros x y; assert ({ x = y } + { x <> y}) by decide equality.
unfold decidable; destruct H; eauto.
Qed.
Lemma hprop_implies_hset : forall A : Type, hprop A -> hset A.
intros.
assert (forall x y p, p = eq_trans (eq_sym (H x x)) (H x y)) as C by
(intros x ? p; induction p using J; induction (H x x) using J; reflexivity).
intros ? ? ? ?; etransitivity; [| symmetry]; eapply C.
Qed.
Lemma neg_hprop : forall A : Type, hprop (¬ A).
intros ? ? ?.
extensionality x.
destruct (a x).
Qed.
Definition topluseqleft {A : Type} {B : Type} {x y : A} : x = y -> @inl A B x = inl y :=
fun e => match e with
eq_refl => eq_refl
end.
Definition frompluseqleft {A : Type} {B : Type} {x y : A} : @inl A B x = inl y -> x = y.
intros e; inversion e; auto.
Defined.
Definition topluseqright {A : Type} {B : Type} {x y : B} : x = y -> @inr A B x = inr y :=
fun e => match e with
eq_refl => eq_refl
end.
Definition frompluseqright {A : Type} {B : Type} {x y : B} : @inr A B x = inr y -> x = y.
intros e; inversion e; auto.
Defined.
Lemma tofrompluseqleft {A B : Type} {x y : A} : forall p : @inl A B x = inl y, p = topluseqleft (frompluseqleft p).
exact (fun p => J (A + B)%type (inl x) (fun y => match y with
inl y => fun p => p = topluseqleft (frompluseqleft p)
| inr y => fun p => False end) (eq_refl) (inl y) p).
Qed.
Lemma tofrompluseqright {A B : Type} {x y : B} : forall p : @inr A B x = inr y, p = topluseqright (frompluseqright p).
exact (fun p => J (A + B)%type (inr x) (fun y => match y with
inr y => fun p => p = topluseqright (frompluseqright p)
| inl y => fun p => False end) (eq_refl) (inr y) p).
Qed.
Lemma plus_hset : forall (A B : Type), hset A -> hset B -> hset (A + B)%type.
intros ? ? ? ? x y ?.
destruct x, y; try congruence; intro.
+ assert (frompluseqleft a = frompluseqleft b) by apply H.
rewrite tofrompluseqleft.
rewrite <-H1; apply tofrompluseqleft.
+ rewrite tofrompluseqright.
assert (frompluseqright b1 = frompluseqright a) by apply H0.
rewrite H1; apply tofrompluseqright.
Qed.
Lemma forall_hprop : forall (A : Type) (B : A -> Type), (forall x, hprop (B x)) -> hprop (forall x, B x).
intros.
intros ? ?.
extensionality z.
apply H.
Qed.
Lemma forall_hset : forall (A : Type) (B : A -> Type), (forall x, hset (B x)) -> hset (forall x, B x).
Admitted.
Definition τ {A : Type} (P : A -> Type) {x : A} (t : P x) {y : A} (p : x = y) : P y :=
J A x (fun z _ => P z) t y p.
Lemma Sigma_eq : forall (A : Type) (B : A -> Type), forall x y : Σ z : A, B z, forall p : π₁ x = π₁ y, τ _ (π₂ x) p = π₂ y -> x = y.
intros ? ? [? ?] [? ?] p q.
simpl in *.
revert b0 q.
destruct p; intros ? []; reflexivity.
Defined.
Lemma Sigma_eq_uncurried : forall (A : Type) (B : A -> Type), forall x y : Σ z : A, B z, (Σ p : π₁ x = π₁ y, τ _ (π₂ x) p = π₂ y) -> x = y.
intros.
destruct H; eapply Sigma_eq; eassumption.
Defined.
Definition Sigma_eq_inv1 : forall (A : Type) (B : A -> Type), forall x y : Σ z : A, B z, x = y -> π₁ x = π₁ y := fun _ _ x y p => f_equal (fun x => π₁ x) p.
Definition Sigma_eq_inv2 : forall (A : Type) (B : A -> Type), forall x y (p : x = y), τ _ (π₂ x) (Sigma_eq_inv1 _ B _ _ p) = π₂ y.
intros; destruct p; reflexivity.
Defined.
Lemma Sigma_eq_uncurried_inv : forall (A : Type) (B : A -> Type), forall x y : Σ z : A, B z, x = y -> (Σ p : π₁ x = π₁ y, τ _ (π₂ x) p = π₂ y).
intros. exists (Sigma_eq_inv1 _ _ _ _ H).
apply Sigma_eq_inv2.
Defined.
Lemma Sigma_eq_equiv : forall (A : Type) (B : A -> Type), forall x y : Σ z : A, B z, forall p : x = y, Sigma_eq_uncurried _ _ _ _ (Sigma_eq_uncurried_inv _ _ _ _ p) = p.
intros; destruct p, x; reflexivity.
Qed.
Lemma range_hprop : forall {A B : Type} (b : B) (f : A -> B), hset B -> injective f -> hprop (range f b).
intros.
intros [? ?] [? ?].
unshelve eapply Sigma_eq.
- simpl; apply H0; congruence.
- apply H.
Qed.
Lemma Sigma_hprop : forall {A : Type} (B : A -> Type), (forall a a', B a -> B a' -> a = a') -> (forall a, hprop (B a)) -> hprop (Σ a, B a).
intros.
intros [? ?] [? ?].
unshelve eapply Sigma_eq.
- apply H; assumption.
- apply H0.
Qed.
Lemma Sigma_hset : forall {A : Type} (B : A -> Type), hset A -> (forall a, hset (B a)) -> hset (Σ a, B a).
intros.
intros ? ? ? ?.
rewrite <-(Sigma_eq_equiv _ _ _ _ a0); rewrite <-(Sigma_eq_equiv _ _ _ _ b0).
apply (f_equal (Sigma_eq_uncurried _ _ _ _)).
unfold Sigma_eq_uncurried_inv; simpl.
apply Sigma_eq_uncurried; simpl.
unshelve eexists.
- apply H.
- apply H0.
Qed.
Lemma prod_hprop : forall A B : Type, hprop A -> hprop B -> hprop (A × B).
intros ? ? ? ? [? ?] [? ?].
erewrite (H a), (H0 b); reflexivity.
Qed.
Lemma plus_hprop : forall A B : Type, (A -> ¬ B) -> (B -> ¬ A) -> hprop A -> hprop B -> hprop (A + B).
intros; intros [?|?] [?|?]; try (exfalso; auto; fail).
+ specialize (H1 a0 a). rewrite H1. reflexivity.
+ specialize (H2 b0 b). rewrite H2. reflexivity.
Qed.
Lemma hpropEM_hprop : forall A : Type, hprop A -> hprop (A + ¬ A).
intros; apply plus_hprop; auto.
apply neg_hprop.
Qed.