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
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
Inductive pack (A: Type) : Type :=
packer : A -> pack A.
Arguments packer {A}.
Definition uncover (A : Type) (packed : pack A) : A :=
match packed with packer v => v end.
Notation "!!!" := (pack _) (at level 0, only printing).
(* The following data is used as material for automatic proofs
based on type classes. *)
Class EvenNat the_even := {half : nat; half_prop : 2 * half = the_even}.
Instance EvenNat0 : EvenNat 0 := {half := 0; half_prop := eq_refl}.
Lemma even_rec n h : 2 * h = n -> 2 * S h = S (S n).
Proof.
intros [].
simpl. rewrite <-plus_n_O, <-plus_n_Sm.
reflexivity.
Qed.
Instance EvenNat_rec n (p : EvenNat n) : EvenNat (S (S n)) :=
{half := S (@half _ p); half_prop := even_rec n (@half _ p) (@half_prop _ p)}.
Definition tuto_div2 n (p : EvenNat n) := @half _ p.
(* to be used in the following examples
Compute (@half 8 _).
Check (@half_prop 8 _).
Check (@half_prop 7 _).
and in command Tuto3_3 8. *)
(* The following data is used as material for automatic proofs
based on canonical structures. *)
Record S_ev n := Build_S_ev {double_of : nat; _ : 2 * n = double_of}.
Definition s_half_proof n (r : S_ev n) : 2 * n = double_of n r :=
match r with Build_S_ev _ _ h => h end.
Canonical Structure can_ev_default n d (Pd : 2 * n = d) : S_ev n :=
Build_S_ev n d Pd.
Canonical Structure can_ev0 : S_ev 0 :=
Build_S_ev 0 0 (@eq_refl _ 0).
Lemma can_ev_rec n : forall (s : S_ev n), S_ev (S n).
Proof.
intros s; exists (S (S (double_of _ s))).
destruct s as [a P].
exact (even_rec _ _ P).
Defined.
Canonical Structure can_ev_rec.
Record cmp (n : nat) (k : nat) :=
C {h : S_ev k; _ : double_of k h = n}.
(* To be used in, e.g.,
Check (C _ _ _ eq_refl : cmp 6 _).
Check (C _ _ _ eq_refl : cmp 7 _).
*)
|
