The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Merlin,

 

in case the question is how to explicitly apply well founded induction in your case, it might look something like this:

 

Require Import Arith.

 

Definition complexity {P E : Type} (p : list P) (ed : E) : nat := length p.

 

Theorem test (P E : Type) (p : list P) (ed : E) : p = p.

Proof.

  induction p using (well_founded_induction (Arith.Wf_nat.well_founded_ltof _ (fun p => complexity p ed))).

  unfold ltof in *.

 

This gives you the induction hypothesis:

 

P : Type

E : Type

ed : E

p : list P

H : forall y : list P, complexity y ed < complexity p ed -> y = y

______________________________________(1/1)

p = p

 

Is such a hypothesis more useful for you?

 

Best regards,

 

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928