Structural recursion

Stream: lean4

[Sofia]

Hey again. I'm having an issue with structural recursion. Any hints?

The depth function is structurally recursive in the 4th argument, the surface. Yet the errors pretend the 4th doesn't exist. Is there some class I need to implement or something?

inductive Surface
| Unresolved
| Inside
| Outside
| Ambiguious (inner : Array Surface)

instance : Inhabited Surface := ⟨Surface.Unresolved⟩

def depth (x y d : Nat) : Surface -> Nat
| Surface.Ambiguious a => depth (y >>> 1) x (d + 1) (a.get! y)
| _ => d

: error: fail to show termination for
  depth
with errors
argument #1 was not used for structural recursion
  failed to eliminate recursive application
    depth (y >>> 1) x (d + 1) (Array.get! a y)

argument #2 was not used for structural recursion
  failed to eliminate recursive application
    depth (y >>> 1) x (d + 1) (Array.get! a y)

argument #3 was not used for structural recursion
  failed to eliminate recursive application
    depth (y >>> 1) x (d + 1) (Array.get! a y)

structural recursion cannot be used

'termination_by' modifier missing

[Sofia]

Tried inlining the array (for a fixed length) as Ambiguious (a b c d e f g h : Surface), no luck. Doesn't change the result.

[Sofia]

Inlining as in, matching on x directly, then selecting the variant... Guess I can do that in the top level match maybe?

[Sofia]

The hack worked. But ... obviously undesired.

def depth : Nat -> Nat -> Nat -> Surface -> Nat
| 0, y, q, Surface.Ambiguious a b c d e f g h => depth (y >>> 1) 0 (q + 1) a
| 1, y, q, Surface.Ambiguious a b c d e f g h => depth (y >>> 1) 1 (q + 1) b
| 2, y, q, Surface.Ambiguious a b c d e f g h => depth (y >>> 1) 2 (q + 1) c
| 3, y, q, Surface.Ambiguious a b c d e f g h => depth (y >>> 1) 3 (q + 1) d
| 4, y, q, Surface.Ambiguious a b c d e f g h => depth (y >>> 1) 4 (q + 1) e
| 5, y, q, Surface.Ambiguious a b c d e f g h => depth (y >>> 1) 5 (q + 1) f
| 6, y, q, Surface.Ambiguious a b c d e f g h => depth (y >>> 1) 6 (q + 1) g
| 7, y, q, Surface.Ambiguious a b c d e f g h => depth (y >>> 1) 7 (q + 1) h
| _, _, q, _ => q

[Sofia]

Reverting and trying that trick with the original code, no dice.

def depth : Nat -> Nat -> Nat -> Surface -> Nat
| x, y, d, Surface.Ambiguious a => depth (y >>> 1) x (d + 1) (a.get! y)
| _, _, d, _ => d

[Sofia]

Suspect it might relate to the use of a.get! because the inhabited case is not structurally recursive, but it is a constant and that constant terminates....

[Sebastian Ullrich]

Recursion through arrays is not structural in Lean's sense - a.get! y is not a strict subterm of the parameter's pattern. But well-founded recursion is simple enough here.

termination_by sizeOfWfRel

[Sofia]

I do not see sizeOfWfRel anywhere. Is that a hint to implement it?

[Sofia]

Ah, it is capital F. Case sensitive search!

[Sofia]

Can confirm it worked. Thanks. :)

Magic trick aside, I already scratched that code. Was just testing anyway.

[Sebastian Ullrich]

Sebastian Ullrich said:

Recursion through arrays is not structural in Lean's sense - a.get! y is not a strict subterm of the parameter's pattern. But well-founded recursion is simple enough here.

termination_by sizeOfWfRel

Sorry, I didn't know what parts of wellfounded recursion were finished and which weren't. This will need an explicit decreasing_by proof, and I've made sure that it will fail properly without one from now on.

[Sofia]

Huh? No. The termination_by sizeOfWFRel sufficed.

[Sofia]

def depth (x y d : Nat) : Surface -> Nat
| Surface.Ambiguious a => depth y x (d + 1) (a.get! y)
| Surface.Unresolved => d + 1
| _ => d
termination_by sizeOfWFRel

[Sebastian Ullrich]

Not really, it was defaulting to admit

[Sofia]

I don't know what that means.

[Sebastian Ullrich]

It was equivalent to

decreasing_by exact sorry

i.e. it did not actually prove wellfoundedness

[Sebastian Ullrich]

Just checking, do you know about partial in case you do not want to prove something about this function?

[Sofia]

I know I can use partial; but my understanding is that colours the function so it cannot be used from total functions?

[Sebastian Ullrich]

No, you simply cannot unfold it in proofs

[Sofia]

If it was equivalent to such a sorry proof, why do I not see any errors and I'm able to run the program?

[Sofia]

Hmm. Okay. I guess this is related to how assert! and panic! exist at all?

[Sebastian Ullrich]

Yes, all three require Inhabited

[Sofia]

Ah, I see. Explains the no proving false part trivially. :D

[Sofia]

Noted, partial functions are not scary. Just more difficult to prove.

[Sofia]

How did you see it failed? I see no errors when using the sorry in the proof.

[Sebastian Ullrich]

The point of sorry is to accept an incomplete proof (with a warning when used explicitly). #print axiom depthbefore the fix would show that the definition depends on the sorryAx axiom.

[Sofia]

I get this when I try that print?

././Main.lean:112:7: error: expected 'axioms', identifier or string literal
././Main.lean:113:0: error: expected ':'
././Main.lean:113:4: error: 'depth' has already been declared

[Sebastian Ullrich]

Yes, please apply the spell check in the first error message

[Sebastian Ullrich]

#print axioms depth

[Sofia]

I tried that, should have mentioned that didn't work either. ././Main.lean:112:14: error: unknown constant 'depth'

[Sofia]

Ah, after the failure.

'depth' depends on axioms: [sorryAx]

[Sofia]

Ran it on the wrong line, whoops.

[Sofia]

I processed it as a setopt kind of verbose thing.

[Sofia]

Is there an option to show this globally?

[Sofia]

Seems #print options is missing on Lean 4. https://leanprover.github.io/reference/other_commands.html#instructions

[Sofia]

Either way, I need to sleep. TTYL. o/