The Coq mailing list

[Joachim Breitner <mail AT joachim-breitner.de>]

Hi,


Am Mittwoch, den 16.05.2018, 11:55 -0400 schrieb ikdc:
> The Derive extension does what you want.
> 
> https://coq.inria.fr/refman/addendum/miscellaneous-extensions.html
> 

thanks for the hint. It works great in a small example:

   Require Import Coq.derive.Derive.

   Section foo.
   Variable (P : nat -> Prop).
   Derive HTy
   SuchThat (forall (H : HTy), forall n, P n)
   As nat_ind.
   Proof.
     intros.
     pose proof H as IH1. eapply proj1 in IH1. eapply proj2 in H.
     rename H into IH2.
     induction n.
     * refine IH1.
     * revert n IHn. refine IH2.
   Qed.
   End foo.

I can even fix the type to no longer mention HTy:

   Definition nat_ind' :=
     ltac:(let ty := type of nat_ind in
           let ty' := eval unfold HTy in ty in
           exact (nat_ind : ty')).
   Check nat_ind'.
   (* nat_ind'
      : forall P : nat -> Prop, P 0 /\ (forall n : nat, P n -> P (S n)) -> 
forall n : nat, P n
   *)

Unfortunately, when when I do it in my real, big example, I get this:

   Anomaly "the kernel does not support existential variables." Please
   report at http://coq.inria.fr/bugs/.

And I am not sure what aspect is causing that (surely not just size).


Tangentially, it would be even more useful if I could define more than
one at the same time:
    
   Section foo.
   Variable (P : nat -> Prop).
   Derive H1Ty H2Ty
   SuchThat (forall (Hbase : H1Ty) (Hstep : H2Ty), forall n, P n)
   As nat_ind.
   Proof.
     intros.
     induction n.
     * refine Hbase.
     * revert n IHn. refine Hstep.
   Qed.
   End foo.

Cheers,
Joachim

-- 
Joachim Breitner
  
mail AT joachim-breitner.de
  http://www.joachim-breitner.de/

Attachment: signature.asc
Description: This is a digitally signed message part