ProofCafe01 のバックアップ(No.1)

• バックアップ一覧
• 差分 を表示
• 現在との差分 を表示
• ソース を表示
• ProofCafe01 へ行く。
  • 1 (2010-04-03 (土) 16:31:04)

ocaml-nagoya

Inductive list (A: Type) : Type :=
 | nil  : list A
 | cons : A -> list A -> list A.

(* Check (cons nat 3 (nil nat)). *)

Implicit Arguments nil [A].
Implicit Arguments cons [A].
(* Check (cons 3 nil). *)

Fixpoint append {A : Type} (xs ys: list A) : list A :=
 match xs with
 | nil => ys
 | cons x xs => cons x (append xs ys)
 end.
Infix "++" := append (at level 60).

Fixpoint length {A : Type} (xs : list A) : nat :=
 match xs with
 | nil => O
 | cons x xs => S (length xs)
 end.

Theorem append_assoc : forall (A: Type) (xs ys zs : list A),
 (xs ++ ys) ++ zs = xs ++ (ys ++ zs).
Proof.
 (* あなたの証明を書いてね *)
Qed.

Theorem append_length : forall (A: Type) (xs ys: list A),
  length (xs ++ ys) = length xs + length ys.
Proof.
 (* あなたの証明を書いてね *)
Qed.