matita/matita/lib/basics/types.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||
   8     \   /  This file is distributed under the terms of the
   9      \ /   GNU General Public License Version 2
  10       V_______________________________________________________________ *)
  11
  12 include "basics/logic.ma".
  13
  14 (* void *)
  15 inductive void : Type[0] ≝.
  16
  17 (* unit *)
  18 inductive unit : Type[0] ≝ it: unit.
  19
  20 (* Prod *)
  21 record Prod (A,B:Type[0]) : Type[0] ≝ {
  22    fst: A
  23  ; snd: B
  24  }.
  25
  26 interpretation "Pair construction" 'pair x y = (mk_Prod ? ? x y).
  27
  28 interpretation "Product" 'product x y = (Prod x y).
  29
  30 interpretation "pair pi1" 'pi1 = (fst ? ?).
  31 interpretation "pair pi2" 'pi2 = (snd ? ?).
  32 interpretation "pair pi1" 'pi1a x = (fst ? ? x).
  33 interpretation "pair pi2" 'pi2a x = (snd ? ? x).
  34 interpretation "pair pi1" 'pi1b x y = (fst ? ? x y).
  35 interpretation "pair pi2" 'pi2b x y = (snd ? ? x y).
  36
  37 theorem eq_pair_fst_snd: ∀A,B.∀p:A × B.
  38   p = 〈 \fst p, \snd p 〉.
  39 #A #B #p (cases p) // qed.
  40
  41 lemma fst_eq : ∀A,B.∀a:A.∀b:B. \fst 〈a,b〉 = a.
  42 // qed.
  43
  44 lemma snd_eq : ∀A,B.∀a:A.∀b:B. \snd 〈a,b〉 = b.
  45 // qed.
  46
  47 (* sum *)
  48 inductive Sum (A,B:Type[0]) : Type[0] ≝
  49   inl : A → Sum A B
  50 | inr : B → Sum A B.
  51
  52 interpretation "Disjoint union" 'plus A B = (Sum A B).
  53
  54 (* option *)
  55 inductive option (A:Type[0]) : Type[0] ≝
  56    None : option A
  57  | Some : A → option A.
  58
  59 (* sigma *)
  60 inductive Sig (A:Type[0]) (f:A→Type[0]) : Type[0] ≝
  61   dp: ∀a:A.(f a)→Sig A f.
  62
  63 interpretation "Sigma" 'sigma x = (Sig ? x).