CoC 之 Dependent Types

- encode predicates and connectives

- encode forall

(* Typing predicates *)

Parameters (prime_divisor : nat -> nat)

  (prime : nat -> Prop)

  (divides : nat->nat-> Prop).

Check prime_divisor 220. (* prime_divisor n is a prime number *)

Check prime 5.  (* 5 is prime *) 

(* Parameterize data type *)

Parameter binary_word : nat -> Type.

Definition short : Set = binary_word 32.

(* encode forall *)

Check (forall A B :Set, A->B->A*B).

Parameter prime_divisor_correct : forall n:nat, 2 <= n -> let d := prime_divisor n in prime d /\ divides d n.

Check prime_divisor_correct 220.

Check le_S.

Check cons.

Check pair.

(* Polymorphism *)

(* Parameter iterate : forall A:Set, (A->A)->nat->A->A.  *)

Fixpoint iterate (A:Type)(f:A->A)(n:nat)(x:A) : A :=

  match n with

  | O => x

  | S p => f (iterate A f p x)

  end.

Check (iterate nat).

Compute (iterate _ (mult 2) 10 2).

Definition twice : forall A:Set, (A->A)->A->A := fun A f a => f (f a).

Require Import ZArith.

Compute (twice Z (fun z=>(z*z)%Z) 2%Z).

Compute (twice _ (fun n=>(n*n)) 2).