weblib/cr/cr.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 include "lambda.ma".
  16
  17 (*
  18  * beta reduction relation
  19  * EASY TO SEE THAT BETA IS EQUIVARIANT, IMPLIES WELL-FORMEDNESS AND
  20  * DOES NOT CREATE NEW FREE GLOBAL VARIABLES
  21  *)
  22 inductive beta (F: X → S_exp → Y) : S_exp → S_exp → Prop ≝
  23 | b_redex : ∀y,M,N.L F (Abs y M) → L F N →
  24                    beta F (App (Abs y M) N) (subst_Y M y N)
  25 | b_app1  : ∀M1,M2,N.beta F M1 M2 → L F N → beta F (App M1 N) (App M2 N)
  26 | b_app2  : ∀M,N1,N2.L F M → beta F N1 N2 → beta F (App M N1) (App M N2)
  27 | b_xi    : ∀M,N,x.beta F M N → beta F (Abs (F x M) (subst_X M x (Var (F x M))))
  28                                        (Abs (F x N) (subst_X N x (Var (F x N)))).
  29
  30 (* parallel reduction relation, should have the same properties *)
  31 inductive pr (F: X → S_exp → Y) : S_exp → S_exp → Prop ≝
  32 | pr_par   : ∀x.pr F (Par x) (Par x)
  33 | pr_redex : ∀x,M1,M2,N1,N2.pr F M1 M2 → pr F N1 N2 →
  34              pr F (App (Abs (F x M1) (subst_X M1 x (Var (F x M1)))) N1)
  35                   (subst_X M2 x N2)
  36 | pr_app   : ∀M1,M2,N1,N2.pr F M1 M2 → pr F N1 N2 → pr F (App M1 N1) (App M2 N2)
  37 | pr_xi    : ∀M,N,x.pr F M N → pr F (Abs (F x M) (subst_X M x (Var (F x M))))
  38                                     (Abs (F x N) (subst_X N x (Var (F x N)))).
  39
  40 (* complete development relation, should have the same properties *)
  41 inductive cd (F: X → S_exp → Y) : S_exp → S_exp → Prop ≝
  42 | cd_par   : ∀x.cd F (Par x) (Par x)
  43 | cd_redex : ∀x,M1,M2,N1,N2.cd F M1 M2 → cd F N1 N2 →
  44              cd F (App (Abs (F x M1) (subst_X M1 x (Var (F x M1)))) N1)
  45                   (subst_X M2 x N2)
  46 | cd_app   : ∀M1,M2,N1,N2.(∀y,P.M1 ≠ Abs y P) →
  47                           cd F M1 M2 → cd F N1 N2 → cd F (App M1 N1) (App M2 N2)
  48 | cd_xi    : ∀M,N,x.cd F M N → cd F (Abs (F x M) (subst_X M x (Var (F x M))))
  49                                     (Abs (F x N) (subst_X N x (Var (F x N)))).
  50
  51 notation < "hvbox(a break maction (>) (> \sub f) b)"
  52   non associative with precedence 45
  53 for @{ 'gt $f $a $b }.
  54 notation < "hvbox(a break maction (≫) (≫\sub f) b)"
  55   non associative with precedence 45
  56 for @{ 'ggt $f $a $b }.
  57 notation < "hvbox(a break maction (⋙) (⋙\sub f) b)"
  58   non associative with precedence 45
  59 for @{ 'gggt $f $a $b }.
  60
  61 notation > "hvbox(a break >[f] b)"
  62   non associative with precedence 45
  63 for @{ 'gt $f $a $b }.
  64 notation > "hvbox(a break ≫[f] b)"
  65   non associative with precedence 45
  66 for @{ 'ggt $f $a $b }.
  67 notation > "hvbox(a break ⋙[f] b)"
  68   non associative with precedence 45
  69 for @{ 'gggt $f $a $b }.
  70
  71 interpretation "pollack-sato beta reduction" 'gt F M N = (beta F M N).
  72 interpretation "pollack-sato parallel reduction" 'ggt F M N = (pr F M N).
  73 interpretation "pollack-sato complete development" 'gggt F M N = (cd F M N).
  74
  75 lemma cd_exists : ∀F:xheight.∀M.L F M → ∃N.M ⋙[F] N.
  76 intros;elim H
  77 [autobatch
  78 |generalize in match H2;generalize in match H1;clear H1 H2;cases s;intros
  79  [1,2,3:cases H2;cases H4;exists [1,3,5:apply (App x x1)]
  80   apply cd_app
  81   [1,4,7:intros;intro;destruct
  82   |*:assumption]
  83  |inversion H1;simplify;intros;destruct;clear H5 H6;
  84   cases H2;clear H2;inversion H5;simplify;intros;destruct;
  85   cases H4;clear H4 H6;exists
  86   [2:apply cd_redex
  87    [3:apply H2
  88    |4:apply H7
  89    |*:skip]
  90   |skip]]
  91 |cases H2;clear H2;exists
  92  [|apply cd_xi
  93   [|apply H3]]]
  94 qed.
  95
  96 axiom pi_swap_inv : ∀u,v,M.pi_swap ? u v · (pi_swap ? u v · M) = M.
  97
  98 (* useless... *)
  99 lemma pr_swap : ∀F:xheight.∀M,N,x1,x2.
 100                 M ≫[F] N → pi_swap ? x1 x2 · M ≫[F] pi_swap ? x1 x2 · N.
 101 intros;elim H
 102 [simplify;autobatch
 103 |simplify;do 2 rewrite > pi_lemma1;simplify;
 104  rewrite > (? : F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s));
 105  autobatch
 106 |simplify;autobatch
 107 |simplify;do 2 rewrite > pi_lemma1;simplify;
 108  rewrite > (? : F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s));
 109  [rewrite > (? : F c s1 = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s1));
 110   autobatch
 111  |autobatch]]
 112 qed.
 113
 114 inductive pr2 (F: X → S_exp → Y) : S_exp → S_exp → Prop ≝
 115 | pr2_par   : ∀x.pr2 F (Par x) (Par x)
 116 | pr2_redex : ∀x1,M1,M2,N1,N2.
 117               (∀x2.(x2 ∈ GV M1 → x2 = x1) →
 118                     pr2 F (subst_X M1 x1 (Par x2)) (subst_X M2 x1 (Par x2))) →
 119               pr2 F N1 N2 →
 120               pr2 F (App (Abs (F x1 M1) (subst_X M1 x1 (Var (F x1 M1)))) N1)
 121                    (subst_X M2 x1 N2)
 122 | pr2_app   : ∀M1,M2,N1,N2.pr2 F M1 M2 → pr2 F N1 N2 → pr2 F (App M1 N1) (App M2 N2)
 123 | pr2_xi    : ∀M,N,x1.
 124               (∀x2.(x2 ∈ GV M → x2 = x1) →
 125                     pr2 F (subst_X M x1 (Par x2)) (subst_X N x1 (Par x2))) →
 126               pr2 F (Abs (F x1 M) (subst_X M x1 (Var (F x1 M))))
 127                                  (Abs (F x1 N) (subst_X N x1 (Var (F x1 N)))).
 128
 129 inductive np (F: X → S_exp → Y) : S_exp → S_exp → Prop ≝
 130 | k1 : ∀x,M1,M2,N1,N2.np F M1 M2 → np F N1 N2 →
 131        np F (App (Abs (F x M1) (subst_X M1 x (Var (F x M1)))) N1)
 132                   (subst_X M2 x N2).
 133
 134 (*lemma np_strong_swap : ∀F:X→S_exp→Y.∀P:S_exp→S_exp→Prop.
 135  (∀c:X.
 136   ∀s:S_exp.
 137   ∀s1:S_exp.
 138   ∀s2:S_exp.
 139   ∀s3:S_exp.
 140   (∀x.(x ∈ GV s → x = c) →
 141        P (subst_X s c (Par x)) (subst_X s1 c (Par x))) →
 142   P s2 s3 →
 143   P (App (Abs (F c s) (subst_X s c (Var (F c s)))) s2) (subst_X s1 c s3)) →
 144   ∀s:S_exp.∀s1:S_exp.np F s s1→∀f:finite_perm X.P (f · s) (f · s1).
 145 intros 6;elim H1;simplify;
 146 rewrite > (?: f ·subst_X s3 c s5 = subst_X (f · s3) (f c) (f · s5))
 147 [rewrite > (?: f ·subst_X s2 c (Var (F c s2)) = subst_X (f · s2) (f c) (Var (F c s2)))
 148  [rewrite > (? : F c s2 = F (f c) (f · s2))
 149   [apply H
 150    [intros;rewrite > subst_X_fp [|assumption]
 151     rewrite > subst_X_fp [|elim daemon]
 152     [
 153    |apply H5]
 154 apply H;
 155 [intros;
 156 |assumption]*)
 157
 158 lemma pr2_swap : ∀F:xheight.∀M,N,x1,x2.
 159                 pr2 F M N → pr2 F (pi_swap ? x1 x2 · M) (pi_swap ? x1 x2 · N).
 160 intros;elim H
 161 [simplify;autobatch
 162 |simplify;do 2 rewrite > pi_lemma1;simplify;
 163  rewrite > (? : F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s))
 164  [apply pr2_redex
 165   [intros;lapply (H2 (pi_swap ? x1 x2 x))
 166    [rewrite > (? : Par x = pi_swap X x1 x2 · (Par (pi_swap X x1 x2 x)));
 167     autobatch
 168    |intro;rewrite < (swap_inv ? x1 x2 c);rewrite < eq_swap_pi;
 169     apply eq_f;apply H5;
 170     rewrite < (swap_inv ? x1 x2 x);autobatch]
 171   |assumption]
 172  |autobatch]
 173 |simplify;autobatch
 174 |simplify;do 2 rewrite > pi_lemma1;simplify;
 175  rewrite > (? : F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s));
 176  [rewrite > (? : F c s1 = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s1));
 177   [apply pr2_xi;intros;lapply (H2 (pi_swap ? x1 x2 x))
 178    [rewrite > (? : Par x = pi_swap X x1 x2 · (Par (pi_swap X x1 x2 x)));
 179     autobatch
 180    |intro;rewrite < (swap_inv ? x1 x2 c);rewrite < eq_swap_pi;
 181     apply eq_f;apply H3;
 182     rewrite < (swap_inv ? x1 x2 x);autobatch]
 183   |autobatch]
 184  |autobatch]]
 185 qed.
 186
 187 (* TODO : a couple of clear but not trivial open subproofs *)
 188 lemma pr_GV_incl : ∀F:xheight.∀M,N.M ≫[F] N → GV N ⊆ GV M.
 189 intros;elim H;simplify
 190 [autobatch
 191 |cut (GV (subst_X s1 c s3) ⊆ filter ? (GV s1) (λz.¬ (c ≟ z)) @ GV s3)
 192  [unfold;intros;cases (in_list_append_to_or_in_list ???? (Hcut ? H5))
 193   [apply in_list_to_in_list_append_l;
 194    cases (GV_subst_X_Var s c (F c s) x);clear H7;apply H8;
 195    (* reasoning from H2 and monotonicity of filter *)
 196    elim daemon
 197   |autobatch]
 198  |(* boring *) elim daemon]
 199 |unfold;intros;cases (in_list_append_to_or_in_list ???? H5);autobatch
 200 |unfold;intros;cases (GV_subst_X_Var s c (F c s) x);
 201  clear H4;apply H5;
 202  cases (GV_subst_X_Var s1 c (F c s1) x);lapply (H4 H3);clear H4 H6;
 203  (* Hletin and monotonicity of filter *)
 204  elim daemon]
 205 qed.
 206
 207 lemma pr_to_pr2 : ∀F:xheight.∀M,N.M ≫[F] N → pr2 F M N.
 208 intros;elim H
 209 [autobatch
 210 |apply pr2_redex
 211  [intros;rewrite > subst_X_fp
 212   [rewrite > subst_X_fp
 213    [autobatch
 214    |intro;apply H5;apply pr_GV_incl;
 215     [3,4:autobatch
 216     |*:skip]]
 217   |assumption]
 218  |assumption]
 219 |autobatch
 220 |apply pr2_xi;intros;rewrite > subst_X_fp
 221  [rewrite > subst_X_fp
 222   [autobatch
 223   |intro;apply H3;apply pr_GV_incl
 224    [3,4:autobatch
 225    |*:skip]]
 226  |assumption]]
 227 qed.
 228
 229 lemma pr2_to_pr : ∀F:xheight.∀M,N.pr2 F M N → M ≫[F] N.
 230 intros;elim H
 231 [1,3:autobatch
 232 |apply pr_redex
 233  [applyS (H2 c);intro;reflexivity
 234  |assumption]
 235 |apply pr_xi;applyS (H2 c);intro;reflexivity]
 236 qed.
 237
 238 (* ugly, must factorize *)
 239 lemma pr_subst_X : ∀F:xheight.∀M1,M2,x,N1,N2.
 240                    M1 ≫[F] M2 → N1 ≫[F] N2 →
 241                    subst_X M1 x N1 ≫[F] subst_X M2 x N2.
 242 intros;lapply (pr_to_pr2 ??? H) as H';clear H;
 243 generalize in match H1;generalize in match N2 as N2;generalize in match N1 as N1;
 244 clear H1 N1 N2;
 245 elim H'
 246 [simplify;apply (bool_elim ? (x ≟ c));simplify;intro;autobatch
 247 |generalize in match (p_fresh ? (x::GV s @GV N1));
 248  generalize in match (N_fresh ??);
 249  intros (c1 Hc1);
 250  rewrite > (?: Abs (F c s) (subst_X s c (Var (F c s))) =
 251                Abs (F c1 (pi_swap ? c c1 · s))
 252                  (subst_X (pi_swap ? c c1 · s) c1 (Var (F c1 (pi_swap ? c c1 · s)))))
 253  [rewrite > (?: subst_X s1 c s3 = subst_X (pi_swap ? c c1 · s1) c1 s3)
 254   [simplify;rewrite > subst_X_lemma
 255    [rewrite > subst_X_lemma in ⊢ (???%)
 256     [rewrite > (?: F c1 (pi_swap ? c c1 · s) =
 257                    F c1 (subst_X (pi_swap ? c c1 · s) x  N1))
 258      [simplify in ⊢ (? ? (? (? ? (? ? ? %)) ?) ?);apply pr_redex
 259       [rewrite < subst_X_fp
 260        [rewrite < subst_X_fp
 261         [apply H1
 262          [intro Hfalse;elim Hc1;autobatch
 263          |assumption]
 264         |intro Hfalse;elim Hc1;
 265          apply in_list_cons;apply in_list_to_in_list_append_l;
 266          lapply (H c) [|intro;reflexivity]
 267          lapply (pr2_to_pr ??? Hletin);
 268          do 2 rewrite > subst_X_x_x in Hletin1;
 269          apply (pr_GV_incl ??? Hletin1);assumption]
 270        |intro Hfalse;elim Hc1;autobatch]
 271       |autobatch]
 272      |apply p_eqb1;apply XHP
 273       [apply p_eqb4;intro Hfalse;apply Hc1;rewrite > Hfalse;autobatch
 274       |apply apart_to_apartb_true;unfold;autobatch]]
 275     |*:intro Hfalse;autobatch]
 276    |*:intro Hfalse;autobatch]
 277   |rewrite < subst_X_fp
 278    [rewrite > subst_X_merge
 279     [reflexivity
 280     |intro Hfalse;autobatch]
 281    |intro Hfalse;elim Hc1;
 282     apply in_list_cons;apply in_list_to_in_list_append_l;
 283     lapply (H c) [|intro;reflexivity]
 284     do 2 rewrite > subst_X_x_x in Hletin;
 285     lapply (pr2_to_pr ??? Hletin);autobatch]]
 286   |rewrite < (swap_left ? c c1) in ⊢ (? ? ? (? (??%?) (? ? % (? (? ? % ?)))));
 287    rewrite > eq_swap_pi;rewrite < XHE;
 288    change in ⊢ (???(??(???%))) with (pi_swap ? c c1 · (Var (F c s)));
 289    rewrite < pi_lemma1;rewrite < subst_X_fp
 290    [rewrite > (subst_X_apart ?? (Par c1))
 291     [reflexivity
 292     |elim daemon (* don't we have a lemma? *)]
 293    |intro Hfalse;elim Hc1;
 294     apply in_list_cons;apply in_list_to_in_list_append_l;(* lemma?? *) elim daemon]]
 295 |simplify;autobatch
 296 |generalize in match (p_fresh ? (x::GV s @GV N1));
 297  generalize in match (N_fresh ??);
 298  intros (c1 Hc1);
 299  rewrite > (?: Abs (F c s) (subst_X s c (Var (F c s))) =
 300                Abs (F c1 (pi_swap ? c c1 · s))
 301                (subst_X (pi_swap ? c c1 · s) c1 (Var (F c1 (pi_swap ? c c1 · s)))));
 302  [rewrite > (?: Abs (F c s1) (subst_X s1 c (Var (F c s1))) =
 303                Abs (F c1 (pi_swap ? c c1 · s1))
 304                (subst_X (pi_swap ? c c1 · s1) c1 (Var (F c1 (pi_swap ? c c1 · s1)))));
 305   [simplify;rewrite > subst_X_lemma
 306    [rewrite > subst_X_lemma in ⊢ (???%)
 307     [simplify;rewrite > (? : F c1 (pi_swap ? c c1 · s) = F c1 (subst_X (pi_swap ? c c1 · s) x N1))
 308      [rewrite > (? : F c1 (pi_swap ? c c1 · s1) = F c1 (subst_X (pi_swap ? c c1 · s1) x N2))
 309       [apply pr_xi;rewrite < subst_X_fp
 310        [rewrite < subst_X_fp
 311         [apply H1
 312          [intro Hfalse;elim Hc1;autobatch
 313          |assumption]
 314         |intro Hfalse; (* meglio fare qualcosa di più furbo *) elim daemon]
 315        |intro;elim Hc1;autobatch]
 316       |apply p_eqb1;apply XHP
 317        [apply p_eqb4;intro Hfalse;autobatch
 318        |apply apart_to_apartb_true;intro;autobatch]]
 319      |apply p_eqb1;apply XHP
 320       [apply p_eqb4;intro Hfalse;autobatch
 321       |apply apart_to_apartb_true;intro;autobatch]]
 322     |*:intro;apply Hc1;autobatch]
 323    |*:intro;apply Hc1;autobatch]
 324   |apply eq_f2
 325    [autobatch
 326    |rewrite < (swap_left ? c c1) in ⊢ (??? (??% (? (??%?))));
 327     rewrite > eq_swap_pi;rewrite < XHE;
 328     change in ⊢ (???(???%)) with (pi_swap ? c c1 · (Var (F c s1)));
 329     rewrite < pi_lemma1;rewrite < subst_X_fp
 330     [rewrite > (subst_X_apart ?? (Par c1))
 331      [reflexivity
 332      |elim daemon (* don't we have a lemma? *)]
 333     |intro Hfalse;elim Hc1;
 334      apply in_list_cons;apply in_list_to_in_list_append_l;(* lemma?? *) elim daemon]]]
 335  |apply eq_f2
 336   [autobatch
 337   |rewrite < (swap_left ? c c1) in ⊢ (??? (??% (? (??%?))));
 338    rewrite > eq_swap_pi;rewrite < XHE;
 339    change in ⊢ (???(???%)) with (pi_swap ? c c1 · (Var (F c s)));
 340    rewrite < pi_lemma1;rewrite < subst_X_fp
 341    [rewrite > (subst_X_apart ?? (Par c1))
 342     [reflexivity
 343     |elim daemon (* don't we have a lemma? *)]
 344    |intro Hfalse;elim Hc1;
 345     apply in_list_cons;apply in_list_to_in_list_append_l;(* lemma?? *) elim daemon]]]]
 346 qed.
 347
 348 lemma L_subst_X : ∀F:xheight.∀M,x,N.L F M → L F N → L F (subst_X M x N).
 349 intros;elim (L_to_LL ?? H);
 350 [simplify;cases (x ≟ c);simplify;autobatch
 351 |simplify;autobatch
 352 |generalize in match (p_fresh ? (x::GV s @GV N));
 353  generalize in match (N_fresh ??);
 354  intros (c1 Hc1);
 355  rewrite > (?: Abs (F c s) (subst_X s c (Var (F c s))) =
 356                Abs (F c1 (pi_swap ? c c1 · s))
 357                (subst_X (pi_swap ? c c1 · s) c1 (Var (F c1 (pi_swap ? c c1 · s)))));
 358  [simplify;rewrite > subst_X_lemma
 359   [simplify;rewrite > (? : F c1 (pi_swap ? c c1 · s) = F c1 (subst_X (pi_swap ? c c1 · s) x N))
 360     [apply LAbs;rewrite < subst_X_fp
 361       [apply H3;intro Hfalse;elim Hc1;autobatch
 362       |intro Hfalse;elim Hc1;autobatch]
 363     |apply p_eqb1;apply XHP
 364      [apply p_eqb4;intro Hfalse;autobatch
 365      |apply apart_to_apartb_true;intro;autobatch]]
 366   |*:intro;apply Hc1;autobatch]
 367  |apply eq_f2
 368   [autobatch
 369   |rewrite < (swap_left ? c c1) in ⊢ (??? (??% (? (??%?))));
 370    rewrite > eq_swap_pi;rewrite < XHE;
 371    change in ⊢ (???(???%)) with (pi_swap ? c c1 · (Var (F c s)));
 372    rewrite < pi_lemma1;rewrite < subst_X_fp
 373    [rewrite > (subst_X_apart ?? (Par c1))
 374     [reflexivity
 375     |elim daemon (* don't we have a lemma? *)]
 376    |intro Hfalse;elim Hc1;
 377     apply in_list_cons;apply in_list_to_in_list_append_l;
 378     (* lemma?? *) elim daemon]]]]
 379 qed.
 380
 381 inductive cd2 (F: X → S_exp → Y) : S_exp → S_exp → Prop ≝
 382 | cd2_par   : ∀x.cd2 F (Par x) (Par x)
 383 | cd2_redex : ∀x,M1,M2,N1,N2.
 384              (∀x2.(x2 ∈ GV M1 → x2 = x) →
 385                   cd2 F (subst_X M1 x (Par x2)) (subst_X M2 x (Par x2))) →
 386              cd2 F N1 N2 →
 387              cd2 F (App (Abs (F x M1) (subst_X M1 x (Var (F x M1)))) N1)
 388                   (subst_X M2 x N2)
 389 | cd2_app   : ∀M1,M2,N1,N2.(∀y,P.M1 ≠ Abs y P) →
 390                           cd2 F M1 M2 → cd2 F N1 N2 → cd2 F (App M1 N1) (App M2 N2)
 391 | cd2_xi    : ∀M,N,x.(∀x2.(x2 ∈ GV M → x2 = x) →
 392                      cd2 F (subst_X M x (Par x2)) (subst_X N x (Par x2))) →
 393                     cd2 F (Abs (F x M) (subst_X M x (Var (F x M))))
 394                           (Abs (F x N) (subst_X N x (Var (F x N)))).
 395
 396 lemma cd2_swap : ∀F:xheight.∀M,N,x1,x2.
 397                 cd2 F M N → cd2 F (pi_swap ? x1 x2 · M) (pi_swap ? x1 x2 · N).
 398 intros;elim H
 399 [simplify;autobatch
 400 |simplify;do 2 rewrite > pi_lemma1;simplify;
 401  rewrite > (? : F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s))
 402  [apply cd2_redex
 403   [intros;lapply (H2 (pi_swap ? x1 x2 x))
 404    [rewrite > (? : Par x = pi_swap X x1 x2 · (Par (pi_swap X x1 x2 x)));
 405     autobatch
 406    |intro;rewrite < (swap_inv ? x1 x2 c);rewrite < eq_swap_pi;
 407     apply eq_f;apply H5;
 408     rewrite < (swap_inv ? x1 x2 x);autobatch]
 409   |assumption]
 410  |autobatch]
 411 |simplify;apply cd2_app;
 412  [intros;generalize in match H1;cases s;simplify;intros 2;destruct;
 413   elim H6;[3:reflexivity|*:skip]
 414  |*:assumption]
 415 |simplify;do 2 rewrite > pi_lemma1;simplify;
 416  rewrite > (? : F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s));
 417  [rewrite > (? : F c s1 = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s1));
 418   [apply cd2_xi;intros;lapply (H2 (pi_swap ? x1 x2 x))
 419    [rewrite > (? : Par x = pi_swap X x1 x2 · (Par (pi_swap X x1 x2 x)));
 420     autobatch
 421    |intro;rewrite < (swap_inv ? x1 x2 c);rewrite < eq_swap_pi;
 422     apply eq_f;apply H3;
 423     rewrite < (swap_inv ? x1 x2 x);autobatch]
 424   |autobatch]
 425  |autobatch]]
 426 qed.
 427
 428 lemma cd_GV_incl : ∀F:xheight.∀M,N.M ⋙[F] N → GV N ⊆ GV M.
 429 intros;elim H;simplify
 430 [autobatch
 431 |cut (GV (subst_X s1 c s3) ⊆ filter ? (GV s1) (λz.¬ (c ≟ z)) @ GV s3)
 432  [unfold;intros;cases (in_list_append_to_or_in_list ???? (Hcut ? H5))
 433   [apply in_list_to_in_list_append_l;
 434    cases (GV_subst_X_Var s c (F c s) x);clear H7;apply H8;
 435    (* reasoning from H2 and monotonicity of filter *)
 436    elim daemon
 437   |autobatch]
 438  |(* boring *) elim daemon]
 439 |unfold;intros;cases (in_list_append_to_or_in_list ???? H6);autobatch
 440 |unfold;intros;cases (GV_subst_X_Var s c (F c s) x);
 441  clear H4;apply H5;
 442  cases (GV_subst_X_Var s1 c (F c s1) x);lapply (H4 H3);clear H4 H6;
 443  (* Hletin and monotonicity of filter *)
 444  elim daemon]
 445 qed.
 446
 447 lemma cd_to_cd2 : ∀F:xheight.∀M,N.M ⋙[F] N → cd2 F M N.
 448 intros;elim H
 449 [autobatch
 450 |apply cd2_redex
 451  [intros;rewrite > subst_X_fp
 452   [rewrite > subst_X_fp
 453    [autobatch
 454    |intro;apply H5;apply cd_GV_incl;
 455     [3,4:autobatch
 456     |*:skip]]
 457   |assumption]
 458  |assumption]
 459 |autobatch
 460 |apply cd2_xi;intros;rewrite > subst_X_fp
 461  [rewrite > subst_X_fp
 462   [autobatch
 463   |intro;apply H3;apply cd_GV_incl
 464    [3,4:autobatch
 465    |*:skip]]
 466  |assumption]]
 467 qed.
 468
 469 lemma pr_cd_triangle : ∀F:xheight.∀M,N,P.M ≫[F] N → M ⋙[F] P → N ≫[F] P.
 470 intros;generalize in match H;generalize in match N;clear H N;
 471 elim (cd_to_cd2 ??? H1)
 472 [inversion H;simplify;intros;destruct;autobatch
 473 |inversion (pr_to_pr2 ??? H5);simplify;intros;destruct;
 474  [clear H7 H9;
 475   lapply (H4 ? (pr2_to_pr ??? H8)) as H9;clear H4;
 476   generalize in match (p_fresh ? (GV s));
 477   generalize in match (N_fresh ? (GV s));intros;
 478   rewrite > (? : subst_X s6 c1 s8 = subst_X (subst_X s6 c1 (Par c2)) c2 s8)
 479   [rewrite > (? : subst_X s1 c s3 = subst_X (subst_X s1 c (Par c2)) c2 s3)
 480    [apply pr_subst_X
 481     [apply H2;
 482      [intro;elim H4;assumption
 483      |rewrite > (? : subst_X s c (Par c2) = subst_X s5 c1 (Par c2))
 484       [apply pr2_to_pr;apply H6;intro; (* must be fresh in s5 *) elim daemon
 485       |(* by Hcut2 *) elim daemon]]
 486     |assumption]
 487    |(* as long as it's fresh in s1 too *) elim daemon]
 488   |(* as long as it's fresh in s6 too *) elim daemon]
 489  |lapply (H4 ? (pr2_to_pr ??? H8));inversion H6;intros;simplify;destruct;
 490   clear H11 H7 H9;
 491   generalize in match (p_fresh ? (GV s));
 492   generalize in match (N_fresh ? (GV s));intros;
 493   rewrite > (? : subst_X s5 c1 (Var (F c1 s5)) = subst_X (subst_X s5 c1 (Par c2)) c2 (Var (F c1 s5)))
 494   [rewrite > (? : F c1 s5 = F c2 (subst_X s5 c1 (Par c2)))
 495    [rewrite > (? : subst_X s1 c s3 = subst_X (subst_X s1 c (Par c2)) c2 s3)
 496     [apply pr_redex
 497      [apply H2
 498       [intro;elim H7;assumption
 499       |rewrite > (?: subst_X s c (Par c2) = subst_X s4 c1 (Par c2))
 500        [apply pr2_to_pr;apply H10;(* suff fresh *) elim daemon
 501        |(* by Hcut1 *) elim daemon]]
 502      |assumption]
 503     |(* suff. fresh *) elim daemon]
 504    |(* eqvariance *) elim daemon]
 505   |(* eqvariance *) elim daemon]]
 506 |inversion H6;simplify;intros;destruct;
 507  [elim H [3:reflexivity|*:skip]
 508  |autobatch]
 509 |inversion (pr_to_pr2 ??? H3);simplify;intros;destruct;clear H5;
 510  generalize in match (p_fresh ? (GV s));
 511  generalize in match (N_fresh ? (GV s));intros;
 512  rewrite > (?: subst_X s4 c1 (Var (F c1 s4)) = subst_X (subst_X s4 c1 (Par c2)) c2 (Var (F c1 s4)))
 513  [rewrite > (?: subst_X s1 c (Var (F c s1)) = subst_X (subst_X s1 c (Par c2)) c2 (Var (F c s1)))
 514   [rewrite > (?: F c1 s4 = F c2 (subst_X s4 c1 (Par c2)))
 515    [rewrite > (?: F c s1 = F c2 (subst_X s1 c (Par c2)))
 516     [apply pr_xi;apply H2
 517      [intro;elim H5;assumption
 518      |rewrite > (?: subst_X s c (Par c2) = subst_X s3 c1 (Par c2))
 519       [apply pr2_to_pr;apply H4;(*suff. fresh*) elim daemon
 520       |(*by Hcut1*)elim daemon]]
 521     |(*perm*)elim daemon]
 522    |(*perm*)elim daemon]
 523   |(*suff.fresh*) elim daemon]
 524  |(*suff.fresh*) elim daemon]]
 525  qed.
 526
 527 lemma diamond_pr : ∀F:xheight.∀a,b,c.a ≫[F] b → a ≫[F] c →
 528                    ∃d.b ≫[F] d ∧ c ≫[F] d.
 529 intros;
 530 cut (L F a)
 531 [cases (cd_exists ?? Hcut) (d);
 532  exists[apply d]
 533  split;autobatch;
 534 |elim H;autobatch]
 535 qed.
 536
 537 inductive tc (A:Type) (R:A → A → Prop) : A → A → Prop ≝
 538 | tc_refl  : ∀x:A.tc A R x x
 539 | tc_trans : ∀x,y,z.R x y → tc A R y z → tc A R x z.
 540
 541 lemma strip_tc_pr : ∀F:xheight.∀a,b,c.pr F a b → tc ? (pr F) a c →
 542                       ∃d.tc ? (pr F) b d ∧ pr F c d.
 543 intros;generalize in match H;generalize in match b;clear H b;elim H1
 544 [autobatch;
 545 |cases (diamond_pr ???? H H4);cases H5;clear H5;
 546  cases (H3 ? H6);cases H5;clear H5;exists[apply x1]
 547  split;autobatch]
 548 qed.
 549
 550 lemma diamond_tc_pr : ∀F:xheight.∀a,b,c.tc ? (pr F) a b → tc ? (pr F) a c →
 551                       ∃d.tc ? (pr F) b d ∧ tc ? (pr F) c d.
 552 intros 5;generalize in match c; clear c;elim H
 553 [autobatch;
 554 |cases (strip_tc_pr ???? H1 H4);cases H5;clear H5;
 555  cases (H3 ? H6);cases H5;clear H5;
 556  exists[apply x1]
 557  split;autobatch]
 558 qed.
 559
 560 lemma tc_split : ∀A,R,a,b,c.tc A R a b → tc A R b c → tc A R a c.
 561 intros 6;elim H;autobatch;
 562 qed.
 563
 564 lemma tc_single : ∀A,R,a,b.R a b → tc A R a b.
 565 intros;autobatch;
 566 qed.
 567
 568 lemma tcb_app1 : ∀F:xheight.∀M1,M2,N.tc ? (beta F) M1 M2 → L F N →
 569                                      tc ? (beta F) (App M1 N) (App M2 N).
 570 intros;elim H;autobatch;
 571 qed.
 572
 573 lemma tcb_app2 : ∀F:xheight.∀M,N1,N2.L F M → tc ? (beta F) N1 N2 →
 574                                      tc ? (beta F) (App M N1) (App M N2).
 575 intros;elim H1;autobatch;
 576 qed.
 577
 578 lemma tcb_xi : ∀F:xheight.∀M,N,x.
 579                tc ? (beta F) M N →
 580                tc ? (beta F) (Abs (F x M) (subst_X M x (Var (F x M))))
 581                               (Abs (F x N) (subst_X N x (Var (F x N)))).
 582 intros;elim H;autobatch;
 583 qed.
 584
 585 lemma red_lemma :
 586   ∀F:xheight.∀x,M,N.L F M →
 587   subst_X M x N = subst_Y (subst_X M x (Var (F x M))) (F x M) N.
 588 intros;rewrite < subst_X_decompose;
 589 [reflexivity
 590 |rewrite > L_to_closed;autobatch
 591 |autobatch]
 592 qed.
 593
 594 lemma b_redex2 :
 595   ∀F:xheight.∀x,M,N.L F M → L F N →
 596   beta F (App (Abs (F x M) (subst_X M x (Var (F x M)))) N) (subst_X M x N).
 597 intros;rewrite > (red_lemma ???? H) in ⊢ (???%);
 598 apply b_redex;autobatch;
 599 qed.
 600
 601 lemma pr_to_L_1 : ∀F:xheight.∀a,b.a ≫[F] b → L F a.
 602 intros;elim H;autobatch;
 603 qed.
 604
 605 lemma pr_to_L_2 : ∀F:xheight.∀a,b.a ≫[F] b → L F b.
 606 intros;elim H;autobatch;
 607 qed.
 608
 609 lemma pr_to_tc_beta : ∀F:xheight.∀a,b.a ≫[F] b → tc ? (beta F) a b.
 610 intros;elim H
 611 [autobatch
 612 |apply (tc_split ?????? (?: tc ? (beta F) (App (Abs (F c s) (subst_X s c (Var (F c s)))) s3) ?));
 613  [apply tcb_app2;autobatch
 614  |apply (tc_split ?????? (?: tc ? (beta F) (App (Abs (F c s1) (subst_X s1 c (Var (F c s1)))) s3) ?));
 615   [apply tcb_app1;autobatch
 616   |apply tc_single;apply b_redex2;autobatch]]
 617 |apply (tc_split ????? (?: tc ?? (App s s2) (App s s3)))
 618  [apply tcb_app2;autobatch
 619  |apply tcb_app1;autobatch]
 620 |autobatch]
 621 qed.
 622
 623 lemma pr_refl : ∀F:xheight.∀a.L F a → a ≫[F] a.
 624 intros;elim H;try autobatch;
 625 qed.
 626
 627 lemma tc_pr_to_tc_beta: ∀F:xheight.∀a,b.tc ? (pr F) a b → tc ? (beta F) a b.
 628 intros;elim H;autobatch;
 629 qed.
 630
 631 lemma beta_to_pr : ∀F:xheight.∀a,b.a >[F] b → a ≫[F] b.
 632 intros;elim H
 633 [inversion H1;intros;destruct;
 634  rewrite < subst_X_decompose
 635  [autobatch
 636  |rewrite > (L_to_closed ?? H3);autobatch
 637  |autobatch]
 638 |2,3:apply pr_app;autobatch
 639 |apply pr_xi;assumption]
 640 qed.
 641
 642 lemma tc_beta_to_tc_pr: ∀F:xheight.∀a,b.tc ? (beta F) a b → tc ? (pr F) a b.
 643 intros;elim H;autobatch;
 644 qed.
 645
 646 theorem church_rosser:
 647   ∀F:xheight.∀a,b,c.tc ? (beta F) a b → tc ? (beta F) a c →
 648   ∃d.tc ? (beta F) b d ∧ tc ? (beta F) c d.
 649 intros;lapply (tc_beta_to_tc_pr ??? H);lapply (tc_beta_to_tc_pr ??? H1);
 650 cases (diamond_tc_pr ???? Hletin Hletin1);cases H2;
 651 exists[apply x]
 652 split;autobatch;
 653 qed.