The Coq mailing list

[Michael Shulman <viritrilbia AT gmail.com>]

Hi,

Apparently the use of the UIP axiom can sometimes be avoided by a
dependent elimination, as long as enough definitions are transparent.
Are there reasons to prefer UIP in such situations?


The context of my question is section 9.3 of CPDT, in which the
associativity of concatenation of heterogeneous lists is proven, using
elimination on associativity of concatenation for ordinary lists to make
the theorem statement type-check.

  Theorem fhapp_ass : forall ls1 ls2 ls3
    (pf : (ls1 ++ ls2) ++ ls3 = ls1 ++ (ls2 ++ ls3))
    (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
    fhapp hls1 (fhapp hls2 hls3)
    = match pf in (_ = ls) return fhlist _ ls with
        | refl_equal => fhapp (fhapp hls1 hls2) hls3
      end.

The proof is fairly tricky (to my inexperienced eyes, anyway) and
requires UIP (i.e. the Eqdep library).  However, if instead of allowing
any proof of (ls1 ++ ls2) ++ ls3 = ls1 ++ (ls2 ++ ls3), we use a
transparent redefinition of app_ass, then we can prove the theorem with
a dependent elimination:

  Definition app_ass_transparent (A:Type)(l m n:list A) : ((l ++ m) ++
n) = (l ++ (m ++ n)).
    intros; induction l; simpl in |- *; auto; rewrite <- IHl; auto.
  Defined.

  Theorem fhapp_ass' : forall ls1 ls2 ls3
    (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
    fhapp hls1 (fhapp hls2 hls3)
    = match (app_ass_transparent ls1 ls2 ls3) in (_ = ls) return fhlist
_ ls with
        | refl_equal => fhapp (fhapp hls1 hls2) hls3
      end.
    induction ls1; crush; generalize (app_ass ls1 ls2 ls3); intro e;
case e; crush.
  Qed.

The second approach is easier for me to understand, and doesn't require
assuming an additional axiom.  Given this, are there reasons to prefer
the first?

A secondary question is, given that having transparent theorems is
useful in situations such as this, what is the advantage of making them
opaque by default?

Thanks!
Mike