Recursive RBSet in an inductive

Stream: new members

[Harry Goldstein]

Hi all, I was here a few days ago asking about putting recursive lists in inductives, now I'm trying to put recursive RBSets in inductives. The problem is that I can't get the Ord instances to work out:

import Batteries.Data.RBMap.Basic
open Batteries (RBSet)

instance [Ord α] : Ord (List α) :=
  let rec aux
    | [], [] => Ordering.eq
    | [], _ => Ordering.lt
    | _, [] => Ordering.gt
    | a::as, b::bs => match Ord.compare a b with
      | Ordering.eq => aux as bs
      | o => o
  { compare := λ x y => aux x y }

instance [Ord α] : Ord (RBSet α Ord.compare) := by
  refine { compare := λ x y => Ord.compare x.toList y.toList }

inductive Value : Type :=
  | unit
  | map (m : RBSet Value Ord.compare)
deriving Ord

This should be valid in theory (the Ord instance is well-defined) but I can't tell if there's a way to convince Lean. Would love advice if you have any.

[Bbbbbbbbba]

I'm not sure the problem is in the Ord instance, because changing to   | map (m : RBSet Value fun x y => Ordering.eq) gives the same error message ((kernel) arg #1 of 'Value.map' contains a non valid occurrence of the datatypes being declared).

[Bbbbbbbbba]

I wonder if it helps to first define

inductive Value : Type :=
  | unit
  | map (m : Batteries.RBNode Value)

and define the well-formedness of a Value instance later.

[Henrik Böving]

Yes the RBNode approach is the way to go here.

[Notification Bot]

Harry Goldstein has marked this topic as resolved.

[Harry Goldstein]

Got it, thanks!

[Notification Bot]

Harry Goldstein has marked this topic as unresolved.

[Harry Goldstein]

Hmm, I think there may still be an issue. If I define my well-formedness condition as a separate inductive, the proof that recursively contained values are actually well-formed can't be used for computation:

inductive Value.WF : Value → Prop
  | wf_unit : WF Value.unit
  | wf_map :
    (∀ x ∈ m, WF x) →
    m.WF Ord.compare →
    WF (Value.map m)

def recursive : {v : Value // v.WF} → {v : Value // v.WF}
  | ⟨Value.unit, h⟩ => ⟨Value.unit, h⟩
  | ⟨Value.map m, h⟩ => by
    refine ⟨Value.map (RBNode.map (λ v => recursive v) m), ?_⟩

In that last line, I can't prove that v is a {v : Value // v.WF} because in order to do that I'd need to pattern match on h (which doesn't seem to be allowed).

[Bbbbbbbbba]

But one problem is that in refine ⟨Value.map f m), ?_⟩, f must take any v : Value as its argument, without the hypothesis v ∈ m so we cannot assert that the output of f is well-formed. Maybe there is an alternate version (or a better use pattern) of map that solves this problem.

[Harry Goldstein]

Even if we could show that v ∈ m, I'm not sure we could actually get to the proof that it is a valid Value, but yes, that's an issue too.

[Bbbbbbbbba]

This is where I got to

def recursive : {v : Value // v.WF} → {v : Value // v.WF}
  | ⟨Value.unit, h⟩ => ⟨Value.unit, h⟩
  | ⟨Value.map m, h⟩ => by
    have f := λ v => recursive ⟨v, by
      cases h with
      | wf_map h0 h1 =>
        have hv : v ∈ m := sorry
        exact h0 v hv
    ⟩
    let f0 := λ v => (f v).val
    refine ⟨Value.map (RBNode.map f0 m), ?_⟩
    constructor
    . intro x hx
      have hmap: ∃v ∈ m, x = f0 v := sorry
      match hmap with
      | ⟨v, ⟨hv0, hv1⟩⟩ =>
        rw [hv1]
        exact (f v).property
    . show RBNode.WF compare (RBNode.map f0 m)
      sorry
    decreasing_by sorry

[Mario Carneiro]

To do this you probably need something like docs#List.attach for RBNode, which can then be composed with RBNode.map so that you have a condition to make the descent well founded. Ping @Joachim Breitner : this is another instance of the general problem where proving theorems about nested inductives requires some user-extensible mechanism for doing the equivalent of the ite -> dite replacement trick to get more assumptions in the context when doing a recursive call via map