2
$\begingroup$

I want to declare a property that a recursive structure was constructed using a smart constructor. The smart constructor mainly constructs with 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)
    (reader: Bool)
  : Desc
  deriving Repr

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

def Desc.get_hash (desc: Desc): UInt64 :=
  match desc with
  | ⟨ _, hash, _, _ ⟩ => hash

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.get_hash 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 reader
    → hash = hash_with_name name params
    → reader = true \/ reader = List.any params get_reader
    → Forall IsSmart params
    → IsSmart d

I am getting the following 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.

Secondly is there a Forall for lists in the standard library or core lean somewhere? The closest thing I could find was VecPred.

$\endgroup$

2 Answers 2

1
$\begingroup$

Indeed, the issue comes from your use of Forall. What you want is called a nested inductive type, ie an inductive type I where I appears inside another inductive type L in one of its constructors. Here I is IsSmart, and the other inductive type is Forall.

Lean 4's manual claims that these are supported, and indeed in the case of Desc which is also nested (because of the param field), things work fine. My guess is that your issue comes from the fact that both IsSmart and Forall are inductive predicates, and thus have indices. This makes compiling nested types back to mutual ones, as Lean does in the simpler case of Desc, much more tricky, and is why your definition is not supported.

My advice would be trying to define this mutual inductive type by hand, ie define a version of Forall specialized to List Desc and IsSmart mutually with IsSmart itself. You can show after the fact that this specialized version is equivalent to Forall IsSmart (List Desc). This is more or less the boilerplate that would be automatically generated by Lean in the simple case where is accepts a nested definition.

Note that other proof assistants would accept your definition as is. Here is code for Coq (I did not define the hash_with_name function, as it is not relevant to the issue):

Require Import String List.

Inductive Desc :=
  | intro
    (name: string)
    (hash: nat)
    (params: list Desc)
    (reader: bool).

Definition get_reader d := match d with | intro _ _ _ r => r end.

Variable hash_with_name : string -> list Desc -> nat.

Inductive IsSmart (d: Desc): Prop :=
  | isSmart: forall
    (name: string)
    (params: list Desc)
    (hash: nat)
    (reader: bool),
    d = intro name hash params reader
    -> hash = hash_with_name name params
    -> reader = true \/ reader = existsb get_reader params
    -> Forall IsSmart params
    -> IsSmart d.

I did not try with Agda but it is generally even more permissive than Coq in terms of inductive definitions.

$\endgroup$
2
0
$\begingroup$

The solution is to index the Desc in IsSmart

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

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

I think there is still room to improve the error message, but at least I am unblocked

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.