The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

I think proving this kind of goal is simpler via first building a 
library of theorems for porting UIP between types, like so:


Set Implicit Arguments.

(** * Step 1: UIP ports across type isomorphism. *)

Section UIP_iso.
  Variables A B : Type.
  Variable AtoB : A -> B.
  Variable BtoA : B -> A.

  Hypothesis AtoB_BtoA : forall a, AtoB (BtoA a) = a.
  Hypothesis A_UIP_refl : forall (a : A) (e : a = a), e = eq_refl.

  Lemma f_equal_cancel : forall (x y : B) (e : x = y),
      e = match AtoB_BtoA x in _ = X return X = _ with
          | eq_refl =>
            match AtoB_BtoA y in _ = Y return _ = Y with
            | eq_refl => f_equal AtoB (f_equal BtoA e)
            end
          end.
  Proof.
    intros.
    subst.
    simpl.
    generalize (AtoB_BtoA y).
    destruct e.
    reflexivity.
  Qed.

  Theorem UIP_iso : forall (b : B) (e : b = b), e = eq_refl.
  Proof.
    intros.
    rewrite (f_equal_cancel e).
    rewrite (A_UIP_refl (f_equal BtoA e)).
    simpl.
    generalize (AtoB_BtoA b).
    generalize (AtoB (BtoA b)).
    intros.
    subst.
    reflexivity.
  Qed.
End UIP_iso.

Section example.
  Variable A : Type.
  Hypothesis A_UIP_refl : forall (a : A)(e : a=a), e=eq_refl.

  Record Foo := foo { foo_a : A }.

  Lemma Foo_UIP_refl : forall (f : Foo)(e: f=f), e=eq_refl.
  Proof.
    apply UIP_iso with (AtoB := foo) (BtoA := foo_a); auto.
    destruct a; auto.
  Qed.
End example.

(** * Step 2: UIP is preserved by pairing. *)

Section UIP_pair.
  Variables A B : Type.

  Hypothesis A_UIP_refl : forall (a : A) (e : a = a), e = eq_refl.
  Hypothesis B_UIP_refl : forall (b : B) (e : b = b), e = eq_refl.

  Lemma pair_eta : forall p : A * B,
      (fst p, snd p) = p.
  Proof.
    destruct p; reflexivity.
  Defined.

  Lemma pair_cong : forall (a1 a2 : A) (b1 b2 : B),
      a1 = a2
      -> b1 = b2
      -> (a1, b1) = (a2, b2).
  Proof.
    intros.
    subst.
    reflexivity.
  Defined.

  Lemma f_equal_cancel' : forall (x y : A * B) (e : x = y),
      e = match pair_eta x in _ = X return X = _ with
          | eq_refl =>
            match pair_eta y in _ = Y return _ = Y with
            | eq_refl => pair_cong (f_equal (@fst _ _) e) (f_equal 
(@snd _ _) e)
            end
          end.
  Proof.
    intros.
    subst.
    generalize (pair_eta y).
    destruct e.
    reflexivity.
  Qed.

  Theorem UIP_pair : forall (a_b : A * B) (e : a_b = a_b), e = eq_refl.
  Proof.
    intros.
    destruct a_b.
    rewrite (f_equal_cancel' e).
    rewrite (A_UIP_refl (f_equal (@fst _ _) e)).
    rewrite (B_UIP_refl (f_equal (@snd _ _) e)).
    reflexivity.
  Qed.
End UIP_pair.

Section example2.
  Variables A B : Type.
  Hypothesis A_UIP_refl : forall (a : A)(e : a=a), e=eq_refl.
  Hypothesis B_UIP_refl : forall (b : B)(e : b=b), e=eq_refl.

  Record Bar := bar { bar_a : A; bar_b : B }.

  Lemma Bar_UIP_refl : forall (f : Bar)(e: f=f), e=eq_refl.
  Proof.
    apply UIP_iso with (AtoB := fun x => bar (fst x) (snd x))
                       (BtoA := fun x => (bar_a x, bar_b x)).
    destruct a; auto.
    apply UIP_pair; auto.
  Qed.
End example2.