Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Check 3. Check 3 + 5. Check true. (* Erroneous command : Check 3 + true. *) Search nat. Check plus 3. Check plus 3 (plus 4 5). (* implicit parentheses on the left. *) Check (plus 3) 4. (* Constructing functions *) Check fun x => x + 3. Check (fun x => x + 3) 5. Check fun x : nat -> nat => x (x (x 3)). Definition a_big_number := ((123 * 1000) + 456) * 1000 + 789. Definition iter3on3 f := f (f (f 3)). Check let x := 3 in x * (x + x). Eval vm_compute in iter3on3 (plus 3). Eval lazy in iter3on3 (plus 3). Check S (S (S O)). Locate "_ * _". Locate "*". (* Predefined boolean type. *) Require Import Bool. Locate "&&". Locate "||". (* Erroneous command: Check fun x y:nat => if x <= y then 0 else 1. *) Require Import Arith. Check beq_nat. Check leb. Search bool. Definition evenb x := beq_nat (2 * Div2.div2 x) x. Definition Collatz x := if evenb x then Div2.div2 x else 3*x+1. Require Import ZArith. Open Scope Z_scope. Definition ZCollatz (x : Z) := if Zeven_bool x then x / 2 else 3 * x + 1. Eval vm_compute in iter 10 Z ZCollatz 31. Definition fact (x:Z) := let (_, r) := iter x (Z * Z) (fun p => let (n, r) := p in (n+1, n * r)) (1, 1) in r. Eval vm_compute in fact 100. (* Lists *) Require Import List. (* Erroneous command: Check nil. *) Check nil:list nat. Definition mx_row (M :list (list Z)) (n:nat) := nth n M nil. Definition mx_col (M :list (list Z)) (n:nat) := map (fun row => nth n row 0) M. Definition vec_sum (v : list Z) := fold_right Zplus 0 v. Definition pairwise_mult (V1 V2 : list Z) := map (fun (p : Z * Z) => let (x,y) := p in x*y) (combine V1 V2). Definition vec_prod (V1 V2 : list Z) := vec_sum (pairwise_mult V1 V2). Definition coord_mx (n m:nat) := map (fun i => map (fun j => (i, j)) (seq 0 m)) (seq 0 n). Definition mx_prod (n m p : nat) (M N:list (list Z)) := map (map (fun t : nat*nat => let (i, j) := t in vec_prod (mx_row M i) (mx_col N j))) (coord_mx n p).