Added implementation of count trailing zeros function.

[klinashka]

This PR implements a functional version of the count trailing zeros function. The implementation first defines it on positive integers (where the function always has a value), then lifts the operation on integers. For 0 and negative inputs, a default value is given as a parameter to the lifted function and the result will always be that value.

A default value is necessary for 0, since zero would have an infinite number of trailing zeros. For negative inputs, there are a number of possible implementations. We chose to also give a default value for simplicity, as the use case of this function only needs to reason about positive integers.

In addition to the definition of the function, a number of lemmas are implemented, including a testbit specification and an arithmetic specification for positive inputs.

[miriampolzer]

Thank you for adding these! Looks good overall, I mostly have simplification/style comments.

[miriampolzer]

You can make this a context variable so you don't have to repeat it on all lemmas and function calls. Also I'd tend towards calling it d or default for consistency with existing functions that have a default argument. (See e.g. https://rocq-prover.org/doc/V9.0.0/stdlib/Stdlib.Lists.List.html#nth)

[klinashka]

That is a good suggestion! I will make def a context variable and change its name to default.

[miriampolzer]

Optional (Naming): I think I would have omitted the _pos. Usually we name the lemma beased on its final statement. I like just naming it in order of function names, or by describing its property. E.g. this one could be pow2_lctz_gt_0.

[klinashka]

I have renamed some of the names of the theorems. Feel free to take a look and tell me if you think the names are appropriate.

[miriampolzer]

rewrite Nat2Z.inj_succ, <-Z.add_1_l, Z.pow_add_r by lia. suffices here, saves you explicit replace and makes the proof more idiomatic.

[klinashka]

Thank you for the suggestion! I will change this.

[miriampolzer]

Same as above, replace with rewrite Nat2Z.inj_succ, <-Z.add_1_l, Z.pow_add_r by lia.

[miriampolzer]

nit: dot goes on the line above.

[miriampolzer]

nit: use {} for consistency.

[miriampolzer]

pos_range and pos_testbit_z_testbit are not used in this file, and they don't seem to be about lctz specifically. Are you using them somewhere else in your proofs?

[klinashka]

On a closer look, I do not use them anywhere, I will thus remove them from the file, as they likely belong in some other place either way.

[miriampolzer]

There are a few simplifications possible in this proof, here is how I boiled it down:

    Lemma lctz_pos_testbit_2 (z : Z) : z > 0 -> 
        forall c, Z.testbit z c = true -> (forall i , i < c -> Z.testbit z i = false) ->
            c = lctz z.
    Proof.
        destruct z as [ | p | p]; try lia. intros Hz.
        induction p; intros c H1 H2; cbn [lctz pos_ctz]; 
        destruct (Ztrichotomy c (Z.of_nat 0)) as [H | [H | H]]; 
        destruct c; inversion H; inversion H1; eauto.
        { specialize (H2 (Z.of_nat 0) ltac:(lia)). inversion H2. }
        { rewrite testbit_xO_2 in H1. rewrite Nat2Z.inj_succ.
          cbn [lctz] in IHp.
          erewrite <- IHp; try eassumption; try lia.
          intros i Hi. rewrite <- (Z.pred_succ i). rewrite <- testbit_xO_2.
          apply H2. lia. }
    Qed.

Things I did:

• pull the c destruction up, since it's easy to see what happens and we do it in every case.
• move the c argument to avoid having to revert
• use ltac:(lia) as argument instead of assert.
• use erewrite to avoid manually having to set the c. (This may seem lazy, but these kind of things allow for changes in definitions later without having to adapt the proof script.)
• instead of specialize H2, work backwards from the goal, to avoid explictly spelling out Z.succ i.

None of these is particulary complex or fancy, but I find having them in mind useful in the long run.

[klinashka]

Thank you for the nice proof and the tips. I will change my proof.

[miriampolzer]

Looks good, thank you!