simplifying everything

Stream: new members

[Jonathan Protzenko]

I am now generating complete pure terms via the Rust --aeneas--> Lean toolchain... one nice feature of the translation: because terms are pure, unit tests (of the form assert!(f foo == bar) can be executed at type-checking time using the simplifier, rather than be left as run-time errors...

this means that I now have goals of the form :

do
    let hm ←
      do
        let slots ←
          if
                { val := { val := 32, isLt := hashmap_hash_map_new_fwd.proof_1 } } >
                  USize.ofNatCore 0 (_ : 0 < USize.size) then
              do
              let slots0 ←
                vec_push_back (hashmap_list_t UInt64) (vec_new (hashmap_list_t UInt64)) hashmap_list_t.HashmapListNil
              let n0 ←
                USize.checked_sub { val := { val := 32, isLt := hashmap_hash_map_new_fwd.proof_1 } }
                    (USize.ofNatCore 1 (_ : 1 < USize.size))
              hashmap_hash_map_allocate_slots_loop_fwd UInt64 slots0 n0
            else result.ret (vec_new (hashmap_list_t UInt64))
        let i ←
          if h : 32 * 4 < USize.size then result.ret { val := { val := 32 * 4, isLt := (_ : 32 * 4 < USize.size) } }
            else result.fail error.integerOverflow
        let i0 ← USize.checked_div i { val := { val := 5, isLt := hashmap_hash_map_new_fwd.proof_3 } }
        result.ret
            {
              hashmap_hash_map_num_entries :=
                { val := { val := 0, isLt := hashmap_hash_map_new_with_capacity_fwd.proof_1 } },
              hashmap_hash_map_max_load_factor :=
                ({ val := { val := 4, isLt := hashmap_hash_map_new_fwd.proof_2 } },
                  { val := { val := 5, isLt := hashmap_hash_map_new_fwd.proof_3 } }),
              hashmap_hash_map_max_load := i0, hashmap_hash_map_slots := slots }
  << ... much more ... >>
  = result ()

ideally, I would like a magic flag for simp that reduces everything and runs the entire computation on the simplifier... possibly with tweaks such as "ok to unfold these recursive functions"... (this is my F* habit speaking here)

here's where I'm at:

• reading https://leanprover.github.io/theorem_proving_in_lean4/tactics.html, I couldn't find such a "reduce everything" mode, so I resorted to listing all of the functions one by one (as a temporary thing: if there's a better way, I'd love to know, because this is not sustainable, there are dozens of such functions)
• even so, trying to reduce this term, if I do simp [ LT.lt ], I exceed the recursion limit
• to debug the recursion limit error, I tried running several unfold manually to see where the problem lies, and ended up stuck on System.Platform.getNumBits which (intentionally) does not reduce... I guess I could add an instance of LT.lt for USize that first checks if it's < 2^32, and otherwise falls back to the comparison to System.Platform.getNumBits ()... but at this stage, I figured out I could use advice on how to best achieve all of the above

side remark:

• generally, is there a list of important tactics that one might want to use? I've read https://leanprover.github.io/theorem_proving_in_lean4/tactics.html but I guess I'd be looking for a directory of tactics (rather than grepping through the Lean source)

thanks!