The Coq mailing list

[Feró <ferenc.tamasi AT gmail.com>]

If you could prove this,

Goal forall (a1 a2 : A), proj1_sig a1 = proj1_sig a2 -> a1 = a2.

then you could also prove a similar equality on B. See attachment for a proof.

On 8/13/13, Victor Porton 
<porton AT narod.ru>
 wrote:
> [[[
> Definition A := { x:nat | x > 1 }.
>
> Record B := {
>              x: nat;
>              c: x > 1
> }.
> ]]]
>
> A and B are essentially the same thing.
>
> But for proofs of equality of objects of type B proof irrelevance is
> required, while for proofs of equality of objects of type A proof
> irrelevance is not required. Right?
>
> What is the deep reason of proof irrelevance required in one case and not
> required in an other case?
>
> It seems I misunderstand something.
>
> --
> Victor Porton - http://portonvictor.org
>


-- 
Give me liberty or give me cash!
Definition A := { x:nat | x > 1 }.

Record B := {
             x: nat;
             c: x > 1
}.

Definition AtoB (a : A) : B := Build_B (proj1_sig a) (proj2_sig a).
Definition BtoA (b : B) : A := exist _ (x b) (c b).
Goal forall a : A, BtoA (AtoB a) = a. destruct a. unfold AtoB. unfold BtoA. simpl. reflexivity. Qed.
Goal forall b : B, AtoB (BtoA b) = b. destruct b. unfold BtoA. unfold AtoB. simpl. reflexivity. Save isom.

Goal
  forall
    X Y (f : X -> Y) (g : Y -> X)
    (m : forall x : X, g (f x) = x)
    (P : X -> Prop)
    (x1 x2 : X) (fx1eqfx2 : f x1 = f x2),
    P x1 -> P x2.
intros. rewrite <- m. rewrite <- fx1eqfx2. rewrite m. exact H.
Save isopf.

Goal A -> B. intro. destruct H. apply (Build_B x0 g). Qed.
Goal B -> A. intro. destruct H. apply (exist _ x0 c0). Qed.

Goal forall (b1 b2 : B), x b1 = x b2 -> b1 = b2.
intros. destruct b1. destruct b2. simpl in *. (*rewrite H.*) Abort.
Goal forall (a1 a2 : A), proj1_sig a1 = proj1_sig a2 -> a1 = a2.
intros.  destruct a1. destruct a2. simpl in H. (*rewrite H.*) Abort.

Goal
  (forall (a1 a2 : A), proj1_sig a1 = proj1_sig a2 -> a1 = a2) ->
  (forall (b1 b2 : B), x b1 = x b2 -> b1 = b2).
intros.
apply (isopf _ _ _ _ isom (fun b => b1 = b) b1 b2).
- apply (H (BtoA b1) (BtoA b2)).
  destruct b1; destruct b2.
  simpl in *. exact H0.
- reflexivity.
Qed.