Stream: Coq users

Topic: Custom induction principle for inductive proposition

Joshua Grosso (Oct 24 2020 at 17:02):

I'm trying to define a custom induction principle for an inductive proposition that's stronger than the autogenerated one. I can't use structural recursion, so I'm trying to define a measure with which to use well-founded recursion. However, because defining the measure requires inspecting a value within Prop, I can't define a Fixpoint as usual (since I'm trying to return a nat). Is there a good solution, or should I try to define my inductive proposition differently (i.e. to use structural recursion)?

Joshua Grosso (Oct 24 2020 at 18:57):

Ah, maybe I can define the inductive proposition to be in Type instead of Prop....

Paolo Giarrusso (Oct 24 2020 at 19:56):

Yeah you can't define a useful measure from Props to Types. Here's a reminder of why:

Inductive fakeBool : Prop := | ftrue | ffalse.

Lemma okay : true = false -> False.
Proof. discriminate. Qed.
Lemma nope : ftrue = ffalse -> False.
Proof. Fail discriminate. Abort.

Require Import ProofIrrelevance.
Print ProofIrrelevance.

Lemma fakeBool_irrelevant : ftrue = ffalse.
Proof. apply proof_irrelevance. Qed.

Print Assumptions fakeBool_irrelevant.
(* Axioms:
proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2 *)

Paolo Giarrusso (Oct 24 2020 at 20:00):

in particular, if the following unfake were allowed:

Fail Definition unfake (fb : fakeBool) :=
  match fb with
  | ftrue => true
  | ffalse => false
  end.

then from proof_irrelevance (in particular, fakeBool_irrelevant) you could deduce false = unfake ffalse = unfake ftrue = true.

Paolo Giarrusso (Oct 24 2020 at 20:01):

you sound like you probably know part of this — but I think this code makes it clearer why you _have_ to move your Prop to Type.

Paolo Giarrusso (Oct 24 2020 at 20:04):

I wonder a bit if you could try to define a measure to fakeNat : Prop, but given the above, I'd be surprised if you could show that fake_le : fakeNat -> fakeNat -> Prop is well founded.

Joshua Grosso (Oct 24 2020 at 20:14):

Just out of curiosity, does defining a measure from Props to Types become safe if one doesn't assume proof irrelevance? Or is it still an issue assuming the existence of any type for which proof irrelevance can be manually proved (which is true IIRC)?

Shea Levy (Oct 24 2020 at 20:52):

If proof irrelevance can be directly proved and your indices are not in Prop, you can in fact define the stronger induction principle (essentially by matching on/recursing on the indices)

Paolo Giarrusso (Oct 24 2020 at 21:13):

Coq only lets you do things that remain safe if proof irrelevance gets postulated later.

Paolo Giarrusso (Oct 24 2020 at 21:14):

In principle, it should be possible to postulate the negation of proof irrelevance, but that doesn’t mean it’s useful.

Paolo Giarrusso (Oct 24 2020 at 21:15):

Under “not-irrelevance “ you could probably eliminate Prop into Type, but I don’t think Coq lets you.

Paolo Giarrusso (Oct 24 2020 at 21:15):

However, rather than use such a postulate, you can mostly just avoid using Prop.

Paolo Giarrusso (Oct 24 2020 at 21:17):

However, if you never use Prop, you lose impredicativity, unless you switch to impredicative Set, which is anticlassical.

Paolo Giarrusso (Oct 24 2020 at 21:19):

But I think that’s unavoidable: in a setting like Coq, proof-relevant impredicativity is necessarily anticlassical — see https://github.com/FStarLang/FStar/issues/360.

Paolo Giarrusso (Oct 24 2020 at 21:20):

(crucially, when I say “in a setting like Coq”, I imply that in Coq having proof relevance also gives you large eliminations)

Paolo Giarrusso (Oct 24 2020 at 21:25):

I’m sure weaker settings with the same problem exist — even for (set-theoretic) models of System F, supporting both impredicativity and booleans in a setting with excluded middle leads to paradoxes (which goes back to “Polymorphism is not set-theoretic” and “Polymorphism is set-theoretic, constructively”, but at least the latter is not an easy read)

Jakob Botsch Nielsen (Oct 24 2020 at 21:26):

An alternative that might work might be to define a type that relates the thing in prop to its size, i.e. something like

Inductive foo : Prop :=
| foo_a : foo -> foo -> foo.
Inductive foo_size : foo -> nat -> Type :=
| foo_a_size f1 f2 n1 n2 :
  foo_size f1 n1 ->
  foo_size f2 n2 ->
  foo_size (foo_a f1 f2) (S (n1 + n2)).

I have had this problem before and thought about this solution, but I have always just ended up moving things to Type because it is way more convenient and does not require inversions.

Paolo Giarrusso (Oct 24 2020 at 21:27):

So you’d use structural induction on foo_size, or on its index?

Jakob Botsch Nielsen (Oct 24 2020 at 21:29):

I suppose you want to induct on the number with strong induction to be able to apply it to something that's not just subterms.

Paolo Giarrusso (Oct 24 2020 at 21:29):

Actually, it does sound like from foo_size you could try defining a well-founded relation on foo.

Paolo Giarrusso (Oct 24 2020 at 21:31):

But I’d guess my earlier argument should still forbid this (for relations in Prop at least), so I wonder where you’d end up.

Jakob Botsch Nielsen (Oct 24 2020 at 21:32):

I don't think you can ever extract the number, no, but you can prove something like
forall f, exists n, foo_size f n
and then you get to work with n without having squashed it when you aren't in large contexts

Paolo Giarrusso (Oct 24 2020 at 21:42):

Yeah the wf relations would be exists m n, m <= n and foosize f1 m and foosize f2 n (sorry for notation, I’m on ipad)

Last updated: Oct 13 2024 at 01:02 UTC