matita/contribs/LOGIC/Track/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/LOGIC/Track/inv".
  16
  17 include "Track/defs.ma".
  18
  19 theorem track_inv_lref: \forall Q,S,i. Track Q (lref i) S \to
  20                         \exists P. Insert S i P Q.
  21  intros. inversion H; clear H; intros; subst. autobatch.
  22 qed.
  23
  24 theorem track_inv_parx: \forall P,S,h. Track P (parx h) S \to
  25                         S = pair (posr h) (posr h).
  26  intros. inversion H; clear H; intros; subst. autobatch.
  27 qed.
  28
  29 theorem track_inv_impw: \forall P,p,S. Track P (impw p) S \to
  30                         \exists B,a,b.
  31                         S = pair (impl a b) B \land
  32                         Track P p (pair lleaf B).
  33  intros. inversion H; clear H; intros; subst. autobatch depth = 5.
  34 qed.
  35
  36 theorem track_inv_impi: \forall P,p,S. Track P (impi p) S \to
  37                         \exists a,b:Formula.
  38                         S = pair lleaf (impl a b) \land
  39                         Track P p (pair a b).
  40  intros. inversion H; clear H; intros; subst. autobatch depth = 4.
  41 qed.
  42
  43 theorem track_inv_impe: \forall P,r,S. Track P (impe r) S \to
  44                         \exists Q,D,i. \exists a,b:Formula.
  45                         S = pair (impl a b) D \land
  46                         Track Q r (pair lleaf D) \land
  47                         Insert (pair a b) i P Q.
  48  intros. inversion H; clear H; intros; subst. autobatch depth = 8 size = 10.
  49 qed.
  50
  51 theorem track_inv_lleaf_impl:
  52    \forall Q,p,a,b. Track Q p (pair lleaf (impl a b)) \to
  53    (\exists P,i. p = lref i \land Insert (pair lleaf (impl a b)) i P Q) \lor
  54    (\exists r. p = impi r \land Track Q r (pair a b)).
  55  intros. inversion H; clear H; intros; subst;
  56  [ autobatch depth = 5
  57  | subst. autobatch depth = 4
  58  ].
  59 qed.
  60 (*
  61 theorem track_inv_impe: \forall P,p,q,r,S. Track P (impe p q r) S \to
  62                         \exists A,B,D. \exists a,b:Formula.
  63                         S = pair (impl a b) D \land
  64                         Track P p (pair A a) \land
  65                         Track P q (pair b B) \land
  66                         Track (abst P (pair A B)) r (pair lleaf D).
  67  intros. inversion H; clear H; intros; subst;
  68  [ destruct H2
  69  | destruct H1
  70  | destruct H3
  71  | destruct H3
  72  | destruct H7. clear H7. subst. autobatch depth = 9
  73  ].
  74 qed.
  75 *)