gistfile1.coq

Require Import List.

Inductive prop : list (bool * nat) -> Prop :=
| Case_cons : forall hb hn t, hb = true -> prop ((hb, hn) :: t)
| Case_nil : prop nil
.


Goal prop ((true, 0) :: nil).
apply Case_cons; reflexivity.
Defined.
(* that's ok. *)

Goal forall (f : nat -> nat) lst,
  prop lst ->
  prop
    (match lst with
     | nil => nil
     | cons h t =>
         match h with
         | (hb, hn) =>
             let hn' := f hn in
             (hb, hn') :: t
         end
     end
    )
.
intros.
induction lst.
(* nil *)
  apply Case_nil.
(* cons *)
  (* compute in *. // doesn't change anything *)
  cbv.
  apply Case_cons.

(*
Error: Impossible to unify "prop ((?18952, ?18953) :: ?18954)" with
 "prop (let (hb, hn) := a in (hb, f hn) :: lst)".


same error for "eapply Case_cons"
*)