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

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