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 theorem lift_inv_sort_1: \forall l, i, h, x.
  20                          Lift l i (leaf (sort h)) x \to
  21                          x = leaf (sort h).
  22  intros. inversion H; clear H; intros;
  23  [ auto
  24  | destruct H2
  25  | destruct H3
  26  | destruct H5
  27  | destruct H5
  28  ].
  29 qed.
  30
  31 theorem lift_inv_lref_1: \forall l, i, j1, x.
  32                          Lift l i (leaf (lref j1)) x \to
  33                          (i > j1 \land x = leaf (lref j1)) \lor
  34                          (i <= j1 \land
  35                           \exists j2. (l + j1 == j2) \land x = leaf (lref j2)
  36                          ).
  37  intros. inversion H; clear H; intros;
  38  [ destruct H1
  39  | destruct H2. clear H2. subst. auto
  40  | destruct H3. clear H3. subst. auto depth = 5
  41  | destruct H5
  42  | destruct H5
  43  ].
  44 qed.
  45
  46 theorem lift_inv_bind_1: \forall l, i, r, u1, t1, x.
  47                          Lift l i (intb r u1 t1) x \to
  48                          \exists u2, t2.
  49                          Lift l i u1 u2 \land
  50                          Lift l (succ i) t1 t2 \land
  51                          x = intb r u2 t2.
  52  intros. inversion H; clear H; intros;
  53  [ destruct H1
  54  | destruct H2
  55  | destruct H3
  56  | destruct H5. clear H5 H1 H3. subst. auto depth = 5
  57  | destruct H5
  58  ].
  59 qed.
  60
  61 theorem lift_inv_flat_1: \forall l, i, r, u1, t1, x.
  62                          Lift l i (intf r u1 t1) x \to
  63                          \exists u2, t2.
  64                          Lift l i u1 u2 \land
  65                          Lift l i t1 t2 \land
  66                          x = intf r u2 t2.
  67  intros. inversion H; clear H; intros;
  68  [ destruct H1
  69  | destruct H2
  70  | destruct H3
  71  | destruct H5
  72  | destruct H5. clear H5 H1 H3. subst. auto depth = 5
  73  ].
  74 qed.