Strategies for recursion on a DAG in Lean?

Stream: lean4

[Arien Malec]

What's the general strategy in Lean to show that I'm never going to create a cycle in the following?

inductive Calc where
  | const (n : Nat) : Calc
  | var (l: String) (n: Nat): Calc
  | plus (s: Calc) (t: Calc):  Calc
  | times (s: Calc) (t: Calc): Calc
deriving Repr

namespace Calc

def eval (c: Calc): Nat :=
  match c with
  | const n => n
  | var _ n => n
  | plus s t => eval s + eval t
  | times s t => eval s * eval t

def isLeaf (c: Calc): Bool :=
  match c with
  | const _ => true
  | var _ _ => true
  | _ => false

def assign (l: String) (n: Nat) (c: Calc) : Calc :=
  match c with
  | var l' _ => if l == l' then var l n else c
  | const _ => c
  | plus s t => plus (assign l n s) (assign l n t)
  | times s t => times (assign l n s) (assign l n t)
termination_by _ _ c => c.isLeaf -- totally insufficient for Lean...

[Henrik Böving]

Lean types are acyclic per definition, it is impossible to construct a cycle of an inductive type, you also dont have to show anything to Lean in the piece of code you are showing us right now, if you just leave your termination hint away Lean will accept it.

[Locria Cyber]

Maybe it's not? the first branch val l' _ => says assign _ _ c can be c

[Locria Cyber]

I totally misunderstood your code

[Arien Malec]

Henrik Böving said:

Lean types are acyclic per definition, it is impossible to construct a cycle of an inductive type, you also dont have to show anything to Lean in the piece of code you are showing us right now, if you just leave your termination hint away Lean will accept it.

So it does -- I had a bug, added a termination_by, fixed the bug and it turns out the termination_by made Lean grumpy...

[Henrik Böving]

In general as long as you are doing what we call structural recursion. That is, doing a recursive call on something that has at least one constructor less than your input the auto termination checker will accept your things.

[Arien Malec]

Yeah, I confused myself then confused the checker :-) The error message here is strange, BTW...

[Wojciech Nawrocki]

(So what you have here is really a tree, not a graph; even though its memory representation can be a graph in case multiple nodes use the same shared reference).

[Henrik Böving]

Hm, I'd say its as good as we can do. You gave it a measure for termination, it simplified with that measure as far as it could and noticed you have to derive False in a certain branch and told you it cannot close that proof so you have to do that for it. What else would you have expected to happen?

[Trebor Huang]

What would be an idiomatic way to use "real" DAGs in Lean? I mean you should be able to fine grain control what nodes are shared etc

[Sebastian Ullrich]

You can use indices into a graph node array instead of direct references, like in Rust. Then you can even represent cycles.

[Chris Bailey]

It will also be much nicer to work with than it is in rust since you have StateT/do.