(** Simply typed programming *) (** for masking stdlib definnitions *) Module LocalDefinitions. Check true. Check false. Definition negb (b:bool) := match b with | true => false | false => true end. Compute negb (negb false). Definition orb (b1 b2: bool) := if b1 then true else b2. (** exercice : definir andb, implb, iffb *) Compute implb true false. (** Peano numbers *) Definition pred (n : nat) := match n with O => O | S p => p end. Compute pred 10. Fixpoint plus (n p : nat) : nat := match n with |O => p | S m => S (plus m p) end. Infix "+" := plus : nat_scope. Compute 3 + 9. (** exercice Definir la multiplication sur nat *) End LocalDefinitions. (** On retrouve les definitions de la bibliotheque standard ...*) (** exercice : definir une fonction puissance expt (x n : nat) : nat (non adaptée aux grands nombres) *) (* Compute expt 2 3. *) (** Binary numbers *) Require Import ZArith. Print positive. (* Inductive positive : Set := xI : positive -> positive | xO : positive -> positive | xH : positive *) Check xO (xI xH). Check 6%positive. Open Scope positive_scope. Check 6. Fixpoint pos_succ (p:positive) : positive := match p with | xH => 2 | xO q => xI q | xI q => xO (pos_succ q) end. Compute pos_succ 9. Fixpoint pos_plus (p q : positive) : positive := match p, q with | xH, _ => pos_succ q | _, xH => pos_succ p | p ~0, q ~0 => (pos_plus p q) ~ 0 | p ~0, q ~1| p ~1, q ~0 => (pos_plus p q) ~ 1 | p ~1, q ~1 => (pos_succ (pos_plus p q)) ~0 end. Compute pos_plus 9 8. Compute pos_plus 67679 89899999. Print N. (* Inductive N : Set := N0 : N | Npos : positive -> N *) Definition N_succ (n:N) : N := match n with 0%N => 1%N | Npos p => Npos (pos_succ p) end. Compute N_succ 9999%N. Definition N_plus (n m:N) := match n, m with | 0%N, _ => m | _, 0%N => n | Npos p, Npos q => Npos (pos_plus p q) end. Compute N_plus 56 999. Print Z. (* Inductive Z : Set := Z0 : Z | Zpos : positive -> Z | Zneg : positive -> Z *) Check xO (xO (xI (xO xH))). (* 20%positive : positive *) Check Zneg (xO (xO (xI (xO xH)))). (** Exercice Definir la division entière par deux N_div2 : N -> N et le logarithme de base 2 pos_log2 : positive -> N *)