The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

> So if there is more than one proof of [x = y], there will be more elements in [sigT (fun x => member x xs)] than [members xs]. Usually I've found that I prefer [members] to [member] for this reason.

Not so.  Even if there are multiple proofs of [x = x], the type [sigT (fun y => x = y)] has only one element up to equality.  Here's a proof that [sigT (fun x => member x xs)] has decidable equality, based on the encode-decode method of HoTT:

Require Import List.

Section with_type.

  Context {A : Type}.

  Inductive member (x : A) : list A -> Type :=

  | here : forall y xs, x = y -> member x (y :: xs)

  | there : forall y xs, member x xs -> member x (y :: xs).

  Definition members ls := { x : A & member x ls }.

  Fixpoint beq_hetero {ls ls'} {x0} (x : member x0 ls) {y0} (y : member y0 ls')

    : bool

    := match x, y with

       | here _ _ _ _, here _ _ _ _ => true

       | here _ _ _ _, _ => false

       | there _ _ _ m, there _ _ _ m' => @beq_hetero _ _ _ m _ m'

       | there _ _ _ _, _ => false

       end.

  Definition beq {ls} (x y : members ls) : bool

    := @beq_hetero ls ls _ (projT2 x) _ (projT2 y).

  Definition code ls (x y : members ls) := beq x y = true.

  Fixpoint encode'_exploded ls x0 (x : member x0 ls)

    : @beq_hetero ls ls _ x _ x = true

    := match x with

       | here _ _ _ _ => eq_refl

       | there _ _ _ m => @encode'_exploded _ _ m

       end.

  Definition encode {ls} {x y} (H : x = y :> members ls) : code ls x y

    := match H with

       | eq_refl => encode'_exploded _ _ _

       end.

  Local Ltac do_member_small_inversion_on m :=

    (* adjust the goal so that all things which depend on arguments of [member]

       are reverted, and so that the arguments come first, followed by [m] *)

    is_var m; move m at top;

    lazymatch type of m with

    | member _ (cons ?x ?xs)

      => is_var x; is_var xs;

         revert dependent x; intros x m; move m at top;

         revert dependent xs; revert x

    | ?T => fail "wrong type" T

    end;

    let P := match goal with |- forall x xs y, @?P x xs y => P end in

    let x := fresh "x" in

    let xs := fresh "xs" in

    intros x xs m;

    refine match m in member _ ls

                 return match ls with

                        | nil => fun _ => False

                        | cons x xs => P x xs

                        end m

           with

           | here _ _ _ _ => _

           | _ => _

           end.

  Import EqNotations.

  Fixpoint decode_exploded {ls}

           {x0} {x : member x0 ls} {y0} {y : member y0 ls}

    : code ls (existT _ _ x) (existT _ _ y)

      -> { p : x0 = y0 | rew [fun x' => member x' ls] p in x = y }.

  Proof.

    destruct x as [x xs H|x xs m];

      [ clear decode_exploded | specialize (decode_exploded xs _ m) ];

      do_member_small_inversion_on y;

      unfold code, beq; simpl; repeat intro; subst;

        repeat first [ reflexivity

                     | exists eq_refl; reflexivity

                     | repeat intro; exfalso; apply Bool.diff_false_true; assumption

                     | match goal with

                       | [ IH : forall y y', _ = true -> _, H' : _ = true |- _ ]

                         => specialize (IH _ _ H'); destruct IH; subst

                       end ].

  Defined.

  Definition decode {ls} {x y : members ls} (H : code ls x y) : x = y.

  Proof.

    destruct (decode_exploded H), x, y; simpl in *; subst; reflexivity.

  Defined.

  Definition decode_false {ls} {x y : members ls} (H : beq x y = false)

    : x <> y.

  Proof.

    unfold beq in *; intro H'; subst; rewrite encode'_exploded in H; congruence.

  Qed.

  Definition dec (P : Prop) := {P} + {~ P}.

  Definition dec_eq_members (xs : list A) (m m' : members xs) : dec (m = m')

    := (if beq m m' as c return beq m m' = c -> _

        then fun H => left (decode H)

        else fun H => right (decode_false H))

         eq_refl.

End with_type.

On Wed, May 17, 2017 at 8:46 AM Ben Sherman <sherman AT csail.mit.edu> wrote:

From: Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>

Subject: Re: [Coq-Club] How to represent tabular data in Coq

Date: May 10, 2017 at 4:19:57 AM EDT

To: coq-club AT inria.fr

Dear Ben,

thanks these are very useful pointers.

A few question, though: Why don't you use the "In" predicate from
the standard library instead of "member"?

Note that [In] is a prop, whereas [member] is a type. Since [In] is a prop, it can't be used to retrieve any information, like looking up an element in a list. For example, imagine the list [1; 1]. If I have [p : In 1 [1; 1]], I don't know whether the proof was made with the first or second member of the list (in particular, it is admissible to assume that all elements of [In 1 [1; 1] are equal), but if I have [p : member 1 [1; 1]], that data may be used computationally.

Haven't you only given me the interface for tables but not their
representation?
How would I construct an actual table?

You would write a lambda that computes the value from the indices (i.e., [members] terms) that are input. So you'd be pattern matching on those [members] terms. Here's some example code that might give some idea:

Fixpoint get_members {A} {xs : list A} (m : members xs) : A

  := match m with

  | here' x _ => x

  | there' _ _ m' => get_members m'

  end.

Fixpoint to_nat {A} {xs : list A} (m : members xs) : nat 

  := match m with

  | here' _ _ => 0

  | there' _ _ m' => S (to_nat m')

  end.

Fixpoint eq_members {A B} {xs : list A} {ys : list B}

  (m : members xs) (m' : members ys) :=

  Nat.eqb (to_nat m) (to_nat m').

Definition ComputeTable {R C A} (r : list R) (c : list C)

  (f : R -> C -> A) : Table' R C r c A :=

  {| lookup' := fun mr mc => f (get_members mr) (get_members mc) |}.

Definition UpdateTable {R C A r c}

  (t : Table' R C r c A) (mr : members r) (mc : members c)

  (a : A)

  : Table' R C r c A

  := {| lookup' := fun mr' mc' =>

   if andb (eq_members mr mr') (eq_members mc mc')

     then a

     else lookup' _ _ _ _ _ t mr' mc' |}.

The difference between "member" and "members" is also interesting.
How do I "see" that "member" requires UIP?

Sorry, I wasn't clear about this. Neither one requires UIP. But I believe the types [members xs] and [sigT (fun x => member x xs)] are isomorphic only if [A] satisfies UIP. The reason is that [member] could be equivalently defined

Inductive member {A} (x : A) : list A -> Type :=

  | here : forall y xs, x = y -> member x (y :: xs)

  | there : forall y xs, member x xs -> member x (y :: xs).

So if there is more than one proof of [x = y], there will be more elements in [sigT (fun x => member x xs)] than [members xs]. Usually I've found that I prefer [members] to [member] for this reason.