helm/software/matita/library/datatypes/constructors.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "logic/equality.ma".
  16
  17 inductive void : Set \def.
  18
  19 inductive unit : Set ≝ something: unit.
  20
  21 inductive Prod (A,B:Type) : Type \def
  22 pair : A \to B \to Prod A B.
  23
  24 interpretation "Pair construction" 'pair x y = (pair ? ? x y).
  25
  26 interpretation "Product" 'product x y = (Prod x y).
  27
  28 definition fst \def \lambda A,B:Type.\lambda p: Prod A B.
  29 match p with
  30 [(pair a b) \Rightarrow a].
  31
  32 definition snd \def \lambda A,B:Type.\lambda p: Prod A B.
  33 match p with
  34 [(pair a b) \Rightarrow b].
  35
  36 interpretation "pair pi1" 'pi1 = (fst ? ?).
  37 interpretation "pair pi2" 'pi2 = (snd ? ?).
  38 interpretation "pair pi1" 'pi1a x = (fst ? ? x).
  39 interpretation "pair pi2" 'pi2a x = (snd ? ? x).
  40 interpretation "pair pi1" 'pi1b x y = (fst ? ? x y).
  41 interpretation "pair pi2" 'pi2b x y = (snd ? ? x y).
  42
  43 theorem eq_pair_fst_snd: \forall A,B:Type.\forall p:Prod A B.
  44 p = 〈 \fst p, \snd p 〉.
  45 intros.elim p.simplify.reflexivity.
  46 qed.
  47
  48 inductive Sum (A,B:Type) : Type \def
  49   inl : A \to Sum A B
  50 | inr : B \to Sum A B.
  51
  52 interpretation "Disjoint union" 'plus A B = (Sum A B).
  53
  54 inductive option (A:Type) : Type ≝
  55    None : option A
  56  | Some : A → option A.