matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fwd.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/fwd".
  16
  17 include "Lift/defs.ma".
  18
  19 theorem lift_sort_1: \forall q, h, d, k, x.
  20                      Lift q h d (leaf (sort k)) x \to
  21                      x = leaf (sort k).
  22  intros. inversion H; clear H; intros;
  23  [ auto
  24  | destruct H3
  25  | destruct H4
  26  | destruct H5
  27  | destruct H7
  28  | destruct H7
  29  | destruct H8
  30  ].
  31 qed.
  32
  33 theorem lift_lref_1: \forall q, h, d, k, x.
  34                      Lift q h d (leaf (lref k)) x \to
  35                      (q = false \land x = leaf (lref k)) \lor
  36                      (q = true \land k < d \land x = leaf (lref k)) \lor
  37                      (q = true \land d <= k \land
  38                       \exists e. (k + h == e) \land x = leaf (lref e)
  39                      ).
  40  intros. inversion H; clear H; intros;
  41  [ destruct H3
  42  | destruct H3. clear H3. subst. auto depth = 4
  43  | destruct H4. clear H4. subst. auto depth = 5
  44  | destruct H5. clear H5. subst. auto depth = 5
  45  | destruct H7
  46  | destruct H7
  47  | destruct H8
  48  ].
  49 qed.
  50
  51 theorem lift_head_1: \forall q, l, i, p, z, u1, t1, x.
  52                      Lift q l i (head p z u1 t1) x \to
  53                      (p = q \land
  54                                   \exists r, u2, t2.
  55                                   z = bind r \land
  56                                   Lift true l i u1 u2 \land Lift q l (succ i) t1 t2 \land
  57                                   x = head p z u2 t2
  58                                  ) \lor
  59                                  (p = q \land
  60                                   \exists r,u2,t2.
  61                                   z = flat r \land
  62                                   Lift true l i u1 u2 \land Lift q l i t1 t2 \land
  63                                   x = head p z u2 t2
  64                                  ) \lor
  65                                  ((p = q \to False) \land
  66                                   \exists u2,t2.
  67                                   Lift true l i u1 u2 \land Lift q l i t1 t2 \land
  68                                   x = head p z u2 t2
  69                                  ).
  70  intros. inversion H; clear H; intros;
  71  [ destruct H3
  72  | destruct H3
  73  | destruct H4
  74  | destruct H5
  75  | destruct H7. clear H7 H1 H3. subst. auto depth = 10
  76  | destruct H7. clear H7 H1 H3. subst. auto depth = 10
  77  | destruct H8. clear H8 H2 H4. subst. auto depth = 7
  78  ].
  79 qed.