blob: 00e067ac5aa7e98cbd3a71ddabf27d2029bebb2b (
plain)
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 Int63.
Open Scope int63_scope.
Definition div_eucl_plus_one i1 i2 :=
let (q,r) := diveucl i1 i2 in
(q+1, r+1)%int63.
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)%int63 with
| Lt => (n + m)%int63
| _ => (2*m)%int63
end.
Goal forall n, (n ?= 42)%int63 = Gt -> f n 256 = 512%int63.
intros. unfold f.
cbn. Undo. cbv. (* Test reductions under match clauses *)
rewrite H. reflexivity.
Qed.
|
