matita/matita/lib/pts_dummy/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 (*
  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,6: #n #H destruct|3,5: #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. pr M M1 → pr (D M) (D M1).
  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   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
  70   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
  71   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
  72   |#M #N #_ #_ #H destruct
  73   ]
  74 qed.
  75
  76 lemma prRel: ∀M,n. pr (Rel n) M → M = Rel n.
  77 #M #n #prH (inversion prH)
  78   [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
  79   |//
  80   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
  81   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
  82   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
  83   |#M #N #_ #_ #H destruct
  84   ]
  85 qed.
  86
  87 lemma prD: ∀M,N. pr (D N) M → ∃P.M = D P ∧ pr N P.
  88 #M #N #prH (inversion prH)
  89   [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
  90   |#M #eqM #_ @(ex_intro … N) /2/
  91   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
  92   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
  93   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
  94   |#M1 #N1 #pr #_ #H destruct #eqM @(ex_intro … N1) /2/
  95   ]
  96 qed.
  97
  98 lemma prApp_not_lambda:
  99 ∀M,N,P. pr (App M N) P → is_lambda M = false →
 100   ∃M1,N1. (P = App M1 N1 ∧ pr M M1 ∧ pr N N1).
 101 #M #N #P #prH (inversion prH)
 102   [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct #_ #H1 destruct
 103   |#M1 #eqM1 #_ #_ @(ex_intro … M) @(ex_intro … N) /3/
 104   |#M1 #N1 #M2 #N2 #pr1 #pr2 #_ #_ #H #H1 #_ destruct
 105    @(ex_intro … N1) @(ex_intro … N2) /3/
 106   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 107   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 108   |#M #N #_ #_ #H destruct
 109   ]
 110 qed.
 111
 112 lemma prApp_lambda:
 113 ∀Q,M,N,P. pr (App (Lambda Q M) N) P →
 114   ∃M1,N1. (P = M1[0:=N1] ∧ pr M M1 ∧ pr N N1) ∨
 115    (P = (App M1 N1) ∧ pr (Lambda Q M) M1 ∧ pr N N1).
 116 #Q #M #N #P #prH (inversion prH)
 117   [#R #M #N #M1 #N1 #pr1 #pr2 #_ #_ #H destruct #_
 118    @(ex_intro … M1) @(ex_intro … N1) /4/
 119   |#M1 #eqM1 #_ @(ex_intro … (Lambda Q M)) @(ex_intro … N) /4/
 120   |#M1 #N1 #M2 #N2 #pr1 #pr2 #_ #_ #H destruct #_
 121    @(ex_intro … N1) @(ex_intro … N2) /4/
 122   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 123   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 124   |#M #N #_ #_ #H destruct
 125   ]
 126 qed.
 127
 128 lemma prLambda: ∀M,N,P. pr (Lambda M N) P →
 129   ∃M1,N1. (P = Lambda M1 N1 ∧ pr M M1 ∧ pr N N1).
 130 #M #N #P #prH (inversion prH)
 131   [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
 132   |#Q #eqQ #_ @(ex_intro … M) @(ex_intro … N) /3/
 133   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 134   |#Q #Q1 #S #S1 #pr1 #pr2 #_ #_ #H #H1 destruct
 135    @(ex_intro … Q1) @(ex_intro … S1) /3/
 136   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 137   |#M #N #_ #_ #H destruct
 138   ]
 139 qed.
 140
 141 lemma prProd: ∀M,N,P. pr (Prod M N) P →
 142   ∃M1,N1. P = Prod M1 N1 ∧ pr M M1 ∧ pr N N1.
 143 #M #N #P #prH (inversion prH)
 144   [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
 145   |#Q #eqQ #_ @(ex_intro … M) @(ex_intro … N) /3/
 146   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 147   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
 148   |#Q #Q1 #S #S1 #pr1 #pr2 #_ #_ #H #H1 destruct
 149    @(ex_intro … Q1) @(ex_intro … S1) /3/
 150   |#M #N #_ #_ #H destruct
 151   ]
 152 qed.
 153
 154 let rec full M ≝
 155   match M with
 156   [ Sort n ⇒ Sort n
 157   | Rel n ⇒ Rel n
 158   | App P Q ⇒ full_app P (full Q)
 159   | Lambda P Q ⇒ Lambda (full P) (full Q)
 160   | Prod P Q ⇒ Prod (full P) (full Q)
 161   | D P ⇒ D (full P)
 162   ]
 163 and full_app M N ≝
 164   match M with
 165   [ Sort n ⇒ App (Sort n) N
 166   | Rel n ⇒ App (Rel n) N
 167   | App P Q ⇒ App (full_app P (full Q)) N
 168   | Lambda P Q ⇒ (full Q) [0 ≝ N]
 169   | Prod P Q ⇒ App (Prod (full P) (full Q)) N
 170   | D P ⇒ App (D (full P)) N
 171   ]
 172 .
 173
 174 lemma pr_lift: ∀N,N1,n. pr N N1 →
 175   ∀k. pr (lift N k n) (lift N1 k n).
 176 #N #N1 #n #pr1 (elim pr1)
 177   [#P #M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k
 178    normalize >lift_subst_up @beta; //
 179   |//
 180   |#M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k
 181    normalize @appl; [@Hind1 |@Hind2]
 182   |#M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k
 183    normalize @lam; [@Hind1 |@Hind2]
 184   |#M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k
 185    normalize @prod; [@Hind1 |@Hind2]
 186   |#M1 #M2 #pr2 #Hind #k normalize @d //
 187   ]
 188 qed.
 189
 190 theorem pr_subst: ∀M,M1,N,N1,n. pr M M1 → pr N N1 →
 191   pr M[n≝N] M1[n≝N1].
 192 @Telim_size #P (cases P)
 193   [#i #Hind #N #M1 #N1 #n #pr1 #pr2 >(prSort … pr1) //
 194   |#i #Hind #N #M1 #N1 #n #pr1 #pr2 >(prRel … pr1)
 195     (cases (true_or_false (leb i n)))
 196     [#lein (cases (le_to_or_lt_eq i n (leb_true_to_le … lein)))
 197       [#ltin >(subst_rel1 … ltin) >(subst_rel1 … ltin) //
 198       |#eqin >eqin >subst_rel2 >subst_rel2 /2/
 199       ]
 200     |#lefalse (cut (n < i)) [@not_le_to_lt /2/] #ltni
 201      >(subst_rel3 … ltni) >(subst_rel3 … ltni) //
 202     ]
 203   |#Q #M #Hind #M1 #N #N1 #n #pr1 #pr2
 204    (cases (true_or_false (is_lambda Q)))
 205     [#islambda (cases (is_lambda_to_exists … islambda))
 206      #M2 * #N2 #eqQ >eqQ in pr1 #pr3 (cases (prApp_lambda … pr3))
 207      #M3 * #N3 *
 208       [* * #eqM1 #pr4 #pr5 >eqM1
 209        >(plus_n_O n) in ⊢ (??%) >subst_lemma @beta;
 210         [<plus_n_Sm <plus_n_O @Hind // >eqQ
 211          @(transitive_lt ? (size (Lambda M2 N2))) normalize //
 212         |@Hind // normalize //
 213         ]
 214       |* * #eqM1 #pr4 #pr5 >eqM1 @appl;
 215         [@Hind // <eqQ normalize //
 216         |@Hind // normalize //
 217         ]
 218       ]
 219     |#notlambda (cases (prApp_not_lambda … pr1 ?)) //
 220      #M2 * #N2 * * #eqM1 #pr3 #pr4 >eqM1 @appl;
 221       [@Hind // normalize // |@Hind // normalize // ]
 222     ]
 223   |#Q #M #Hind #M1 #N #N1 #n #pr1 #pr2
 224    (cases (prLambda … pr1))
 225    #N2 * #Q1 * * #eqM1 #pr3 #pr4 >eqM1 @lam;
 226     [@Hind // normalize // | @Hind // normalize // ]
 227   |#Q #M #Hind #M1 #N #N1 #n #pr1 #pr2
 228    (cases (prProd … pr1)) #M2 * #N2 * * #eqM1 #pr3 #pr4 >eqM1
 229    @prod; [@Hind // normalize // | @Hind // normalize // ]
 230   |#Q #Hind #M1 #N #N1 #n #pr1 #pr2 (cases (prD … pr1))
 231    #M2 * #eqM1 #pr1 >eqM1 @d @Hind // normalize //
 232   ]
 233 qed.
 234
 235 lemma pr_full_app: ∀M,N,N1. pr N N1 →
 236   (∀S.subterm S M → pr S (full S)) →
 237   pr (App M N) (full_app M N1).
 238 #M (elim M) normalize /2/
 239   [#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @appl // @Hind1 /3/
 240   |#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @beta /2/
 241   |#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @appl // @prod /2/
 242   |#P #Hind #N1 #N2 #prN #H @appl // @d /2/
 243   ]
 244 qed.
 245
 246 theorem pr_full: ∀M. pr M (full M).
 247 @Telim #M (cases M) normalize
 248   [//
 249   |//
 250   |#M1 #N1 #H @pr_full_app /3/
 251   |#M1 #N1 #H normalize /3/
 252   |#M1 #N1 #H @prod /2/
 253   |#P #H @d /2/
 254   ]
 255 qed.
 256
 257 lemma complete_app: ∀M,N,P.
 258   (∀S,P.subterm S (App M N) → pr S P → pr P (full S)) →
 259   pr (App M N) P → pr P (full_app M (full N)).
 260 #M (elim M) normalize
 261   [#n #P #Q #subH #pr1 cases (prApp_not_lambda … pr1 ?) //
 262    #M1 * #N1 * * #eqQ #pr1 #pr2 >eqQ @appl;
 263     [@(subH (Sort n)) // |@subH //]
 264   |#n #P #Q #subH #pr1 cases (prApp_not_lambda … pr1 ?) //
 265    #M1 * #N1 * * #eqQ #pr1 #pr2 >eqQ @appl;
 266     [@(subH (Rel n)) // |@subH //]
 267   |#P #Q #Hind1 #Hind2 #N1 #N2 #subH #prH
 268    cases (prApp_not_lambda … prH ?) //
 269    #M2 * #N2 * * #eqQ #pr1 #pr2 >eqQ @appl;
 270     [@Hind1 /3/ |@subH //]
 271   |#P #Q #Hind1 #Hind2 #N1 #P2 #subH #prH
 272    cases (prApp_lambda … prH) #M2 * #N2 *
 273     [* * #eqP2 #pr1 #pr2 >eqP2 @pr_subst /3/
 274     |* * #eqP2 #pr1 #pr2 >eqP2 (cases (prLambda … pr1))
 275      #M3 * #M4 * * #eqM2 #pr3 #pr4 >eqM2 @beta @subH /2/
 276     ]
 277   |#P #Q #Hind1 #Hind2 #N1 #N2 #subH #prH
 278    cases (prApp_not_lambda … prH ?) //
 279    #M2 * #N2 * * #eqQ #pr1 #pr2 >eqQ @appl;
 280     [@(subH (Prod P Q)) // |@subH //]
 281   |#P #Hind #N1 #N2 #subH #pr1
 282    cases (prApp_not_lambda … pr1 ?) //
 283    #M1 * #N1 * * #eqQ #pr2 #pr3 >eqQ @appl;
 284     [@(subH (D P) M1) // |@subH //]
 285   ]
 286 qed.
 287
 288 theorem complete: ∀M,N. pr M N → pr N (full M).
 289 @Telim #M (cases M)
 290   [#n #Hind #N #prH normalize >(prSort … prH) //
 291   |#n #Hind #N #prH normalize >(prRel … prH) //
 292   |#M #N #Hind #Q @complete_app
 293    #S #P #subS @Hind //
 294   |#P #P1 #Hind #N #Hpr
 295    (cases (prLambda …Hpr)) #M1 * #N1 * * #eqN >eqN normalize /3/
 296   |#P #P1 #Hind #N #Hpr
 297    (cases (prProd …Hpr)) #M1 * #N1 * * #eqN >eqN normalize /3/
 298   |#N #Hind #P #prH normalize cases (prD … prH)
 299    #Q * #eqP >eqP #prN @d @Hind //
 300   ]
 301 qed.
 302
 303 theorem diamond: ∀P,Q,R. pr P Q → pr P R → ∃S.
 304 pr Q S ∧ pr P S.
 305 #P #Q #R #pr1 #pr2 @(ex_intro … (full P)) /3/
 306 qed.
 307