Mutual definition with axiom / forward declaration

Stream: lean4

[bruno cuconato]

Hello,

I am trying to write type whose constructor includes a predicate on this type, but I do not want to go into the definition of this predicate, I take it as given. In Agda I can write

data MyType : Set

postulate
  MyPredicateOnType : MyType → MyType → Set

data MyType where
    init : MyType
    cons : (e1 e2 : MyType) → MyPredicateOnType e1 e2 → MyType

But I fail to write the Lean equivalent, as Lean does not seem to support this kind of forward declaration (see this thread https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/forward.20declarations), and I do not seem to be able use an axiom or an opaque definition in a mutual block.

A workaround is defining two types, with the first one not including the predicate, whereas the second one would include it, something like

inductive MyType1 : Type where
| init : MyType1
| cons : MyType1 → MyType1 → MyType1

axiom MyPredicateOnType : MyType1 → MyType1 → Prop

inductive MyType2 : Type where
| init : MyType1 → MyType2
| cons : (e1 e2 : MyType1) → MyPredicateOnType e1 e2 → MyType2

But I'd prefer a clear solution. Is there any? Thank you!

[Timo Carlin-Burns]

I think the standard approach here is approximately what you've proposed:

1. Define the inductive type without restricting to any predicates
2. Define a recursive validity predicate on the initial inductive type
3. Use the subtype defined by the validity predicate instead of the base type thereafter

The Lean 4 manual has an example of this for a binary search tree data structure

[Timo Carlin-Burns]

Note that MyType2 as you've defined it above isn't exactly what you want: it only ensures that the outermost cons-pair satisfies MyPredicateOnType, not that every cons-pair does so recursively

[Timo Carlin-Burns]

I doubt the agda behavior here was sound. If you just want to emulate what you were doing in Agda and bypass Lean's soundness checks, I imagine that one of your original ideas would work with unsafe inductive

[bruno cuconato]

Thank you @Timo Carlin-Burns! That helps. Out of curiosity, do you perchance have an example of how this Agda behaviour can lead to an unsoundness?

[Timo Carlin-Burns]

Lean has a number of limitations on inductive type definitions that mostly boil down to something called "strict positivity". "strict positivity" has a precise definition in Theorem Proving in Lean but basically means that you only refer to your type within its own definition in certain positions:

• As the return type of a constructor
• As an argument to a constructor
• As the return type of a function which is an argument to a constructor

So e.g. the following is fine:

inductive MyInfiniteTree : Type where
| leaf : MyInfiniteTree
| node : (Nat -> MyInfiniteTree) -> MyInfiniteTree -- each node has infinite children
--               ^ occurs as return type, not input type, of a function

An example which is not fine is

inductive Bad : Type where
| ofFn : (Bad -> Bool) -> Bad

Here ofFn is a constructor, and all constructors are injective, so we have an injective function from (Bad -> Bool) -> Bad which is impossible by cantor's diagonal argument.

I don't know how to construct an example where you would try to define a type and a predicate on it in a mutual inductive fashion and it would lead to inconsistency, but in general, the strict positivity check means you're not really supposed to use your type as an input to anything while you're defining it.

[bruno cuconato]

Thanks for the explanation. Agda does not accept this Bad example, but I guess it accepts my former example because the expression MyPredicateOnType e1 e2 has type Set. So I don't see why the strict positivity check would be a problem here, and thus I am led to think (maybe wrongly, I'll gladly take further corrections/explanations!) that Lean would accept my Lean code if I could forward declare MyPredicateOnType or mutually define it.

[Floris van Doorn]

I believe Agda supports both inductive-inductive datatypes and inductive-recursive datatypes. Lean accepts neither of them.

Your example is an inductive-inductive datatype (at least if MyPredicateOnType is data instead of a postulate). You can encode these in Lean, see for example this thread. Inductive-recursive datatypes significantly increase the proof-theoretic strength of a system, hence cannot be encoded in Lean in general.

[Mario Carneiro]

@bruno cuconato Here's a basic example of issues that could come up if you aren't careful what is allowed in the definition of MyPredicateOnType:

mutual

inductive MyType : Type where
| init : MyType → MyType
| cons : (e1 e2 : MyType) → MyPredicateOnType e1 e2 → MyType

def MyPredicateOnType : MyType → MyType → Prop :=
  fun a b => ∀ e h, e = MyType.cons a b h → False

end

This is only a lightly obfuscated version of the liar paradox:

def MyPredicateOnType : MyType → MyType → Prop :=
  fun a b => ¬ MyPredicateOnType a b

which causes inconsistency in any system that allows the definition

[bruno cuconato]

Thank you @Floris van Doorn and @Mario Carneiro ! That helped me understand why I should follow the Lean modus operandi and do something similar to the BST example Timo linked. I don't actually need inductive-inductive or inductive-recursive datatypes for what I'm doing after all :)