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/core_notation/pair_2.ma".
  13 include "basics/logic.ma".
  14
  15 (* void *)
  16 inductive void : Type[0] ≝.
  17
  18 (* unit *)
  19 inductive unit : Type[0] ≝ it: unit.
  20
  21 (* sum *)
  22 inductive Sum (A,B:Type[0]) : Type[0] ≝
  23   inl : A → Sum A B
  24 | inr : B → Sum A B.
  25
  26 interpretation "Disjoint union" 'plus A B = (Sum A B).
  27
  28 (* option *)
  29 inductive option (A:Type[0]) : Type[0] ≝
  30    None : option A
  31  | Some : A → option A.
  32
  33 definition option_map : ∀A,B:Type[0]. (A → B) → option A → option B ≝
  34 λA,B,f,o. match o with [ None ⇒ None B | Some a ⇒ Some B (f a) ].
  35
  36 lemma option_map_none : ∀A,B,f,x.
  37   option_map A B f x = None B → x = None A.
  38 #A #B #f * [ // | #a #E whd in E:(??%?); destruct ]
  39 qed.
  40
  41 lemma option_map_some : ∀A,B,f,x,v.
  42   option_map A B f x = Some B v → ∃y. x = Some ? y ∧ f y = v.
  43 #A #B #f *
  44 [ #v normalize #E destruct
  45 | #y #v normalize #E %{y} destruct % //
  46 ] qed.
  47
  48 definition option_map_def : ∀A,B:Type[0]. (A → B) → B → option A → B ≝
  49 λA,B,f,d,o. match o with [ None ⇒ d | Some a ⇒ f a ].
  50
  51 lemma refute_none_by_refl : ∀A,B:Type[0]. ∀P:A → B. ∀Q:B → Type[0]. ∀x:option A. ∀H:x = None ? → False.
  52   (∀v. x = Some ? v → Q (P v)) →
  53   Q (match x return λy.x = y → ? with [ Some v ⇒ λ_. P v | None ⇒ λE. match H E in False with [ ] ] (refl ? x)).
  54 #A #B #P #Q *
  55 [ #H cases (H (refl ??))
  56 | #a #H #p normalize @p @refl
  57 ] qed.
  58
  59 (* dependent pair *)
  60 record DPair (A:Type[0]) (f:A→Type[0]) : Type[0] ≝ {
  61     dpi1:> A
  62   ; dpi2: f dpi1
  63   }.
  64
  65 interpretation "DPair" 'dpair x = (DPair ? x).
  66
  67 interpretation "mk_DPair" 'mk_DPair x y = (mk_DPair ?? x y).
  68
  69 (* sigma *)
  70 record Sig (A:Type[0]) (f:A→Prop) : Type[0] ≝ {
  71     pi1: A  (* not a coercion due to problems with Cerco *)
  72   ; pi2: f pi1
  73   }.
  74
  75 interpretation "Sigma" 'sigma x = (Sig ? x).
  76
  77 interpretation "mk_Sig" 'dp x y = (mk_Sig ?? x y).
  78
  79 lemma sub_pi2 : ∀A.∀P,P':A → Prop. (∀x.P x → P' x) → ∀x:Σx:A.P x. P' (pi1 … x).
  80 #A #P #P' #H1 * #x #H2 @H1 @H2
  81 qed.
  82
  83 lemma inj_mk_Sig: ∀A,P.∀x. x = mk_Sig A P (pi1 A P x) (pi2 A P x).
  84 #A #P #x cases x //
  85 qed-.
  86 (* Prod *)
  87
  88 record Prod (A,B:Type[0]) : Type[0] ≝ {
  89    fst: A
  90  ; snd: B
  91  }.
  92
  93 interpretation "Pair construction" 'pair x y = (mk_Prod ? ? x y).
  94
  95 interpretation "Product" 'product x y = (Prod x y).
  96
  97 interpretation "pair pi1" 'pi1 = (fst ? ?).
  98 interpretation "pair pi2" 'pi2 = (snd ? ?).
  99 interpretation "pair pi1" 'pi1a x = (fst ? ? x).
 100 interpretation "pair pi2" 'pi2a x = (snd ? ? x).
 101 interpretation "pair pi1" 'pi1b x y = (fst ? ? x y).
 102 interpretation "pair pi2" 'pi2b x y = (snd ? ? x y).
 103
 104 notation "π1" with precedence 10 for @{ (proj1 ??) }.
 105 notation "π2" with precedence 10 for @{ (proj2 ??) }.
 106
 107 (* Yeah, I probably ought to do something more general... *)
 108 notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c\rangle)"
 109 with precedence 90 for @{ 'triple $a $b $c}.
 110 interpretation "Triple construction" 'triple x y z = (mk_Prod ? ? (mk_Prod ? ? x y) z).
 111
 112 notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c, break term 19 d\rangle)"
 113 with precedence 90 for @{ 'quadruple $a $b $c $d}.
 114 interpretation "Quadruple construction" 'quadruple w x y z = (mk_Prod ? ? (mk_Prod ? ? w x) (mk_Prod ? ? y z)).
 115
 116
 117 theorem eq_pair_fst_snd: ∀A,B.∀p:A × B.
 118   p = 〈 \fst p, \snd p 〉.
 119 #A #B #p (cases p) // qed.
 120
 121 lemma fst_eq : ∀A,B.∀a:A.∀b:B. \fst 〈a,b〉 = a.
 122 // qed.
 123
 124 lemma snd_eq : ∀A,B.∀a:A.∀b:B. \snd 〈a,b〉 = b.
 125 // qed.
 126
 127 notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
 128  with precedence 10
 129 for @{ match $t with [ mk_Prod ${ident x} ${ident y} ⇒ $s ] }.
 130
 131 notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉 \nbsp≝ break t \nbsp 'in' \nbsp) break s)"
 132  with precedence 10
 133 for @{ match $t with [ mk_Prod (${ident x}:$X) (${ident y}:$Y) ⇒ $s ] }.
 134
 135 (* Also extracts an equality proof (useful when not using Russell). *)
 136 notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)"
 137  with precedence 10
 138 for @{ match $t return λx.x = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒
 139         λ${ident E}.$s ] (refl ? $t) }.
 140
 141 notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉 \nbsp 'as'\nbsp ident E\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
 142  with precedence 10
 143 for @{ match $t return λ${ident k}:$X.$eq $T $k $t → ? with [ mk_Prod (${ident x}:$U) (${ident y}:$W) ⇒
 144         λ${ident E}:$e.$s ] ($refl $T $t) }.
 145
 146 notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
 147  with precedence 10
 148 for @{ match $t return λx.x = $t → ? with [ mk_Prod ${fresh xy} ${ident z} ⇒
 149        match ${fresh xy} return λx. ? = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒
 150         λ${ident E}.$s ] ] (refl ? $t) }.
 151
 152 notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y,ident z〉 \nbsp 'as' \nbsp ident E\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
 153  with precedence 10
 154 for @{ match $t return λ${ident k}:$X.$eq $T $k $t → $U with [ mk_Prod (${ident xy}:$V) (${ident z}:$Z) ⇒
 155        match $xy return λ${ident a}. $eq $R $r $t → ? with [ mk_Prod (${ident x}:$L) (${ident y}:$I) ⇒
 156         λ${ident E}:$J.$s ] ] ($refl $A $t) }.
 157
 158 notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)"
 159  with precedence 10
 160 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 ] ] ] }.
 161
 162 notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)"
 163  with precedence 10
 164 for @{ match $t with [ mk_Prod ${fresh xy} ${ident z} ⇒ match ${fresh xy} with [ mk_Prod ${ident x} ${ident y} ⇒ $s ] ] }.
 165
 166 (* This appears to upset automation (previously provable results require greater
 167    depth or just don't work), so use example rather than lemma to prevent it
 168    being indexed. *)
 169 example contract_pair : ∀A,B.∀e:A×B. (let 〈a,b〉 ≝ e in 〈a,b〉) = e.
 170 #A #B * // qed.
 171
 172 lemma extract_pair : ∀A,B,C,D.  ∀u:A×B. ∀Q:A → B → C×D. ∀x,y.
 173 ((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) →
 174 ∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉.
 175 #A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed.
 176
 177 lemma breakup_pair : ∀A,B,C:Type[0].∀x. ∀R:C → Prop. ∀P:A → B → C.
 178   R (P (\fst x) (\snd x)) → R (let 〈a,b〉 ≝ x in P a b).
 179 #A #B #C *; normalize /2/
 180 qed.
 181
 182 lemma pair_elim:
 183   ∀A,B,C: Type[0].
 184   ∀T: A → B → C.
 185   ∀p.
 186   ∀P: A×B → C → Prop.
 187     (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) →
 188       P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
 189  #A #B #C #T * /2/
 190 qed.
 191
 192 lemma pair_elim2:
 193   ∀A,B,C,C': Type[0].
 194   ∀T: A → B → C.
 195   ∀T': A → B → C'.
 196   ∀p.
 197   ∀P: A×B → C → C' → Prop.
 198     (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) →
 199       P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
 200  #A #B #C #C' #T #T' * /2/
 201 qed.
 202
 203 (* Useful for avoiding destruct's full normalization. *)
 204 lemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → a1 = a2.
 205 #A #B #a1 #a2 #b1 #b2 #H destruct //
 206 qed.
 207
 208 lemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → b1 = b2.
 209 #A #B #a1 #a2 #b1 #b2 #H destruct //
 210 qed.
 211
 212 lemma pair_destruct_1:
 213  ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → a = \fst c.
 214  #A #B #a #b *; /2/
 215 qed.
 216
 217 lemma pair_destruct_2:
 218  ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c.
 219  #A #B #a #b *; /2/
 220 qed.
 221
 222 lemma coerc_pair_sigma:
 223  ∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x).
 224 #A #B #P * #a #b #p % [@a | /2/]
 225 qed.
 226 coercion coerc_pair_sigma:∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x)
 227 ≝ coerc_pair_sigma on p: (? × ?) to (? × (Sig ??)).