matita/contribs/LOGIC/Track/order.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/LOGIC/Track/order".
  16
  17 include "Track/props.ma".
  18
  19 (* Order properties *********************************************************)
  20
  21 theorem track_refl: \forall P. \forall c:Formula. \exists r.
  22                     Track P r (pair c c).
  23  intros. elim c; clear c;
  24  [ autobatch
  25  | lapply (insert_total (pair f f1) zero P); [2:autobatch];
  26    decompose. autobatch depth = 5
  27  ].
  28 qed.
  29
  30 theorem track_trans: \forall p,q,A,B. \forall c:Formula.
  31                      Track leaf p (pair A c) \to Track leaf q (pair c B) \to
  32                      \exists r. Track leaf r (pair A B).
  33  intros 1; elim p names 0; clear p;
  34  [ intros. clear H1.
  35    lapply linear track_inv_lref to H. decompose.
  36    lapply insert_inv_leaf_2 to H. decompose
  37  | intros.
  38    lapply linear track_inv_parx to H. subst. autobatch.
  39  | intros.
  40    lapply linear track_inv_impw to H1.
  41    decompose. subst.
  42    lapply linear H to H4, H2. decompose. autobatch
  43  | intros 3. elim q; clear q;
  44    [ clear H H1.
  45      lapply linear track_inv_lref to H2. decompose.
  46      lapply insert_inv_leaf_2 to H. decompose
  47    | lapply linear track_inv_parx to H2. subst. autobatch
  48    | clear H H1.
  49      lapply linear track_inv_impi to H2.
  50      lapply linear track_inv_impw to H3.
  51      decompose. subst. autobatch
  52    | clear H H1 H2.
  53      lapply linear track_inv_impi to H3.
  54      decompose. subst
  55    | clear H H1.
  56      lapply linear track_inv_impi to H2.
  57      lapply linear track_inv_impe to H3.
  58      decompose. subst. autobatch
  59    ]
  60  | intros 3. elim q; clear q;
  61    [ clear H H1.
  62      lapply linear track_inv_lref to H2. decompose.
  63      lapply insert_inv_leaf_2 to H. decompose
  64    | clear H.
  65      lapply linear track_inv_parx to H2.
  66      subst. autobatch
  67    | clear H H1.
  68      lapply linear track_inv_impe to H2.
  69      lapply linear track_inv_impw to H3.
  70      decompose. subst. autobatch
  71    | clear H H1 H2.
  72      lapply linear track_inv_impi to H3. decompose. subst
  73    | clear H H1.
  74      lapply linear track_inv_impe to H2.
  75      lapply linear track_inv_impe to H3.
  76      decompose. subst.
  77      lapply linear track_inv_lleaf_impl to H5. decompose; subst;
  78      [ clear H4 H6.
  79        lapply linear insert_inv_leaf_1 to H3. decompose. subst.
  80        lapply linear insert_inv_abst_2 to H2. decompose. subst
  81      | lapply insert_conf to H3, H4. clear H4. decompose.
  82        lapply linear track_weak to H6, H4. decompose.
  83        lapply linear track_comp to H2, H, H1. decompose. autobatch
  84      ]
  85    ]
  86  ].
  87 qed.
  88 (*
  89    | lapply linear track_inv_impi to H4.
  90      lapply linear track_inv_impe to H5.
  91      decompose. subst.
  92      destruct H4. destruct H5. clear H4 H5. subst.
  93      unfold linj in Hcut. unfold rinj in Hcut3. destruct Hcut. destruct Hcut3. clear Hcut Hcut3. subst.
  94      destruct Hcut2. clear Hcut2. subst.
  95 *)