WtypesInCoq

root edited this page Oct 11, 2017 · 3 revisions
``````(** * Primitives constructions of W_types *)
(** ** Definition of W_trees for the recursivity *)
Inductive W_tree
(constructeur : Type)
(parametre: constructeur -> Type)
: Type :=
W_acc: forall (cons: constructeur)
(pars: parametre cons -> W_tree constructeur parametre),
W_tree constructeur parametre.
(** ** Definition of empty type to have leaves in W_trees *)
Inductive Empty: Type :=.
(** ** Definition of the binary sum to have a type with at least two constructors *)
Inductive BinarySum (A: Type) (B: Type): Type :=
| Left: A -> BinarySum A B
| Right: B -> BinarySum A B.
(** ** Definition of the dependant sum for existentials *)
Inductive DependantSum (A: Type) (f: A -> Type): Type :=
| Exist: forall a, f a -> DependantSum A f.
(** ** Definition of the dependant products for universals *)
Inductive DependantProduct (A: Type) (f: A -> Type) :=
| Forall: (forall a, f a) -> DependantProduct A f.
(** * Given a type, we have a predicate to tell if it is a W_type one *)
Inductive WTYPE: Type -> Prop :=
| WW_tree: forall C P, WTYPE C -> (forall c, WTYPE (P c)) -> WTYPE (W_tree C P)
| WEmpty: WTYPE Empty
| WBSum: forall A B, WTYPE A -> WTYPE B -> WTYPE (BinarySum A B)
| WDSum: forall A f, WTYPE A -> (forall a, WTYPE (f a)) ->
WTYPE (DependantSum A f)
| WProduct: forall A f, WTYPE A -> (forall a, WTYPE (f a)) ->
WTYPE (DependantProduct A f).
(** * Now, we require extensionnality to build w_types such as natural numbers *)
Axiom ext: forall A B (f g: A -> B),
(forall a, f a = g a) -> g = f.
Ltac cext H := case (ext _ _ _ _ H).
(** * A cast from empty type to any other *)
Definition Leaf (T: Type) (a: Empty): T := match a with end.
Lemma Leaf_elim: forall (A: Type) (f g: Empty -> A), g = f.
Proof.
intros A f g.
apply ext; intros [].
Qed.
(** Now, w_types are fully defined.
Next section presents some examples. *)
(** * Some well known types seen as w_types *)
(** ** Unit type *)
Definition Unit := DependantProduct Empty (fun _ => Empty).
Lemma WUnit: WTYPE Unit.
Proof WProduct _ _ WEmpty (Leaf (WTYPE Empty)).
Definition single: Unit := Forall _ _ (Leaf Empty).
Lemma all_unit_is_single: forall u, single = u.
Proof.
intros u; destruct u.
case (Leaf_elim _ e (Leaf Empty)).
split.
Qed.
(** ** Booleans type *)
Definition Bool := BinarySum Unit Unit.
Lemma WBool: WTYPE Bool.
Proof WBSum _ _ WUnit WUnit.
Definition top: Bool := Left _ _ single.
Definition bottom: Bool := Right _ _ single.
Definition Ift (A B: Type) (t: Bool): Type :=
if t then A else B.
Definition If (A B: Type) (P: Type -> Type) (Pt: P A) (Pb: P B)
(t: Bool): P (Ift A B t) :=
if t as t0 return P (Ift A B t0)
then Pt
else Pb.
(** ** Naturals type *)
Definition Nat := W_tree Bool (Ift Empty Unit).
Lemma WNat: WTYPE Nat.
Proof WW_tree _ _ WBool (If _ _ _ WEmpty WUnit).
Definition O: Nat := W_acc _ _ top (Leaf _).
Definition S (n: Nat) : Nat := W_acc _ _ bottom (fun _ => n).
Lemma Nat_ind: forall (P : Nat -> Prop), P O -> (forall n, P n -> P (S n)) ->
forall n, P n.
induction n.
destruct cons; simpl in *.
case (Leaf_elim _ pars (Leaf Nat)).
case (all_unit_is_single u).
assumption.
unfold S in H0.
case (all_unit_is_single u).
assert (K := H0 _ (H1 single)); clear H0; simpl in K.
assert ((fun _ : Unit => pars single) = pars).
apply ext; intro a; case (all_unit_is_single a); split.
case H0; assumption.
Qed.
(** ** And eventually parametric lists type *)
Definition List (A : Type) := W_tree (BinarySum Unit A)
(fun b => if b then Empty else Unit).
Lemma WList: forall A, WTYPE A -> WTYPE (List A).
Proof.
intros A WA; apply WW_tree.
apply WBSum.
exact WUnit.
exact WA.
intros []; intro.
exact WEmpty.
exact WUnit.
Qed.
Definition Nil A : List A := W_acc _ _ (Left _ _ single) (Leaf _).
Definition Cons A (a: A) (l: List A): List A :=
W_acc _ _ (Right _ _ a) (fun _ => l).
``````
Clone this wiki locally
You can’t perform that action at this time.
Press h to open a hovercard with more details.