matita/matita/lib/lambda/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 axiom pr_subst_lam: ∀Q,M,M1,N,N1,n. pr (Lambda Q M) M1 → pr N N1 →
 253   pr (Lambda Q M)[n≝N] M1[n≝N1].
 254 (*
 255 #Q #M (elim M)
 256   [#i #M1 #N #N1 #n #pr1 #pr2
 257    (cases (prLambda_not_dummy … pr1 ?)) //
 258    #M2 * #N2 * * #eqM1 #pr3 #pr4 >eqM1 normalize @lam // *)
 259 (*
 260   cases(prLambda … pr1);
 261     [* #M2 * #N2 * * #eqM2 #pr3 #pr4 >eqM2 normalize
 262      @lam; [@Hind1 // | @Hind2 // ]
 263     |* #M2 * #Q1 * #eqM * #eqM1 #pr3 >eqM >eqM1
 264      normalize @dlam *)
 265 (* axiom pr_subst: ∀M,M1,N,N1. pr M M1 → pr N N1 →
 266   pr M[0≝N] M1[0≝N1]. *)
 267
 268 theorem pr_subst: ∀M,M1,N,N1,n. pr M M1 → pr N N1 →
 269   pr M[n≝N] M1[n≝N1].
 270 #M (elim M)
 271   [#i #M1 #N #N1 #n #pr1 #pr2 normalize >(prSort … pr1) //
 272   |#i #M1 #N #N1 #n #pr1 #pr2 >(prRel … pr1)
 273    (* gran casino
 274    normalize (cases n) // *)
 275   |#Q #M #Hind1 #Hind2 #M1 #N #N1 #pr1 #pr2
 276   |#Q #M #Hind1 #Hind2 #M1 #N #N1 #n #pr1 #pr2
 277    @pr_subst_lam //
 278   |#Q #M #Hind1 #Hind2 #M1 #N #N1 #n #pr1 #pr2
 279    (cases (prProd … pr1)) #M2 * #N2 * * #eqM1 #pr3 #pr4 >eqM1
 280    @prod [@Hind1 // | @Hind2 // ]
 281   |#Q #Hind #M1 #N #N1 #n #pr1 #pr2 (cases (prD … pr1))
 282    #M2 * #eqM1 #pr1 >eqM1 @d @Hind //
 283   ]
 284
 285 lemma pr_full_app: ∀M,N,N1. pr N N1 →
 286   (∀S.subterm S M → pr S (full S)) →
 287   pr (App M N) (full_app M N1).
 288 #M (elim M) normalize /2/
 289   [#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @appl // @Hind1 /3/
 290   |#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @beta /2/
 291   |#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @appl // @prod /2/
 292   |#P #Hind #N1 #N2 #prN #H @dapp @Hind /3/
 293   ]
 294 qed.
 295
 296 lemma pr_full_lam: ∀M,N,N1. pr N N1 →
 297   (∀S.subterm S M → pr S (full S)) →
 298   pr (Lambda N M) (full_lam N1 M).
 299 #M (elim M) normalize /2/
 300   [#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @lam // @pr_full_app /3/
 301   |#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @lam // @Hind2 /3/
 302   |#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @lam // @prod /2/
 303   |#P #Hind #N1 #N2 #prN #H @dlam @Hind /3/
 304   ]
 305 qed.
 306
 307 theorem pr_full: ∀M. pr M (full M).
 308 @Telim #M (cases M)
 309   [//
 310   |//
 311   |#M1 #N1 #H @pr_full_app /3/
 312   |#M1 #N1 #H @pr_full_lam /3/
 313   |#M1 #N1 #H @prod /2/
 314   |#P #H @d /2/
 315   ]
 316 qed.
 317
 318 lemma complete_beta: ∀Q,N,N1,M,M1.(* pr N N1 → *) pr N1 (full N) →
 319  (∀S,P.subterm S (Lambda Q M) → pr S P → pr P (full S)) →
 320  pr (Lambda Q M) M1 → pr (App M1 N1) ((full M) [O ≝ (full N)]).
 321 #Q #N #N1 #M (elim M)
 322   [1,2:#n #M1 #prN1 #sub #pr1
 323    (cases (prLambda_not_dummy … pr1 ?)) // #M2 * #N2
 324    * * #eqM1 #pr3 #pr4 >eqM1 @beta /3/
 325   |3,4,5:#M1 #M2 #_ #_ #M3 #prN1 #sub #pr1
 326    (cases (prLambda_not_dummy … pr1 ?)) // #M4 * #N3
 327    * * #eqM3 #pr3 #pr4 >eqM3 @beta /3/
 328   |#M1 #Hind #M2 #prN1 #sub #pr1
 329    (cases (prLambda_dummy … pr1))
 330     [* #M3 * #N3 * * #eqM2 #pr3 #pr4 >eqM2
 331      @beta // normalize @d @sub /2/
 332     |* #P * #eqM2 #pr3 >eqM2 normalize @dapp
 333      @Hind // #S #P #subH #pr4 @sub //
 334      (cases (sublam … subH)) [* [* /2/ | /2/] | /3/
 335     ]
 336   ]
 337 qed.
 338
 339 lemma complete_beta1: ∀Q,N,M,M1.
 340  (∀N1. pr N N1 → pr N1 (full N)) →
 341  (∀S,P.subterm S (Lambda Q M) → pr S P → pr P (full S)) →
 342  pr (App (Lambda Q M) N) M1 → pr M1 ((full M) [O ≝ (full N)]).
 343 #Q #N #M #M1 #prH #subH #prApp
 344 (cases (prApp_lambda … prApp)) #M2 * #N2 *
 345   [* * #eqM1 #pr1 #pr2 >eqM1 @pr_subst; [@subH // | @prH //]
 346   |* * #eqM1 #pr1 #pr2 >eqM1 @(complete_beta … pr1);
 347     [@prH //
 348     |#S #P #subS #prS @subH //
 349     ]
 350   ]
 351 qed.
 352
 353 lemma complete_app: ∀M,N,P.
 354   (∀S,P.subterm S (App M N) → pr S P → pr P (full S)) →
 355   pr (App M N) P → pr P (full_app M (full N)).
 356 #M (elim M) normalize
 357   [#n #P #Q #Hind #pr1
 358    cases (prApp_not_dummy_not_lambda … pr1 ??) //
 359    #M1 * #N1 * * #eqQ #pr1 #pr2 >eqQ @appl;
 360     [@(Hind (Sort n)) // |@Hind //]
 361   |#n #P #Q #Hind #pr1
 362    cases (prApp_not_dummy_not_lambda … pr1 ??) //
 363    #M1 * #N1 * * #eqQ #pr1 #pr2 >eqQ @appl;
 364     [@(Hind (Rel n)) // |@Hind //]
 365   |#P #Q #Hind1 #Hind2 #N1 #N2 #subH #prH
 366    cases (prApp_not_dummy_not_lambda … prH ??) //
 367    #M2 * #N2 * * #eqQ #pr1 #pr2 >eqQ @appl;
 368     [@Hind1 /3/ |@subH //]
 369   |#P #Q #Hind1 #Hind2 #N1 #P2 #subH #prH
 370    @(complete_beta1 … prH);
 371      [#N2 @subH // | #S #P1 #subS @subH
 372       (cases (sublam … subS)) [* [* /2/ | /2/] | /2/]
 373      ]
 374   |#P #Q #Hind1 #Hind2 #N1 #N2 #subH #prH
 375    cases (prApp_not_dummy_not_lambda … prH ??) //
 376    #M2 * #N2 * * #eqQ #pr1 #pr2 >eqQ @appl;
 377     [@(subH (Prod P Q)) // |@subH //]
 378   |#P #Hind #N1 #N2 #subH #prH
 379    (cut (∀S. subterm S (App P N1) → subterm S (App (D P) N1)))
 380     [#S #sub (cases (subapp …sub)) [* [ * /2/ | /3/] | /2/]] #Hcut
 381    cases (prApp_D … prH);
 382     [* #N3 * #eqN3 #pr1 >eqN3 @d @Hind //
 383      #S #P1 #sub1 #prS @subH /2/
 384     |* #N3 * #N4 * * #eqN2 #prP #prN1 >eqN2 @dapp @Hind;
 385       [#S #P1 #sub1 #prS @subH /2/ |@appl // ]
 386     ]
 387   ]
 388 qed.
 389
 390 lemma complete_lam: ∀M,Q,M1.
 391  (∀S,P.subterm S (Lambda Q M) → pr S P → pr P (full S)) →
 392  pr (Lambda Q M) M1 → pr M1 (full_lam (full Q) M).
 393 #M (elim M)
 394   [#n #Q #M1 #sub #pr1 normalize
 395    (cases (prLambda_not_dummy … pr1 ?)) // #M2 * #N2
 396    * * #eqM1 #pr3 #pr4 >eqM1 @lam;
 397     [@sub /2/ | @(sub (Sort n)) /2/]
 398   |#n #Q #M1 #sub #pr1 normalize
 399    (cases (prLambda_not_dummy … pr1 ?)) // #M2 * #N2
 400    * * #eqM1 #pr3 #pr4 >eqM1 @lam;
 401     [@sub /2/ | @(sub (Rel n)) /2/]
 402   |#M1 #M2 #_ #_ #M3 #Q #sub #pr1
 403    (cases (prLambda_not_dummy … pr1 ?)) // #M4 * #N3
 404    * * #eqM3 #pr3 #pr4 >eqM3 @lam;
 405     [@sub // | @complete_app // #S #P1 #subS @sub
 406      (cases (subapp …subS)) [* [* /2/ | /2/] | /3/ ]
 407     ]
 408   |#M1 #M2 #_ #Hind #M3 #Q #sub #pr1
 409    (cases (prLambda_not_dummy … pr1 ?)) // #M4 * #N3
 410    * * #eqM3 #pr3 #pr4 >eqM3 @lam;
 411     [@sub // |@Hind // #S #P1 #subS @sub
 412      (cases (sublam …subS)) [* [* /2/ | /2/] | /3/ ]
 413     ]
 414   |#M1 #M2 #_ #_ #M3 #Q #sub #pr1
 415    (cases (prLambda_not_dummy … pr1 ?)) // #M4 * #N3
 416    * * #eqM3 #pr3 #pr4 >eqM3 @lam;
 417     [@sub // | (cases (prProd … pr4)) #M5 * #N4 * * #eqN3
 418      #pr5 #pr6 >eqN3 @prod;
 419       [@sub /3/ | @sub /3/]
 420     ]
 421   |#P #Hind #Q #M2 #sub #pr1 (cases (prLambda_dummy … pr1))
 422     [* #M3 * #N3 * * #eqM2 #pr3 #pr4 >eqM2 normalize
 423      @dlam @Hind;
 424       [#S #P1 #subS @sub (cases (sublam …subS))
 425         [* [* /2/ | /2/ ] |/3/ ]
 426       |@lam //
 427       ]
 428     |* #P * #eqM2 #pr3 >eqM2 normalize @d
 429      @Hind // #S #P #subH @sub
 430      (cases (sublam … subH)) [* [* /2/ | /2/] | /3/]
 431     ]
 432   ]
 433 qed.
 434
 435 theorem complete: ∀M,N. pr M N → pr N (full M).
 436 @Telim #M (cases M)
 437   [#n #Hind #N #prH normalize >(prSort … prH) //
 438   |#n #Hind #N #prH normalize >(prRel … prH) //
 439   |#M #N #Hind #Q @complete_app
 440    #S #P #subS @Hind //
 441   | #P #P1 #Hind #N #Hpr @(complete_lam … Hpr)
 442    #S #P #subS @Hind //
 443   |5: #P #P1 #Hind #N #Hpr
 444    (cases (prProd …Hpr)) #M1 * #N1 * * #eqN >eqN normalize /3/
 445   |6:#N #Hind #P #prH normalize cases (prD … prH)
 446    #Q * #eqP >eqP #prN @d @Hind //
 447   ]
 448 qed.
 449
 450 theorem diamond: ∀P,Q,R. pr P Q → pr P R → ∃S.
 451 pr Q S ∧ pr P S.
 452 #P #Q #R #pr1 #pr2 @(ex_intro … (full P)) /3/
 453 qed.
 454
 455
 456