The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

This is an erratum to a rather old mail from 2009. Thanks to Jonas
Oberhauser for pointing out the mistake and sorry for the confusion it
induced.

On 11 August 2009, Taral asked if the following was provable:

  Inductive B: bool -> Set := ff: B false | tt: B true. 
  Goal forall (x : bool) (b : B x), b = (if x as x0 return (B x0) then tt 
else ff).

I said it is equivalent to Uniqueness of Reflexive Identity Proofs
(UIP_refl). This would have been correct if I had added "on bool".

Taral's goal is not at all equivalent to the general form of UIP_refl
(nor to JMeq_eq) on an arbitrary domain. Indeed, on bool, UIP_refl is
provable (see Hedberg's proof of UIP_refl on types whose equality is
decidable, in Coq.Logic.Eqdep_dec).

Taral's goal is simply provable by "destruct b; reflexivity.".

This simple proof shows incidentally how UIP_refl can be concisely
proved on finite enumerated domains such as bool (a kind of short
proof that I remember was actually known at least by Sylvain Lebresne
in 2005, private communication):

Lemma UIP_refl_bool (b:bool) (x : b = b) : x = eq_refl.
destruct b.
- change (match true as b return true=b -> Prop with
          | true => fun x => x = eq_refl
          | _ => fun _ => True
          end x).
  destruct x; simpl; trivial.
- change (match false as b return false=b -> Prop with
          | false => fun x => x = eq_refl
          | _ => fun _ => True
          end x).
  destruct x; simpl; trivial.
Defined.

Amazingly, the same pattern applies to get UIP_refl on nat, replacing
case analysis by induction:

Lemma UIP_refl_nat (n:nat) (x : n = n) : x = eq_refl.
Proof.
induction n.
- change (match 0 as n return 0 = n -> Prop with
          | 0 => fun x => x = eq_refl
          | _ => fun _ => True
          end x).
  destruct x; reflexivity.
- specialize IHn with (f_equal pred x).
  change eq_refl with
         (match (@eq_refl _ n) in _ = n' return S n = S n' with
          | eq_refl => eq_refl
          end).
  rewrite <- IHn; clear IHn.
  change (match S n as n' return S n = n' -> Prop with
          | 0 => fun _ => True
          | S n' => fun x => x = match f_equal pred x in _ = n' return S n = 
S n' with
                               | eq_refl => eq_refl
                               end
        end x).
  pattern (S n) at 2 3, x.
  destruct x; reflexivity.
Defined.

Hugo Herbelin

On Wed, Aug 12, 2009 at 12:10:54AM +0200, Hugo Herbelin wrote:
> Hi,
> 
> Damien Pous' goal was not provable ("B true" and "B false" are
> distinct types of same cardinality and they can be interpreted by the
> same set in a model).
> 
> This one is a variant of Hofmann-Streicher's Uniqueness of Reflexive
> Identity Proofs (UIP_refl) and it is probably equivalent to it. It
> requires one of the (weak) axioms equivalent to UIP_refl, e.g. JMeq_eq
> from file JMeq.v or eq_rect_eq in Eqdep.v.
> 
> Require Import JMeq.
> Inductive B: bool -> Set := ff: B false | tt: B true. 
> Goal forall (x : bool) (b : B x), b = (if x as x0 return (B x0) then tt 
> else ff).
> intros x b.
> apply JMeq_eq.
> assert (H:x=x) by reflexivity.
> destruct x in H at 1 |- * at 2 3; 
>   destruct b; discriminate || reflexivity.
> Qed.
> 
> The third line may need some Set Printing All (or some Maj-Alt-A or
> whatever binding you have for that in CoqIDE) to know how to number
> occurrences.
> 
> Hugo