helm/software/matita/contribs/assembly/compiler/sigma.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                                                                        *)
  17 (* Sviluppato da:                                                         *)
  18 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  19 (*                                                                        *)
  20 (* ********************************************************************** *)
  21
  22 (* coppia dipendente *)
  23
  24 inductive sigma (A:Type) (P:A → Type) : Type ≝
  25     sigma_intro: ∀x:A.P x → sigma A P.
  26
  27 notation < "hvbox(\Sigma ident i opt (: tx) break . p)"
  28   right associative with precedence 20
  29 for @{ 'Sigma ${default
  30   @{\lambda ${ident i} : $tx. $p}
  31   @{\lambda ${ident i} . $p}}}.
  32
  33 notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px"
  34   with precedence 20
  35   for ${ default
  36           @{ ${ fold right @{$Px} rec acc @{'Sigma (λ${ident x}:$T.$acc)} } }
  37           @{ ${ fold right @{$Px} rec acc @{'Sigma (λ${ident x}.$acc)} } }
  38        }.
  39
  40 notation "\ll term 19 a, break term 19 b \gg"
  41 with precedence 90 for @{'dependent_pair (λx:?.? x) $a $b}.
  42 interpretation "dependent pair" 'dependent_pair \eta.c a b = (sigma_intro _ c a b).
  43
  44 interpretation "sigma" 'Sigma \eta.x = (sigma _ x).
  45
  46 definition sigmaFst ≝
  47 λT:Type.λf:T → Type.λs:sigma T f.match s with [ sigma_intro x _ ⇒ x ].
  48 definition sigmaSnd ≝
  49 λT:Type.λf:T → Type.λs:sigma T f.match s return λs.f (sigmaFst ?? s) with [ sigma_intro _ x ⇒ x ].
  50
  51 (* tripla dipendente, suggerimento \SHcy *)
  52
  53 inductive bisigma (A,B:Type) (P:A → B → Type) : Type ≝
  54     bisigma_intro: ∀x:A.∀y:B.P x y → bisigma A B P.
  55
  56 definition bisigmaFst ≝
  57 λT1,T2:Type.λf:T1 → T2 → Type.λs:bisigma T1 T2 f.match s with [ bisigma_intro x _ _ ⇒ x ].
  58 definition bisigmaSnd ≝
  59 λT1,T2:Type.λf:T1 → T2 → Type.λs:bisigma T1 T2 f.match s with [ bisigma_intro _ x _ ⇒ x ].
  60 definition bisigmaThd ≝
  61 λT1,T2:Type.λf:T1 → T2 → Type.λs:bisigma T1 T2 f.match s return λs.f (bisigmaFst ??? s) (bisigmaSnd ??? s) with [ bisigma_intro _ _ x ⇒ x ].