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

   1 (*#* #stop file *)
   2
   3 Require pr0_confluence.
   4 Require pr1_defs.
   5
   6 (*#* #caption "main properties of predicate \\texttt{pr1}" *)
   7 (*#* #clauses pr1_props *)
   8
   9    Section pr1_confluence. (*************************************************)
  10
  11 (*#* #caption "confluence with single step reduction: strip lemma" *)
  12 (*#* #cap #cap t0, t1, t2, t *)
  13
  14       Theorem pr1_strip : (t0,t1:?) (pr1 t0 t1) -> (t2:?) (pr0 t0 t2) ->
  15                           (EX t | (pr1 t1 t) & (pr1 t2 t)).
  16       Intros until 1; XElim H; Intros.
  17 (* case 1 : pr1_r *)
  18       XEAuto.
  19 (* case 2 : pr1_u *)
  20       Pr0Confluence.
  21       LApply (H1 x); [ Clear H1 H2; Intros H1 | XAuto ].
  22       XElim H1; Intros; XEAuto.
  23       Qed.
  24
  25 (*#* #caption "confluence with itself: Church-Rosser property" *)
  26 (*#* #cap #cap t0, t1, t2, t *)
  27
  28       Theorem pr1_confluence : (t0,t1:?) (pr1 t0 t1) -> (t2:?) (pr1 t0 t2) ->
  29                                (EX t | (pr1 t1 t) & (pr1 t2 t)).
  30       Intros until 1; XElim H; Intros.
  31 (* case 1 : pr1_r *)
  32       XEAuto.
  33 (* case 2 : pr1_u *)
  34       LApply (pr1_strip t3 t5); [ Clear H2; Intros H2 | XAuto ].
  35       LApply (H2 t2); [ Clear H H2; Intros H | XAuto ].
  36       XElim H; Intros.
  37       LApply (H1 x); [ Clear H1 H2; Intros H1 | XAuto ].
  38       XElim H1; Intros; XEAuto.
  39       Qed.
  40
  41    End pr1_confluence.
  42
  43       Tactic Definition Pr1Confluence :=
  44          Match Context With
  45             | [ H1: (pr1 ?1 ?2); H2: (pr0 ?1 ?3) |-? ] ->
  46                LApply (pr1_strip ?1 ?2); [ Clear H1; Intros H1 | XAuto ];
  47                LApply (H1 ?3); [ Clear H1 H2; Intros H1 | XAuto ];
  48                XElim H1; Intros
  49             | [ H1: (pr1 ?1 ?2); H2: (pr1 ?1 ?3) |-? ] ->
  50                LApply (pr1_confluence ?1 ?2); [ Clear H1; Intros H1 | XAuto ];
  51                LApply (H1 ?3); [ Clear H1 H2; Intros H1 | XAuto ];
  52                XElim H1; Intros
  53             | _ -> Pr0Confluence.
  54
  55 (*#* #single *)
  56