The Coq mailing list

[Matthieu Sozeau <sozeau AT lri.fr>]

Le 21 nov. 08 à 10:09, Thomas Braibant a écrit :

> Hi,

Hi,

> Maybe this is a very naive question, but I have trouble using  
> dependent
> destruction under coq 8.2 beta4.

It's alright, it's a recent addition :)

> In the following minimal exemple, I want to prove inversion lemmas on
> (dependent) inductive objects. I am able to use the dependent  
> destruction
> tactic if our inductive definition is defined in Type, but not in  
> Prop.
> However, converting by hand the proof term generated for the Type  
> lemma, we are
> able to construct a valid proof term for the Prop lemma. Is there a  
> general way
> to prove this kind of lemmas in Prop (using tactics), rather than  
> hacking a
> proof term ?

Yes, there is. The problem is that no dependent elimination principle  
is generated
for eliminating [t_typ] to [Prop], so the [destruct] behind [dependent  
destruction]
fails. Only [case] is able to handle this case by generating an ad-hoc  
elimination.
Sadly, the tactic [dependent destruction] is defined in 8.2beta4 as:
<< Tactic Notation "dependent" "destruction" ident(H) :=
  do_depind' ltac:(fun hyp => destruct hyp) H.>>

One way to fix it is to use [case] instead of [destruct] here, but  
that means
generating ad-hoc principles on the fly which could be costly. Once  
you generate
the proper induction scheme using:
<<Scheme t_prop_dep := Induction for t_prop Sort Prop.>>, you can add
[using t_prop_dep] clauses to your [dependent desctruction/induction]  
calls
to get the expected behavior.

You can still improve on that using some existing infrastructure in
[Program.Equality] that I didn't use in [dependent destruction] tactics
that allows to register the prefered dependent elimination principle
associated to a datatype to avoid repeating it everywhere.
There is a typeclass
<<
Class DependentEliminationPackage (A : Type) :=
  elim_type : Type ; elim : elim_type.
>>

and two tactics [elim_case] and [elim_ind] that check the type of the  
eliminated
object, try to retrieve their eliminator and finally apply [destruct  
using] or
[induction using]. Now you can redefine [dependent destruction] using  
this tactic,
even falling back to [case] in case no eliminator is declared. As a  
side note,
[case] doesn't cleanup the goal at all after application, so you might  
have some
manual simplifications to do. Anyway, by declaring the dependent  
elimination
principle for [t_prop] you get what you want:
<<
 Require Import Coq.Program.Equality.

  Tactic Notation "dependent" "destruction" ident(H) :=
      do_depind' ltac:(fun hyp => elim_case hyp || case hyp) H.

    Variable Z : Type.
    Inductive Obj : Type :=
    | Eq : Obj
    | Neq : Obj.
    Inductive t_prop : Z -> Z -> Obj -> Prop :=
    | t_prop_eq : forall A, t_prop A A Eq
    | t_prop_neq : forall A B, t_prop A B Neq
      .

    Scheme t_prop_dep := Induction for t_prop Sort Prop.

    Instance t_depelim x y o : DependentEliminationPackage (t_prop x  
y o) :=
      elim := t_prop_dep.

    Lemma lemma_prop : forall A B (u : t_prop A B Eq), (A=B)/\ (JMeq  
u (t_prop_eq A)).
    Proof.
      intros A B u ; dependent destruction u; constructor; reflexivity.
    Qed.

> Moreover, the last part of the code deals with an exemple where I  
> can't use
> induction, because it leads to an ill-typed term. Could someone  
> explain this
> situation ? It seems that this could be related to the inductives  
> Scheme
> generated by default when using "Inductive" keyword, sometimes the  
> Minimality
> Scheme, and sometimes the "Normal" one.

In this case, it's even more important to use the [elim_ind] tactic,  
as there's
no equivalent to [case] which would build an ad-hoc induction  
principle on the fly.
The fact that [induction] fails is just a regular occurence of the  
problem with the
elimination of dependent objects, as [u] has type [t_prop A B Neq]  
where [Neq] is
some constructor and [u] appears in the goal. One cannot generalize  
the type of [u] to
some [t_prop A' B' O] for fresh variable [A', B', O], which is needed  
to apply the
[induction] tactic.

Again, you can rebind the [dependent induction] tactic notation and do:
<<
  Tactic Notation "dependent" "induction" ident(H) :=
    do_depind' ltac:(fun hyp => elim_ind hyp || induction hyp) H.

  (* Another exemple : even induction goes wrong *)
  Parameter X : Z -> Z -> Type.
  Parameter zero : forall A B,   X A B.
  Parameter one  : forall A,     X A A.
  Set Implicit Arguments.

  Inductive eval :  forall A B u, t_prop A B u -> X A B -> Prop :=
  | eval_eq : forall A, eval (t_prop_eq A) (one A : X A A)
  | eval_neq : forall A B, eval (t_prop_neq A B) (zero A B: X A B)
    .

  Lemma ex_ind_prop : forall A B (u : t_prop A B Neq), eval u (zero A  
B) .
    intros A B u. dependent induction u. constructor.
  Qed.>>

Hope this helps,
-- Matthieu