|
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 _).
*)
¤ Dauer der Verarbeitung: 0.7 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
