The Coq mailing list

[jean-francois.monin AT imag.fr]

Hello,

I did not try to understand the example (too many complicated 
formulas for my small head), I was just interested by a usage
of dependent rewrite.

However a vanilla "rewrite H3" instead of "dependent rewrite; simpl" 
seems to do the job in that case.

  JF

Yves Bertot a ecrit :
 > 
 > 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.
rewrite H3.
discriminate.
Qed.

-----------------------------------------------------------------