1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
|
Require Import Uint63.
Open Scope uint63_scope.
Definition div_eucl_plus_one i1 i2 :=
let (q,r) := diveucl i1 i2 in
(q+1, r+1)%uint63.
Definition rcbn := Eval cbn in div_eucl_plus_one 3 2.
Check (eq_refl : rcbn = (2, 2)).
Definition rcbv := Eval cbv in div_eucl_plus_one 3 2.
Check (eq_refl : rcbv = (2, 2)).
Definition rvmc := Eval vm_compute in div_eucl_plus_one 3 2.
Check (eq_refl : rvmc = (2, 2)).
Definition f n m :=
match (n ?= 42)%uint63 with
| Lt => (n + m)%uint63
| _ => (2*m)%uint63
end.
Goal forall n, (n ?= 42)%uint63 = Gt -> f n 256 = 512%uint63.
intros. unfold f.
cbn. Undo. cbv. (* Test reductions under match clauses *)
rewrite H. reflexivity.
Qed.
|