How to pattern match exist to transform proofs

Question

I'm messing around with coq and I'm trying to create a function that can be used to lookup something in a list and return an associated proof with it that the specified element is in the list.

In my case I have a list of tuples and I want to lookup based on the first element of the tuple.

So first I defined an assoc inductive predicate that proves an element is in the list. This has two cases. Either the element is in the head of the list or it is in the tail.

Inductive assoc (A : Set) (B : Set) : list (A * B) -> A -> B -> Prop :=
  | assocHead : forall (l : list (A * B)) (a : A) (b : B), assoc A B (cons (a,b) l) a b
  | assocTail : forall (l : list (A * B)) (a x : A) (b y : B), assoc A B l a b -> assoc A B ((x,y) :: l) a b.

Then I define a lookup function that given a list of tuples, a first element and an equality predicate returns either None or Some with the looked up element and a proof that the element is in the list.

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
                           -- In the case below we have proven it's in the
                           -- tail of the list.
                           -- How to use that to create new proof with assocTail?
                           | Some (exist _ _ _) => None
                           | None => None
                           end
   end.

The way it's written above compiles fine. But I can't figure out how to use the proof that is in the tl of the list to create a new proof that it's in the total list. I have tried various things like pattern matching in the third argument of exist but I can never get it to work.

Any help is appreciated!

Answer 1

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.

Answer 2

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.

Answer 3

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.