gistfile1.coq

Definition get_existent
  vt
  (k : kt)
  (mr : list (kt * vt))
  (H_in_mr : in_mr vt k mr)
 :
  vt
.
refine
  ( (fix _self_ lst (Hin : in_mr vt k lst) :=
       match lst as lst0 return (lst = lst0) -> vt with
       | nil => fun Heq_lst => False_rect _ (_as "nil")
       | cons hkv t => fun Heq_lst =>
           match hkv as hkv0 return (hkv = hkv0) -> vt with
           | (hk, hv) => fun Heq_hkv =>
               if K.eq_dec k hk
               then
                 hv
               else
                 _self_ t (_as "new Hin")
           end
           (eq_refl hkv)
       end
       (eq_refl lst)
    )
    mr
    H_in_mr
  )
.

proving goal "nil"%string.
apply in_mr_empty with (k := k) (vt := vt).
subst; now assumption.

proving goal "new Hin"%string.
subst.
unfold in_mr in *.
inversion Hin.
(* In_head *)
  au.
(* In_tail *)
  au.
Defined.


Extraction get_existent.

(*

(** val get_existent : kt -> (kt, 'a1) prod list -> 'a1 **)

let rec get_existent k = function
| Nil -> assert false (* absurd case *)
| Cons (hkv, t0) ->
  let Pair (hk, hv) = hkv in
  (match K.eq_dec k hk with
   | Left -> hv
   | Right -> get_existent k t0)

*)