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 width = 4 size = 8
  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_impr to H2;
  50      lapply linear track_inv_impw to H3;
  51      decompose; subst; autobatch
  52    | clear H H1 H2;
  53      lapply linear track_inv_impr to H3;
  54      decompose; subst
  55    | clear H2 H3;
  56      lapply linear track_inv_impr to H4;
  57      lapply linear track_inv_impi to H5;
  58      decompose; subst;
  59      lapply linear H to H5, H8; decompose;
  60
  61
  62      lapply linear insert_inv_leaf_1 to H4; decompose; subst;
  63      apply ex_intro; [| ]
  64
  65      autobatch depth = 100 width = 40 size = 100
  66    ]
  67  | intros 3; elim q; clear q;
  68    [ clear H H1;
  69      lapply linear track_inv_lref to H2; decompose;
  70      lapply insert_inv_leaf_2 to H; decompose
  71    | clear H;
  72      lapply linear track_inv_parx to H2;
  73      subst; autobatch
  74    | clear H H1;
  75      lapply linear track_inv_impe to H2;
  76      lapply linear track_inv_impw to H3;
  77      decompose; subst; autobatch
  78    | clear H H1 H2;
  79      lapply linear track_inv_impi to H3; decompose; subst
  80    | clear H H1;
  81      lapply linear track_inv_impe to H2;
  82      lapply linear track_inv_impe to H3;
  83      decompose; subst;
  84      lapply linear track_inv_lleaf_impl to H5; decompose; subst;
  85      [ clear H4 H6;
  86        lapply linear insert_inv_leaf_1 to H3; decompose; subst;
  87        lapply linear insert_inv_abst_2 to H2; decompose; subst
  88      | lapply insert_conf to H3, H4; clear H4; decompose;
  89        lapply linear track_weak to H6, H4; decompose;
  90        lapply linear track_comp to H2, H, H1; decompose; autobatch
  91      ]
  92    ]
  93  ].
  94 qed.
  95 (*
  96    | lapply linear track_inv_impi to H4;
  97      lapply linear track_inv_impe to H5;
  98      decompose; subst;
  99      destruct H4; destruct H5; clear H4 H5; subst;
 100      unfold linj in Hcut; unfold rinj in Hcut3; destruct Hcut; destruct Hcut3; clear Hcut Hcut3; subst;
 101      destruct Hcut2; clear Hcut2; subst;
 102 *)
 103 *)