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

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