Skip to content

Commit

Permalink
adapt to coq/coq#18730
Browse files Browse the repository at this point in the history
  • Loading branch information
andres-erbsen committed Feb 28, 2024
1 parent c96ee95 commit de880ce
Showing 1 changed file with 13 additions and 13 deletions.
26 changes: 13 additions & 13 deletions Kami/Lib/Word.v
Original file line number Diff line number Diff line change
Expand Up @@ -2054,8 +2054,8 @@ Qed.

Lemma wones_pow2_minus_one: forall {sz}, wordToNat (wones sz) = pow2 sz - 1.
Proof.
induction sz; simpl; auto.
rewrite IHsz; pose (pow2_zero sz).
induction sz; simpl; auto;
rewrite IHsz; pose (pow2_zero sz);
lia.
Qed.

Expand Down Expand Up @@ -5203,9 +5203,9 @@ Proof.
}
remember (wordToN (wneg w)) as ww; clear Heqww.
destruct ww; simpl.
* split; try lia.
change 0%Z with (Z.of_nat 0).
apply Nat2Z.inj_lt.
* split; try lia;
change 0%Z with (Z.of_nat 0);
apply Nat2Z.inj_lt;
apply zero_lt_pow2.
* split.
{ rewrite <-Pos2Z.opp_pos, <-N2Z.inj_pos.
Expand All @@ -5225,9 +5225,9 @@ Proof.
}
- apply eq_sym, wmsb_false_bound in Heqmsb.
destruct (wordToN w); simpl.
* split; try lia.
change 0%Z with (Z.of_nat 0).
apply Nat2Z.inj_lt.
* split; try lia;
change 0%Z with (Z.of_nat 0);
apply Nat2Z.inj_lt;
apply zero_lt_pow2.
* split.
{ etransitivity.
Expand Down Expand Up @@ -6387,9 +6387,9 @@ Proof.
rewrite wordToN_to_nat.
rewrite Nnat.Nat2N.id.
simpl.
rewrite wordToNat_natToWord_idempotent'; auto.
pose proof (pow2_zero sz).
unfold Pos.to_nat; simpl.
rewrite wordToNat_natToWord_idempotent'; auto;
pose proof (pow2_zero sz);
unfold Pos.to_nat; simpl;
lia.
Qed.

Expand Down Expand Up @@ -6693,8 +6693,8 @@ Proof.
rewrite wordToNat_combine; simpl.
rewrite Nat.mul_0_r, Nat.add_0_r.
rewrite wordToNat_natToWord_idempotent'; auto.
destruct sz; simpl; try lia.
pose proof (pow2_zero sz).
destruct sz; simpl; try lia;
pose proof (pow2_zero sz);
lia.
Qed.

Expand Down

0 comments on commit de880ce

Please sign in to comment.