The Coq mailing list

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

Hi Jonathan,

Sorry, "Set Implicit Arguments" was missing from my post
because it already occured in Adam's code. This does work
as is with 8.4pl3 and 8.5pl1

(******************************)

Set Implicit Arguments.

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 nil
          | _    => 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.

(**************************************)

Would be interesting to see if it can be generalized to W_types ?

Best,

Dominique

----- Mail original -----
> De: "Jonathan Leivent" 
> <jonikelee AT gmail.com>
> À: "Coq Club" 
> <coq-club AT inria.fr>
> Envoyé: Mercredi 31 Août 2016 19:13:44
> Objet: Re: [Coq-Club] help with automating derived UIP_refl proofs
> 
> 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.
> >>
> 
>