The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

!!

I realised that trunk infers this complicated return clause for me (and is hence smarter than destruct in this case):

Lemma inject_project : forall x y (p:member x (cons y nil)), inject (project p) = p.
Proof.
  intros x y p.
  refine match p
               with
          | MZ _ _ =>  _
          | MN _ _ _ m =>  _
          end; swap 1 2.
  all:destruct l; [|exact (fun A x => x)].
  { inversion m. }
  reflexivity.
Qed.

It's quite nice (except we may have to add a case for IDProp in easy). My congratulations to Pierre Boutiller who implemented this feature.

On 6 August 2014 22:31, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> wrote:

For completeness (member x [y] and x=y are indeed isomorphic types):

Lemma inject_project : forall x y (p:member x (cons y nil)), inject (project p) = p.
Proof.
  intros x y p.
  refine match p in member _ l
               return match l return member x l -> Prop with cons z nil => fun p => inject (project p) = p | _ => fun _ => True end p

               with
          | MZ _ _ =>  _

          | MN _ _ _ m =>  _
          end; swap 1 2.
  all:destruct l; [|easy].
  { inversion m. }
  reflexivity.
Qed.

On 6 August 2014 22:01, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

On 06/08/2014 21:07, Jason Gross wrote:
> I think your lemma implies UIP on T.  If you strip off the MN constructor,
> and instantiate ls to nil, then you've defined the equality type on T.  So
> you should be able to show that [member a (b::nil)] and [a = b] are
> equivalent types.  (Note that there is only one proof of [nil = nil],
> regardless of what type your list has; this is because you can always
> decide whether or not [ls = nil] for any [ls], and the "decidable equality
> -> UIP" implication works even when you fix the parameter to eq; I've
> gotten some development of this merged into the stdlib in trunk.)

Indeed:

Context {T : Type}.

Inductive member (a : T) : list T -> Type :=
| MZ : forall ls, member a (a :: ls)
| MN : forall l ls, member a ls -> member a (l :: ls).

Section to_nat.
  Variable a : T.

  Fixpoint to_nat {ls} (m : member a ls) : nat :=
    match m with

      | MZ _ _ => 0
      | MN _ _ _ m => S (to_nat m)
    end.
End to_nat.

Definition project {x y} (p : member x (cons y nil)) : x = y.
Proof.
refine (
match p in member _ l return
  match l with
  | nil => True
  | cons x l => (l = nil) -> _
  end
with
| MZ _ _ => fun _ => eq_refl
| MN _ _ _ m => fun e => False_rect _ _
end eq_refl
).
rewrite e in *; inversion m.
Defined.

Definition inject {x y} (p : x = y) : member x (cons y nil).
Proof.
destruct p; constructor.
Defined.

Lemma retract : forall x y (p : x = y), project (inject p) = p.
Proof.
intros x y p; unfold project, inject.
destruct p.
reflexivity.
Qed.

Definition member_eq x ls (a b : member x ls) :=
    to_nat x a = to_nat x b -> a = b.

Lemma to_nat_eq_member_eq : forall x, (forall ls a b, member_eq x ls a b) ->
  (forall (p : x = x), p = eq_refl).
Proof.
intros x Hx p; unfold member_eq in *.
rewrite <- (retract _ _ p), <- (retract _ _ eq_refl).
f_equal.
apply Hx.
destruct p.
reflexivity.
Qed.

PMP