Merging fiat-crypto utilities into coqutil?

[JasonGross]

Should any/all/most of the fiat-crypto src/Util directory be migrated to coqutil? (Currently this directory is more-or-less replicated across fiat, rewriter, and fiat-crypto, with fiat-crypto containing the most complete and up-to-date version.)

An incomplete list of tactics, roughly in order from most-used to least-used:

• destructing discriminees of match subject to various conditions such as "only this type of variable", "only terms which contain no matches inside themselves", "only in the hyps", "only in the conclusion", "only variables" (with intelligent insertion of equations)
• destructing or inverting all hypotheses of a given type family, with performance-optimized variants for common heads
• [a tactic for specializing all hypotheses with non-dependent premises which can be proven by a given tactic (such as assumption, auto, lia, etc))[https://github.com/mit-plv/fiat-crypto/blob/master/src/Util/Tactics/SpecializeBy.v]
• variants of pose and assert which are suitable for use in repeat blocks by ensuring that they don't pose duplicates
• split hypotheses using iff, and, produnderneath binders in a way that preserves the binders, e.g., turningforall x y, P x y /\ Q x yintoforall x y, P x yandforall x y, Q x y`
• finding the head of a term
• attempting to rewrite with any hypothesis that can be rewritten with
• call set or subst on all evars
• a variant of subst that works modulo relations
• printing the context and the goal
• testing if an identifier has a body / can be unfolded
• calling subst on all local definitions
• transparent assert
• a tactic to evar-normalize terms
• a variant of etransitivity that accepts arguments
• run a tactic on any hypothesis that it succeeds on
• a destruct that attempts to work with convoy-pattern terms appearing in the goal
• especialize
• a tactic for getting the goal in fewer characters
• general normalization of hyps and goal with respect to a commutativity lemma
• get all instances of a typeclass (family)
• tac_on_subterms, to be used as e.g. tac_on_subterms ring_simplify
• revert non-dependent hypotheses, roughly the inverse of intros *
• tactics for running tactics while returning constrs and a tryif for returning constrs
• replace_with_vm_compute for getting around vm_compute not inserting casts
• saturate the context with all ways of specializing hypotheses with other hyps
• simplifications of nested if statements

An incomplete list of other utilities:

• A large but not-especially-coherently-organized library of utility lemmas about Z, including automation for:
  • named hint databases that can be used to have (e)auto invoke lia, nia, or lra at the leaves
  • rewrite databases for distributing and factoring various operations, the most useful of which is Z.modulo, which is factored into a tactic
  • general simplification rewrite databases, divided into categories of (a) general simplification that's reversible, (b) ones that further don't require any side conditions, and (c) ones that strip out operations on constants
  • a version of subst which will solve linear equations in variables over Z to substitute
  • tactics for making progress on or simplifying fractions, inequalities, bounds, min/max, Z.testbit
• smaller libraries for lemmas about nat, list, N, Q, MSets
• a general error monad
• a library of lemmas about reflect culminating in a general tactic for turning boolean equality hypotheses into propositions
• a collection of lemmas about string, including
  • a small parser combinator library used in fiat-crypto to parse command-line options and assembly files
  • typeclasses for Show, ShowLevel (for printing with precedence), and ShowLines (printing to lists of strings rather than single strings, for better efficiency) and theory around them
  • sorting
• telescopes and wf and more facts
• a port and adaptation of OCaml's Arg module (maybe this should be split off to a separate project and added on opam? (perhaps to be combined with the method for extracting main functions and executables in OCaml and Haskell?)
• notations for CPS
• function composition and (un)currying
• theory of decidable propositions and relations
• a class for types with default elements
  • a variant for "pointed" types and props
• heterogeneous lists indexed over a list of types (and a primitive projections variant)
• heterogeneous lists not indexed over a list of types
• length-indexed lists/tuples
• some theory about eq
• factorization of Ns into primes
• lemmas and tactics about subsingleton types, including a tactic to replace proofs of x = x with eq_refl when equality on x is decidable
• the Let_In constant for not inlining let ... in ... and a monad around this
• theory of finitely listable types
• fueled loops
• some hints about PERs
• basic theory, including specialized inversion lemmas and tactics (a la inversion_sigma) for option, nat, list, prod, prod with primitive projections, sum, primitive projection versions of sig, sigT, etc, sumbool
• reflective simpliciation of Props
• theory around option (list _) and list (option _)

[samuelgruetter]

I think it would be useful to have these tactics and utilities in coqutil. Some questions:

• What Coq version compatibility constraint does that impose, and will I have to test new code for coqutil with 7 different Coq versions before pushing it? Could we maybe designate the Tactics, Datatypes and the Word subfolders as high-compatibility folders (supporting older Coq versions), while only supporting the most recent released Coq version in the remaining subfolders?
• FixCoqMistakes.v looks like it would be good to have in coqutil too, but I wonder why it has to export GlobalSettings.v? Could we have it in coqutil without GlobalSettings.v?
• What should we do about fiat-crypto Util code that's already present in a somewhat different form in coqutil? I'm not super keen on doing a lot of merging work and updating bedrock2 to use renamed definitions, but having several similar definitions of basically the same thing in coqutil doesn't look great either, on the other hand we also shouldn't perfectionism allow to be the enemy of usefulness... Opinions?

I quickly went through the tactics/utilities you listed above and looked for equivalent ones in coqutil, and here's what I found:

• destructing discriminees of match subject to various conditions such as "only this type of variable", "only terms which contain no matches inside themselves", "only in the hyps", "only in the conclusion", "only variables" (with intelligent insertion of equations)

coqutil.Tactics.Tactics.destruct_one_match_...

• variants of pose and assert which are suitable for use in repeat blocks by ensuring that they don't pose duplicates

coqutil.Tactics.forward.unique_pose

• finding the head of a term

head/head_of_app already appears in 3 different locations in coqutil

• A large but not-especially-coherently-organized library of utility lemmas about Z

coqutil.Z

• theory of decidable propositions and relations

coqutil.Decidable based on BoolSpec rather than sumbool (because we don't want proofs of Props to appear in code that's meant to be executed)

• a class for types with default elements

coqutil.Datatypes.Inhabited

• heterogeneous lists indexed over a list of types (and a primitive projections variant)

coqutil.Datatypes.HList

• length-indexed lists/tuples

also in coqutil.Datatypes.HList

• theory around option (list _) and list (option _)

coqutil.Datatypes.List also contains some lemmas about option (list _) and list (option _)

[andres-erbsen]

FixCoqMistakes sounds like https://github.com/mit-plv/coqutil/blob/master/src/coqutil/sanity.v

https://coq.inria.fr/refman/changes.html

Changed: The default tactic used by firstorder is auto with core instead of auto with *; see Solvers for logic and equality for details; old behavior can be reset by using the -compat 8.12 command-line flag; to ease the migration of legacy code, the default solver can be set to debug auto with * with Set Firstorder Solver debug auto with * (#11760, by Vincent Laporte).