matita/matita/contribs/mf/plus.ma

   1 (* (C) 2014 Luca Bressan *)
   2
   3 include "model.ma".
   4 include "pisigma.ma".
   5
   6 definition eplus: est → est → est ≝
   7  λB,C. mk_est
   8  (B+C)
   9  (λz,z'. (∃b: B. ∃b': B. (z = inl … b) ∧ ((z' = inl … b') ∧ (b ≃ b')))
  10          ∨ (∃c: C. ∃c': C. (z = inr … c) ∧ ((z' = inr … c') ∧ (c ≃ c'))))
  11  ?.
  12  % [ * #x [ %1 | %2 ] %{x} %{x} %
  13      [ 1,3: @(reflexivity …)
  14      | 2: @(mk_conj … (reflexivity …) (ıx))
  15      | 4: @(mk_conj … (reflexivity …) (ıx))
  16      ]
  17    | #z1 #z2 * * #x1 * #x2 * #h1 * #h2 #e [ %1 | %2 ] %{x2} %{x1} %
  18      [ 1,3: @h2
  19      | 2,4: % [ 1,3: @h1
  20               | 2,4: @(e⁻¹)
  21               ]
  22      ]
  23    | #z1 #z2 #z3 * * #x1 * #x12 * #h1 * #h12 #e12 * * #x23 * #x3 * #h23 * #h3 #e23
  24      [ %1 %{x1} %{x3} %
  25        [ @h1
  26        | % [ @h3
  27            | @(e12•
  28                (rewrite_l … x23 (λz. z ≃ x3) e23 …
  29                 (injectivity_inl … (h12⁻¹•h23)⁻¹)))
  30            ]
  31        ]
  32      | @(falsum_rect_CProp0 … (plus_clash … (h12⁻¹•h23)))
  33      | @(falsum_rect_CProp0 … (plus_clash … ((h12⁻¹•h23)⁻¹)))
  34      | %2 %{x1} %{x3} %
  35        [ @h1
  36        | % [ @h3
  37            | @(e12•
  38                (rewrite_l … x23 (λz. z ≃ x3) e23 …
  39                 (injectivity_inr … (h12⁻¹•h23)⁻¹)))
  40            ]
  41        ]
  42      ]
  43    ]
  44 qed.
  45
  46 definition einl: ∀B,C: est. eto B (eplus B C) ≝
  47  λB,C. 〈inl …, ?〉.
  48  #x #y #h %1 %{x} %{y} % % [ % | @h ]
  49 qed.
  50
  51 definition einr: ∀B,C: est. eto C (eplus B C) ≝
  52  λB,C. 〈inr …, ?〉.
  53  #x #y #h %2 %{x} %{y} % % [ % | @h ]
  54 qed.
  55
  56 lemma injectivity_einl: ∀B,C: est. ∀b,b': B. (einl B C)˙b ≃ (einl B C)˙b' → b ≃ b'.
  57  #B #C #b #b' * * #z * #z' * #h1 * #h2 #h3
  58  [ @(rewrite_l … z (λw. w ≃ b')
  59      (rewrite_l … z' (λw. z ≃ w) h3 … (symmetry … (injectivity_inl … h2))) …
  60      (symmetry … (injectivity_inl … h1)))
  61  | @(falsum_rect_CProp0 … (plus_clash … h1))
  62  ]
  63 qed.
  64
  65 lemma injectivity_einr: ∀B,C: est. ∀c,c': C. (einr B C)˙c ≃ (einr B C)˙c' → c ≃ c'.
  66  #B #C #c #c' * * #z * #z' * #h1 * #h2 #h3
  67  [ @(falsum_rect_CProp0 … (plus_clash … (symmetry … h1)))
  68  | @(rewrite_l … z (λw. w ≃ c')
  69      (rewrite_l … z' (λw. z ≃ w) h3 … (symmetry … (injectivity_inr … h2))) …
  70      (symmetry … (injectivity_inr … h1)))
  71  ]
  72 qed.
  73
  74 definition edplus: ∀I: est. edst I → edst I → edst I.
  75  #I #B #C %
  76  [ @(λi. eplus (B i) (C i))
  77  | #i1 #i2 #e * #x [ @(inl … (x∘e)) | @(inr … (x∘e)) ]
  78  | % [ #i1 #i2 #e * #x1 * #x2 #h
  79        cases h * #z1 * #z2 * #h1 * #h2 #d
  80          [ 1: %1 %{(x1∘e)} %{(x2∘e)} % [ % | % [ % | @(pres_eq … (injectivity_einl … h)) ]]
  81          | 2,4: @(falsum_rect_CProp0 … (plus_clash … h1))
  82          | 3: @(falsum_rect_CProp0 … (plus_clash … h2⁻¹))
  83          | 5,7: @(falsum_rect_CProp0 … (plus_clash … h1⁻¹))
  84          | 6: @(falsum_rect_CProp0 … (plus_clash … h2))
  85          | 8: %2 %{(x1∘e)} %{(x2∘e)} % [ % | % [ % | @(pres_eq … (injectivity_einr … h)) ]]
  86          ]
  87      | #i1 #i2 #e1 #e2 * #x [ %1 | %2 ] %{(x∘e1)} %{(x∘e2)} %
  88        [ 1,3: % | 2,4: % [ 1,3: % | 2,4: @not_dep ]]
  89      | #i * #x [ %1 | %2 ] %{(x∘ıi)} %{x} %
  90        [ 1,3: % | 2,4: % [ 1,3: % | 2,4: @pres_id ]]
  91      | #i1 #i2 #i3 * #x #d1 #d2 [ %1 | %2 ] %{(x∘d1∘d2)} %{(x∘d1•d2)} %
  92        [ 1,3: % | 2,4: % [ 1,3: % | 2,4: @clos_comp ]]
  93      ]
  94  ]
  95 qed.
  96