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