The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 08/29/2013 07:30 AM, Casteran Pierre wrote:
> Using cpdt's hlists, I had to define a function
> hset (y:B elm): forall (l:list A)(M:member l) , hlist l -> hlist l.
>
> such that  (hset y M hl) returns  hl with y at the place defined by M.
>
> I got some solution, but in an interactive definition, using inversion 
> twice. Is there a direct solution (as a variation on hget), making
> easy to prove for instance that (hget (hset y M hl)) M = y ?

Yes.  Here are the missing ingredients:

Definition hhd ls (hl : hlist ls) : match ls return Type with
                                      | nil => unit
                                      | x :: _ => B x
                                    end :=
  match hl with
    | HNil => tt
    | HCons _ _ v _ => v
  end.

Definition htl ls (hl : hlist ls) : match ls return Type with
                                      | nil => unit
                                      | _ :: ls' => hlist ls'
                                    end :=
  match hl with
    | HNil => tt
    | HCons _ _ _ hl' => hl'
  end.

Fixpoint hset (y : B elm) l (M : member l) : hlist l -> hlist l :=
  match M in member l return hlist l -> hlist l with
    | HFirst _ => fun hl => HCons y (htl hl)
    | HNext _ _ M' => fun hl => HCons (hhd hl) (hset y M' (htl hl))
  end.

Goal forall (y:B elm)(l:list A)(M:member l)(hl:hlist l),
  (hget (hset y M hl)) M = y.
  induction M; simpl; auto.
Qed.