matita/contribs/LOGIC/PRed/defs.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 (* SINGLE STEP PARALLEL REDUCTION
  18    For cut elimination
  19 *)
  20
  21 include "Insert/defs.ma".
  22
  23 inductive PRed: Context \to Proof \to Sequent \to
  24                 Context \to Proof \to Sequent \to Prop \def
  25    | pred_lref: \forall P,i,S. PRed P (lref i) S P (lref i) S
  26    | pred_prin: \forall P,h,S. PRed P (prin h) S P (prin h) S
  27    | pred_impw: \forall Q1,Q2,p1,p2. (\forall S. PRed Q1 p1 S Q2 p2 S) \to
  28                 \forall S. PRed Q1 (impw p1) S Q2 (impw p2) S
  29    | pred_impr: \forall Q1,Q2,p1,p2. (\forall S. PRed Q1 p1 S Q2 p2 S) \to
  30                 \forall S. PRed Q1 (impr p1) S Q2 (impr p2) S
  31    | pred_impi: \forall Q1,Q2,p1,p2. (\forall S. PRed Q1 p1 S Q2 p2 S) \to
  32                 \forall q1,q2. (\forall S. PRed Q1 q1 S Q2 q2 S) \to
  33                 \forall r1,r2. (\forall S,R. PRed (abst Q1 p1 q1 R) r1 S (abst Q2 p2 q2 R) r2 S) \to
  34                 \forall S. PRed Q1 (impi p1 q1 r1) S Q2 (impi p2 q2 r2) S
  35    | pred_scut: \forall Q1,Q2,p1,p2. (\forall S. PRed Q1 p1 S Q2 p2 S) \to
  36                 \forall q1,q2. (\forall S. PRed Q1 q1 S Q2 q2 S) \to
  37                 \forall S. PRed Q1 (scut p1 q1) S Q2 (scut p2 q2) S
  38    | pred_a_sx: \forall p1,p2,R,P,Q1,i. Insert p1 p2 R i P Q1 \to
  39                 \forall q0,S,Q2. Insert p1 (scut p2 q0) S i P Q2 \to
  40                 \forall q. Lift zero i q0 q \to
  41                 PRed Q1 (scut (lref i) q) S Q2 (lref i) S
  42    | pred_a_dx: \forall q1,q2,R,P,Q1,i. Insert q1 q2 R i P Q1 \to
  43                 \forall p0,S,Q2. Insert (scut p0 q1) q2 S i P Q2 \to
  44                 \forall p. Lift zero i p0 p \to
  45                 PRed Q1 (scut p (lref i)) S Q2 (lref i) S
  46    | pred_b_sx: \forall q1,q2,P1,P2,S. PRed P1 q1 S P2 q2 S \to
  47                 \forall h. PRed P1 (scut (prin h) q1) S P2 q2 S
  48    | pred_b_dx: \forall p1,p2,Q1,Q2,S. PRed Q1 p1 S Q2 p2 S \to
  49                 \forall h. PRed Q1 (scut p1 (prin h)) S Q2 p2 S
  50    | pred_c   : \forall p1,p2,Q1,Q2,S. PRed Q1 p1 S Q2 p2 S \to
  51                 \forall p. PRed Q1 (scut (impr p) (impw p1)) S Q2 p2 S
  52 .
  53
  54 (*CSC: the URI must disappear: there is a bug now *)
  55 interpretation
  56    "single step parallel reduction in B->"
  57    'parred3 x1 y1 z1 x2 y2 z2 =
  58       (cic:/matita/LOGIC/PRed/defs/PRed.ind#xpointer(1/1) x1 y1 z1 x2 y2 z2)
  59 .
  60
  61 notation "hvbox([a1,b1,c1] break => [a2,b2,c2])"
  62   non associative with precedence 45
  63 for @{ 'parred3 $a1 $b1 $c1 $a2 $b2 $c2 }.