Coq example

coq.v

Require Import List.
Import ListNotations.
Require Import Coq.Arith.Arith.
Set Implicit Arguments.
Set Asymmetric Patterns.


Fixpoint lookup_simple {A} (pairs: list (nat * A)) (key :nat) : option (nat * A) := match pairs with
  | [] => None
  | a :: ss => if (beq_nat key (fst a))
               then Some a
               else match (lookup_simple ss key) with 
                | None => None
                | Some b => Some b
               end
end.

Lemma lookup_simple_correct : forall A (pairs : list (nat * A)) key s , 
  lookup_simple pairs key = Some s ->  key = fst s.
Proof.
induction pairs.
- intros. inversion H.
- intros. case_eq (beq_nat key (fst a)).
  + intros. cbn in H. rewrite H0 in H. inversion H; subst. exact(proj1 (beq_nat_true_iff  _ _) H0).
  + intros. cbn in H. rewrite H0 in H. apply IHpairs.
    destruct (lookup_simple pairs key).
    ++  assumption.
    ++ inversion H.
Qed.


Inductive member (A : Type) (x : A) : list A -> Type :=
| here : forall l, member x (x :: l)
| there : forall y l, member x l -> member x (y :: l).


Fixpoint lookup {A} (pairs: list (nat * A)) (key :nat) : option { s: (nat * A) & member s pairs} := match pairs with
  | [] => None
  | a :: ss => if (beq_nat key (fst a))
               then Some (existT _ a (here a ss))
               else match (lookup ss key) with 
                | None => None
                | Some (existT s m) => Some (existT _ s (there a m))
               end
end.

Lemma lookup_correct : forall A (pairs : list (nat * A)) key s (m : member s pairs), 
  lookup pairs key = Some (existT _ s m ) ->  key = fst s.
Proof.
induction pairs.
- intros. inversion m.
- intros. case_eq (beq_nat key (fst a)).
  + intros. cbn in H. rewrite H0 in H. inversion H ; subst.  admit.
  + intros. cbn in H. rewrite H0 in H. inversion m ; subst.
    ++ admit.
    ++ admit.