The Coq mailing list

[Martijn Vermaat <martijn AT vermaat.name>]

Thank you for your help!

Op woensdag 26-05-2010 om 13:11 uur [tijdzone +0200], schreef AUGER:
> 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).

Sorry if that was unclear. I am using Coq 8.3 beta (or SVN trunk) and
the Coq.Program.Equality module. In this module, the dependent
destruction tactic is defined, using the simplify_one_dep_elim tactic.

I managed to create some sort of minimal test case (which does not make
sense semantically at all) that I think still contains the same basic
problem. It is attached to this message.

>From this test case, I conclude that the problem is that the term I
called p in my original message contains an application of a fixpoint
where the structure of the recursive argument is unknown (here pf
applied to q).

This is of course a hint how we can solve this (destruct q), as shown in
the attachment.

I think I managed to do the same thing in my original lemma.
Unfortunately, I am still not able to proof it, but I think this is
unrelated to my question here.

cheers,
Martijn

(*
  Trying to find a minimal test-case where dependent destruction fails.

  The definitions do not make any sense. The point of the test lemma is not
  to prove it, but to show that dependent destruction on the hypothesis fails.
*)


Require Import Equality.


Set Implicit Arguments.


Inductive s : nat -> Type :=
  | C : forall n (r : s n) m, s m.

Fixpoint pf n (r : s n) {struct r} : nat := n.

Inductive le : forall n (r : s n) m (q : s m), Prop :=
  | le_C : forall m (q : s m) (r : s (pf q)),
             le (C r m) q.

Lemma test1 :
  forall n (r : s n) m (q : s n),
    le (C r m) q -> n = m.
Proof.
intros n r m q H.
(*
   At this point, we would like to use dependent destruction on H, but it
   fails because the underlying simplify_one_dep_elim cycles.
   So we try to do it manually.
*)
(* dependent destruction H. *)
generalize_eqs H.
destruct H.
simplify_one_dep_elim.
simplify_one_dep_elim.
simplify_one_dep_elim.
simplify_one_dep_elim.
simplify_one_dep_elim.
simplify_one_dep_elim.
simplify_one_dep_elim.
simplify_one_dep_elim.
simplify_one_dep_elim.
(* ... *)
Admitted.

(* Let's try again *)

Lemma test2 :
  forall n (r : s n) m (q : s n),
    le (C r m) q -> n = m.
Proof.
intros n r m q H.
generalize_eqs H.
destruct H.
(*
   Here we can save the proof by destructing q. The point is that (pf q)
   then simplifies to m.
*)
destruct q.
simplify_one_dep_elim.
simplify_one_dep_elim.
simplify_one_dep_elim.
reflexivity.
Qed.