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)?

Ah, maybe I can define the inductive proposition to be in `Type`

instead of `Prop`

....

Yeah you can't define a useful measure from `Prop`

s to `Type`

s. 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 *)
```

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`

.

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`

.

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.

Just out of curiosity, does defining a measure from `Prop`

s to `Type`

s 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)?

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)

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

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

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

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

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

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.

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

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)

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.

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

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.

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

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.

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

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: Jun 24 2024 at 00:02 UTC