matita/matita/lib/pts_dummy_new/par_reduction.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "pts_dummy_new/subterms.ma".
  13
  14 (*
  15 inductive T : Type[0] ≝
  16   | Sort: nat → T
  17   | Rel: nat → T
  18   | App: T → T → T
  19   | Lambda: T → T → T (* type, body *)
  20   | Prod: T → T → T (* type, body *)
  21   | D: T →T →T
  22 . *)
  23
  24 (*
  25 let rec is_dummy M ≝
  26 match M with
  27   [D P ⇒ true
  28   |_ ⇒ false
  29   ]. *)
  30
  31 let rec is_lambda M ≝
  32 match M with
  33   [Lambda P Q ⇒ true
  34   |_ ⇒ false
  35   ].
  36
  37 (*
  38 theorem is_dummy_to_exists: ∀M. is_dummy M = true →
  39 ∃N. M = D N.
  40 #M (cases M) normalize
  41   [1,2: #n #H destruct|3,4,5: #P #Q #H destruct
  42   |#N #_ @(ex_intro … N) //
  43   ]
  44 qed.*)
  45
  46 theorem is_lambda_to_exists: ∀M. is_lambda M = true →
  47 ∃P,N. M = Lambda P N.
  48 #M (cases M) normalize
  49   [1,2: #n #H destruct|3,5,6: #P #Q #H destruct
  50   |#P #N #_ @(ex_intro … P) @(ex_intro … N) //
  51   ]
  52 qed.
  53
  54 inductive pr : T →T → Prop ≝
  55   | beta: ∀P,M,N,M1,N1. pr M M1 → pr N N1 →
  56       pr (App (Lambda P M) N) (M1[0 ≝ N1])
  57   | none: ∀M. pr M M
  58   | appl: ∀M,M1,N,N1. pr M M1 → pr N N1 → pr (App M N) (App M1 N1)
  59   | lam: ∀P,P1,M,M1. pr P P1 → pr M M1 →
  60       pr (Lambda P M) (Lambda P1 M1)
  61   | prod: ∀P,P1,M,M1. pr P P1 → pr M M1 →
  62       pr (Prod P M) (Prod P1 M1)
  63   | d: ∀M,M1,N,N1. pr M M1 → pr N N1 → pr (D M N) (D M1 N1).
  64
  65 lemma prSort: ∀M,n. pr (Sort n) M → M = Sort n.
  66 #M #n #prH (inversion prH)
  67   [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
  68   |//
  69   |3,4,5,6: #M #M1 #N #N1 #_ #_ #_ #_ #H destruct
  70   ]
  71 qed.
  72
  73 lemma prRel: ∀M,n. pr (Rel n) M → M = Rel n.
  74 #M #n #prH (inversion prH)
  75   [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
  76   |//
  77   |3,4,5,6: #M #M1 #N #N1 #_ #_ #_ #_ #H destruct
  78   ]
  79 qed.
  80
  81 lemma prD: ∀M,N,P. pr (D M N) P →
  82   ∃M1,N1.P = D M1 N1 ∧ pr M M1 ∧ pr N N1.
  83 #M #N #P #prH (inversion prH)
  84   [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
  85   |#Q #eqQ #_ @(ex_intro … M) @(ex_intro … N) /3/
  86   |3,4,5: #M #M1 #N #N1 #_ #_ #_ #_ #H destruct
  87   |#M1 #M2 #N1 #N2 #pr1 #pr2 #_ #_ #H destruct #eqP
  88    @(ex_intro … M2) @(ex_intro … N2) /3/
  89   ]
  90 qed.
  91 (* BEGIN HERE
  92 lemma prApp_not_lambda:
  93 ∀M,N,P. pr (App M N) P → is_lambda M = false →
  94   ∃M1,N1. (P = App M1 N1 ∧ pr M M1 ∧ pr N N1).
  95 #M #N #P #prH (inversion prH)
  96   [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct #_ #H1 destruct
  97   |#M1 #eqM1 #_ #_ @(ex_intro … M) @(ex_intro … N) /3/
  98   |#M1 #N1 #M2 #N2 #pr1 #pr2 #_ #_ #H #H1 #_ destruct
  99    @(ex_intro … N1) @(ex_intro … N2) /3/
 100   |4,5,6: #M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 101   ]
 102 qed.
 103
 104 lemma prApp_lambda:
 105 ∀Q,M,N,P. pr (App (Lambda Q M) N) P →
 106   ∃M1,N1. (P = M1[0:=N1] ∧ pr M M1 ∧ pr N N1) ∨
 107    (P = (App M1 N1) ∧ pr (Lambda Q M) M1 ∧ pr N N1).
 108 #Q #M #N #P #prH (inversion prH)
 109   [#R #M #N #M1 #N1 #pr1 #pr2 #_ #_ #H destruct #_
 110    @(ex_intro … M1) @(ex_intro … N1) /4/
 111   |#M1 #eqM1 #_ @(ex_intro … (Lambda Q M)) @(ex_intro … N) /4/
 112   |#M1 #N1 #M2 #N2 #pr1 #pr2 #_ #_ #H destruct #_
 113    @(ex_intro … N1) @(ex_intro … N2) /4/
 114   |4,5,6: #M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 115   ]
 116 qed.
 117
 118 lemma prLambda: ∀M,N,P. pr (Lambda M N) P →
 119   ∃M1,N1. (P = Lambda M1 N1 ∧ pr M M1 ∧ pr N N1).
 120 #M #N #P #prH (inversion prH)
 121   [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
 122   |#Q #eqQ #_ @(ex_intro … M) @(ex_intro … N) /3/
 123   |3,5,6: #M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 124   |#Q #Q1 #S #S1 #pr1 #pr2 #_ #_ #H #H1 destruct
 125    @(ex_intro … Q1) @(ex_intro … S1) /3/
 126   ]
 127 qed.
 128
 129 lemma prProd: ∀M,N,P. pr (Prod M N) P →
 130   ∃M1,N1. P = Prod M1 N1 ∧ pr M M1 ∧ pr N N1.
 131 #M #N #P #prH (inversion prH)
 132   [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
 133   |#Q #eqQ #_ @(ex_intro … M) @(ex_intro … N) /3/
 134   |3,4,6: #M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 135   |#Q #Q1 #S #S1 #pr1 #pr2 #_ #_ #H #H1 destruct
 136    @(ex_intro … Q1) @(ex_intro … S1) /3/
 137   ]
 138 qed.
 139
 140 let rec full M ≝
 141   match M with
 142   [ Sort n ⇒ Sort n
 143   | Rel n ⇒ Rel n
 144   | App P Q ⇒ full_app P (full Q)
 145   | Lambda P Q ⇒ Lambda (full P) (full Q)
 146   | Prod P Q ⇒ Prod (full P) (full Q)
 147   | D P Q ⇒ D (full P) (full Q)
 148   ]
 149 and full_app M N ≝
 150   match M with
 151   [ Sort n ⇒ App (Sort n) N
 152   | Rel n ⇒ App (Rel n) N
 153   | App P Q ⇒ App (full_app P (full Q)) N
 154   | Lambda P Q ⇒ (full Q) [0 ≝ N]
 155   | Prod P Q ⇒ App (Prod (full P) (full Q)) N
 156   | D P Q ⇒ App (D (full P) (full Q)) N
 157   ]
 158 .
 159
 160 lemma pr_lift: ∀N,N1,n. pr N N1 →
 161   ∀k. pr (lift N k n) (lift N1 k n).
 162 #N #N1 #n #pr1 (elim pr1)
 163   [#P #M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k
 164    normalize >lift_subst_up @beta; //
 165   |//
 166   |#M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k
 167    normalize @appl; [@Hind1 |@Hind2]
 168   |#M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k
 169    normalize @lam; [@Hind1 |@Hind2]
 170   |#M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k
 171    normalize @prod; [@Hind1 |@Hind2]
 172   |#M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k
 173    normalize @d; [@Hind1 |@Hind2]
 174   ]
 175 qed.
 176
 177 theorem pr_subst: ∀M,M1,N,N1,n. pr M M1 → pr N N1 →
 178   pr M[n≝N] M1[n≝N1].
 179 @Telim_size #P (cases P)
 180   [#i #Hind #N #M1 #N1 #n #pr1 #pr2 >(prSort … pr1) //
 181   |#i #Hind #N #M1 #N1 #n #pr1 #pr2 >(prRel … pr1)
 182     (cases (true_or_false (leb i n)))
 183     [#lein (cases (le_to_or_lt_eq i n (leb_true_to_le … lein)))
 184       [#ltin >(subst_rel1 … ltin) >(subst_rel1 … ltin) //
 185       |#eqin >eqin >subst_rel2 >subst_rel2 /2/
 186       ]
 187     |#lefalse (cut (n < i)) [@not_le_to_lt /2/] #ltni
 188      >(subst_rel3 … ltni) >(subst_rel3 … ltni) //
 189     ]
 190   |#Q #M #Hind #M1 #N #N1 #n #pr1 #pr2
 191    (cases (true_or_false (is_lambda Q)))
 192     [#islambda (cases (is_lambda_to_exists … islambda))
 193      #M2 * #N2 #eqQ >eqQ in pr1 #pr3 (cases (prApp_lambda … pr3))
 194      #M3 * #N3 *
 195       [* * #eqM1 #pr4 #pr5 >eqM1
 196        >(plus_n_O n) in ⊢ (??%) >subst_lemma @beta;
 197         [<plus_n_O @Hind // >eqQ
 198          @(transitive_lt ? (size (Lambda M2 N2))) normalize //
 199         |@Hind // normalize //
 200         ]
 201       |* * #eqM1 #pr4 #pr5 >eqM1 @appl;
 202         [@Hind // <eqQ normalize //
 203         |@Hind // normalize //
 204         ]
 205       ]
 206     |#notlambda (cases (prApp_not_lambda … pr1 ?)) //
 207      #M2 * #N2 * * #eqM1 #pr3 #pr4 >eqM1 @appl;
 208       [@Hind // normalize // |@Hind // normalize // ]
 209     ]
 210   |#Q #M #Hind #M1 #N #N1 #n #pr1 #pr2
 211    (cases (prLambda … pr1))
 212    #N2 * #Q1 * * #eqM1 #pr3 #pr4 >eqM1 @lam;
 213     [@Hind // normalize // | @Hind // normalize // ]
 214   |#Q #M #Hind #M1 #N #N1 #n #pr1 #pr2
 215    (cases (prProd … pr1)) #M2 * #N2 * * #eqM1 #pr3 #pr4 >eqM1
 216    @prod; [@Hind // normalize // | @Hind // normalize // ]
 217   |#Q #M #Hind #M1 #N #N1 #n #pr1 #pr2
 218    (cases (prD … pr1)) #M2 * #N2 * * #eqM1 #pr3 #pr4 >eqM1
 219    @d; [@Hind // normalize // | @Hind // normalize // ]
 220   ]
 221 qed.
 222
 223 lemma pr_full_app: ∀M,N,N1. pr N N1 →
 224   (∀S.subterm S M → pr S (full S)) →
 225   pr (App M N) (full_app M N1).
 226 #M (elim M) normalize /2/
 227   [#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @appl // @Hind1 /3/
 228   |#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @beta /2/
 229   |#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @appl // @prod /2/
 230   |#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @appl // @d /2/
 231   ]
 232 qed.
 233
 234 theorem pr_full: ∀M. pr M (full M).
 235 @Telim #M (cases M) normalize
 236   [//
 237   |//
 238   |#M1 #N1 #H @pr_full_app /3/
 239   |#M1 #N1 #H normalize /3/
 240   |#M1 #N1 #H @prod /2/
 241   |#M1 #N1 #H @d /2/
 242   ]
 243 qed.
 244
 245 lemma complete_app: ∀M,N,P.
 246   (∀S,P.subterm S (App M N) → pr S P → pr P (full S)) →
 247   pr (App M N) P → pr P (full_app M (full N)).
 248 #M (elim M) normalize
 249   [#n #P #Q #subH #pr1 cases (prApp_not_lambda … pr1 ?) //
 250    #M1 * #N1 * * #eqQ #pr1 #pr2 >eqQ @appl;
 251     [@(subH (Sort n)) // |@subH //]
 252   |#n #P #Q #subH #pr1 cases (prApp_not_lambda … pr1 ?) //
 253    #M1 * #N1 * * #eqQ #pr1 #pr2 >eqQ @appl;
 254     [@(subH (Rel n)) // |@subH //]
 255   |#P #Q #Hind1 #Hind2 #N1 #N2 #subH #prH
 256    cases (prApp_not_lambda … prH ?) //
 257    #M2 * #N2 * * #eqQ #pr1 #pr2 >eqQ @appl;
 258     [@Hind1 /3/ |@subH //]
 259   |#P #Q #Hind1 #Hind2 #N1 #P2 #subH #prH
 260    cases (prApp_lambda … prH) #M2 * #N2 *
 261     [* * #eqP2 #pr1 #pr2 >eqP2 @pr_subst /3/
 262     |* * #eqP2 #pr1 #pr2 >eqP2 (cases (prLambda … pr1))
 263      #M3 * #M4 * * #eqM2 #pr3 #pr4 >eqM2 @beta @subH /2/
 264     ]
 265   |#P #Q #Hind1 #Hind2 #N1 #N2 #subH #prH
 266    cases (prApp_not_lambda … prH ?) //
 267    #M2 * #N2 * * #eqQ #pr1 #pr2 >eqQ @appl;
 268     [@(subH (Prod P Q)) // |@subH //]
 269   |#P #Q #Hind1 #Hind2 #N1 #N2 #subH #pr1
 270    cases (prApp_not_lambda … pr1 ?) //
 271    #M1 * #N1 * * #eqQ #pr2 #pr3 >eqQ @appl;
 272     [@(subH (D P Q) M1) // |@subH //]
 273   ]
 274 qed.
 275
 276 theorem complete: ∀M,N. pr M N → pr N (full M).
 277 @Telim #M (cases M)
 278   [#n #Hind #N #prH normalize >(prSort … prH) //
 279   |#n #Hind #N #prH normalize >(prRel … prH) //
 280   |#M #N #Hind #Q @complete_app
 281    #S #P #subS @Hind //
 282   |#P #P1 #Hind #N #Hpr
 283    (cases (prLambda …Hpr)) #M1 * #N1 * * #eqN >eqN normalize /3/
 284   |#P #P1 #Hind #N #Hpr
 285    (cases (prProd …Hpr)) #M1 * #N1 * * #eqN >eqN normalize /3/
 286   |#P #P1 #Hind #N #Hpr
 287    (cases (prD …Hpr)) #M1 * #N1 * * #eqN >eqN normalize /3/
 288   ]
 289 qed.
 290
 291 theorem diamond: ∀P,Q,R. pr P Q → pr P R → ∃S.
 292 pr Q S ∧ pr P S.
 293 #P #Q #R #pr1 #pr2 @(ex_intro … (full P)) /3/
 294 qed.
 295 *)