matita/matita/contribs/mf/list.ma

   1 (* (C) 2014 Luca Bressan *)
   2
   3 include "model.ma".
   4 include "pisigma.ma".
   5
   6 definition proj1: ∀C: est. ∀r: list (Σx. Σy. x ≃ y). list C ≝
   7  λC. lift_to_list … (π1 …).
   8
   9 definition proj2: ∀C: est. ∀r: list (Σx. Σy. x ≃ y). list C ≝
  10  λC. lift_to_list … (λz: Σx. Σy. x ≃ y. π1 (π2 z)).
  11
  12 definition elist: est → est ≝
  13  λC. mk_est
  14  (list C)
  15  (λz,z'. ∃l: list (Σx. Σy. x ≃ y). (proj1 … l = z) ∧ (proj2 … l = z'))
  16  ?.
  17  % [ @list_rect_CProp0
  18      [ %{ϵ} % %
  19      | #l #c * #r * #h1 #h2
  20        %{⌈r, 〈c, 〈c, ıc〉〉⌉}
  21        % [ @(rewrite_l … ⌈proj1 … r, c⌉
  22              (λz. z = ⌈l, c⌉)
  23              (rewrite_l … (proj1 … r) (λz. ⌈proj1 … r, c⌉ = ⌈z, c⌉) (reflexivity …) … h1)
  24              … (reflexivity …))
  25          | @(rewrite_l … ⌈proj2 … r, c⌉
  26              (λz. z = ⌈l, c⌉)
  27              (rewrite_l … (proj2 … r) (λz. ⌈proj2 … r, c⌉ = ⌈z, c⌉) (reflexivity …) … h2)
  28              … (reflexivity …))
  29          ]
  30      ]
  31    | @list_rect_CProp0
  32      [ *
  33        [ //
  34        | #l2' #c * *
  35          [ * #_ #abs @(falsum_rect_CProp0 … (list_clash … abs))
  36          | #r #s * normalize #abs @(falsum_rect_CProp0 … (list_clash … abs⁻¹))
  37          ]
  38        ]
  39      | #l1' #c1 #h *
  40        [ * *
  41          [ * #abs @(falsum_rect_CProp0 … (list_clash … abs))
  42          | #r #s * #_ normalize #abs @(falsum_rect_CProp0 … (list_clash … abs⁻¹))
  43          ]
  44        | #l2' #c2 * *
  45          [ * #abs @(falsum_rect_CProp0 … (list_clash … abs))
  46          | #r #s * #h1 #h2
  47            cut (∃l. (proj1 … l = l2') ∧ (proj2 … l = l1'))
  48            [ @(h l2') %{r} % [ @(injectivity_cons1 … h1) | @(injectivity_cons1 … h2) ]
  49            | * #r' * #h1' #h2' %{⌈r', 〈c2, 〈c1, ?〉〉⌉}
  50              [ cut (π1 (π2 s) = c2)
  51                [ cut (⌈proj2 … r, π1 (π2 s)⌉ = ⌈l2', c2⌉)
  52                  [ @(rewrite_l … (proj2 … ⌈r, s⌉)
  53                      (λz. z = ⌈l2', c2⌉) h2 … (reflexivity …))
  54                  | @injectivity_cons2
  55                  ]
  56                | #k2 cut (π1 s = c1)
  57                  [ cut (⌈proj1 … r, sig1 … s⌉ = ⌈l1', c1⌉)
  58                    [ @(rewrite_l … (proj1 … ⌈r, s⌉)
  59                        (λz. z = ⌈l1', c1⌉) h1 … (reflexivity …))
  60                    | @injectivity_cons2
  61                    ]
  62                  | #k1 cut (π1 (π2 s) ≃ π1 s)
  63                    [ @((π2 (π2 s))⁻¹)
  64                    | #e cut (c2 ≃ π1 s)
  65                      [ @(rewrite_l … (π1 (π2 s)) (λz. z ≃ π1 s) e … k2)
  66                      | #e' @(rewrite_l … (π1 s) (λz. c2 ≃ z) e' … k1)
  67                      ]
  68                    ]
  69                  ]
  70                ]
  71              |
  72                % [ @(rewrite_l … (proj1 … r') (λz. ⌈proj1 … r', c2⌉ = ⌈z, c2⌉) (reflexivity …) … h1')
  73                  | @(rewrite_l … (proj2 … r') (λz. ⌈proj2 … r', c1⌉ = ⌈z, c1⌉) (reflexivity …) … h2')
  74                  ]
  75              ]
  76            ]
  77          ]
  78        ]
  79      ]
  80    | @list_rect_CProp0
  81      [ *
  82        [ *
  83          [ //
  84          | #l3' #c3 #_ //
  85          ]
  86        | #l2 #c2 *
  87          [ #_ #_ %{ϵ} % %
  88          | #l3' #c3 * *
  89            [ * #_ #abs @(falsum_rect_CProp0 … (list_clash … abs))
  90            | #r1' #s1 * #abs @(falsum_rect_CProp0 … (list_clash … abs⁻¹))
  91            ]
  92          ]
  93        ]
  94      | #l1' #c1 #h *
  95        [ *
  96          [ * | #l3' #c3 * ] *
  97          [ 1,3: * #abs @(falsum_rect_CProp0 … (list_clash … abs))
  98          | 2,4: #r' #s * #_ #abs @(falsum_rect_CProp0 … (list_clash … abs⁻¹))
  99          ]
 100        | #l2' #c2 *
 101          [ #_ * *
 102            [ * #abs @(falsum_rect_CProp0 … (list_clash … abs))
 103            | #r' #s * #_ #abs @(falsum_rect_CProp0 … (list_clash … abs⁻¹))
 104            ]
 105          | #l3' #c3 * *
 106            [ * #abs @(falsum_rect_CProp0 … (list_clash … abs))
 107            | #r1 #s1 * #h1 #h2 * *
 108              [ * #abs @(falsum_rect_CProp0 … (list_clash … abs))
 109              | #r2 #s2 * #h3 #h4
 110                cut (⌈proj1 … r1, π1 s1⌉ = ⌈l1', c1⌉)
 111                [ @(rewrite_l … (proj1 … ⌈r1, s1⌉)
 112                    (λz. z = ⌈l1', c1⌉) h1 … (reflexivity …))
 113                | -h1 #h1
 114                  cut (⌈proj2 … r1, π1 (π2 s1)⌉ = ⌈l2', c2⌉)
 115                  [ @(rewrite_l … (proj2 … ⌈r1, s1⌉)
 116                      (λz. z = ⌈l2', c2⌉) h2 … (reflexivity …))
 117                  | -h2 #h2
 118                    cut (⌈proj1 … r2, π1 s2⌉ = ⌈l2', c2⌉)
 119                    [ @(rewrite_l … (proj1 … ⌈r2, s2⌉)
 120                        (λz. z = ⌈l2', c2⌉) h3 … (reflexivity …))
 121                    | -h3 #h3
 122                      cut (⌈proj2 … r2, π1 (π2 s2)⌉ = ⌈l3', c3⌉)
 123                      [ @(rewrite_l … (proj2 … ⌈r2, s2⌉)
 124                          (λz. z = ⌈l3', c3⌉) h4 … (reflexivity …))
 125                      | -h4 #h4
 126                        cut (∃l. (proj1 … l = l1') ∧ (proj2 … l = l3'))
 127                        [ @(h l2' l3')
 128                          [ %{r1} @(mk_conj … (injectivity_cons1 … h1) (injectivity_cons1 … h2))
 129                          | %{r2} @(mk_conj … (injectivity_cons1 … h3) (injectivity_cons1 … h4))
 130                          ]
 131                        | * #r * #e1 #e2 %{⌈r, 〈c1, 〈c3, ?〉〉⌉}
 132                          [ @(tra …
 133                              (rewrite_l … (π1 s1) (λz. z ≃ c2)
 134                               (rewrite_l … (π1 (π2 s1)) (λz. π1 s1 ≃ z) (π2 (π2 s1))
 135                                 … (injectivity_cons2 … h2))
 136                               … (injectivity_cons2 … h1))
 137                              (rewrite_l … (π1 (π2 s2)) (λz. c2 ≃ z)
 138                                (rewrite_l … (π1 s2) (λz. z ≃ π1 (π2 s2)) (π2 (π2 s2))
 139                                 … (injectivity_cons2 … h3))
 140                               … (injectivity_cons2 … h4)))
 141                          | %
 142                            [ @(rewrite_l … (proj1 … r) (λz. ⌈proj1 … r, c1⌉ = ⌈z, c1⌉) (reflexivity …) … e1)
 143                            | @(rewrite_l … (proj2 … r) (λz. ⌈proj2 … r, c3⌉ = ⌈z, c3⌉) (reflexivity …) … e2)
 144                            ]
 145                          ]
 146                        ]
 147                      ]
 148                    ]
 149                  ]
 150                ]
 151              ]
 152            ]
 153          ]
 154        ]
 155      ]
 156    ]
 157 qed.
 158
 159 definition eepsilon: ∀C: est. elist C ≝ epsilon.
 160
 161 definition econs: ∀C: est. eto (elist C) (eto C (elist C)) ≝
 162  λC. 〈λl. 〈cons … l, ?〉, ?〉.
 163  [ #c1 #c2 #d
 164    cut (subst C (constant_edst C (elist C)) c1 c2 d ⌈l, c1⌉ = ⌈l, c1⌉)
 165    [ %
 166    | #h @(rewrite_l (list (sup C)) ⌈l, c1⌉ (λz. eq (elist C) z ⌈l, c2⌉) ?
 167           (subst C (constant_edst C (elist C)) c1 c2 d ⌈l, c1⌉) h)
 168      @(list_rect_CProp0 … l)
 169      [ %{⌈ϵ, 〈c1, 〈c2, d〉〉⌉} % %
 170      | #l' #c * *
 171        [ * #abs @(falsum_rect_CProp0 … (list_clash … abs))
 172        | #r' #s * #h1 #h2 %{⌈⌈r', 〈c, 〈c, ıc〉〉⌉, 〈c1, 〈c2, d〉〉⌉} %
 173          [ change with (⌈⌈proj1 … , ?⌉, ?⌉) in ⊢ (??%?);
 174            cut (proj1 … r' = l')
 175            [ @(injectivity_cons1 … h1)
 176            | #h @(rewrite_l ????? h) @reflexivity
 177            ]
 178          | @(rewrite_l … ⌈⌈proj2 … r', c⌉, c2⌉ (λz. z = ⌈⌈l', c⌉, c2⌉) ?
 179              (proj2 … ⌈⌈r', 〈c, 〈c, ıc〉〉⌉, 〈c1, 〈c2, d〉〉⌉) (reflexivity …))
 180            cut (proj2 … r' = l')
 181            [ @(injectivity_cons1 …
 182                (rewrite_l … (proj2 … ⌈r', s⌉) (λz. ⌈proj2 … r', sig1 … (sig2 … s)⌉ = z)
 183                 (reflexivity …) ⌈l', c2⌉ h2))
 184            | #h @(rewrite_l … l' (λz. ⌈⌈z, c⌉, c2⌉ = ⌈⌈l', c⌉, c2⌉) (reflexivity …)
 185                   (proj2 C r') (symmetry … h))
 186            ]
 187          ]
 188        ]
 189      ]
 190    ]
 191  | #l1 #l2 * #r * #h1 #h2 #c %{⌈r, 〈c, 〈c, ıc〉〉⌉} %
 192    [ @(rewrite_l … l1 (λz. ⌈z, c⌉ = ⌈l1, c⌉) (reflexivity …) (proj1 … r) (symmetry … h1))
 193    | @(rewrite_l … l2 (λz. ⌈z, c⌉ = ⌈l2, c⌉) (reflexivity …) (proj2 … r) (symmetry … h2))
 194    ]
 195  ]
 196 qed.
 197