gistfile1.coq

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

proving goal "nil"%string.
apply in_mr_empty with (k := k) (vt := vt) in Hin.
contradiction.

proving goal "new Hin"%string.
inversion Hin.
au.
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)

*)