The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Hello,

I believe I understood your problem and found a solution.

I would like to be able to brag that the answer was in the Coq'Art, but it
requires a lot of ingenuity to find it.   The pages to read are p.221 and 
p.248.   On the first location, we discover that sigS terms are sometimes
produced by injection.  On the second page, we discover that inversion
relies on injection.

On page 221, a solution is also described to exploit the
sigS terms: this solution is a tactic called "dependent rewrite".  Here is
my example, which I re-constructed from the partial information that
you sent us (in the future, I beg you to give a full running example, so
that we can be faster at devising a solution).

Inductive Pos : Set :=
  empty : Pos | P0 : Pos -> Pos | P1 : Pos -> Pos.

Inductive q0_type : Set :=
  Fun : q0_type -> q0_type -> q0_type | Base : q0_type.

Parameter Var : q0_type -> Set.

Inductive Trm : q0_type -> Set :=
  Apply : forall a b, Trm (Fun b a) -> Trm a -> Trm b
| Lambda : forall a b, Var a -> Trm b -> Trm (Fun b a)
| Tvar : forall a, Var a -> Trm a.

Implicit Arguments Apply.
Implicit Arguments Lambda.
Implicit Arguments Var.

Inductive subtrm : forall a b, Trm a -> Trm b -> Pos -> Prop :=
   subtrm_empty : forall a A, subtrm a a A A empty
| subtrm_apply0 :
        forall a b t M N T p,
           subtrm t (Fun b a) T M p ->
           subtrm _ _ T (Apply M N) (P0 p)
| subtrm_apply1 :
        forall a b t M N T p,
           subtrm t b T N p ->
           subtrm _ a T (Apply M N) (P1 p)
| subtrm_lambda1 :
        forall a b t x M T p,
           subtrm t b T M p ->
           subtrm t (Fun b a) T (Lambda x M) (P1 p).
Implicit Arguments subtrm.

Theorem the_problem :
forall s : q0_type,
forall t : q0_type,
forall M : Trm (Fun s t),
forall N : Trm t,
forall x0 : q0_type,
forall x1 : q0_type,
forall x2 : Var x0,
forall x3 : Trm x1,
 subtrm (Lambda x2 x3)(Apply M N) empty
 -> False.
Proof.
 intros s t M N x0 x1 x2 x3 H; inversion H.
(* we get to the situation you did not like. *)
generalize H5.
dependent rewrite H3.
(* Now we are out of trouble. *)
simpl; discriminate.
Qed.