(*********************************************) (* You can ignore the following definitions. *) Require Import List. Notation UNIT := unit. Notation "()" := tt. Definition case {A : Type} {B : Type} {R : Type} : (A + B) -> (A -> R) -> (B -> R) -> R. tauto. Defined. Definition caseu {A : Type} {R : Type} : (unit + A) -> R -> (A -> R) -> R := fun ua => fun r => fun fr => match ua with inl () => r | inr a => fr a end. Notation BOOL := bool. Notation TRUE := true. Notation FALSE := false. Notation "'IFBOOL' e 'THEN' e1 'ELSE' e2" := (match e with true => e1 | false => e2 end) (at level 0). Inductive NAT : Type := inNAT : (unit + NAT) -> NAT. Fixpoint recNAT {A : Type} (f : (UNIT + A) -> A) (n : NAT) : A := match n with inNAT(inl ()) => f (inl _ ()) |inNAT(inr n') => f (inr _ (recNAT f n')) end. Inductive LIST : Type := inLIST : (UNIT + NAT * LIST) -> LIST. Fixpoint recLIST {A : Type} (f : (UNIT + NAT * A) -> A) (l : LIST) : A := match l with inLIST(inl ()) => f (inl _ ()) |inLIST(inr (n, l')) => f (inr _ (n, recLIST f l')) end. CoInductive STREAM : Type := mkstream : NAT * STREAM -> STREAM. CoFixpoint genSTREAM {A : Type} (f : A -> NAT * A) (seed : A) : STREAM := match f seed with (n, a') => mkstream (n, genSTREAM f a') end. Definition outSTREAM (s : STREAM) : NAT * STREAM := match s with mkstream p => p end. Notation ZERO := (inNAT (inl _ ())). Notation SUCC := (fun n => inNAT (inr _ n)). Notation NIL := (inLIST (inl _ ())). Notation CONS := (fun a => fun b => inLIST (inr _ (a, b))). Fixpoint NAT_of_nat (n : nat) : NAT := match n with O => ZERO |S n => SUCC (NAT_of_nat n) end. Coercion NAT_of_nat : nat >-> NAT. Fixpoint nat_of_NAT (n : NAT) : nat := match n with ZERO => O | inNAT (inr n) => S (nat_of_NAT n) end. Coercion nat_of_NAT : NAT >-> nat. Fixpoint listnat_of_LIST (l : LIST) : list nat := match l with NIL => nil |inLIST (inr (hd,tl)) => (hd : nat) :: (listnat_of_LIST tl) end. Definition listnat := list nat. (***********************) (* Start reading here. *) (* type UNIT - intro form: () - elimination form: none type A * B - intro form: (a, b) - elimination forms: fst, snd also: let (a, b) := A in ... type A + B - intro forms: inl _ a, inr _ b - elimination form: case e (fun x1 => e1) (fun x2 => e2) also, if you want to eliminate on (unit + A) then you can use: caseu e e1 (fun x2 => e2) type BOOL - intro forms: TRUE, FALSE - elimination form: IFBOOL b THEN e1 ELSE e2 type A -> B - intro forms: fun x : A => e - elimination form: e1 e2 type NAT = mu_i t.(unit + t) - intro form: inNAT :: (unit + NAT) -> NAT syntactic sugar: ZERO :: NAT = inNAT (inl _ ()), SUCC :: NAT -> NAT = fun n => inNAT (inr _ n) also, you can use normal number literals, provided that you convert them into the NAT type (otherwise you'll get a type error because they have Coq's default natural number type): 1:NAT, 2:NAT, 3:NAT, ... if you want to evaluate and print an expression E of natural number type, you can use the command: Eval cbv in (E : nat). - elimination forms: recNAT :: ((unit + A) -> A) -> (NAT -> A) type LIST = mu_i t.(unit + NAT * t) - intro form: inLIST :: (unit + NAT * LIST) -> LIST syntactic sugar: NIL :: LIST = inLIST (inl _ ()) CONS :: NAT -> LIST -> LIST = fun a => fun b => inLIST (inr _ (a,b)) - elimination forms: recLIST :: ((unit + NAT * A) -> A) -> (LIST -> A) if you want to evaluate and print an expression E of LIST type, you can use the command: Eval cbv in (listnat_of_LIST E). listnat_of_LIST converts the list into Coq's native type, so that you can get a more readable output. type STREAM = mu_f t.(NAT * t) - intro forms: genSTREAM :: (A -> (NAT * A)) -> A -> STREAM - elimination form: outSTREAM :: STREAM -> NAT * STREAM *) Definition PLUS : NAT -> NAT -> NAT := fun a : NAT => fun b : NAT => recNAT (fun r : UNIT + NAT => caseu r b SUCC) a. Eval cbv in (PLUS 2 3) : nat.