helm/coq-contribs/LAMBDA-TYPES/pr3_confluence.v

   1 Require pr2_confluence.
   2 Require pr3_defs.
   3
   4    Section pr3_confluence. (*************************************************)
   5
   6 (*#* #stop theorem *)
   7
   8 (*#* #caption "confluence with single step reduction: strip lemma" *)
   9 (*#* #cap #cap c, t0, t1, t2, t *)
  10
  11       Theorem pr3_strip : (c:?; t0,t1:?) (pr3 c t0 t1) -> (t2:?) (pr2 c t0 t2) ->
  12                           (EX t | (pr3 c t1 t) & (pr3 c t2 t)).
  13       Intros until 1; XElim H; Intros.
  14 (* case 1 : pr3_refl *)
  15       XEAuto.
  16 (* case 2 : pr3_sing *)
  17       Pr2Confluence.
  18       LApply (H1 x); [ Clear H1 H2; Intros H1 | XAuto ].
  19       XElim H1; Intros; XEAuto.
  20       Qed.
  21
  22 (*#* #start theorem *)
  23
  24 (*#* #caption "confluence with itself: Church-Rosser property" *)
  25 (*#* #cap #cap c, t0, t1, t2, t *)
  26
  27       Theorem pr3_confluence : (c:?; t0,t1:?) (pr3 c t0 t1) -> (t2:?) (pr3 c t0 t2) ->
  28                                (EX t | (pr3 c t1 t) & (pr3 c t2 t)).
  29
  30 (*#* #stop file *)
  31
  32       Intros until 1; XElim H; Intros.
  33 (* case 1 : pr3_refl *)
  34       XEAuto.
  35 (* case 2 : pr3_sing *)
  36       LApply (pr3_strip c t3 t5); [ Clear H2; Intros H2 | XAuto ].
  37       LApply (H2 t2); [ Clear H H2; Intros H | XAuto ].
  38       XElim H; Intros.
  39       LApply (H1 x); [ Clear H1 H2; Intros H1 | XAuto ].
  40       XElim H1; Intros; XEAuto.
  41       Qed.
  42
  43    End pr3_confluence.
  44
  45       Tactic Definition Pr3Confluence :=
  46          Match Context With
  47             | [ H1: (pr3 ?1 ?2 ?3); H2: (pr2 ?1 ?2 ?4) |-? ] ->
  48                LApply (pr3_strip ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
  49                LApply (H1 ?4); [ Clear H1 H2; Intros H1 | XAuto ];
  50                XElim H1; Intros
  51             | [ H1: (pr3 ?1 ?2 ?3); H2: (pr3 ?1 ?2 ?4) |-? ] ->
  52                LApply (pr3_confluence ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
  53                LApply (H1 ?4); [ Clear H1 H2; Intros H1 | XAuto ];
  54                XElim H1; Intros
  55             | _ -> Pr2Confluence.
  56
  57 (*#* #start file *)
  58
  59 (*#* #single *)