How to pattern match exist to transform proofs

First off, it's probably better to write assoc like this

Inductive assoc {A B : Type} (k : A) (v : B) : list (A * B) -> Prop :=
| assoc_head : forall l, assoc k v ((k, v) :: l)
| assoc_tail : forall l x, assoc k v l -> assoc k v (x :: l).
Arguments assoc_head {A B} {k v}, {A B} k v, A B k v.
Arguments assoc_tail {A B} {k v} {l}, {A B} {k v} l, {A B} k v l, A B k v l.

Basically, the more things you can fit on the left side of the :, the easier it is to deal with the type (more parameters, fewer indices). I'd actually go further and write

Inductive elem {A : Type} (x : A) : list A -> Prop :=
| in_here : forall l, elem x (x :: l)
| in_there : forall l y, elem x l -> elem x (y :: l).
Definition assoc {A B : Type} (k : A) (v : B) l := elem (k, v) l.

but that's getting sidetracked.

Anyway, you don't need to inspect the third argument of exists in your code. You just give it to assoc_tail. Done.

#[program] Fixpoint lookup
  {A B : Type} (dec : forall x y : A, {x = y} + {x <> y})
  (l : list (A * B)) (k : A) {struct l}
: option {v : B | assoc k v l}
:=
  match l with
  | [] => None
  | (k', v') as h :: l =>
    if dec k' k (* writing the first argument to exist is usually just clutter *)
      then Some (exist _ v' (assoc_head k' v' l))
      else
        match lookup dec l k with
        | Some (exist _ v prf) => Some (exist _ v (assoc_tail h prf))
        | None => None
        end
  end.

Do note that part of the magic of Program is that it's supposed to let you write the actual program without worrying about the proof part first. In particular, you're supposed to imagine that values with refined type like x : {v : B | assoc k v l} are just x : B, and then the proof part of the refinement is handled later.

#[program] Fixpoint lookup
  {A B : Type} (dec : forall x y : A, {x = y} + {x <> y})
  (l : list (A * B)) (k : A) {struct l}
: option {v : B | assoc k v l}
:=
  match l with
  | [] => None
  | (k', v') :: l =>
    if dec k' k
      then Some v'
      else
        match lookup dec l k with (* looks weird but is still necessary *)
        | Some v => Some v
        | None => None
        end
  end.
Solve Obligations with program_simpl; now constructor.

On that note, lookup can do better than just return an option!

#[local] Hint Constructors assoc : core.
#[local] Unset Program Cases.

#[program] Fixpoint lookup
  {A B : Type} (dec : forall x y : A, {x = y} + {x <> y})
  (l : list (A * B)) (k : A) {struct l}
: {v : B | assoc k v l} + {~exists v : B, assoc k v l}
:=
  match l with
  | [] => inright _ (* Underscores as an "escape hatch" to an obligation *)
  | (k', v') :: l =>
    if dec k' k
      then inleft v'
      else
        match lookup dec l k with
        | inleft v => inleft v
        | inright no => inright _
        end
  end.
Next Obligation.
  intros [v no].
  inversion no.
Qed.
Next Obligation.
  intros [v nono].
  inversion nono as [? | ? ? nono']; eauto.
Qed.

After pattern-matching on the pair exist from the recursive call, you know the first component of the pair is also the first component of your result. Then the second component is a proof that you can fill up as a separate obligation.

match lookup ... with
| Some (exist _ b _) => Some (exist _ b _ (* this underscore becomes an obligation *))
| None => None
end

That allows the Program Definition command to complete, and then you have to prove an obligation (a lemma) to actually finish that definition. Be sure to terminate the proof with Defined instead of Qed because the guardedness checker somehow needs your proof to be transparent.

Next Obligation.
  (* finish the proof *)
Defined.

Program Fixpoint lookup
  (A : Set)
  (B : Set)
  (dec : (forall x y : A, {x = y} + {x <> y}))
  (l : list (A * B))
  (a : A)
  {struct l}
  : option {b : B | assoc A B l a b}
:= match l with
   | [] => None
   | (pair v t) :: tl =>
     if dec v a
     then (Some (exist (assoc A B ((pair v t) :: tl) a) t (assocHead A B tl a t)))
     else match (lookup A B dec tl a) with
          | Some (exist _ b _) => Some (exist _ b _)
          | None => None
          end
   end.

Next Obligation.
  apply assocTail.
  assumption.
Defined.

There is already a predicate In in the library that specifies whether a list contains an element, so you don't really need to define a new assoc predicate.

And you could try to use the refine tactic which I find really helpful to build up the term step by step. It is a bit like using Program but it feels less magical. You write as much of the term as you can (i.e. the match statement that a destruct would generate), and put in _ where you want to get a proof obligation. You can use proof tactics for the obligations, and see what kind of term you build up. It can be quite enlightening.

I ended up with this program:

Require Import List.

Fixpoint lookup {A B} (dec: forall (a a':A), {a=a'}+{a<>a'})
         (l:list (A*B)) (a:A) {struct l} : option {b | In (a,b) l}.
  refine (
      match l with
      | nil => None
      | cons (a',b) l' =>
        match dec a a' with
        | left _ y => Some (exist _ b (or_introl _))
        | right _ y  =>
          match lookup _ _ dec l' a with
          | None => None
          | Some (exist _ b' H') => Some (exist _ b' (or_intror H'))
          end
        end
      end).
  congruence.
Defined.

Note that I for pedagogical reasons left one _ in the term, that was taken care of with the congruence tactic.