DMM_Coq_School_Day4.v

Require Import String List.
Import ListNotations.
Open Scope string_scope.

Definition aaa := 1+2.
Definition bbb := aaa * 5.

Definition foo x y:= 2*x + y.
Compute foo 1 2.

Definition is_zero n :=
   match n with
   | 0 => true (* 定数パターン *)
   | x => false (* 変数パターン *)
 end.
 
 Check (1, true).
 Check ("abc", 1, true).
 
Definition minus1 n :=
  match n with
  | 0 => None
  | x => Some (x-1)
  end.
Compute minus1 10.
Compute minus1 0.

Definition sample :=
  let i := 3 in
  let incr x := x + 1 in
  incr (incr i).

Compute List.map is_zero [0; 1; 2; 0].

Compute List.filter is_zero [0; 1; 2; 0].

Check (fun x => x+3).
Compute List.map (fun x => x+3) [1;2;3].

Check plus.
Check (plus 1).

Compute (plus 1) 10.
Compute List.map (plus 1) [1; 2; 3].

Definition id {A:Set} (x:A) := x.	
 
Check id "abc".
Check id [1; 2; 3].
Check id [].
 
(** 4.2 Inductive データ型 *)
Inductive light : Set :=
  | Green : light
  | Yellow : light
  | Red : light.
 
Definition next (x : light) : light :=
  match x with
  | Green => Yellow
  | Yellow => Red
  | Red => Green
  end.

Compute next (next (next Green)).

Require Import String.
Open Scope string_scope.

Definition user := string.
Inductive login_state : Set :=
  | Guest : login_state
  | LoggedIn : user -> login_state.

Definition greet state :=
  match state with
  | Guest => " ようこそ!ゲストさん! ログインはこちら..."
  | LoggedIn user => (" ようこそ!" ++ user ++ " さん!")
  end.

Print option.

Definition isNone {A : Type} (o : option A) := match o with
| None => true
| Some _ => false
end.

Print nat.

Fixpoint plus x y := match x with
| O => y
| S x0 => S (plus x0 y) end.

Open Scope list_scope.
Print list.

Fixpoint length {A : Type} (xs : list A) :=
  match xs with
  | nil => 0
  | x :: xs' => 1 + length xs'
  end.
  
Fixpoint reverse {A : Type} (xs : list A) :=
  match xs with
  | [] => []
  | x :: xs => reverse xs ++ [x]
  end.
  
Fixpoint revapp {A : Type} (xs ys: list A) :=
  match xs with
  | nil => ys
  | x :: xs => revapp xs (x :: ys)
  end.

Definition reverse' {A : Type} (xs : list A) := revapp xs [].