matita/matita/contribs/mf/mTT.ma

   1 (* (C) 2014 Luca Bressan *)
   2
   3 include "notations.ma".
   4
   5 universe constraint Type[0] < Type[1].
   6 universe constraint Type[1] < Type[2].
   7
   8 notation "'cl'" with precedence 90 for @{ Type[1] }.
   9 notation "'st'" with precedence 90 for @{ Type[0] }.
  10 notation "'prop'" with precedence 90 for @{ CProp[1] }.
  11 notation "'props'" with precedence 90 for @{ CProp[0] }.
  12
  13 record Sigma (B: cl) (C: B → cl) : cl ≝
  14  { Sig1: B
  15  ; Sig2: C Sig1
  16  }.
  17 interpretation "Strong Indexed Sum" 'sigma x = (Sigma ? x).
  18 interpretation "Strong Indexed Sum constructor" 'mk_sigma x y = (mk_Sigma ?? x y).
  19 interpretation "First projection of Strong Indexed Sum" 'sig1 x = (Sig1 ?? x).
  20 interpretation "Second projection of Strong Indexed Sum" 'sig2 x = (Sig2 ?? x).
  21
  22 definition Times: cl → cl → cl ≝
  23  λB,C. Sigma B (λ_. C).
  24 interpretation "Binary collection product" 'times B C = (Times B C).
  25
  26 inductive n0: st ≝ .
  27
  28 inductive n1: st ≝
  29  star: n1.
  30 interpretation "Element of the singleton" 'star = star.
  31
  32 record sigma (B: st) (C : B → st) : st ≝
  33  { sig1: B
  34  ; sig2: C sig1
  35  }.
  36 interpretation "Strong Indexed Sum set" 'sigma x = (sigma ? x).
  37 interpretation "Strong Indexed Sum set constructor" 'mk_sigma x y = (mk_sigma ?? x y).
  38 interpretation "First projection of Strong Indexed Sum set" 'sig1 x = (sig1 ?? x).
  39 interpretation "Second projection of Strong Indexed Sum set" 'sig2 x = (sig2 ?? x).
  40
  41 definition times: st → st → st ≝
  42  λB,C. sigma B (λ_. C).
  43 interpretation "Binary set product" 'times B C = (times B C).
  44
  45 inductive list (C: st) : st (*CSC: Type[0]*) ≝
  46    epsilon: list C
  47  | cons: list C → C → list C.
  48 interpretation "Empty list" 'epsilon = (epsilon ?).
  49 interpretation "List constructor" 'cons l c = (cons ? l c).
  50
  51 inductive plus (B: st) (C: st) : st ≝
  52    inl: B → plus B C
  53  | inr: C → plus B C.
  54 interpretation "Disjoint Sum set" 'plus B C = (plus B C).
  55
  56 inductive Falsum: prop ≝ .
  57 interpretation "Falsum" 'falsum = Falsum.
  58
  59 inductive Disj (B: prop) (C: prop) : prop ≝
  60    lOr: B → Disj B C
  61  | rOr: C → Disj B C.
  62 interpretation "Disjunction" 'disj B C = (Disj B C).
  63
  64 record Conj (B: prop) (C: prop) : prop ≝
  65  { Conj1: B
  66  ; Conj2: C
  67  }.
  68 interpretation "Conjunction" 'conj B C = (Conj B C).
  69
  70 definition Implies: prop → prop → prop ≝
  71  λB,C: prop. B → C.
  72 interpretation "Implication" 'implies B C = (Implies B C).
  73
  74 record Exists (B: cl) (C: B → prop) : prop ≝
  75  { Ex1: B
  76  ; Ex2: C Ex1
  77  }.
  78 interpretation "Existential quantification" 'exists x = (Exists ? x).
  79 interpretation "Existential quantification constructor" 'mk_exists x y = (mk_Exists ?? x y).
  80
  81 definition Forall: ∀B: cl. (B → prop) → prop ≝ λB,C. ∀b: B. C b.
  82
  83 inductive Id (A: cl) (a: A) : A → prop ≝
  84  Reflexivity: Id A a a.
  85 interpretation "Propositional Equality" 'id a b = (Id ? a b).
  86 interpretation "Reflexivity in Extensional Collections" 'rfl x = (Reflexivity ? x).
  87
  88 definition Verum: prop ≝ Implies Falsum Falsum.
  89 interpretation "Verum" 'verum = Verum.
  90
  91 inductive falsum: props ≝ .
  92 interpretation "Small Falsum" 'falsum = falsum.
  93
  94 inductive disj (B: props) (C: props) : props ≝
  95    lor: B → disj B C
  96  | ror: C → disj B C.
  97 interpretation "Small Disjunction" 'disj B C = (disj B C).
  98
  99 record conj (B: props) (C: props) : props ≝
 100  { conj1: B
 101  ; conj2: C
 102  }.
 103 interpretation "Small Conjunction" 'conj B C = (conj B C).
 104
 105 definition implies: props → props → props ≝
 106  λB,C. B → C.
 107 interpretation "Small Implication" 'implies B C = (implies B C).
 108
 109 record exists (B: st) (C: B → props) : props ≝
 110  { exs1: B
 111  ; exs2: C exs1
 112  }.
 113 interpretation "Small Existential quantification" 'exists x = (exists ? x).
 114 interpretation "Small Existential quantification constructor" 'mk_exists x y = (mk_exists ?? x y).
 115
 116 definition forall: ∀B: st. (B → props) → props ≝ λB,C. ∀b: B. C b.
 117
 118 inductive id (A: st) (a: A) : A → props ≝
 119  reflexivity: id A a a.
 120 interpretation "Small Propositional Equality" 'id a b = (id ? a b).
 121 interpretation "Reflexivity in Extensional Sets" 'rfl x = (reflexivity ? x).
 122
 123 definition verum: props ≝ implies falsum falsum.
 124 interpretation "Verum" 'verum = verum.
 125
 126 definition fun_to_props: st → cl ≝ λB. B → props.
 127
 128 lemma Symmetry: ∀A: cl. ∀x,x': A. x = x' → x' = x.
 129  #A #x #x' * %
 130 qed.
 131 interpretation "Symmetry in Intensional Collections" 'sym d = (Symmetry ??? d).
 132
 133 lemma Transitivity: ∀A: cl. ∀x,x',x'': A. x = x' → x' = x'' → x = x''.
 134  #A #x #x' #x'' * * %
 135 qed.
 136 interpretation "Transitivity in Intensional Collections" 'tra d = (Transitivity ???? d).
 137
 138 lemma rewrite_l: ∀A: st. ∀x: A. ∀P: A → props. P x → ∀y: A. x = y → P y.
 139  #A #x #P #h #y * @h
 140 qed.
 141
 142 notation "hvbox(> h)"
 143  non associative with precedence 45
 144  for @{ 'rewrite_l $h }.
 145 interpretation "Rewrite left" 'rewrite_l h = (rewrite_l ????? h).
 146
 147 lemma symmetry: ∀A: st. ∀x,x': A. x = x' → x' = x.
 148  #A #x #x' * %
 149 qed.
 150 interpretation "Symmetry in Intensional Sets" 'sym d = (symmetry ??? d).
 151
 152 notation "hvbox(< h)"
 153  non associative with precedence 45
 154  for @{ 'rewrite_r $h }.
 155 interpretation "Rewrite right" 'rewrite_r h = (rewrite_l ????? (symmetry ??? h)).
 156
 157 lemma transitivity: ∀A: st. ∀x,x',x'': A. x = x' → x' = x'' → x = x''.
 158  #A #x #x' #x'' * * %
 159 qed.
 160 interpretation "Transitivity in Intensional Sets" 'tra d = (transitivity ???? d).
 161
 162 definition lift_to_list: ∀A,A': st. (A → A') → list A → list A' ≝
 163  λA,A',f. list_rect_Type0 … (λ_. list A') ϵ (λl,x,l'. ⌈l', f x⌉).
 164
 165 definition proj_l: ∀B,C: st. B → plus B C → B ≝
 166  λB,C,b'. plus_rect_Type0 B C (λ_. B) (λb. b) (λ_. b').
 167
 168 definition proj_r: ∀B,C: st. C → plus B C → C ≝
 169  λB,C,c'. plus_rect_Type0 B C (λ_. C) (λ_. c') (λc. c).
 170
 171 lemma injectivity_inl: ∀B,C: st. ∀x,x'. inl B C x = inl B C x' → x = x'.
 172  #B #C #x #x'
 173  @(rewrite_l … (inl … x) (λz. proj_l … x (inl … x) = proj_l … x z)
 174    (ı(proj_l … x (inl … x))) (inl … x'))
 175 qed.
 176
 177 lemma injectivity_inr: ∀B,C: st. ∀y,y'. inr B C y = inr B C y' → y = y'.
 178  #B #C #y #y'
 179  @(rewrite_l … (inr … y) (λz. proj_r … y (inr … y) = proj_r … y z)
 180    (ı(proj_r … y (inr … y))) (inr … y'))
 181 qed.
 182
 183 lemma injectivity_cons1: ∀C: st. ∀l,l': list C. ∀c,c': C. ⌈l, c⌉ = ⌈l', c'⌉ → l = l'.
 184  #C #l1 #l2 #c1 #c2
 185  @(rewrite_l … ⌈l1, c1⌉
 186    (list_rect_Type1 … (λ_. props) ⊥ (λl,c,h. l1 = l))
 187    (ı…) ⌈l2, c2⌉)
 188 qed.
 189
 190 lemma injectivity_cons2: ∀C: st. ∀l,l': list C. ∀c,c': C. ⌈l, c⌉ = ⌈l', c'⌉ → c = c'.
 191  #C #l1 #l2 #c1 #c2
 192  @(rewrite_l … ⌈l1, c1⌉
 193    (list_rect_Type1 … (λ_. props) ⊥ (λl,c,h. c1 = c))
 194    (ı…) ⌈l2, c2⌉)
 195 qed.
 196
 197 lemma plus_clash: ∀B,C: st. ∀b: B. ∀c: C. inl … b = inr … c → ⊥.
 198  #B #C #b #c #h
 199  @(rewrite_l … (inl … b) (plus_rect_Type1 … (λ_. props) (λ_. ⊤) (λ_. ⊥))
 200    (λx. x) … h)
 201 qed.
 202
 203 lemma list_clash: ∀C: st. ∀l: list C. ∀c: C. ϵ = ⌈l, c⌉ → ⊥.
 204  #C #l #c #h
 205  @(rewrite_l … ϵ (list_rect_Type1 … (λ_. props) ⊤ (λ_,_,_. ⊥))
 206    (λx. x) … h)
 207 qed.
 208
 209 definition nat: st ≝ list n1.
 210 definition zero: nat ≝ ϵ.
 211 definition succ: nat → nat ≝ λn. cons … n ⋆.
 212 definition nat_rect_Type0: ∀Q: nat → st. Q zero → (∀n. Q n → Q (succ n)) → ∀n. Q n.
 213  #Q #h0 #hi @list_rect_Type0 [ @h0 | #n @n1_rect_Type0 @(hi n) ]
 214 qed.
 215 definition nat_rect_Type1: ∀Q: nat → cl. Q zero → (∀n. Q n → Q (succ n)) → ∀n. Q n.
 216  #Q #h0 #hi @list_rect_Type1 [ @h0 | #n @n1_rect_Type1 @(hi n) ]
 217 qed.
 218 definition nat_rect_CProp0: ∀Q: nat → props. Q zero → (∀n. Q n → Q (succ n)) → ∀n. Q n.
 219  #Q #h0 #hi @list_rect_CProp0 [ @h0 | #n @n1_rect_CProp0 @(hi n) ]
 220 qed.
 221 definition nat_rect_CProp1: ∀Q: nat → prop. Q zero → (∀n. Q n → Q (succ n)) → ∀n. Q n.
 222  #Q #h0 #hi @list_rect_CProp1 [ @h0 | #n @n1_rect_CProp1 @(hi n) ]
 223 qed.
 224
 225 inductive De (I: st) : st ≝
 226  | c_unit: De I
 227  | c_ev: I → De I
 228  | c_times: De I → De I → De I
 229  | c_plus: De I → De I → De I.
 230
 231 definition int: ∀I: st. De I → (I → st) → st.
 232  #I @De_rect_Type1
 233  [ #_ @n1
 234  | #i #X @(X i)
 235  | #L #R #intL #intR #X @((intL X)×(intR X))
 236  | #L #R #intL #intR #X @((intL X)+(intR X))
 237  ]
 238 qed.
 239
 240 definition napply: nat → (st → st) → st → st.
 241  @nat_rect_Type1
 242  [ #F #X @X
 243  | #_ #F' #F #X @(F' F X)
 244  ]
 245 qed.
 246
 247 definition mu: ∀I: st. (I → De I) → I → st.
 248  #I #F #i @(Σn: nat. napply n (λX: st. int I (F i) (λ_. X)) n0)
 249 qed.
 250
 251 definition is_c_unit: ∀I: st. ∀F: De I. props.
 252  #I * [ @verum | #_ @falsum | 3,4: #_ #_ @falsum ]
 253 qed.
 254
 255 lemma De_clash_unit_ev: ∀I: st. ∀i: I. c_ev I i = c_unit I → falsum.
 256  #I #i #h
 257  @(rewrite_l (De I) (c_unit I) (is_c_unit I) (λx. x) (c_ev I i) h⁻¹)
 258 qed.
 259 lemma De_clash_unit_times: ∀I: st. ∀F,G: De I. c_times I F G = c_unit I → falsum.
 260  #I #F #G #h
 261  @(rewrite_l (De I) (c_unit I) (is_c_unit I) (λx. x) (c_times I F G) h⁻¹)
 262 qed.
 263 lemma De_clash_unit_plus: ∀I: st. ∀F,G: De I. c_plus I F G = c_unit I → falsum.
 264  #I #F #G #h
 265  @(rewrite_l (De I) (c_unit I) (is_c_unit I) (λx. x) (c_plus I F G) h⁻¹)
 266 qed.
 267
 268 inductive mu_ (I: st) (F: I → De I) : I → De I → st ≝
 269    fold_unit: ∀i: I. mu_ I F i (c_unit I)
 270  | fold_ev: ∀i,i': I. mu_ I F i' (F i') → mu_ I F i (c_ev I i')
 271  | fold_times: ∀i: I. ∀G1,G2: De I. mu_ I F i G1 → mu_ I F i G2 → mu_ I F i (c_times I G1 G2)
 272  | fold_plusL: ∀i: I. ∀G1,G2: De I. mu_ I F i G1 → mu_ I F i (c_plus I G1 G2)
 273  | fold_plusR: ∀i: I. ∀G1,G2: De I. mu_ I F i G2 → mu_ I F i (c_plus I G1 G2).
 274