matita/contribs/LOGIC/Insert/props.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 (*
  18 *)
  19
  20 include "Insert/fun.ma".
  21 (*
  22 theorem insert_conf: \forall P,Q1,S1,i1. Insert S1 i1 P Q1 \to
  23                      \forall Q2,S2,i2. Insert S2 i2 P Q2 \to
  24                      \exists Q,j1,j2.
  25                      Insert S2 j2 Q1 Q \land Insert S1 j1 Q2 Q.
  26  intros 5. elim H; clear H i1 P Q1;
  27  [ elim H1; clear H1 i2 c Q2; decompose; autobatch depth = 7 size = 8
  28  | lapply linear insert_inv_abst_1 to H3. decompose; destruct;
  29    [ autobatch depth = 7 size = 8
  30    | lapply linear H2 to H4. decompose. destruct. autobatch depth = 6 size = 8
  31    ]
  32  ].
  33 qed.
  34
  35 theorem insert_trans: \forall P1,Q1,S1,i1. Insert S1 i1 P1 Q1 \to
  36                       \forall Q2,S2,i2. Insert S2 i2 Q1 Q2 \to
  37                       \exists P2,j1,j2.
  38                       Insert S2 j2 P1 P2 \land Insert S1 j1 P2 Q2.
  39  intros 5. elim H; clear H i1 P1 Q1;
  40  [ lapply linear insert_inv_abst_1 to H1. decompose; destruct; autobatch depth = 6 size = 7
  41  | lapply linear insert_inv_abst_1 to H3. decompose; destruct;
  42    [ clear H2. autobatch depth = 7 size = 8
  43    | lapply linear H2 to H4. decompose. destruct. autobatch depth = 6 size = 8
  44    ]
  45  ].
  46 qed.
  47
  48 theorem insert_conf_rev: \forall P1,Q,S1,i1. Insert S1 i1 P1 Q \to
  49                          \forall P2,S2,i2. Insert S2 i2 P2 Q \to
  50                          (i1 = i2 \land P1 = P2) \lor
  51                          \exists Q1,Q2,j1,j2.
  52                          Insert S2 j2 Q2 P1 \land Insert S1 j1 Q1 P2.
  53  intros 5; elim H; clear H i1 P1 Q;
  54  [ inversion H1; clear H1; intros; destruct; autobatch depth = 7 size = 8
  55  | inversion H3; clear H3; intros; destruct;
  56    [ autobatch depth = 7 size = 8
  57    | clear H3; lapply linear H2 to H; decompose; destruct;
  58      autobatch depth = 8 size = 10
  59    ]
  60  ].
  61 qed.
  62
  63 theorem insert_conf_rev_full: \forall P1,Q,S1,i1. Insert S1 i1 P1 Q \to
  64                               \forall P2,S2,i2. Insert S2 i2 P2 Q \to
  65                               (S1 = S2 \land i1 = i2 \land P1 = P2) \lor
  66                               \exists Q1,Q2,j1,j2.
  67                               Insert S2 j2 Q2 P1 \land Insert S1 j1 Q1 P2.
  68  intros; lapply insert_conf_rev to H, H1; decompose; destruct;
  69  [ lapply linear insert_inj to H, H1; destruct; autobatch depth = 4
  70  | autobatch depth = 7 size = 8
  71  ].
  72 qed.
  73 *)