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 (* sum *)
  21 inductive Sum (A,B:Type[0]) : Type[0] ≝
  22   inl : A → Sum A B
  23 | inr : B → Sum A B.
  24
  25 interpretation "Disjoint union" 'plus A B = (Sum A B).
  26
  27 (* option *)
  28 inductive option (A:Type[0]) : Type[0] ≝
  29    None : option A
  30  | Some : A → option A.
  31
  32 (* sigma *)
  33 inductive Sig (A:Type[0]) (f:A→Type[0]) : Type[0] ≝
  34   dp: ∀a:A.(f a)→Sig A f.
  35
  36 interpretation "Sigma" 'sigma x = (Sig ? x).
  37
  38 (* Prod *)
  39
  40 record Prod (A,B:Type[0]) : Type[0] ≝ {
  41    fst: A
  42  ; snd: B
  43  }.
  44
  45 interpretation "Pair construction" 'pair x y = (mk_Prod ? ? x y).
  46
  47 interpretation "Product" 'product x y = (Prod x y).
  48
  49 interpretation "pair pi1" 'pi1 = (fst ? ?).
  50 interpretation "pair pi2" 'pi2 = (snd ? ?).
  51 interpretation "pair pi1" 'pi1a x = (fst ? ? x).
  52 interpretation "pair pi2" 'pi2a x = (snd ? ? x).
  53 interpretation "pair pi1" 'pi1b x y = (fst ? ? x y).
  54 interpretation "pair pi2" 'pi2b x y = (snd ? ? x y).
  55
  56 notation "π1" with precedence 10 for @{ (proj1 ??) }.
  57 notation "π2" with precedence 10 for @{ (proj2 ??) }.
  58
  59 (* Yeah, I probably ought to do something more general... *)
  60 notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c\rangle)"
  61 with precedence 90 for @{ 'triple $a $b $c}.
  62 interpretation "Triple construction" 'triple x y z = (mk_Prod ? ? (mk_Prod ? ? x y) z).
  63
  64 notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c, break term 19 d\rangle)"
  65 with precedence 90 for @{ 'quadruple $a $b $c $d}.
  66 interpretation "Quadruple construction" 'quadruple w x y z = (mk_Prod ? ? (mk_Prod ? ? w x) (mk_Prod ? ? y z)).
  67
  68
  69 theorem eq_pair_fst_snd: ∀A,B.∀p:A × B.
  70   p = 〈 \fst p, \snd p 〉.
  71 #A #B #p (cases p) // qed.
  72
  73 lemma fst_eq : ∀A,B.∀a:A.∀b:B. \fst 〈a,b〉 = a.
  74 // qed.
  75
  76 lemma snd_eq : ∀A,B.∀a:A.∀b:B. \snd 〈a,b〉 = b.
  77 // qed.
  78
  79 notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
  80  with precedence 10
  81 for @{ match $t with [ mk_Prod ${ident x} ${ident y} ⇒ $s ] }.
  82
  83 notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉 \nbsp≝ break t \nbsp 'in' \nbsp) break s)"
  84  with precedence 10
  85 for @{ match $t with [ mk_Prod (${ident x}:$X) (${ident y}:$Y) ⇒ $s ] }.
  86
  87 (* Also extracts an equality proof (useful when not using Russell). *)
  88 notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)"
  89  with precedence 10
  90 for @{ match $t return λx.x = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒
  91         λ${ident E}.$s ] (refl ? $t) }.
  92
  93 notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉 \nbsp 'as'\nbsp ident E\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
  94  with precedence 10
  95 for @{ match $t return λ${ident k}:$X.$eq $T $k $t → ? with [ mk_Prod (${ident x}:$U) (${ident y}:$W) ⇒
  96         λ${ident E}:$e.$s ] ($refl $T $t) }.
  97
  98 notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
  99  with precedence 10
 100 for @{ match $t return λx.x = $t → ? with [ mk_Prod ${fresh xy} ${ident z} ⇒
 101        match ${fresh xy} return λx. ? = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒
 102         λ${ident E}.$s ] ] (refl ? $t) }.
 103
 104 notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y,ident z〉 \nbsp'as'\nbsp ident E\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
 105  with precedence 10
 106 for @{ match $t return λ${ident x}.$eq $T $x $t → $U with [ mk_Prod (${fresh xy}:$V) (${ident z}:$Z) ⇒
 107        match ${fresh xy} return λ${ident y}. $eq $R $r $t → ? with [ mk_Prod (${ident x}:$L) (${ident y}:$I) ⇒
 108         λ${ident E}:$J.$s ] ] ($refl $A $t) }.
 109
 110 notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)"
 111  with precedence 10
 112 for @{ match $t with [ mk_Prod ${fresh wx} ${fresh yz} ⇒ match ${fresh wx} with [ mk_Prod ${ident w} ${ident x} ⇒ match ${fresh yz} with [ mk_Prod ${ident y} ${ident z} ⇒ $s ] ] ] }.
 113
 114 notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)"
 115  with precedence 10
 116 for @{ match $t with [ mk_Prod ${fresh xy} ${ident z} ⇒ match ${fresh xy} with [ mk_Prod ${ident x} ${ident y} ⇒ $s ] ] }.
 117
 118 (* This appears to upset automation (previously provable results require greater
 119    depth or just don't work), so use example rather than lemma to prevent it
 120    being indexed. *)
 121 example contract_pair : ∀A,B.∀e:A×B. (let 〈a,b〉 ≝ e in 〈a,b〉) = e.
 122 #A #B * // qed.
 123
 124 lemma extract_pair : ∀A,B,C,D.  ∀u:A×B. ∀Q:A → B → C×D. ∀x,y.
 125 ((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) →
 126 ∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉.
 127 #A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed.
 128
 129 lemma breakup_pair : ∀A,B,C:Type[0].∀x. ∀R:C → Prop. ∀P:A → B → C.
 130   R (P (\fst x) (\snd x)) → R (let 〈a,b〉 ≝ x in P a b).
 131 #A #B #C *; normalize /2/
 132 qed.
 133
 134 lemma pair_elim:
 135   ∀A,B,C: Type[0].
 136   ∀T: A → B → C.
 137   ∀p.
 138   ∀P: A×B → C → Prop.
 139     (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) →
 140       P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
 141  #A #B #C #T * /2/
 142 qed.
 143
 144 lemma pair_elim2:
 145   ∀A,B,C,C': Type[0].
 146   ∀T: A → B → C.
 147   ∀T': A → B → C'.
 148   ∀p.
 149   ∀P: A×B → C → C' → Prop.
 150     (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) →
 151       P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
 152  #A #B #C #C' #T #T' * /2/
 153 qed.
 154
 155 (* Useful for avoiding destruct's full normalization. *)
 156 lemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → a1 = a2.
 157 #A #B #a1 #a2 #b1 #b2 #H destruct //
 158 qed.
 159
 160 lemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → b1 = b2.
 161 #A #B #a1 #a2 #b1 #b2 #H destruct //
 162 qed.
 163
 164 lemma pair_destruct_1:
 165  ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → a = \fst c.
 166  #A #B #a #b *; /2/
 167 qed.
 168
 169 lemma pair_destruct_2:
 170  ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c.
 171  #A #B #a #b *; /2/
 172 qed.