Require Import VST.floyd.base2.
Require Import VST.floyd.client_lemmas.
Local Open Scope logic.

Definition compute_funspecs_norepeat (l : list (ident*funspec)) :=
  compute_list_norepet (fst (split l)).

Lemma not_in_funspecs_by_id_i {A B} i (l : list (A * B)) l0 l1 :
  split l = (l0,l1) ->
  ~In i l0 ->
  ~In i (map fst l).
Proof.
(* Goal: forall (_ : @eq (prod (list A) (list B)) (@split A B l) (@pair (list A) (list B) l0 l1)) (_ : not (@In A i l0)), not (@In A i (@map (prod A B) A (@fst A B) l)) *)
  revert i l0 l1.
  induction l as [|[a b] l]; intros a' [|a'' la] [|b' lb] E; simpl in *;
    try destruct (split l); congruence || auto.
(* Goal: forall _ : not (or (@eq A a'' a') (@In A a' la)), not (or (@eq A a a') (@In A a' (@map (prod A B) A (@fst A B) l))) *)
  injection E; intros; subst; intuition.
(* Goal: False *)
  eapply IHl; eauto.
Qed.

Lemma compute_funspecs_norepeat_e l :
  compute_funspecs_norepeat l = true ->
  funspecs_norepeat l.
Proof.
(* Goal: forall _ : @eq bool (compute_funspecs_norepeat l) true, funspecs_norepeat l *)
  intros H; hnf.
(* Goal: @list_norepet ident (@map (prod ident funspec) ident (@fst ident funspec) l) *)
  rewrite <-semax_call.fst_split.
(* Goal: @list_norepet ident (@fst (list ident) (list funspec) (@split ident funspec l)) *)
  apply compute_list_norepet_e, H.
Qed.
