Require Import Bool Arith List.

(* DEMO 1 *)
Check true.
Check false.

Check true && false.
Compute true && false.
Compute true && negb false.

Check 7.

Check 3 + 7.
Compute 3 + 7.

(* DEMO 2 *)
Definition myfunc (x : nat) := x + x.

Check myfunc.

Check myfunc 4.

Compute myfunc 5.

Fail Check myfunc true.

Compute let tmp := myfunc 7 in tmp + tmp.

Check fun x : nat => x + x.

Compute let f := fun x : nat => x + x in f (f 3).

Definition myfunc2 (x : nat) (y : nat) := x + y.

Check myfunc2.
Check myfunc2 7.
Check myfunc2 7 3.

Compute myfunc2 7 3.

(* DEMO 3 *)
Locate "_ * _".
Compute mult 2 3.

Check (3, 4).
Locate "_ * _".

Check list.
Check list nat.

(* DEMO 4 *)
Definition add_pair (p : nat * nat) :=
  match p with
  | (n,m) => n + m
  end.

Compute add_pair (3,2).

Print nat.

Definition is_4 (n : nat) :=
  match n with
  | 4 => true
  | _ => false
  end.

Compute is_4 7.
Compute is_4 4.

Check (if true then 0 else 1).

(* DEMO 5 *)
Fixpoint mlnat (l : list nat) :=
  match l with
  | nil => 0
  | x :: xs => x * mlnat xs
  end.

Fail Fixpoint wrong (l : list nat) :=
  match l with
  | nil => wrong (17 :: nil)
  | x :: xs => x + wrong xs
  end.

Fixpoint list_forall (p : nat -> bool) (l : list nat) :=
  match l with
  | nil => true
  | x :: xs => (p x) && (list_forall p xs)
  end.

Compute list_forall (fun x => leb x 17) (33 :: 4 :: nil).