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 inductive Prod (A,B:Type[0]) : Type[0] ≝
  22 pair : A → B → 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 ≝ λA,B.λp:A × B.
  29   match p with [pair a b ⇒ a].
  30
  31 definition snd ≝ λA,B.λp:A × B.
  32   match p with [pair a b ⇒ b].
  33
  34 interpretation "pair pi1" 'pi1 = (fst ? ?).
  35 interpretation "pair pi2" 'pi2 = (snd ? ?).
  36 interpretation "pair pi1" 'pi1a x = (fst ? ? x).
  37 interpretation "pair pi2" 'pi2a x = (snd ? ? x).
  38 interpretation "pair pi1" 'pi1b x y = (fst ? ? x y).
  39 interpretation "pair pi2" 'pi2b x y = (snd ? ? x y).
  40
  41 theorem eq_pair_fst_snd: ∀A,B.∀p:A × B.
  42   p = 〈 \fst p, \snd p 〉.
  43 #A #B #p (cases p) // qed.
  44
  45 lemma fst_eq : ∀A,B.∀a:A.∀b:B. \fst 〈a,b〉 = a.
  46 // qed.
  47
  48 lemma snd_eq : ∀A,B.∀a:A.∀b:B. \snd 〈a,b〉 = b.
  49 // qed.
  50
  51 (* sum *)
  52 inductive Sum (A,B:Type[0]) : Type[0] ≝
  53   inl : A → Sum A B
  54 | inr : B → Sum A B.
  55
  56 interpretation "Disjoint union" 'plus A B = (Sum A B).
  57
  58 (* option *)
  59 inductive option (A:Type[0]) : Type[0] ≝
  60    None : option A
  61  | Some : A → option A.
  62
  63 (* sigma *)
  64 inductive Sig (A:Type[0]) (f:A→Type[0]) : Type[0] ≝
  65   dp: ∀a:A.(f a)→Sig A f.
  66
  67 interpretation "Sigma" 'sigma x = (Sig ? x).