fluiddynamics

(* 巨大数 *)

Print nat.

Definition 十 := 10.

Fixpoint plus (n m:nat) : nat :=
match n with
| O => m
| S n' => S (plus n' m)

fluiddynamics

(*
式とは，シンボルや記号をつなげたもの
Eval simpl inで確認する
*)

Eval simpl in (1).
Eval simpl in (2).
Eval simpl in (nat).
Eval simpl in (Set).
Eval simpl in (1=2).

fluiddynamics

(*
  exercise rev_injective
    日本語：http://proofcafe.org/sf/Lists_J.html#lab63
    英語：https://www.cis.upenn.edu/~bcpierce/sf/current/Lists.html#lab89
*)

(* 自然数のリストのInductive *)
Inductive natlist : Type :=
  | nil : natlist
  | cons : nat -> natlist -> natlist.

fluiddynamics

(*
  exercise palindromes
    日本語：http://proofcafe.org/sf/Prop_J.html#lab200
    英語：https://www.cis.upenn.edu/~bcpierce/sf/current/Prop.html#lab266
*)

(* 多相的なリストのInductive *)
Inductive list (X:Type) : Type :=
  | nil : list X
  | cons : X -> list X -> list X.

fluiddynamics

Require Export Poly_J.

Check (2+2=4).
Check (ble_nat 3 2 = false).
Check 2+2.
Check ble_nat.
Check ble_nat 3 2.
Check false.

Check (2+2=5).

fluiddynamics

Require Export Poly_J.

Print double.

Theorem double_injective_FAILED:
forall n m, double n = double m -> n = m.
Proof.
intros n m.
induction n as [| n'].
Case "n=0". simpl. intros eq.

fluiddynamics

Require Export Lists_J.

Inductive boollist : Type :=
|bool_nil : boollist
|bool_cons : bool -> boollist -> boollist.

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

fluiddynamics

Inductive day : Type :=
| monday : day
| tuesday : day
| wednesday : day
| thursday : day
| friday : day
| saturday : day
| sunday :day.