• Robbert Krebbers's avatar
    Various small changes. · 507a150a
    Robbert Krebbers authored
    * Define the standard strict order on pre orders.
    * Prove that this strict order is well founded for finite sets and finite maps.
      We also provide some utilities to compute with well founded recursion.
    * Improve the "simplify_option_equality" tactic to handle more cases.
    * Axiomatize finiteness of finite maps by translation to lists, instead of by
      them having a finite domain.
    * Prove many additional properties of finite maps.
    * Add many functions and theorems on lists, including: permutations, resize,
      filter, ...
    507a150a
tactics.v 10.5 KB