The Coq mailing list

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

Here is a simple example of proof where I have to do something
manually that is cumbersome.  I would expect the Pattern tactic to do
it for me, but I did not find the right combination of arguments.

Does anybody know a way to use the Pattern tactic so that the
goal is naturally replace by a goal of the form:

(P intzero (int_discr' intzero))

where P is the proposition given below?

If not, could Coq be extend in such a way that this would be possible?

====================
Variables int : Set; intone : int; intzero : int.
Hypothesis I0_neq_I1 : ~intzero = intone.

Inductive int_discr_type : int -> Set :=
  is_zero : (int_discr_type intzero) 
| is_one : (int_discr_type intone)
| is_other : (x:int)~x=intzero->~x=intone->(int_discr_type x).

Theorem intone_eq : intone = Cases (discr_int' intzero) of
                                is_zero => intone
                             | is_one => intzero
                             | (is_other _ _ _) => intzero
                             end.
Cut intzero=intzero.
Apply
 int_discr_type_ind
                    with
                    P:=
                     [x:int; v:(int_discr_type x)]
                       x=intzero
                       ->intone
                          =Cases v of
                             is_zero => intone
                           | is_one => intzero
                           | (is_other x _ _) => intzero
                           end;Intuition.
Intuition.
Qed.