Recursive Forall gives error unexpected inductive type occurrence

[awalterschulze]

Prerequisites

• [X] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

I want to declare a property that a recursive structure was constructed using a smart constructor. The smart constructor mainly constructs a hash field and the property would allow me to trust the hash field's value was properly precomputed.

inductive Desc where
  | intro
    (name: String)
    (hash: UInt64)
    (params: List Desc)
  : Desc
  deriving Repr

def hash_with_name (_name: String) (_params: List Desc): UInt64 := 0 -- mock hash function

def Desc.intro_func (name: String) (params: List Desc): Desc :=
  Desc.intro
    name
    (hash_with_name name params)
    params

inductive Forall {α : Type u} (p : α → Prop) : List α → Prop
  | nil  : Forall p ([] : List α)
  | cons : ∀ {x xs}, p x → Forall p xs → Forall p (x :: xs)

inductive IsSmart (d: Desc): Prop
  | isSmart: ∀
    (name: String)
    (params: List Desc)
    (hash: UInt64)
    (reader: Bool),
    d = Desc.intro name hash params
    → hash = hash_with_name name params
    → Forall IsSmart params
    → IsSmart d

I get an error: error: unexpected inductive type occurrence

I only get the error if I include the line → Forall IsSmart params. So I suspect it has something to do with two recursive inductive types calling each other.

I first asked about this on stack exchange, thinking I was doing something wrong. https://proofassistants.stackexchange.com/questions/2045/unexpected-inductive-type-occurrence-error-for-recursive-inductive-type/2057#2057

I also tried their suggestion of using mutual, but that didn't work https://gist.github.com/awalterschulze/f3e95406063c0e5e6bff97343c93b2b0

I am wondering if this is a bug in Lean or if I am doing something wrong?

Steps to Reproduce

1. Add the code to a file in VS Code
2. See the error in the infoview

Expected behavior: [What you expect to happen]

I expect this to compile without any issues, since it is possible to do this in Coq:

https://github.com/katydid/proofs/blob/old-coq/src/Symbolic/Ast/SmartFunc.v#L8-L18

Actual behavior: [What actually happens]

error: unexpected inductive type occurrence

Reproduces how often: [What percentage of the time does it reproduce?]

100%

Versions

Lean (version 4.0.0-nightly-2023-03-09, commit 0cc9d7a43de7, Release)

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

[hargoniX]

Have you considered using computed fields for this? (example: https://github.com/leanprover/lean4/blob/8a302e6135bc1b0f1f2901702664c56cd424ebc2/src/Lean/Expr.lean#L461-L464) they allow you define functions on your inductives that get pre computed upon creation of an inductive value so they behave like a field but you do not have to do the proofs you are attempting about them.

[awalterschulze]

I don't think computed_field will work, but I tried it

inductive Desc where
  | intro
    (name: String)
    (params: List Desc)
  with
  @[computed_field]
  hash : @& Desc → UInt64
    | .intro name params => hash_list (31 * 17 + hash_string name) (List.map (fun d => d.hash) params)
  deriving Repr

For this I do need to add the whole hash function, which I was trying to avoid, to keep the example small, but it isn't that big

def hash_list (innit: UInt64) (list: List UInt64): UInt64 :=
  List.foldl (fun acc h => 31 * acc + h) innit list

def hash_string (s: String): UInt64 :=
  hash_list 0 (List.map (Nat.toUInt64 ∘ Char.toNat) (String.toList s))

def hash_with_name (name: String) (params: List Desc): UInt64 :=
  hash_list (31 * 17 + hash_string name) (List.map Desc.hash params)

Unfortunately I got an error: error: computed fields require at least two constructors

Also I got another error, which might be fixable:

fail to show termination for
  Desc.hash
with errors
structural recursion cannot be used

failed to prove termination, use `termination_by` to specify a well-founded relation

[hargoniX]

The second one is fixable. It is because Lean's termination checker is right now not capable of understanding that mapping a function recursively onto a list does terminate on its own.

I do not know why Lean requires a thing to have at least two ctors for a computed field to work out. Maybe @Kha or @gebner ?

[awalterschulze]

It looks like it is possible to write

inductive IsSmart : Desc → Prop
  | isSmart: ∀
    (name: String)
    (params: List Desc)
    (hash: UInt64),
    desc = Desc.intro name hash params
    → hash = hash_with_name name params
    → (∀ param, param ∈ params → IsSmart param)
    → IsSmart desc

And not get any of the problems

I think the issue can now be renamed to something to request a more descriptive error message that might guide the user to this solution?

[awalterschulze]

I found the solution on Zulip chat https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20lean4.20struggling.20with.20recursive.20properties

[ammkrn]

I found the solution on Zulip chat https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20lean4.20struggling.20with.20recursive.20properties

@awalterschulze if the solution in the Zulip thread was satisfactory, please consider closing this issue.

[awalterschulze]

The solution on Zulip chat unblocks me.

I am keeping it open because maybe:

• you find the error message can be improved or
• you think this can be fixed and not need to give an error