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

   1 (*#* #stop file *)
   2
   3 Require subst0_confluence.
   4 Require drop_props.
   5 Require pr0_subst0.
   6 Require pr0_confluence.
   7 Require pr2_defs.
   8
   9    Section pr2_confluence. (*************************************************)
  10
  11 (* case 1.1 : pr2_pr0 pr2_pr0 ***********************************************)
  12
  13       Remark pr2_pr0_pr0: (c:?; t0,t1,t2:?)
  14                           (pr0 t0 t1) -> (pr0 t0 t2) ->
  15                           (EX t:T | (pr2 c t1 t) & (pr2 c t2 t)).
  16       Intros; Pr0Confluence; XEAuto.
  17       Qed.
  18
  19 (* case 1.2 : pr2_pr0 pr2_delta *********************************************)
  20
  21       Remark pr2_pr0_delta: (c,d:?; t0,t1,t2,u:?; i:?)
  22                             (pr0 t0 t1) ->
  23                             (drop i (0) c (CTail d (Bind Abbr) u)) ->
  24                             (subst0 i u t0 t2) ->
  25                             (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
  26       Intros; Pr0Subst0; XEAuto.
  27       Qed.
  28
  29 (* case 2.2 : pr2_delta pr2_delta *******************************************)
  30
  31       Remark pr2_delta_delta: (c,d,d0:?; t0,t1,t2,u,u0:?; i,i0:?)
  32                               (drop i (0) c (CTail d (Bind Abbr) u)) ->
  33                               (subst0 i u t0 t1) ->
  34                               (drop i0 (0) c (CTail d0 (Bind Abbr) u0)) ->
  35                               (subst0 i0 u0 t0 t2) ->
  36                               (EX t:T | (pr2 c t1 t) & (pr2 c t2 t)).
  37       Intros.
  38       Apply (neq_eq_e i i0); Intros.
  39 (* case 1 : i != i0 *)
  40       Subst0Confluence; XEAuto.
  41 (* case 2 : i = i0 *)
  42       Rewrite H3 in H; Rewrite H3 in H0; Clear H3 i.
  43       DropDis; Inversion H1; Rewrite H5 in H0; Clear H1 H4 H5 d u.
  44       Subst0Confluence; [ Rewrite H1; XEAuto | XEAuto | XEAuto | XEAuto ].
  45       Qed.
  46
  47 (* main *********************************************************************)
  48
  49       Hints Resolve pr2_pr0_pr0 pr2_pr0_delta pr2_delta_delta : ltlc.
  50
  51 (*#* #start file *)
  52
  53 (*#* #caption "confluence with itself: Church-Rosser property" *)
  54 (*#* #cap #cap c, t0, t1, t2, t *)
  55
  56       Theorem pr2_confluence : (c,t0,t1:?) (pr2 c t0 t1) ->
  57                                (t2:?) (pr2 c t0 t2) ->
  58                                (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
  59
  60 (*#* #stop file *)
  61
  62       Intros; Inversion H; Inversion H0; XEAuto.
  63       Qed.
  64
  65    End pr2_confluence.
  66
  67       Tactic Definition Pr2Confluence :=
  68          Match Context With
  69             | [ H1: (pr2 ?1 ?2 ?3); H2: (pr2 ?1 ?2 ?4) |-? ] ->
  70                LApply (pr2_confluence ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
  71                LApply (H1 ?4); [ Clear H1 H2; Intros H1 | XAuto ];
  72                XElim H1; Intros
  73             | _ -> Pr0Confluence.
  74
  75 (*#* #start file *)
  76
  77 (*#* #single *)