matita/matita/contribs/mf/model.ma

   1 (* (C) 2014 Luca Bressan *)\r
   2 \r
   3 include "mTT.ma".\r
   4 \r
   5 record is_Equiv (Sup: cl) (Eq: Sup → Sup → prop) : prop ≝\r
   6  { Rfl_: ∀x. Eq x x\r
   7  ; Sym_: ∀x,x'. Eq x x' → Eq x' x\r
   8  ; Tra_: ∀x,x',x''. Eq x x' → Eq x' x'' → Eq x x''\r
   9  }.\r
  10 \r
  11 record ecl: Type[2] ≝ \r
  12  { Sup:> cl\r
  13  ; Eq: Sup → Sup → prop\r
  14  ; is_ecl: is_Equiv Sup Eq\r
  15  }.\r
  16 interpretation "Equality in Extensional Collections" 'eq a b = (Eq ? a b).\r
  17 \r
  18 definition Rfl: ∀B: ecl. ∀x: B. x ≃ x ≝\r
  19  λB. Rfl_ … (is_ecl B).\r
  20 interpretation "Reflexivity in Extensional Collections" 'rfl x = (Rfl ? x).\r
  21 \r
  22 definition Sym: ∀B: ecl. ∀x,x': B. x ≃ x' → x' ≃ x ≝\r
  23  λB. Sym_ … (is_ecl B).\r
  24 interpretation "Symmetry in Extensional Collections" 'sym d = (Sym ??? d).\r
  25 \r
  26 definition Tra: ∀B: ecl. ∀x,x',x'': B. x ≃ x' → x' ≃ x'' → x ≃ x'' ≝\r
  27  λB. Tra_ … (is_ecl B).\r
  28 interpretation "Transitivity in Extensional Collections" 'tra d d' = (Tra ???? d d').\r
  29 \r
  30 record is_Subst (A: ecl)\r
  31                 (dSup: A → ecl)\r
  32                 (Subst: ∀x1,x2: A. x1 ≃ x2 → dSup x1 → dSup x2) : prop ≝\r
  33  { Pres_eq_:   ∀x1,x2: A. ∀d: x1 ≃ x2. ∀y,y': dSup x1.\r
  34                 y ≃ y' → Subst … d y ≃ Subst … d y'\r
  35  ; Not_dep_:   ∀x1,x2: A. ∀d,d': x1 ≃ x2. ∀y: dSup x1.\r
  36                 Subst … d y ≃ Subst … d' y\r
  37  ; Pres_id_:   ∀x: A. ∀y: dSup x.\r
  38                 Subst … (ı x) y ≃ y\r
  39  ; Clos_comp_: ∀x1,x2,x3: A. ∀y: dSup x1. ∀d: x1 ≃ x2. ∀d': x2 ≃ x3.\r
  40                 Subst … d' (Subst … d y) ≃ Subst … (d•d') y\r
  41  }.\r
  42 \r
  43 record edcl (A: ecl) : Type[2] ≝ \r
  44  { dSup:1> Sup A → ecl\r
  45  ; Subst: ∀x1,x2: Sup A. x1 ≃ x2 → Sup (dSup x1) → Sup (dSup x2)\r
  46  ; is_edcl: is_Subst A dSup Subst\r
  47  }.\r
  48 interpretation "Substitution morphisms for Extensional Collections"\r
  49  'subst d y = (Subst ???? d y).\r
  50 \r
  51 definition Pres_eq: ∀B: ecl. ∀C: edcl B. ∀x1,x2: B. ∀d: x1 ≃ x2. ∀y,y': C x1.\r
  52                      y ≃ y' → y∘d ≃ y'∘d ≝\r
  53  λB,C. Pres_eq_ … (is_edcl … C).\r
  54 definition Not_dep: ∀B: ecl. ∀C: edcl B. ∀x1,x2: B. ∀d,d': x1 ≃ x2. ∀y: C x1.\r
  55                      y∘d ≃ y∘d' ≝\r
  56  λB,C. Not_dep_ … (is_edcl … C).\r
  57 definition Pres_id: ∀B: ecl. ∀C: edcl B. ∀x: B. ∀y: C x.\r
  58                      y∘(ıx) ≃ y ≝\r
  59  λB,C. Pres_id_ … (is_edcl … C).\r
  60 definition Clos_comp: ∀B: ecl. ∀C: edcl B. ∀x1,x2,x3: B. ∀y: C x1. ∀d: x1 ≃ x2. ∀d': x2 ≃ x3.\r
  61                        y∘d∘d' ≃ y∘d•d' ≝\r
  62  λB,C. Clos_comp_ … (is_edcl … C).\r
  63 \r
  64 definition constant_edcl: ∀A: ecl. ecl → edcl A ≝\r
  65  λA,Y. mk_edcl … (λ_. Y) (λx1,x2,d,y. y) ?.\r
  66  % [ #x1 #x2 #d #y #y' #h @h\r
  67    | #x1 #x2 #_ #_ #y @(ıy)\r
  68    | #_ #y @(ıy)\r
  69    | #x1 #x2 #x3 #y #_ #_ @(ıy)\r
  70    ]\r
  71 qed.\r
  72 \r
  73 lemma inverse_Subst: ∀B: ecl. ∀C: edcl B. ∀x1,x2: B. ∀d: x1 ≃ x2. ∀y: C x2.\r
  74  y∘d⁻¹∘d ≃ y.\r
  75  #B #C #x1 #x2 #d #y\r
  76  @(Tra … (y∘d⁻¹∘d) (y∘d⁻¹•d) y)\r
  77  [ @Clos_comp\r
  78  | @(Tra … (y∘d⁻¹•d) (y∘ıx2) y)\r
  79    [ @Not_dep | @Pres_id ]\r
  80  ]\r
  81 qed.\r
  82 \r
  83 record is_equiv (sup: st) (eq: sup → sup → props) : props ≝\r
  84  { rfl_: ∀x. eq x x\r
  85  ; sym_: ∀x,x'. eq x x' → eq x' x\r
  86  ; tra_: ∀x,x',x''. eq x x' → eq x' x'' → eq x x''\r
  87  }.\r
  88 \r
  89 record est: Type[1] ≝ \r
  90  { sup:> st\r
  91  ; eq: sup → sup → props\r
  92  ; is_est: is_equiv sup eq\r
  93  }.\r
  94 interpretation "Equality in Extensional Sets" 'eq a b = (eq ? a b).\r
  95 \r
  96 definition rfl: ∀B: est. ∀x: B. x ≃ x ≝\r
  97  λB. rfl_ … (is_est B).\r
  98 interpretation "Reflexivity in Extensional Sets" 'rfl x = (rfl ? x).\r
  99 \r
 100 definition sym: ∀B: est. ∀x,x': B. x ≃ x' → x' ≃ x ≝\r
 101  λB. sym_ … (is_est B).\r
 102 interpretation "Symmetry in Extensional Sets" 'sym d = (sym ??? d).\r
 103 \r
 104 definition tra: ∀B: est. ∀x,x',x'': B. x ≃ x' → x' ≃ x'' → x ≃ x'' ≝\r
 105  λB. tra_ … (is_est B).\r
 106 interpretation "Transitivity in Extensional Sets" 'tra d d' = (tra ???? d d').\r
 107 \r
 108 definition est_into_ecl: est → ecl ≝ \r
 109  λB. mk_ecl (sup B) (eq B) ?.\r
 110  % [ @rfl | @sym | @tra ]\r
 111 qed.\r
 112 \r
 113 record is_subst (A: est)\r
 114                 (dsup: A → est)\r
 115                 (subst: ∀x1,x2: A. x1 ≃ x2 → dsup x1 → dsup x2) : props ≝\r
 116  { pres_eq_:   ∀x1,x2: A. ∀d: x1 ≃ x2. ∀y,y': dsup x1.\r
 117                 y ≃ y' → subst … d y ≃ subst … d y'\r
 118  ; not_dep_:   ∀x1,x2: A. ∀d1,d2: x1 ≃ x2. ∀y: dsup x1.\r
 119                 subst … d1 y ≃ subst … d2 y\r
 120  ; pres_id_:   ∀x: sup A. ∀y: dsup x.\r
 121                 subst … (ıx) y ≃ y\r
 122  ; clos_comp_: ∀x1,x2,x3: A. ∀y: dsup x1. ∀d1: x1 ≃ x2. ∀d2: x2 ≃ x3.\r
 123                 subst … d2 (subst … d1 y) ≃ subst … (d1•d2) y\r
 124  }.\r
 125 \r
 126 record edst (A: est) : Type[1] ≝ \r
 127  { dsup:1> sup A → est\r
 128  ; subst: ∀x1,x2: sup A. x1 ≃ x2 → sup (dsup x1) → sup (dsup x2)\r
 129  ; is_edst: is_subst A dsup subst\r
 130  }.\r
 131 interpretation "Substitution morphisms for Extensional Sets"\r
 132  'subst p a = (subst ???? p a).\r
 133 \r
 134 definition pres_eq: ∀B: est. ∀C: edst B. ∀x1,x2: B. ∀d: x1 ≃ x2. ∀y,y': C x1.\r
 135                      y ≃ y' → y∘d ≃ y'∘d ≝\r
 136  λB,C. pres_eq_ … (is_edst … C).\r
 137 definition not_dep: ∀B: est. ∀C: edst B. ∀x1,x2: B. ∀d,d': x1 ≃ x2. ∀y: C x1.\r
 138                      y∘d ≃ y∘d' ≝\r
 139  λB,C. not_dep_ … (is_edst … C).\r
 140 definition pres_id: ∀B: est. ∀C: edst B. ∀x: B. ∀y: C x.\r
 141                      y∘(ıx) ≃ y ≝\r
 142  λB,C. pres_id_ … (is_edst … C).\r
 143 definition clos_comp: ∀B: est. ∀C: edst B. ∀x1,x2,x3: B. ∀y: C x1. ∀d: x1 ≃ x2. ∀d': x2 ≃ x3.\r
 144                        y∘d∘d' ≃ y∘(d•d') ≝\r
 145  λB,C. clos_comp_ … (is_edst … C).\r
 146 \r
 147 definition constant_edst: ∀A: est. est → edst A ≝\r
 148  λA,Y. mk_edst … (λ_. Y) (λx1,x2,d,y. y) ?.\r
 149  % [ #x1 #x2 #d #y #y' #h @h\r
 150    | #x1 #x2 #_ #_ #y @(ıy)\r
 151    | #_ #y @(ıy)\r
 152    | #x1 #x2 #x3 #y #_ #_ @(ıy)\r
 153    ]\r
 154 qed.\r
 155 \r
 156 lemma inverse_subst: ∀B: est. ∀C: edst B. ∀x1,x2: B. ∀d: x1 ≃ x2. ∀y: C x2.\r
 157  y∘d⁻¹∘d ≃ y.\r
 158  #B #C #x1 #x2 #d #y\r
 159  @tra [ @(y∘d⁻¹•d)\r
 160       | @clos_comp\r
 161       | @tra [ @(y∘ıx2) | @not_dep | @pres_id ]\r
 162       ]\r
 163 qed.\r
 164 \r
 165 lemma inverse_subst2: ∀B: est. ∀C: edst B. ∀x1,x2: B. ∀d: x1 ≃ x2. ∀y: C x1.\r
 166  y∘d∘d⁻¹ ≃ y.\r
 167  #B #C #x1 #x2 #d #y @tra [ @(y∘d•d⁻¹)\r
 168                           | @clos_comp\r
 169                           | @tra [ @(y∘(ıx1)) | @not_dep | @pres_id ]\r
 170                           ]\r
 171 qed.\r
 172 \r
 173 lemma eq_reflexivity: ∀B: est. ∀b1,b2: B. b1 = b2 → b1 ≃ b2.\r
 174  #B #b1 #b2 #h @(rewrite_l … b1 (λz. b1 ≃ z) (ıb1) … h)\r
 175 qed.\r
 176 \r
 177 definition eprop: Type[2] ≝ prop.\r
 178 \r
 179 definition eprop_into_ecl: eprop → ecl ≝\r
 180  λP. mk_ecl P (λ_,_. ⊤) ?.\r
 181  % //\r
 182 qed.\r
 183 \r
 184 definition eprops: Type[1] ≝ props.\r
 185 \r
 186 definition eprops_into_est: eprops → est ≝\r
 187  λP. mk_est P (λ_,_. ⊤) ?.\r
 188  % //\r
 189 qed.\r
 190 \r