The Coq mailing list

[Casteran Pierre <pierre.casteran AT labri.fr>]

Hi,

 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 ?

Pierre


Require Import List.

(* from cpdt *)
Section hlist.
Set Implicit Arguments.
Variable A : Type.
Variable B : A -> Type.

Inductive hlist : list A -> Type :=
|  HNil : hlist nil
| HCons : forall (x:A)(ls : list A), B x -> hlist ls -> hlist (x::ls).

Variable elm : A.

Inductive member : list A -> Type :=
| HFirst : forall ls, member (elm :: ls)
| HNext : forall x ls, member ls -> member (x::ls).

(** puts y at the position defined by M *)

Definition hset (y:B elm): forall (l:list A)(M:member l) , hlist l -> hlist l.
intros l M;induction M.
inversion_clear 1  as [|x0 x1].
exact (HCons y X1).
intro hs; inversion_clear  hs .
exact (HCons X (IHM X0)).
Defined.


(** from cpdt again *)
Fixpoint hget ls (mls : hlist ls) : member ls ->  B elm :=
match mls with
| HNil  => fun mem  =>
          match mem in member ls'  return (match ls' with
                                                 | nil => B elm
                                                 | _::_ => unit
                                             end) with
            |  HFirst _ => tt
            |  HNext _ _ _ => tt
          end
| HCons _ _ x mls' => fun mem =>
           match mem in member ls' return (match ls' with 
                                           | nil => Empty_set
                                           | x' :: ls'' =>
                                              B x' -> (member ls'' -> B elm)
                                                        -> B elm
                                            end)
           with
               | HFirst _ => fun x _ => x
               | HNext _ _ mem' => fun _ get_mls' => get_mls' mem'
           end x (hget mls')
end.


Goal forall (y:B elm)(l:list A)(M:member l)(hl:hlist l), 
  (hget (hset y M hl)) M = y.
Admitted.


End hlist.