]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/mf/plus.ma
update in basic_2
[helm.git] / 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