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_free pr2_free *********************************************)
  12
  13       Remark pr2_free_free: (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_free pr2_delta ********************************************)
  20
  21       Remark pr2_free_delta: (c,d:?; t0,t1,t2,t4,u:?; i:?)
  22                              (pr0 t0 t1) ->
  23                              (drop i (0) c (CTail d (Bind Abbr) u)) ->
  24                              (pr0 t0 t4) ->
  25                              (subst0 i u t4 t2) ->
  26                              (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
  27       Intros; Pr0Confluence; Pr0Subst0; XEAuto.
  28       Qed.
  29
  30 (* case 2.2 : pr2_delta pr2_delta *******************************************)
  31
  32       Remark pr2_delta_delta: (c,d,d0:?; t0,t1,t2,t3,t4,u,u0:?; i,i0:?)
  33                               (drop i (0) c (CTail d (Bind Abbr) u)) ->
  34                               (pr0 t0 t3) ->
  35                               (subst0 i u t3 t1) ->
  36                               (drop i0 (0) c (CTail d0 (Bind Abbr) u0)) ->
  37                               (pr0 t0 t4) ->
  38                               (subst0 i0 u0 t4 t2) ->
  39                               (EX t:T | (pr2 c t1 t) & (pr2 c t2 t)).
  40       Intros; Pr0Confluence; Repeat Pr0Subst0;
  41       [ XEAuto | XEAuto | XEAuto | Idtac ].
  42       Apply (neq_eq_e i i0); Intros.
  43 (* case 1 : i != i0 *)
  44       Subst0Confluence; XEAuto.
  45 (* case 2 : i = i0 *)
  46       Rewrite H5 in H; Rewrite H5 in H3; Clear H5 i.
  47       DropDis; Inversion H2; Rewrite H7 in H3; Clear H2 H6 H7 d u.
  48       Subst0Confluence; [ Rewrite H2 in H0; XEAuto | XEAuto | XEAuto | XEAuto ].
  49       Qed.
  50
  51 (* main *********************************************************************)
  52
  53       Hints Resolve pr2_free_free pr2_free_delta pr2_delta_delta : ltlc.
  54
  55 (*#* #caption "confluence with itself: Church-Rosser property" *)
  56 (*#* #cap #cap c, t0, t1, t2, t *)
  57
  58       Theorem pr2_confluence: (c,t0,t1:?) (pr2 c t0 t1) ->
  59                               (t2:?) (pr2 c t0 t2) ->
  60                               (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
  61       Intros; Inversion H; Inversion H0; XDEAuto 3.
  62       Qed.
  63
  64    End pr2_confluence.
  65
  66       Tactic Definition Pr2Confluence :=
  67          Match Context With
  68             | [ H1: (pr2 ?1 ?2 ?3); H2: (pr2 ?1 ?2 ?4) |-? ] ->
  69                LApply (pr2_confluence ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
  70                LApply (H1 ?4); [ Clear H1 H2; Intros H1 | XAuto ];
  71                XElim H1; Intros
  72             | _ -> Pr0Confluence.
  73
  74 (*#* #single *)