Stream: Coq users

Topic: Making induction on proof tree standard


view this post on Zulip Jacob Salzberg (Jan 20 2024 at 17:04):

Hi guys,
is there a way to translate induction over proof trees into more standard math, without talking about inductively defined types or fixpoints?
For example, I have an inductively defined bigstep transition relation. I can show by induction over the proof trees that if you add a timer that increases with every tick, then the values of the program variables will be unchanged.
This is a very coq-specific technique, because the property to be proved starts out:
forall input output (step : Bigstep input output), ...

Is there any way to make this argument more "pencil and paper?"
thanks

view this post on Zulip Jacob Salzberg (Jan 20 2024 at 17:05):

Do you usually make this argument a pencil and paper argument by defining a custom logic?

view this post on Zulip Patrick Nicodemus (Jan 20 2024 at 18:10):

I honestly think that "standard math" is pretty field-specific and sometimes the standard techniques in a given field aren't necessarily well translateable into other areas of math. Programming language theory and proof theory are their own areas of math and they have their own characteristic styles of argument. "Inductively defined bigstep transition relation" basically just sounds to my ear like a typical phrase you hear in any programming language theory conference paper, not something specific to Coq's logic.

view this post on Zulip Karl Palmskog (Jan 20 2024 at 18:29):

in any HOL-based proof assistant like Isabelle/HOL and HOL4, you can define inductive relations and get the usual induction principles (and more if you want), they generalized this to "bounded natural functors"

view this post on Zulip Pierre Courtieu (Jan 21 2024 at 15:43):

Can you explain a bit more your lemma, its proof, and what you dislike about it please? It is unclear for me.

view this post on Zulip Kenji Maillard (Jan 21 2024 at 22:31):

Classically, you can reduce induction on any inductively defined type to induction on some ordinal, the "height" of the inductive. You can describe this height ordinal by taking the least fixpoint of the following operation: the height of the inductive is the ordinal sum of the height of each constructor, and the height of a constructor is the successor of the suprema of the height of its inductive subterms.
I think we rarely use this kind of encoding in proofs assistants because
1) it saves the work of defining the encoding
2) the direct proofs are often more meaningfull
3) a well-behaved theory of ordinals requires some extensionality principles (e.g. function extensionality, and some quotients may be useful to collapse any well-founded relation to an ordinal)

view this post on Zulip Paolo Giarrusso (Jan 22 2024 at 10:14):

Moreover, for many inductive types, the height is always finite so normal induction on naturals is sufficient — but Kenji's points 1 and 2 still apply. The encoding is explained in more detail, for instance, by Pierce's TAPL textbook, in Sec. 3.3 https://www.cis.upenn.edu/~bcpierce/tapl/

There are audiences for which I would choose such a presentation, but I consider it inferior and I would _not_ use it in programming language venues I'm familiar with.


Last updated: Jun 23 2024 at 05:02 UTC