Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Data.v Sprache: Coq

Original von: Coq^©

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.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.