matita/contribs/LOGIC/NTrack/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
  16
  17 include "NTrack/defs.ma".
  18 (*
  19 theorem ntrack_inv_lref: \forall Q,S,i. NTrack Q (lref i) S \to
  20                          \exists P. Insert S i P Q.
  21  intros; inversion H; clear H; intros; destruct; autobatch.
  22 qed.
  23
  24 theorem ntrack_inv_parx: \forall P,S,h. NTrack P (parx h) S \to
  25                          S = pair (posr h) (posr h).
  26  intros; inversion H; clear H; intros; destruct; autobatch.
  27 qed.
  28
  29 theorem ntrack_inv_impw: \forall P,p,S. NTrack P (impw p) S \to
  30                          \exists B,a,b.
  31                          S = pair (impl a b) B \land
  32                          NTrack P p (pair lleaf B).
  33  intros; inversion H; clear H; intros; destruct; autobatch depth = 5.
  34 qed.
  35
  36 theorem ntrack_inv_impr: \forall P,p,S. NTrack P (impr p) S \to
  37                          \exists a,b:Formula.
  38                          S = pair lleaf (impl a b) \land
  39                          NTrack P p (pair a b).
  40  intros; inversion H; clear H; intros; destruct; autobatch depth = 4.
  41 qed.
  42
  43 theorem ntrack_inv_impi: \forall P,p,q,r,S. NTrack P (impi p q r) S \to
  44                          \exists Q,A,B,D,i. \exists a,b:Formula.
  45                          S = pair (impl a b) D \land
  46                          NTrack P p (pair A a) \land
  47                          NTrack P q (pair b B) \land
  48                          NTrack Q r (pair lleaf D) \land
  49                          Insert (pair A B) i P Q.
  50  intros; inversion H; clear H; intros; destruct; autobatch depth = 12 width = 5 size = 16.
  51 qed.
  52
  53 theorem ntrack_inv_scut: \forall P,q,r,S. NTrack P (scut q r) S \to False.
  54  intros; inversion H; clear H; intros; destruct.
  55 qed.
  56
  57 theorem ntrack_inv_lleaf_impl:
  58    \forall Q,p,a,b. NTrack Q p (pair lleaf (impl a b)) \to
  59    (\exists P,i. p = lref i \land Insert (pair lleaf (impl a b)) i P Q) \lor
  60    (\exists r. p = impr r \land NTrack Q r (pair a b)).
  61  intros; inversion H; clear H; intros; destruct;
  62  [ autobatch depth = 5
  63  | destruct; autobatch depth = 4
  64  ].
  65 qed.
  66 *)