Dear all,

I’v got stuck with a lemma like this.

Lemma z_catenate:

Open Scope Z_scope.Lemma z_catenate:

forall ea:Z,

ea > 0 -> Z.lor (Z.shiftl (Z.shiftr ea 16) 16) (Z.land ea 65535) = ea.

Can anyone give some hints?

Dear all,

I’v got stuck with a lemma like this.

Lemma z_catenate:

Open Scope Z_scope.Lemma z_catenate:

forall ea:Z,

ea > 0 -> Z.lor (Z.shiftl (Z.shiftr ea 16) 16) (Z.land ea 65535) = ea.

Can anyone give some hints?

Dear Julian,

the hint is: please read the section on the Search command in the reference manual with all its fancy options. If you master the Search command, the proof is trivial:

```
Require Import ZArith.
Require Import Psatz.
Open Scope Z_scope.
Lemma z_catenate:
forall ea:Z,
ea > 0 -> Z.lor (Z.shiftl (Z.shiftr ea 16) 16) (Z.land ea 65535) = ea.
Proof.
intros.
(* Search for lemmas containign both Z.shiftl and Z.shiftr *)
Search Z.shiftl Z.shiftr.
rewrite <- Z.ldiff_ones_r by lia.
(* Search for lemmas containign both Z.ldiff and Z.land *)
Search Z.ldiff Z.land.
rewrite Z.lor_ldiff_and.
reflexivity.
Qed.
```

1 Like

P.S.: you don’t need the ea>0 premise.

Thank you. The search command is really fantastic.