The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Hi Dominique,

I am getting an error when trying your script for UIP on lists in 
8.5pl2.  The error is on the first mention of eq_refl in eq_inv_prop:

Error:
In environment
X : Type
eqX_uniq : forall (x : X) (e : x = x), e = eq_refl
list_cons_eq := fun (x y : X) (l m : list X) (e1 : x = y) (e2 : l = m) =>
                match e1 in (_ = x0) return (x :: l = x0 :: m) with
                | eq_refl => match e2 in (_ = l0) return (x :: l = x :: 
l0) with
                             | eq_refl => eq_refl
                             end
                end : forall (x y : X) (l m : list X), x = y -> l = m 
-> x :: l = y :: m
n : list ?T
m : list ?T
H : n = ?l@{m1:=nil}
The term "eq_refl" has type "n = n" while it is expected to have type "n 
= ?l@{m1:=nil}"
(cannot unify "?l@{m1:=nil}" and "n").

Also, for my purposes, I would like a generalizable proof mechanism that 
I can automate in Ltac.  Hence, type-specific matches such as in 
eq_inv_prop can be problematic because these are hard to generate from 
Ltac (although I am rethinking if that will be the case in 8.6, due to 
the new open_constr:(...) form).

I wasn't able to use Adam's scheme on recursive inductive types like 
list or nat because it requires UIP to be universal on the substructure, 
but in an inductive proof, one only has UIP at a point on the 
substructure via the inductive hypothesis.  I tried to rewrite Adam's 
UIP_iso proof so that it only requires UIP for the type A at a single 
point, but failed.

For list, I proved UIP this way:


Set Implicit Arguments.

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

Ltac uiptac :=
  lazymatch goal with
    |- ?x = _ =>
    refine (match x with eq_refl => _ end); cbv; reflexivity
  end.

Require Import List.

Lemma UIP_refl_list (A:Type)(UIP_refl_A : forall (a:A)(e:a=a), 
e=eq_refl)(l : list A)(x : l=l) : x = eq_refl.
Proof.
  induction l.
  - uiptac.
  - change eq_refl with (f_equal (fun p => cons (fst p) (snd p)) 
(pair_cong (eq_refl a) (eq_refl l))).
    pose proof (UIP_refl_A _ (f_equal (@hd A a) x)) as ua.
    cbn in ua.
    rewrite <- ua.
    rewrite <- (IHl (f_equal (@tl A) x)).
    cbv.
    uiptac.
Qed.

Which doesn't use a type-specific match - almost: it is true that hd and 
tl incorporate such type-specific matches, but I think I can generate 
projections for multiple-constructor inductive types from Ltac.  Hence, 
I think this mechanism might be generalizable into a  UIP-proof 
generating tactic for arbitrary inductive types.

-- Jonathan


On 08/31/2016 12:14 PM, Dominique Larchey-Wendling wrote:
> 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.