helm/software/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 include "Unified-Sub/Lift/defs.ma".
  16
  17 (* Inversion properties *****************************************************)
  18
  19 theorem lift_inv_sort_1: \forall l, i, h, x.
  20                          Lift l i (sort h) x \to
  21                          x = sort h.
  22  intros. inversion H; clear H; intros; destruct. autobatch.
  23 qed.
  24
  25 theorem lift_inv_lref_1: \forall l, i, j1, x.
  26                          Lift l i (lref j1) x \to
  27                          (i > j1 \land x = lref j1) \lor
  28                          (i <= j1 \land
  29                           \exists j2. (l + j1 == j2) \land x = lref j2
  30                          ).
  31  intros. inversion H; clear H; intros; destruct; autobatch depth = 5 size = 7.
  32 qed.
  33
  34 theorem lift_inv_bind_1: \forall l, i, r, u1, t1, x.
  35                          Lift l i (intb r u1 t1) x \to
  36                          \exists u2, t2.
  37                          Lift l i u1 u2 \land
  38                          Lift l (succ i) t1 t2 \land
  39                          x = intb r u2 t2.
  40  intros. inversion H; clear H; intros; destruct; autobatch depth = 5 size = 7.
  41 qed.
  42
  43 theorem lift_inv_flat_1: \forall l, i, r, u1, t1, x.
  44                          Lift l i (intf r u1 t1) x \to
  45                          \exists u2, t2.
  46                          Lift l i u1 u2 \land
  47                          Lift l i t1 t2 \land
  48                          x = intf r u2 t2.
  49  intros. inversion H; clear H; intros; destruct. autobatch depth = 5 size = 7.
  50 qed.
  51
  52 theorem lift_inv_sort_2: \forall l, i, x, h.
  53                          Lift l i x (sort h) \to
  54                          x = sort h.
  55  intros. inversion H; clear H; intros; destruct. autobatch.
  56 qed.
  57
  58 theorem lift_inv_lref_2: \forall l, i, x, j2.
  59                          Lift l i x (lref j2) \to
  60                          (i > j2 \land x = lref j2) \lor
  61                          (i <= j2 \land
  62                           \exists j1. (l + j1 == j2) \land x = lref j1
  63                          ).
  64  intros. inversion H; clear H; intros; destruct; autobatch depth = 5 size = 10.
  65 qed.
  66
  67 theorem lift_inv_bind_2: \forall l, i, r, x, u2, t2.
  68                          Lift l i x (intb r u2 t2) \to
  69                          \exists u1, t1.
  70                          Lift l i u1 u2 \land
  71                          Lift l (succ i) t1 t2 \land
  72                          x = intb r u1 t1.
  73  intros. inversion H; clear H; intros; destruct. autobatch depth = 5 size = 7.
  74 qed.
  75
  76 theorem lift_inv_flat_2: \forall l, i, r, x, u2, t2.
  77                          Lift l i x (intf r u2 t2) \to
  78                          \exists u1, t1.
  79                          Lift l i u1 u2 \land
  80                          Lift l i t1 t2 \land
  81                          x = intf r u1 t1.
  82  intros. inversion H; clear H; intros; destruct. autobatch depth = 5 size = 7.
  83 qed.
  84
  85 (* Corollaries of inversion properties ***************************************)
  86
  87 theorem lift_inv_lref_1_gt: \forall l, i, j1, x.
  88                             Lift l i (lref j1) x \to
  89                             i > j1 \to x = lref j1.
  90  intros.
  91  lapply linear lift_inv_lref_1 to H. decompose; destruct;
  92  [ autobatch
  93  | lapply linear nle_false to H2, H1. decompose
  94  ].
  95 qed.
  96
  97 theorem lift_inv_lref_1_le: \forall l, i, j1, x.
  98                             Lift l i (lref j1) x \to i <= j1 \to
  99                             \exists j2. (l + j1 == j2) \land x = lref j2.
 100  intros.
 101  lapply linear lift_inv_lref_1 to H. decompose; destruct;
 102  [ lapply linear nle_false to H1, H2. decompose
 103  | autobatch
 104  ].
 105 qed.
 106
 107 theorem lift_inv_lref_1_le_nplus: \forall l, i, j1, x.
 108                                  Lift l i (lref j1) x \to
 109                                  i <= j1 \to \forall j2. (l + j1 == j2) \to
 110                                  x = lref j2.
 111  intros.
 112  lapply linear lift_inv_lref_1 to H. decompose; destruct;
 113  [ lapply linear nle_false to H1, H3. decompose
 114  | lapply linear nplus_mono to H2, H4. destruct. autobatch
 115  ].
 116 qed.
 117
 118 theorem lift_inv_lref_2_gt: \forall l, i, x, j2.
 119                             Lift l i x (lref j2) \to
 120                             i > j2 \to x = lref j2.
 121  intros.
 122  lapply linear lift_inv_lref_2 to H. decompose; destruct;
 123  [ autobatch
 124  | lapply linear nle_false to H2, H1. decompose
 125  ].
 126  qed.
 127
 128 theorem lift_inv_lref_2_le: \forall l, i, x, j2.
 129                             Lift l i x (lref j2) \to i <= j2 \to
 130                             \exists j1. (l + j1 == j2) \land x = lref j1.
 131  intros.
 132  lapply linear lift_inv_lref_2 to H. decompose; destruct;
 133  [ lapply linear nle_false to H1, H2. decompose
 134  | autobatch
 135  ].
 136 qed.
 137
 138 theorem lift_inv_lref_2_le_nplus: \forall l, i, x, j2.
 139                                   Lift l i x (lref j2) \to
 140                                   i <= j2 \to \forall j1. (l + j1 == j2) \to
 141                                   x = lref j1.
 142  intros.
 143  lapply linear lift_inv_lref_2 to H. decompose; destruct;
 144  [ lapply linear nle_false to H1, H3. decompose
 145  | lapply linear nplus_inj_2 to H2, H4. destruct. autobatch
 146  ].
 147 qed.