The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

As a complement to the library of Adam about UIP inheritance properties,
it also works for inductively defined types such as lists, trees ...

Require Import List.

Section UIP_list.

  Variable X : Type.

  Implicit Type l : list X.

  Hypothesis eqX_uniq : forall (x : X) (e : x = x), e = eq_refl.

  Let list_cons_eq x y l m (e1 : x = y) (e2 : l = m) : x::l = y::m :=
    match e1, e2 with
      eq_refl, eq_refl => eq_refl
    end.

  (* eq_inv_type l m H expresses that the proof H : l = m is
     build exclusively from either eq_refl nil or list_cons_eq *)

  Let eq_inv_prop n : forall m, n = m -> Prop :=
    match n with
      | nil => fun m =>
        match m with
          | nil  => fun H => H = eq_refl
          | _    => fun _ => False
        end
      | a::l => fun m =>
        match m with
          | nil  => fun _ => False
          | b::m => fun H => exists (H1 : a = b)
                                    (H2 : l = m), H = list_cons_eq H1 H2
        end
    end.

  Let eq_inv l m H : @eq_inv_prop l m H.
  Proof.
    subst m.
    destruct l; simpl.
     * trivial.
     * exists (eq_refl _), (eq_refl _); reflexivity.
  Qed.

  Theorem UIP_list l (H : l = l) : H = eq_refl.
  Proof.
    induction l as [ | x l IHl ].
     * exact (eq_inv H).
     * destruct (eq_inv H) as (H3 & H4 & HH).
       rewrite HH, (IHl H4), (eqX_uniq H3); reflexivity.
  Qed.

End UIP_list.




On 08/28/2016 09:44 PM, Adam Chlipala wrote:
> 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.
>