The Coq mailing list

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

Hi,

Am Mittwoch, den 16.05.2018, 18:12 +0200 schrieb Pierre Courtieu:
> I have several questions:
> 1) do you use functional induction in the proof of foo_ind_aux? It seems to
> be a good idea.

no, foo is defined in a way that functional induction is not available.
 It is actually defined using a classical fixpoint operator in the
style of https://gitlab.inria.fr/charguer/tlc/blob/master/src/LibFix.v

> 2) I would expect (P x (foo x)) for the conclusion of foo_ind_aux instead
> of (P (foo x)). Did you just simplify your example or do you manage to use
> it like that?

Well spotted. So far, P (foo x) is sufficient, but I do expect that I
might have to change that, depending on how my downstream proofs go. 

Luckily, this whole scheme makes refactoring the induction principle
simpler, as there are less places where I need to change this.

> 3) the shape of this "functional scheme" is probably not accepted by
> "induction ... using foo_ind". Does it? Or do you have to apply the
> principle by hand?

Right now I use

    revert e captured.
    apply go_ind.

in my lemma (e and captured are the actual parameters to my function
go); changing that to

    induction e, captured using go_ind.

gives me “Cannot recognize an induction scheme.”. So far I am happy
with apply; how would I have to change the lemma so that [induction]
works, and what would I gain from it?

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