Why are Hyps a tree instead of a list?

Stream: iris-lean

[Michael Sammler]

Currently the proof mode context is defined as a branching tree

inductive Hyps {prop : Q(Type u)} (bi : Q(BI $prop)) : (e : Q($prop)) → Type where
  | emp (_ : $e =Q emp) : Hyps bi e
  | sep (tm elhs erhs : Q($prop)) (_ : $e =Q iprop($elhs ∗ $erhs))
        (lhs : Hyps bi elhs) (rhs : Hyps bi erhs) : Hyps bi e
  | hyp (tm : Q($prop)) (name uniq : Name) (p : Q(Bool)) (ty : Q($prop))
        (_ : $e =Q iprop(□?$p $ty)) : Hyps bi e

In contrast, the proof mode in Rocq is defined as a list.
What is the reason that iris-lean uses a tree instead of a list? Why is the branching useful?
I found https://github.com/leanprover-community/iris-lean/commit/4d812ef740b7559f9a83be590af70dc2a65ee501 , which says

The tree is not assumed to have any particular structure, but it will
typically be a left-leaning list.

Concretely, would it be possible to change the definition of Hyps to something like the following?

inductive Hyps {prop : Q(Type u)} (bi : Q(BI $prop)) : (e : Q($prop)) → Type where
  | emp (_ : $e =Q emp) : Hyps bi e
  | hyp (tm erhs : Q($prop)) (name uniq : Name) (p : Q(Bool)) (ty : Q($prop))
        (rhs : Hyps bi erhs)
        (_ : $e =Q iprop(□?$p $ty ∗ $erhs)) : Hyps bi e

I am asking because using a tree instead of a list makes writing tactics quite a bit more complex. For example, consider the implementation of iassumption. There the implementation of the .sep case is quite complex.

variable {prop : Q(Type u)} (bi : Q(BI $prop)) (Q : Q($prop)) in
def assumptionSlow (assume : Bool) :
    ∀ {e}, Hyps bi e → MetaM (AssumptionSlow bi Q e)
  | _, .emp _ =>
    Pure.pure (.affine q(emp_affine))
  | out, .hyp _ _ _ b ty _ => do
    let fromAssum (_:Unit) := do
      let _ ← synthInstanceQ q(FromAssumption $b $ty $Q)
      let inst ← try? (synthInstanceQ q(Affine $out))
      return .main q(FromAssumption.from_assumption) inst
    let affine (_:Unit) := return .affine (← synthInstanceQ q(Affine $out))
    if assume then
      try fromAssum () catch _ => try affine () catch _ => return .none
    else
      try affine () catch _ => try fromAssum () catch _ => return .none
  | _, .sep _ elhs erhs _ lhs rhs => do
    match ← assumptionSlow assume rhs with
    | .none => return .none
    | .affine _ =>
      match ← assumptionSlow assume lhs with
      | .none => return .none
      | .affine _ => return .affine q(sep_affine ..)
      | .main lpf linst =>
        return .main q(assumption_l $lpf) <| linst.map fun _ => q(sep_affine $elhs $erhs)
    | .main rpf rinst =>
      match ← assumptionSlow false lhs, rinst with
      | .none, _ | .main _ none, none => return .none
      | .affine _, rinst | .main _ (some _), rinst =>
        return .main q(assumption_r $rpf) <| rinst.map fun _ => q(sep_affine $elhs $erhs)
      | .main lpf none, some _ => return .main q(assumption_l $lpf) none

The Rocq implementation of the same tactic is a lot simpler:

