Missing proofs in code #6

New Issue

aniva · 2023-08-23T13:27:41-07:00

aniva commented

2023-08-23 13:27:41 -07:00

Intuitively this terminates (in Serial.lean)

def serialize_sort_level_ast (level: Level): String :=
  let k := level.getOffset
  let u := level.getLevelOffset
  let u_str := match u with
    | .zero => "0"
    | .succ _ => panic! "getLevelOffset should not return .succ"
    | .max v w | .imax v w =>
      let v := serialize_sort_level_ast v
      let w := serialize_sort_level_ast w
      s!"(max {v} {w})"
    | .param name =>
      let name := name_to_ast name
      s!"{name}"
    | .mvar id =>
      let name := name_to_ast id.name
      s!"(:mvar {name})"
  match k, u with
  | 0, _ => u_str
  | _, .zero => s!"{k}"
  | _, _ => s!"(+ {u_str} {k})"
  termination_by serialize_sort_level_ast level => level_depth level
  decreasing_by
  . sorry

but Lean cannot show it automatically

Intuitively this terminates (in `Serial.lean`) ```lean def serialize_sort_level_ast (level: Level): String := let k := level.getOffset let u := level.getLevelOffset let u_str := match u with | .zero => "0" | .succ _ => panic! "getLevelOffset should not return .succ" | .max v w | .imax v w => let v := serialize_sort_level_ast v let w := serialize_sort_level_ast w s!"(max {v} {w})" | .param name => let name := name_to_ast name s!"{name}" | .mvar id => let name := name_to_ast id.name s!"(:mvar {name})" match k, u with | 0, _ => u_str | _, .zero => s!"{k}" | _, _ => s!"(+ {u_str} {k})" termination_by serialize_sort_level_ast level => level_depth level decreasing_by . sorry ``` but Lean cannot show it automatically

aniva added the

part/Serial

label 2023-08-23 13:27:41 -07:00

aniva self-assigned this 2023-08-23 13:27:41 -07:00

aniva added the

priority

low

label 2023-08-23 13:28:11 -07:00

aniva changed title from ~~The termination of `Lean.Level` serialization is not ensured~~ to Missing proofs in code

2023-08-30 19:19:11 -07:00

aniva commented

2023-08-30 19:19:35 -07:00