Library Coq.Init.Datatypes

Set Implicit Arguments.

Require Import Notations.
Require Import Logic.

Datatypes with zero and one element

Empty_set is a datatype with no inhabitant

Inductive Empty_set : Set :=.

unit is a singleton datatype with sole inhabitant tt

Inductive unit : Set :=
tt : unit.

The boolean datatype

bool is the datatype of the boolean values true and false

Inductive bool : Set :=
| true : bool
| false : bool.

Add Printing If bool.

Delimit Scope bool_scope with bool.

Basic boolean operators

Definition andb (b1 b2:bool) : bool := if b1 then b2 else false.

Definition orb (b1 b2:bool) : bool := if b1 then true else b2.

Definition implb (b1 b2:bool) : bool := if b1 then b2 else true.

Definition xorb (b1 b2:bool) : bool :=
  match b1, b2 with
    | true, true => false
    | true, false => true
    | false, true => true
    | false, false => false
  end.

Definition negb (b:bool) := if b then false else true.

Infix "||" := orb : bool_scope.
Infix "&&" := andb : bool_scope.

Basic properties of andb

Lemma andb_prop : forall a b:bool, andb a b = true -> a = true /\ b = true.
Hint Resolve andb_prop: bool.

Lemma andb_true_intro :
forall b1 b2:bool, b1 = true /\ b2 = true -> andb b1 b2 = true.
Hint Resolve andb_true_intro: bool.

Interpretation of booleans as propositions

Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.

Hint Constructors eq_true : eq_true.

Another way of interpreting booleans as propositions

Definition is_true b := b = true.

is_true can be activated as a coercion by (Local) Coercion is_true : bool >-> Sortclass.

Additional rewriting lemmas about eq_true

Lemma eq_true_ind_r :
  forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true.

Lemma eq_true_rec_r :
  forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true.

Lemma eq_true_rect_r :
  forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true.

The BoolSpec inductive will be used to relate a boolean value and two propositions corresponding respectively to the true case and the false case. Interest: BoolSpec behave nicely with case and destruct. See also Bool.reflect when Q = ~P.

Inductive BoolSpec (P Q : Prop) : bool -> Prop :=
| BoolSpecT : P -> BoolSpec P Q true
| BoolSpecF : Q -> BoolSpec P Q false.
Hint Constructors BoolSpec : core.

Peano natural numbers

nat is the datatype of natural numbers built from O and successor S; note that the constructor name is the letter O. Numbers in nat can be denoted using a decimal notation; e.g. 3%nat abbreviates S (S (S O))

Inductive nat : Set :=
| O : nat
| S : nat -> nat.

Delimit Scope nat_scope with nat.

Container datatypes

option A is the extension of A with an extra element None

#[universes(template)]
Inductive option (A:Type) : Type :=
  | Some : A -> option A
  | None : option A.

Definition option_map (A B:Type) (f:A ->B) (o : option A) : option B :=
  match o with
    | Some a => @Some B (f a)
    | None => @None B
  end.

sum A B, written A + B, is the disjoint sum of A and B

#[universes(template)]
Inductive sum (A B:Type) : Type :=
| inl : A -> sum A B
| inr : B -> sum A B.

Notation "x + y" := (sum x y) : type_scope.

prod A B, written A * B, is the product of A and B; the pair pair A B a b of a and b is abbreviated (a,b)

#[universes(template)]
Inductive prod (A B:Type) : Type :=
  pair : A -> B -> A * B

where "x * y" := (prod x y) : type_scope.

Add Printing Let prod.

Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.

Section projections.
  Context {A : Type} {B : Type}.

  Definition fst (p:A * B) := match p with (x, y) => x end.
  Definition snd (p:A * B) := match p with (x, y) => y end.

End projections.

Hint Resolve pair inl inr: core.

Lemma surjective_pairing :
  forall (A B:Type) (p:A * B), p = (fst p , snd p ).

Lemma injective_projections :
  forall (A B:Type) (p1 p2:A * B),
    fst p1 = fst p2 -> snd p1 = snd p2 -> p1 = p2.

Lemma pair_equal_spec :
  forall (A B : Type) (a1 a2 : A) (b1 b2 : B),
    (a1 , b1 ) = (a2 , b2 ) <-> a1 = a2 /\ b1 = b2.

Definition prod_uncurry (A B C:Type) (f:A * B -> C)
  (x:A) (y:B) : C := f (x ,y ).

