A lemma about number catenating

Using Coq
1

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?

2

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
3

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

4

Thank you. The search command is really fantastic.