The Coq mailing list

[Nikita Karetnikov <nikita AT karetnikov.org>]

Could anyone explain why simpl fails to perform reduction here?  Is it
because of the Eq typeclass?

Fixpoint is_in_order_merge {X : Type} {eq_x : Eq X} {eq_list : Eq (list X)}
                           (l1 l2 l : list X) : bool :=
  match l1 with
    | []      => eqb l2 l
    | (x::xs) =>
      match l2 with
        | []      => eqb l1 l
        | (y::ys) =>
          match l with
            | []      => false
            | (z::zs) =>
              if eqb x z
              then is_in_order_merge xs l2 zs
              else if eqb y z
                   then is_in_order_merge l1 ys zs
                   else false
          end
      end
  end.

Theorem is_iom__iom :
  forall {X : Type} {eq_x : Eq X} {eq_list : Eq (list X)} (l1 l2 l : list X),
    is_in_order_merge l1 l2 l = true -> in_order_merge l1 l2 l.
Proof.
  induction l1 as [|x xs].
  Case "l1 = []".
    intros.
    simpl in H.
    (* XXX: no simplification is performed in H. *)

(*   Case := "l1 = []" : String.string *)
(*   X : Type *)
(*   eq_x : Eq X *)
(*   eq_list : Eq (list X) *)
(*   l2 : list X *)
(*   l : list X *)
(*   H : is_in_order_merge [] l2 l = true *)
(*   ============================ *)
(*    in_order_merge [] l2 l *)

(* subgoal 2 (ID 1555) is: *)
(*  forall l2 l : list X, *)
(*  is_in_order_merge (x :: xs) l2 l = true -> in_order_merge (x :: xs) l2 l 
*)
Abort.