Definition prod_curry (A B C:Type) (f:A -> B -> C)
  (p:A * B) : C := match p with (x, y) => f x y end.

Import EqNotations.

Lemma rew_pair : forall A (P Q : A ->Type) x1 x2 (y1:P x1) (y2:Q x1) (H:x1 =x2),
  (rew H in y1 , rew H in y2 ) = rew [fun x => (P x * Q x)%type] H in (y1 ,y2 ).

Polymorphic lists and some operations

#[universes(template)]
Inductive list (A : Type) : Type :=
| nil : list A
| cons : A -> list A -> list A.

Delimit Scope list_scope with list.

Infix "::" := cons (at level 60, right associativity) : list_scope.

Local Open Scope list_scope.

Definition length (A : Type) : list A -> nat :=
  fix length l :=
  match l with
   | nil => O
   | _ :: l' => S (length l')
  end.

Concatenation of two lists

Definition app (A : Type) : list A -> list A -> list A :=
  fix app l m :=
  match l with
   | nil => m
   | a :: l1 => a :: app l1 m
  end.

Infix "++" := app (right associativity, at level 60) : list_scope.

The comparison datatype

Inductive comparison : Set :=
  | Eq : comparison
  | Lt : comparison
  | Gt : comparison.

Lemma comparison_eq_stable : forall c c' : comparison, ~~ c = c' -> c = c'.

Definition CompOpp (r:comparison) :=
  match r with
    | Eq => Eq
    | Lt => Gt
    | Gt => Lt
  end.

Lemma CompOpp_involutive : forall c, CompOpp (CompOpp c) = c.

Lemma CompOpp_inj : forall c c', CompOpp c = CompOpp c' -> c = c'.

Lemma CompOpp_iff : forall c c', CompOpp c = c' <-> c = CompOpp c'.

The CompareSpec inductive relates a comparison value with three propositions, one for each possible case. Typically, it can be used to specify a comparison function via some equality and order predicates. Interest: CompareSpec behave nicely with case and destruct.

Inductive CompareSpec (Peq Plt Pgt : Prop) : comparison -> Prop :=
| CompEq : Peq -> CompareSpec Peq Plt Pgt Eq
| CompLt : Plt -> CompareSpec Peq Plt Pgt Lt
| CompGt : Pgt -> CompareSpec Peq Plt Pgt Gt.
Hint Constructors CompareSpec : core.

For having clean interfaces after extraction, CompareSpec is declared in Prop. For some situations, it is nonetheless useful to have a version in Type. Interestingly, these two versions are equivalent.

Inductive CompareSpecT (Peq Plt Pgt : Prop) : comparison -> Type :=
| CompEqT : Peq -> CompareSpecT Peq Plt Pgt Eq
| CompLtT : Plt -> CompareSpecT Peq Plt Pgt Lt
| CompGtT : Pgt -> CompareSpecT Peq Plt Pgt Gt.
Hint Constructors CompareSpecT : core.

Lemma CompareSpec2Type : forall Peq Plt Pgt c,
CompareSpec Peq Plt Pgt c -> CompareSpecT Peq Plt Pgt c.

As an alternate formulation, one may also directly refer to predicates eq and lt for specifying a comparison, rather that fully-applied propositions. This CompSpec is now a particular case of CompareSpec.

Definition CompSpec {A} (eq lt : A ->A ->Prop)(x y:A) : comparison -> Prop :=
CompareSpec (eq x y) (lt x y) (lt y x).

Definition CompSpecT {A} (eq lt : A ->A ->Prop)(x y:A) : comparison -> Type :=
CompareSpecT (eq x y) (lt x y) (lt y x).
Hint Unfold CompSpec CompSpecT : core.

Lemma CompSpec2Type : forall A (eq lt:A ->A ->Prop) x y c,
CompSpec eq lt x y c -> CompSpecT eq lt x y c.

Misc Other Datatypes

identity A a is the family of datatypes on A whose sole non-empty member is the singleton datatype identity A a a whose sole inhabitant is denoted identity_refl A a Beware: this inductive actually falls into Prop, as the sole constructor has no arguments and -indices-matter is not activated in the standard library.

Inductive identity (A:Type) (a:A) : A -> Type :=
identity_refl : identity a a.
Hint Resolve identity_refl: core.

Identity type

Definition ID := forall A:Type, A -> A.
Definition id : ID := fun A x => x.

Definition IDProp := forall A:Prop, A -> A.
Definition idProp : IDProp := fun A x => x.