helm/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 set "baseuri" "cic:/matita/datatypes/constructors/".
  16 include "logic/equality.ma".
  17
  18 inductive void : Set \def.
  19
  20 inductive Prod (A,B:Set) : Set \def
  21 pair : A \to B \to Prod A B.
  22
  23 definition fst \def \lambda A,B:Set.\lambda p: Prod A B.
  24 match p with
  25 [(pair a b) \Rightarrow a].
  26
  27 definition snd \def \lambda A,B:Set.\lambda p: Prod A B.
  28 match p with
  29 [(pair a b) \Rightarrow b].
  30
  31 theorem eq_pair_fst_snd: \forall A,B:Set.\forall p: Prod A B.
  32 p = pair A B (fst A B p) (snd A B p).
  33 intros.elim p.simplify.reflexivity.
  34 qed.
  35
  36 inductive Sum (A,B:Set) : Set \def
  37   inl : A \to Sum A B
  38 | inr : B \to Sum A B.