The Coq mailing list

[AUGER <Cedric.Auger AT lri.fr>]

Le Tue, 25 May 2010 13:52:08 +0200, Martijn Vermaat <martijn AT vermaat.name>  
a écrit:

> Hello all,
>
> I stumbled upon a strange (to me) problem with dependent destruction (or
> dependent induction for that matter) where it gets stuck in a cycle.
>
> I tracked down the problem to the repeated invocation of
> simplify_one_dep_elim, which keeps generating the same simple equality.
>
> The context is pretty involved, so I will try to simplify what happens
> here and provide more details if they are asked for. For lack of
> creativity, I will simply use _ wherever I leave out details.
>
> We start with a hypothesis H on a inductive predicate E and a goal G:
>
>   H : E _ _
>   ============================
>    G
>
> After 'generalize_eqs H' we get
>
>   H : E _ _
>   ============================
>    _ = _ -> _ = _ -> _ ~= _ -> G
>
> where H is now simplified, as expected. Now 'destruct H' gives us three
> cases, of which we are interested in the second one. The first
> invocation of simplify_one_dep_elim adds two dependent pair equalities
> to the goal, I will show the first:
(A)
>   ============================
>    existT _ p (existT _ a x) = existT _ q (existT _ a y) ->
>    ... -> G
>
> All two subsequent simplify_one_dep_elim invocations will generate the
> simple equality p = q and introduce it to the context, so we get
>
>   ============================
>    p = q ->
>    existT _ p (existT _ a x) = existT _ q (existT _ a y) ->
>    ... -> G
>
> and then
(B)
>   x : p = q
>   ============================
>    existT _ p (existT _ a x) = existT _ q (existT _ a y) ->
>    ... -> G
>
> and after another two invocations
>
>   x0 : p = q
>   x : p = q
>   ============================
>    existT _ p (existT _ a x) = existT _ q (existT _ a y) ->
>    ... -> G
>
> and so on, each time introducing the same equality as x1, x2, etc.
>
> Now I know close to nothing about how this all works, but I'm guessing
> that the problem is in the nested use of existT.

Can you explain what you expected to get?
At (B) step you have the same thing as in (A) (having just an equation  
more).
So it is normal, to have the same behaviour then.

We don't know much of your goal, so we can't really help.
Maybe that at step (B) you don't need the first equality of your goal  
anymore,
and should "intros _." to get rid of it, then perform a "case x." after  
reverting all hypotheses using "q"
(or a "subst." if you don't mind getting awful proof terms) and continue.
You should also tell the library you are using; according to Coq reference  
manual, "simplify_one_dep_elim"
is not a standard tactic (my Coq version >= 8.2 didn't recognized it at  
all).

If you need to prove also that "x = y" to continue, you will need more  
things
(by the way, don't mess with variables and hypotheses, you use "x" both as  
a hypothesis of type "p=q" and a parameter of "existT").
Of course you can't prove it as it doesn't type-check, take a look at  
JMeq, or this piece of code:


Coq < Lemma L1: forall A (P: A -> Type) x y z t, existT P x y = existT P z  
t -> exists H: P x = P z, (match H in (_=b) return b -> Prop with  
refl_equal => fun t => y = t end) t.
1 subgoal

  ============================
   forall (A : Type) (P : A -> Type) (x : A) (y : P x) (z : A) (t : P z),
   existT P x y = existT P z t ->
   exists H : P x = P z,
     match H in (_ = b) return (b -> Prop) with
     | refl_equal => fun t0 : P x => y = t0
     end t

L1 < intros.
1 subgoal

  A : Type
  P : A -> Type
  x : A
  y : P x
  z : A
  t : P z
  H : existT P x y = existT P z t
  ============================
   exists H0 : P x = P z,
     match H0 in (_ = b) return (b -> Prop) with
     | refl_equal => fun t0 : P x => y = t0
     end t

L1 < inversion_clear H.
1 subgoal

  A : Type
  P : A -> Type
  x : A
  y : P x
  z : A
  t : P z
  ============================
   exists H : P x = P (projT1 (existT (fun x0 : A => P x0) x y)),
     match H in (_ = b) return (b -> Prop) with
     | refl_equal => fun t0 : P x => y = t0
     end (projT2 (existT (fun x0 : A => P x0) x y))

L1 < simpl.
1 subgoal

  A : Type
  P : A -> Type
  x : A
  y : P x
  z : A
  t : P z
  ============================
   exists H : P x = P x,
     match H in (_ = b) return (b -> Prop) with
     | refl_equal => fun t0 : P x => y = t0
     end y

L1 < exists (refl_equal _).
1 subgoal

  A : Type
  P : A -> Type
  x : A
  y : P x
  z : A
  t : P z
  ============================
   y = y

L1 < split.
Proof completed.

L1 < Qed.
intros.
inversion_clear H.
simpl in |- *.
exists (refl_equal _).
split.

L1 is defined

> Is this something simplify_one_dep_elim cannot handle? Could I adjust
> the tactic simplify_one_dep_elim_term in some way?
>
> Or is this a sign there is something wrong with my development?
>
> Thanks for any help,
> Martijn


--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay