matita/matita/lib/lambda/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 "lambda/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
  22 . *)
  23
  24 let rec is_dummy M ≝
  25 match M with
  26   [D P ⇒ true
  27   |_ ⇒ false
  28   ].
  29
  30 let rec is_lambda M ≝
  31 match M with
  32   [Lambda P Q ⇒ true
  33   |_ ⇒ false
  34   ].
  35
  36 theorem is_dummy_to_exists: ∀M. is_dummy M = true →
  37 ∃N. M = D N.
  38 #M (cases M) normalize
  39   [1,2: #n #H destruct|3,4,5: #P #Q #H destruct
  40   |#N #_ @(ex_intro … N) //
  41   ]
  42 qed.
  43
  44 theorem is_lambda_to_exists: ∀M. is_lambda M = true →
  45 ∃P,N. M = Lambda P N.
  46 #M (cases M) normalize
  47   [1,2,6: #n #H destruct|3,5: #P #Q #H destruct
  48   |#P #N #_ @(ex_intro … P) @(ex_intro … N) //
  49   ]
  50 qed.
  51
  52 inductive pr : T →T → Prop ≝
  53   | beta: ∀P,M,N,M1,N1. pr M M1 → pr N N1 →
  54       pr (App (Lambda P M) N) (M1[0 ≝ N1])
  55   | dapp: ∀M,N,P. pr (App M N) P →
  56       pr (App (D M) N) (D P)
  57   | dlam: ∀M,N,P. pr (Lambda M N) P → pr (Lambda M (D N)) (D P)
  58   | none: ∀M. pr M M
  59   | appl: ∀M,M1,N,N1. pr M M1 → pr N N1 → pr (App M N) (App M1 N1)
  60   | lam: ∀P,P1,M,M1. pr P P1 → pr M M1 →
  61       pr (Lambda P M) (Lambda P1 M1)
  62   | prod: ∀P,P1,M,M1. pr P P1 → pr M M1 →
  63       pr (Prod P M) (Prod P1 M1)
  64   | d: ∀M,M1. pr M M1 → pr (D M) (D M1).
  65
  66 lemma prSort: ∀M,n. pr (Sort n) M → M = Sort n.
  67 #M #n #prH (inversion prH)
  68   [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
  69   |#M #N #P1 #_ #_ #H destruct
  70   |#M #N #P1 #_ #_ #H destruct
  71   |//
  72   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
  73   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
  74   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
  75   |#M #N #_ #_ #H destruct
  76   ]
  77 qed.
  78
  79 lemma prRel: ∀M,n. pr (Rel n) M → M = Rel n.
  80 #M #n #prH (inversion prH)
  81   [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
  82   |#M #N #P1 #_ #_ #H destruct
  83   |#M #N #P1 #_ #_ #H destruct
  84   |//
  85   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
  86   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
  87   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
  88   |#M #N #_ #_ #H destruct
  89   ]
  90 qed.
  91
  92 lemma prD: ∀M,N. pr (D N) M → ∃P.M = D P ∧ pr N P.
  93 #M #N #prH (inversion prH)
  94   [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
  95   |#M #N #P #_ #_ #H destruct
  96   |#M #N #P1 #_ #_ #H destruct
  97   |#R #eqR <eqR #_ @(ex_intro … N) /2/
  98   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
  99   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 100   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 101   |#M1 #N1 #pr #_ #H destruct #eqM @(ex_intro … N1) /2/
 102   ]
 103 qed.
 104
 105 lemma prApp_not_dummy_not_lambda:
 106 ∀M,N,P. pr (App M N) P → is_dummy M = false → is_lambda M = false →
 107 ∃M1,N1. (P = App M1 N1 ∧ pr M M1 ∧ pr N N1).
 108 #M #N #P #prH (inversion prH)
 109   [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct #_ #_ #H1 destruct
 110   |#M1 #N1 #P1 #_ #_ #H destruct #_ #H1 destruct
 111   |#M #N #P1 #_ #_ #H destruct
 112   |#Q #eqProd #_ #_ #_ @(ex_intro … M) @(ex_intro … N) /3/
 113   |#M1 #N1 #M2 #N2 #pr1 #pr2 #_ #_ #H #H1 #_ #_ destruct
 114    @(ex_intro … N1) @(ex_intro … N2) /3/
 115   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 116   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 117   |#M #N #_ #_ #H destruct
 118   ]
 119 qed.
 120
 121 lemma prApp_D:
 122 ∀M,N,P. pr (App (D M) N) P →
 123   (∃Q. (P = D Q ∧ pr (App M N) Q)) ∨
 124   (∃M1,N1.(P = (App (D M1) N1) ∧ pr M M1 ∧ pr N N1)).
 125 #M #N #P #prH (inversion prH)
 126   [#R #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
 127   |#M1 #N1 #P1 #pr1 #_ #H destruct #eqP
 128    @or_introl @(ex_intro … P1) /2/
 129   |#M #N #P1 #_ #_ #H destruct
 130   |#R #eqR #_ @or_intror @(ex_intro … M) @(ex_intro … N) /3/
 131   |#M1 #N1 #M2 #N2 #pr1 #pr2 #_ #_ #H destruct #_
 132    cases (prD … pr1) #S * #eqN1 >eqN1 #pr3
 133    @or_intror @(ex_intro … S) @(ex_intro … N2) /3/
 134   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 135   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 136   |#M #N #_ #_ #H destruct
 137   ]
 138 qed.
 139
 140 lemma prApp_lambda:
 141 ∀Q,M,N,P. pr (App (Lambda Q M) N) P →
 142 ∃M1,N1. (P = M1[0:=N1] ∧ pr M M1 ∧ pr N N1) ∨
 143    (P = (App M1 N1) ∧ pr (Lambda Q M) M1 ∧ pr N N1).
 144 #Q #M #N #P #prH (inversion prH)
 145   [#R #M #N #M1 #N1 #pr1 #pr2 #_ #_ #H destruct #_
 146    @(ex_intro … M1) @(ex_intro … N1) /4/
 147   |#M1 #N1 #P1 #_ #_ #H destruct
 148   |#M #N #P1 #_ #_ #H destruct
 149   |#R #eqR #_ @(ex_intro … (Lambda Q M)) @(ex_intro … N) /4/
 150   |#M1 #N1 #M2 #N2 #pr1 #pr2 #_ #_ #H destruct #_
 151    @(ex_intro … N1) @(ex_intro … N2) /4/
 152   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 153   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 154   |#M #N #_ #_ #H destruct
 155   ]
 156 qed.
 157
 158 lemma prLambda_not_dummy: ∀M,N,P. pr (Lambda M N) P → is_dummy N = false →
 159 ∃M1,N1. (P = Lambda M1 N1 ∧ pr M M1 ∧ pr N N1).
 160 #M #N #P #prH (inversion prH)
 161   [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
 162   |#M #N #P1 #_ #_ #H destruct
 163   |#M #N #P1 #_ #_ #H destruct #_ #eqH destruct
 164   |#Q #eqProd #_ #_ @(ex_intro … M) @(ex_intro … N) /3/
 165   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 166   |#Q #Q1 #S #S1 #pr1 #pr2 #_ #_ #H #H1 #_ destruct
 167    @(ex_intro … Q1) @(ex_intro … S1) /3/
 168   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 169   |#M #N #_ #_ #H destruct
 170   ]
 171 qed.
 172
 173 lemma prLambda_dummy: ∀M,N,P. pr (Lambda M (D N)) P →
 174   (∃M1,N1. P = Lambda M1 (D N1) ∧ pr M M1 ∧ pr N N1) ∨
 175   (∃Q. (P = D Q ∧ pr (Lambda M N) Q)).
 176 #M #N #P #prH (inversion prH)
 177   [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
 178   |#M #N #P1 #_ #_ #H destruct
 179   |#M1 #N1 #P1 #prM #_ #eqlam destruct #H @or_intror
 180    @(ex_intro … P1) /3/
 181   |#Q #eqLam #_ @or_introl @(ex_intro … M) @(ex_intro … N) /3/
 182   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 183   |#Q #Q1 #S #S1 #pr1 #pr2 #_ #_ #H #H1 destruct
 184    cases (prD …pr2) #S2 * #eqS1 #pr3 >eqS1 @or_introl
 185    @(ex_intro … Q1) @(ex_intro … S2) /3/
 186   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 187   |#M #N #_ #_ #H destruct
 188   ]
 189 qed.
 190
 191 lemma prLambda: ∀M,N,P. pr (Lambda M N) P →
 192 (∃M1,N1. (P = Lambda M1 N1 ∧ pr M M1 ∧ pr N N1))  ∨
 193 (∃N1,Q. (N=D N1) ∧ (P = (D Q) ∧ pr (Lambda M N1) Q)).
 194 #M #N #P #prH (inversion prH)
 195   [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
 196   |#M #N #P1 #_ #_ #H destruct
 197   |#M1 #N1 #P1 #prM1 #_ #eqlam #eqP destruct @or_intror
 198    @(ex_intro … N1) @(ex_intro … P1) /3/
 199   |#Q #eqProd #_ @or_introl @(ex_intro … M) @(ex_intro … N) /3/
 200   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 201   |#Q #Q1 #S #S1 #pr1 #pr2 #_ #_ #H #H1 destruct @or_introl
 202    @(ex_intro … Q1) @(ex_intro … S1) /3/
 203   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 204   |#M #N #_ #_ #H destruct
 205   ]
 206 qed.
 207
 208 lemma prProd: ∀M,N,P. pr (Prod M N) P →
 209 ∃M1,N1. P = Prod M1 N1 ∧ pr M M1 ∧ pr N N1.
 210 #M #N #P #prH (inversion prH)
 211   [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
 212   |#M #N #P1 #_ #_ #H destruct
 213   |#M #N #P1 #_ #_ #H destruct
 214   |#Q #eqProd #_ @(ex_intro … M) @(ex_intro … N) /3/
 215   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 216   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 217   |#Q #Q1 #S #S1 #pr1 #pr2 #_ #_ #H #H1 destruct
 218    @(ex_intro … Q1) @(ex_intro … S1) /3/
 219   |#M #N #_ #_ #H destruct
 220   ]
 221 qed.
 222
 223 let rec full M ≝
 224   match M with
 225   [ Sort n ⇒ Sort n
 226   | Rel n ⇒ Rel n
 227   | App P Q ⇒ full_app P (full Q)
 228   | Lambda P Q ⇒ full_lam (full P) Q
 229   | Prod P Q ⇒ Prod (full P) (full Q)
 230   | D P ⇒ D (full P)
 231   ]
 232 and full_app M N ≝
 233   match M with
 234   [ Sort n ⇒ App (Sort n) N
 235   | Rel n ⇒ App (Rel n) N
 236   | App P Q ⇒ App (full_app P (full Q)) N
 237   | Lambda P Q ⇒ (full Q) [0 ≝ N]
 238   | Prod P Q ⇒ App (Prod (full P) (full Q)) N
 239   | D P ⇒ D (full_app P N)
 240   ]
 241 and full_lam M N on N≝
 242   match N with
 243   [ Sort n ⇒ Lambda M (Sort n)
 244   | Rel n ⇒ Lambda M (Rel n)
 245   | App P Q ⇒ Lambda M (full_app P (full Q))
 246   | Lambda P Q ⇒  Lambda M (full_lam (full P) Q)
 247   | Prod P Q ⇒ Lambda M (Prod (full P) (full Q))
 248   | D P ⇒ D (full_lam M P)
 249   ]
 250 .
 251
 252 lemma pr_lift: ∀N,N1,n. pr N N1 → ∀k. pr (lift N k n) (lift N1 k n).
 253 #N #N1 #n #pr1 (elim pr1)
 254   [#P #M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k
 255    normalize >lift_subst_up @beta; //
 256   |#M1 #N1 #P #pr2 #Hind normalize #k @dapp @Hind
 257   |#M1 #N1 #P #pr2 #Hind normalize #k @dlam @Hind
 258   |//
 259   |#M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k
 260    normalize @appl; [@Hind1 |@Hind2]
 261   |#M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k
 262    normalize @lam; [@Hind1 |@Hind2]
 263   |#M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k
 264    normalize @prod; [@Hind1 |@Hind2]
 265   |#M1 #M2 #pr2 #Hind #k normalize @d //
 266   ]
 267 qed.
 268
 269 theorem pr_subst: ∀M,M1,N,N1,n. pr M M1 → pr N N1 →
 270   pr M[n≝N] M1[n≝N1].
 271 @Telim_size #P (cases P)
 272   [#i #Hind #N #M1 #N1 #n #pr1 #pr2 >(prSort … pr1) //
 273   |#i #Hind #N #M1 #N1 #n #pr1 #pr2 >(prRel … pr1)
 274     (cases (true_or_false (leb i n)))
 275     [#lein (cases (le_to_or_lt_eq i n (leb_true_to_le … lein)))
 276       [#ltin >(subst_rel1 … ltin) >(subst_rel1 … ltin) //
 277       |#eqin >eqin >subst_rel2 >subst_rel2 /2/
 278       ]
 279     |#lefalse (cut (n < i)) [@not_le_to_lt /2/] #ltni
 280      >(subst_rel3 … ltni) >(subst_rel3 … ltni) //
 281     ]
 282   |#Q #M #Hind #M1 #N #N1 #n #pr1 #pr2
 283     (cases (true_or_false (is_dummy Q)))
 284     [#isdummy (cases (is_dummy_to_exists … isdummy))
 285      #Q1 #eqM >eqM in pr1 #pr3 (cases (prApp_D … pr3))
 286       [* #Q2 * #eqM1 #pr4 >eqM1 @dapp @(Hind (App Q1 M)) //
 287        >eqM normalize //
 288       |* #M2 * #N2 * * #eqM1 #pr4 #pr5 >eqM1 @appl;
 289         [@Hind // [<eqM normalize // | @d //]
 290         |@Hind // normalize //
 291         ]
 292       ]
 293     |#notdummy
 294      (cases (true_or_false (is_lambda Q)))
 295       [#islambda (cases (is_lambda_to_exists … islambda))
 296        #M2 * #N2 #eqQ >eqQ in pr1 #pr3 (cases (prApp_lambda … pr3))
 297        #M3 * #N3 *
 298         [* * #eqM1 #pr4 #pr5 >eqM1
 299          >(plus_n_O n) in ⊢ (??%) >subst_lemma
 300          @beta;
 301           [<plus_n_Sm <plus_n_O @Hind // >eqQ
 302            @(transitive_lt ? (size (Lambda M2 N2))) normalize //
 303           |@Hind // normalize //
 304           ]
 305         |* * #eqM1 #pr4 #pr5 >eqM1 @appl;
 306           [@Hind // <eqQ normalize //
 307           |@Hind // normalize //
 308           ]
 309         ]
 310       |#notlambda (cases (prApp_not_dummy_not_lambda … pr1 ??)) //
 311        #M2 * #N2 * * #eqM1 #pr3 #pr4 >eqM1 @appl;
 312         [@Hind // normalize // |@Hind // normalize // ]
 313       ]
 314     ]
 315   |#Q #M #Hind #M1 #N #N1 #n #pr1 #pr2
 316    (cases (prLambda … pr1))
 317     [* #M2 * #N2 * * #eqM1 #pr3 #pr4 >eqM1 @lam;
 318       [@Hind // normalize // | @Hind // normalize // ]
 319     |* #N2 * #Q1 * #eqM * #eqM1 #pr3 >eqM >eqM1 @dlam
 320      @(Hind (Lambda Q N2)) // >eqM normalize //
 321     ]
 322   |#Q #M #Hind #M1 #N #N1 #n #pr1 #pr2
 323    (cases (prProd … pr1)) #M2 * #N2 * * #eqM1 #pr3 #pr4 >eqM1
 324    @prod; [@Hind // normalize // | @Hind // normalize // ]
 325   |#Q #Hind #M1 #N #N1 #n #pr1 #pr2 (cases (prD … pr1))
 326    #M2 * #eqM1 #pr1 >eqM1 @d @Hind // normalize //
 327   ]
 328 qed.
 329
 330 lemma pr_full_app: ∀M,N,N1. pr N N1 →
 331   (∀S.subterm S M → pr S (full S)) →
 332   pr (App M N) (full_app M N1).
 333 #M (elim M) normalize /2/
 334   [#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @appl // @Hind1 /3/
 335   |#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @beta /2/
 336   |#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @appl // @prod /2/
 337   |#P #Hind #N1 #N2 #prN #H @dapp @Hind /3/
 338   ]
 339 qed.
 340
 341 lemma pr_full_lam: ∀M,N,N1. pr N N1 →
 342   (∀S.subterm S M → pr S (full S)) →
 343   pr (Lambda N M) (full_lam N1 M).
 344 #M (elim M) normalize /2/
 345   [#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @lam // @pr_full_app /3/
 346   |#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @lam // @Hind2 /3/
 347   |#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @lam // @prod /2/
 348   |#P #Hind #N1 #N2 #prN #H @dlam @Hind /3/
 349   ]
 350 qed.
 351
 352 theorem pr_full: ∀M. pr M (full M).
 353 @Telim #M (cases M)
 354   [//
 355   |//
 356   |#M1 #N1 #H @pr_full_app /3/
 357   |#M1 #N1 #H @pr_full_lam /3/
 358   |#M1 #N1 #H @prod /2/
 359   |#P #H @d /2/
 360   ]
 361 qed.
 362
 363 lemma complete_beta: ∀Q,N,N1,M,M1.(* pr N N1 → *) pr N1 (full N) →
 364  (∀S,P.subterm S (Lambda Q M) → pr S P → pr P (full S)) →
 365  pr (Lambda Q M) M1 → pr (App M1 N1) ((full M) [O ≝ (full N)]).
 366 #Q #N #N1 #M (elim M)
 367   [1,2:#n #M1 #prN1 #sub #pr1
 368    (cases (prLambda_not_dummy … pr1 ?)) // #M2 * #N2
 369    * * #eqM1 #pr3 #pr4 >eqM1 @beta /3/
 370   |3,4,5:#M1 #M2 #_ #_ #M3 #prN1 #sub #pr1
 371    (cases (prLambda_not_dummy … pr1 ?)) // #M4 * #N3
 372    * * #eqM3 #pr3 #pr4 >eqM3 @beta /3/
 373   |#M1 #Hind #M2 #prN1 #sub #pr1
 374    (cases (prLambda_dummy … pr1))
 375     [* #M3 * #N3 * * #eqM2 #pr3 #pr4 >eqM2
 376      @beta // normalize @d @sub /2/
 377     |* #P * #eqM2 #pr3 >eqM2 normalize @dapp
 378      @Hind // #S #P #subH #pr4 @sub //
 379      (cases (sublam … subH)) [* [* /2/ | /2/] | /3/
 380     ]
 381   ]
 382 qed.
 383
 384 lemma complete_beta1: ∀Q,N,M,M1.
 385  (∀N1. pr N N1 → pr N1 (full N)) →
 386  (∀S,P.subterm S (Lambda Q M) → pr S P → pr P (full S)) →
 387  pr (App (Lambda Q M) N) M1 → pr M1 ((full M) [O ≝ (full N)]).
 388 #Q #N #M #M1 #prH #subH #prApp
 389 (cases (prApp_lambda … prApp)) #M2 * #N2 *
 390   [* * #eqM1 #pr1 #pr2 >eqM1 @pr_subst; [@subH // | @prH //]
 391   |* * #eqM1 #pr1 #pr2 >eqM1 @(complete_beta … pr1);
 392     [@prH //
 393     |#S #P #subS #prS @subH //
 394     ]
 395   ]
 396 qed.
 397
 398 lemma complete_app: ∀M,N,P.
 399   (∀S,P.subterm S (App M N) → pr S P → pr P (full S)) →
 400   pr (App M N) P → pr P (full_app M (full N)).
 401 #M (elim M) normalize
 402   [#n #P #Q #Hind #pr1
 403    cases (prApp_not_dummy_not_lambda … pr1 ??) //
 404    #M1 * #N1 * * #eqQ #pr1 #pr2 >eqQ @appl;
 405     [@(Hind (Sort n)) // |@Hind //]
 406   |#n #P #Q #Hind #pr1
 407    cases (prApp_not_dummy_not_lambda … pr1 ??) //
 408    #M1 * #N1 * * #eqQ #pr1 #pr2 >eqQ @appl;
 409     [@(Hind (Rel n)) // |@Hind //]
 410   |#P #Q #Hind1 #Hind2 #N1 #N2 #subH #prH
 411    cases (prApp_not_dummy_not_lambda … prH ??) //
 412    #M2 * #N2 * * #eqQ #pr1 #pr2 >eqQ @appl;
 413     [@Hind1 /3/ |@subH //]
 414   |#P #Q #Hind1 #Hind2 #N1 #P2 #subH #prH
 415    @(complete_beta1 … prH);
 416      [#N2 @subH // | #S #P1 #subS @subH
 417       (cases (sublam … subS)) [* [* /2/ | /2/] | /2/]
 418      ]
 419   |#P #Q #Hind1 #Hind2 #N1 #N2 #subH #prH
 420    cases (prApp_not_dummy_not_lambda … prH ??) //
 421    #M2 * #N2 * * #eqQ #pr1 #pr2 >eqQ @appl;
 422     [@(subH (Prod P Q)) // |@subH //]
 423   |#P #Hind #N1 #N2 #subH #prH
 424    (cut (∀S. subterm S (App P N1) → subterm S (App (D P) N1)))
 425     [#S #sub (cases (subapp …sub)) [* [ * /2/ | /3/] | /2/]] #Hcut
 426    cases (prApp_D … prH);
 427     [* #N3 * #eqN3 #pr1 >eqN3 @d @Hind //
 428      #S #P1 #sub1 #prS @subH /2/
 429     |* #N3 * #N4 * * #eqN2 #prP #prN1 >eqN2 @dapp @Hind;
 430       [#S #P1 #sub1 #prS @subH /2/ |@appl // ]
 431     ]
 432   ]
 433 qed.
 434
 435 lemma complete_lam: ∀M,Q,M1.
 436  (∀S,P.subterm S (Lambda Q M) → pr S P → pr P (full S)) →
 437  pr (Lambda Q M) M1 → pr M1 (full_lam (full Q) M).
 438 #M (elim M)
 439   [#n #Q #M1 #sub #pr1 normalize
 440    (cases (prLambda_not_dummy … pr1 ?)) // #M2 * #N2
 441    * * #eqM1 #pr3 #pr4 >eqM1 @lam;
 442     [@sub /2/ | @(sub (Sort n)) /2/]
 443   |#n #Q #M1 #sub #pr1 normalize
 444    (cases (prLambda_not_dummy … pr1 ?)) // #M2 * #N2
 445    * * #eqM1 #pr3 #pr4 >eqM1 @lam;
 446     [@sub /2/ | @(sub (Rel n)) /2/]
 447   |#M1 #M2 #_ #_ #M3 #Q #sub #pr1
 448    (cases (prLambda_not_dummy … pr1 ?)) // #M4 * #N3
 449    * * #eqM3 #pr3 #pr4 >eqM3 @lam;
 450     [@sub // | @complete_app // #S #P1 #subS @sub
 451      (cases (subapp …subS)) [* [* /2/ | /2/] | /3/ ]
 452     ]
 453   |#M1 #M2 #_ #Hind #M3 #Q #sub #pr1
 454    (cases (prLambda_not_dummy … pr1 ?)) // #M4 * #N3
 455    * * #eqM3 #pr3 #pr4 >eqM3 @lam;
 456     [@sub // |@Hind // #S #P1 #subS @sub
 457      (cases (sublam …subS)) [* [* /2/ | /2/] | /3/ ]
 458     ]
 459   |#M1 #M2 #_ #_ #M3 #Q #sub #pr1
 460    (cases (prLambda_not_dummy … pr1 ?)) // #M4 * #N3
 461    * * #eqM3 #pr3 #pr4 >eqM3 @lam;
 462     [@sub // | (cases (prProd … pr4)) #M5 * #N4 * * #eqN3
 463      #pr5 #pr6 >eqN3 @prod;
 464       [@sub /3/ | @sub /3/]
 465     ]
 466   |#P #Hind #Q #M2 #sub #pr1 (cases (prLambda_dummy … pr1))
 467     [* #M3 * #N3 * * #eqM2 #pr3 #pr4 >eqM2 normalize
 468      @dlam @Hind;
 469       [#S #P1 #subS @sub (cases (sublam …subS))
 470         [* [* /2/ | /2/ ] |/3/ ]
 471       |@lam //
 472       ]
 473     |* #P * #eqM2 #pr3 >eqM2 normalize @d
 474      @Hind // #S #P #subH @sub
 475      (cases (sublam … subH)) [* [* /2/ | /2/] | /3/]
 476     ]
 477   ]
 478 qed.
 479
 480 theorem complete: ∀M,N. pr M N → pr N (full M).
 481 @Telim #M (cases M)
 482   [#n #Hind #N #prH normalize >(prSort … prH) //
 483   |#n #Hind #N #prH normalize >(prRel … prH) //
 484   |#M #N #Hind #Q @complete_app
 485    #S #P #subS @Hind //
 486   | #P #P1 #Hind #N #Hpr @(complete_lam … Hpr)
 487    #S #P #subS @Hind //
 488   |5: #P #P1 #Hind #N #Hpr
 489    (cases (prProd …Hpr)) #M1 * #N1 * * #eqN >eqN normalize /3/
 490   |6:#N #Hind #P #prH normalize cases (prD … prH)
 491    #Q * #eqP >eqP #prN @d @Hind //
 492   ]
 493 qed.
 494
 495 theorem diamond: ∀P,Q,R. pr P Q → pr P R → ∃S.
 496 pr Q S ∧ pr P S.
 497 #P #Q #R #pr1 #pr2 @(ex_intro … (full P)) /3/
 498 qed.
 499
 500
 501