トップ
新規
単語検索
ヘルプ
ProofCafe01
をテンプレートにして作成
開始行:
[[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...
(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.
** append_assocの証明の解説 [#j97ea64b]
:intros|~
ゴールがforallで始まっているので、introsによって前提に移...
:induction xs|~
induction xs. で xs に関する帰納法が始まる。 xs が nil の...
:simpl|~
x=nilの場合です。まずは simpl. で式を簡約します。
:reflexivity|~
簡約すると、 = の両辺は 構文的に等価になります。このとき ...
:simpl|~
次はconsの場合です。まずは simpl。
:rewrite IHxs|~
このときのゴールをじっと見つめると。。。どうやら 帰納法の...
~
この IHxs : (xs ++ ys) ++ zs = xs ++ (ys ++ zs) は等式の...
:reflexivity|~
両辺が構文的に等価になるので、reflexivityで証明終了。
これで append 関数の 結合則が証明できた。 似たようなやり...
終了行:
[[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...
(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.
** append_assocの証明の解説 [#j97ea64b]
:intros|~
ゴールがforallで始まっているので、introsによって前提に移...
:induction xs|~
induction xs. で xs に関する帰納法が始まる。 xs が nil の...
:simpl|~
x=nilの場合です。まずは simpl. で式を簡約します。
:reflexivity|~
簡約すると、 = の両辺は 構文的に等価になります。このとき ...
:simpl|~
次はconsの場合です。まずは simpl。
:rewrite IHxs|~
このときのゴールをじっと見つめると。。。どうやら 帰納法の...
~
この IHxs : (xs ++ ys) ++ zs = xs ++ (ys ++ zs) は等式の...
:reflexivity|~
両辺が構文的に等価になるので、reflexivityで証明終了。
これで append 関数の 結合則が証明できた。 似たようなやり...
ページ名:
![[PukiWiki]](image/caml3.jpg "[PukiWiki]")
