matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/inv".
  16
  17 include "Lift/defs.ma".
  18
  19 (* Inversion properties *****************************************************)
  20
  21 theorem lift_inv_sort_1: \forall l, i, h, x.
  22                          Lift l i (sort h) x \to
  23                          x = sort h.
  24  intros. inversion H; clear H; intros;
  25  [ auto
  26  | destruct H2
  27  | destruct H3
  28  | destruct H5
  29  | destruct H5
  30  ].
  31 qed.
  32
  33 theorem lift_inv_lref_1: \forall l, i, j1, x.
  34                          Lift l i (lref j1) x \to
  35                          (i > j1 \land x = lref j1) \lor
  36                          (i <= j1 \land
  37                           \exists j2. (l + j1 == j2) \land x = lref j2
  38                          ).
  39  intros. inversion H; clear H; intros;
  40  [ destruct H1
  41  | destruct H2. clear H2. subst. auto
  42  | destruct H3. clear H3. subst. auto depth = 5
  43  | destruct H5
  44  | destruct H5
  45  ].
  46 qed.
  47
  48 theorem lift_inv_bind_1: \forall l, i, r, u1, t1, x.
  49                          Lift l i (intb r u1 t1) x \to
  50                          \exists u2, t2.
  51                          Lift l i u1 u2 \land
  52                          Lift l (succ i) t1 t2 \land
  53                          x = intb r u2 t2.
  54  intros. inversion H; clear H; intros;
  55  [ destruct H1
  56  | destruct H2
  57  | destruct H3
  58  | destruct H5. clear H5 H1 H3. subst. auto depth = 5
  59  | destruct H5
  60  ].
  61 qed.
  62
  63 theorem lift_inv_flat_1: \forall l, i, r, u1, t1, x.
  64                          Lift l i (intf r u1 t1) x \to
  65                          \exists u2, t2.
  66                          Lift l i u1 u2 \land
  67                          Lift l i t1 t2 \land
  68                          x = intf r u2 t2.
  69  intros. inversion H; clear H; intros;
  70  [ destruct H1
  71  | destruct H2
  72  | destruct H3
  73  | destruct H5
  74  | destruct H5. clear H5 H1 H3. subst. auto depth = 5
  75  ].
  76 qed.
  77
  78 theorem lift_inv_sort_2: \forall l, i, x, h.
  79                          Lift l i x (sort h) \to
  80                          x = sort h.
  81  intros. inversion H; clear H; intros;
  82  [ auto
  83  | destruct H3
  84  | destruct H4
  85  | destruct H6
  86  | destruct H6
  87  ].
  88 qed.
  89
  90 theorem lift_inv_lref_2: \forall l, i, x, j2.
  91                          Lift l i x (lref j2) \to
  92                          (i > j2 \land x = lref j2) \lor
  93                          (i <= j2 \land
  94                           \exists j1. (l + j1 == j2) \land x = lref j1
  95                          ).
  96  intros. inversion H; clear H; intros;
  97  [ destruct H2
  98  | destruct H3. clear H3. subst. auto
  99  | destruct H4. clear H4. subst. auto depth = 5
 100  | destruct H6
 101  | destruct H6
 102  ].
 103 qed.
 104
 105 theorem lift_inv_bind_2: \forall l, i, r, x, u2, t2.
 106                          Lift l i x (intb r u2 t2) \to
 107                          \exists u1, t1.
 108                          Lift l i u1 u2 \land
 109                          Lift l (succ i) t1 t2 \land
 110                          x = intb r u1 t1.
 111  intros. inversion H; clear H; intros;
 112  [ destruct H2
 113  | destruct H3
 114  | destruct H4
 115  | destruct H6. clear H5 H1 H3. subst. auto depth = 5
 116  | destruct H6
 117  ].
 118 qed.
 119
 120 theorem lift_inv_flat_2: \forall l, i, r, x, u2, t2.
 121                          Lift l i x (intf r u2 t2) \to
 122                          \exists u1, t1.
 123                          Lift l i u1 u2 \land
 124                          Lift l i t1 t2 \land
 125                          x = intf r u1 t1.
 126  intros. inversion H; clear H; intros;
 127  [ destruct H2
 128  | destruct H3
 129  | destruct H4
 130  | destruct H6
 131  | destruct H6. clear H6 H1 H3. subst. auto depth = 5
 132  ].
 133 qed.
 134
 135 (* Corollaries of inversion properties ***************************************)
 136
 137 theorem lift_inv_lref_1_gt: \forall l, i, j1, x.
 138                             Lift l i (lref j1) x \to
 139                             i > j1 \to x = lref j1.
 140  intros.
 141  lapply linear lift_inv_lref_1 to H. decompose; subst;
 142  [ auto
 143  | lapply linear nle_false to H2, H1. decompose
 144  ].
 145 qed.
 146
 147 theorem lift_inv_lref_1_le: \forall l, i, j1, x.
 148                             Lift l i (lref j1) x \to i <= j1 \to
 149                             \exists j2. (l + j1 == j2) \land x = lref j2.
 150  intros.
 151  lapply linear lift_inv_lref_1 to H. decompose; subst;
 152  [ lapply linear nle_false to H1, H2. decompose
 153  | auto
 154  ].
 155 qed.
 156
 157 theorem lift_inv_lref_1_le_nplus: \forall l, i, j1, x.
 158                                  Lift l i (lref j1) x \to
 159                                  i <= j1 \to \forall j2. (l + j1 == j2) \to
 160                                  x = lref j2.
 161  intros.
 162  lapply linear lift_inv_lref_1 to H. decompose; subst;
 163  [ lapply linear nle_false to H1, H3. decompose
 164  | lapply linear nplus_mono to H2, H4. subst. auto
 165  ].
 166 qed.
 167
 168 theorem lift_inv_lref_2_gt: \forall l, i, x, j2.
 169                             Lift l i x (lref j2) \to
 170                             i > j2 \to x = lref j2.
 171  intros.
 172  lapply linear lift_inv_lref_2 to H. decompose; subst;
 173  [ auto
 174  | lapply linear nle_false to H2, H1. decompose
 175  ].
 176  qed.
 177
 178 theorem lift_inv_lref_2_le: \forall l, i, x, j2.
 179                             Lift l i x (lref j2) \to i <= j2 \to
 180                             \exists j1. (l + j1 == j2) \land x = lref j1.
 181  intros.
 182  lapply linear lift_inv_lref_2 to H. decompose; subst;
 183  [ lapply linear nle_false to H1, H2. decompose
 184  | auto
 185  ].
 186 qed.
 187
 188 theorem lift_inv_lref_2_le_nplus: \forall l, i, x, j2.
 189                                   Lift l i x (lref j2) \to
 190                                   i <= j2 \to \forall j1. (l + j1 == j2) \to
 191                                   x = lref j1.
 192  intros.
 193  lapply linear lift_inv_lref_2 to H. decompose; subst;
 194  [ lapply linear nle_false to H1, H3. decompose
 195  | lapply linear nplus_inj_2 to H2, H4. subst. auto
 196  ].
 197 qed.