weblib/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 \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 B.
  29   match p with [pair a b ⇒ a].
  30
  31 definition snd ≝ λA,B.λp:A \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 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 \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 B.
  42   p \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p, \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 p 〉.
  43 #A #B #p (cases p) // qed.
  44
  45 (* sum *)
  46 inductive Sum (A,B:Type[0]) : Type[0] ≝
  47   inl : A → Sum A B
  48 | inr : B → Sum A B.
  49
  50 interpretation "Disjoint union" 'plus A B = (Sum A B).
  51
  52 (* option *)
  53 inductive option (A:Type[0]) : Type[0] ≝
  54    None : option A
  55  | Some : A → option A.
  56
  57 (* sigma *)
  58 inductive Sig (A:Type[0]) (f:A→Type[0]) : Type[0] ≝
  59   dp: ∀a:A.(f a)→Sig A f.
  60
  61 interpretation "Sigma" 'sigma x = (Sig ? x).