Lemma tac_assumption Δ i p P Q :
  envs_lookup i Δ = Some (p,P) →
  FromAssumption p P Q →
  (let Δ' := envs_delete true i p Δ in
   if env_spatial_is_nil Δ' then TCTrue
   else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ'))) →
  envs_entails Δ Q.

[Markus de Medeiros]

I don't know enough to say which way is better, but the "why" is explained in Lars's thesis Screenshot_20250704-061407.png

[Markus de Medeiros]

How does the Rocq proofmode separate the spatial and intuitionistic contexts?

[Remy Seassau]

It's essentially just a pair of lists, one being the spatial environment and the other being the intuitionistic environment (where environment ~= context)

[Markus de Medeiros]

Michael Sammler said:

The Rocq implementation of the same tactic is a lot simpler:

FYI we also have Hyps.findWithInfo (kind of like envs_lookup) and Hyps.remove (kind of like envs_delete). I think iassumption might be inlining and optimizing these?

[Markus de Medeiros]

Remy Seassau said:

It's essentially just a pair of lists, one being the spatial environment and the other being the intuitionistic environment (where environment ~= context)

Ah right, I think I was asking about the wrong thing actually since iris-lean uses two Envs too

[Markus de Medeiros]

Lars' thesis brings up this example:
Screenshot 2025-07-04 at 6.48.17 AM.png

How is this represented in a Rocq iris list?

[Remy Seassau]

My understanding is that you only have multiplicative combination between elements of the list.
So Q₁ ∧ Q₂ would have to be one single element: [ P ; Q₁ ∧ Q₂ ]

[Michael Sammler]

My understanding is that it used to be two lists in the original iris-lean implementation by Lars, but then @Mario Carneiro changed it to use this tree version in this commit. The commit message describes some justification for the change, which makes sense, but I do not understand why iris-lean does not use a more list-like version instead of the tree-structure.

[Markus de Medeiros]

Oh brother, you're right. Sorry for the misunderstanding!

[Mario Carneiro]

it was a performance optimization. It means that you don't have to do as much administrative pushing of variables around. This is actually a performance issue when you have a long context

[Michael Sammler]

I understand that there was a performance optimization in the commit from switching from reduction in the proof to traversing the term at the meta level and not storing the identifiers in the proof term. But I do not see why it is necessary to use a tree with arbitrary branching instead of a left-leaning tree where one side is always a hypothesis for this.

Concretely, would using the following definition for Hyps also work? (This is just a specialized version of the current Hyps where the .sep and .hyp constructors are merged.)

inductive Hyps {prop : Q(Type u)} (bi : Q(BI $prop)) : (e : Q($prop)) → Type where
  | emp (_ : $e =Q emp) : Hyps bi e
  | hyp (tm erhs : Q($prop)) (name uniq : Name) (p : Q(Bool)) (ty : Q($prop))
        (rhs : Hyps bi erhs)
        (_ : $e =Q iprop(□?$p $ty ∗ $erhs)) : Hyps bi e

[Mario Carneiro]

I'm saying there is a performance advantage from not needing to renormalize the shape of the tree to be left leaning, in the underlying expression

[Mario Carneiro]

oh and your list is forcing the expression to be right leaning, which is actually much worse because most action happens at the end of the list so enforcing the wrong lean will add O(n) shuffles on every operation

[Michael Sammler]

Thank you for this answer, though I have to admit I still don't fully understand the situation.

Mario Carneiro said:

I'm saying there is a performance advantage from not needing to renormalize the shape of the tree to be left leaning, in the underlying expression

Is there actually any case where the tree is not full left-leaning? I do not know which Iris tactic would create such a tree. Note that you still need to convert a separation logic expression to a Hyps to add it to the context, which means traversing it, so you don't actually add a full tree at once.

To test this, I modified parseIrisGoal? to check whether the Hyps are left-leaning as follows:

partial def Hyps.isLeaning? {u prop bi} :
    ∀ {s}, @Hyps u prop bi s → Bool
  | _, .emp _ => true
  | _, .hyp _ _ _ _ _ _ => true
  | _, .sep _ _ _ _ lhs rhs =>
    match rhs with
    | .sep _ _ _ _ _ _ => false
    | _ => lhs.isLeaning?

def parseIrisGoal? (expr : Expr) : Option IrisGoal := do
  let some #[prop, bi, P, goal] := expr.appM? ``Entails' | none
  let u := expr.getAppFn.constLevels![0]!
  let ⟨e, hyps⟩ ← parseHyps? bi P
  if !hyps.isLeaning? then
    none
  else
    some { u, prop, bi, e, hyps, goal }

With this change, everything still builds. So it seems like at least all tactics that currently exist only create left-leaning Hyps.

Mario Carneiro said:

oh and your list is forcing the expression to be right leaning, which is actually much worse because most action happens at the end of the list so enforcing the wrong lean will add O(n) shuffles on every operation

Are you saying that with this definition of Hyps the top most .hyp in Hyps would be the displayed at the top of the goal? In that case one indeed wants to make it left-leaning instead of right-leaning such that tactics first look at the hypothesis at the bottom not at the one at the top. (But that is an easy change.)

[Mario Carneiro]

the hypotheses are ordered: the ones on the left appear on top of the hypothesis goal view. So you would want the list to be left leaning.

[Mario Carneiro]

As for whether there are any tactics that don't produce a left-leaning list, no I never got around to that. These observations actually stem from some work I did in a different system that had analogous concerns. I think there might be advantages to spontaneously introducing a tree structure to keep it balanced, but beyond that if you do operations that pull items out of the middle that can be a good reason to introduce a branch there. It's easier to implement the version of the tactic that doesn't do this, but you can get quadratic overhead in bad cases.

When it comes to traversing the list it doesn't really matter whether it's a tree or not, they are both linear. But the proof term will end up proportional to the depth of the target item if you are pulling one out.

[Mario Carneiro]

Lean itself is using a considerably more sophisticated data structure for the actual local context (a persistent hash map), so I feel the least we can do is try to make the linear context also a bit more treeish.

[Michael Sammler]

I see, thanks for the explanation. I would be interested to hear if there is any tactic in the Iris proof mode that would actually generate a tree. (See here for the list of tactics.)

The idea of replacing Hyps with something more efficient like a hashmap also sounds intriguing. For this, I guess it would be good if Hyps has a clearly defined interface. At the moment, tactics like assumption are a bit of a mess (as shown in the initial message of this thread), but with a proper interface for Hyps this could be a lot nicer (and then one could also more easily change out the definition of Hyps).

[Mario Carneiro]

Because the term has to be part of the expression, you don't have the shortcut of being able to use different .fvar names to refer to hypotheses directly, and as a result the programming model is closer to a pure functional setting, where balanced trees represent the best case scenario. If you assume searches not in the kernel are cheap, then it doesn't even need to be a sorted tree, you just reach in and grab the element you want because you know where it is. The limiting cost becomes the number of tree rotations you have to do to move an element to the root and that's basically linear in the max depth.

So you would think the optimal would be a balanced binary tree, but it's not actually because it's O(log n) to add elements to a perfect binary tree (or worse depending on how much perfection you ask for), while you can get O(1) with a left leaning path. It turns out you can actually get the best of both worlds, with O(1) amortized append and O(log n) depth, by using a left leaning tree where the k'th node on the spine from the root has a complete binary tree of size 2^k hanging off it. (Alternatively, you can think of this as what you get if you take a complete binary tree and rotate the root all the way right until you have what used to be the rightmost leaf at the root.)

[Markus de Medeiros]

Michael Sammler said:

The idea of replacing Hyps with something more efficient like a hashmap also sounds intriguing

Just to register it in text, my advisor (Joe Tassarotti) also mentioned this as something that iris-lean may be able to meaningfully improve over Iris-Rocq. The speed of the proofmode has apparently caused issues for some of his projects in the past.