Confluence.v

Section Props_Confluence.

  Variable R,R': red_rule.

  Hypothesis same_rel: (e:env)(same_relation term (R e) (R' e)).
  Hypothesis R_confl: (confluent R).

  Lemma confluent_is_ext: (confluent R').
Unfold confluent commut transp.
Intros.
Elim same_rel with e.
(Unfold inclusion ; Intros).
(Elim R_confl with e x y z; Auto with arith pts; Intros).
(Exists x0; Auto with arith pts).
Save.

  Lemma strip_confl: (e:env)(commut term (R_rt R e) (transp term (R e))).
Unfold commut transp .
(Induction 1; Intros).
(Elim R_confl with e y0 x0 z; Intros; Auto with arith pts).
(Exists x1; Auto with arith pts).

(Exists z; Auto with arith pts).

(Elim H1 with z0; Intros; Auto with arith pts).
(Elim H3 with x1; Intros; Auto with arith pts).
(Exists x2; Auto with arith pts).
Red.
(Apply rt_trans with x1; Auto with arith pts).
Save.

  Lemma strongly_confluent: (confluent (R_rt R)).
Unfold confluent commut transp .
(Induction 1; Intros).
(Elim strip_confl with e z x0 y0; Intros; Auto with arith pts).
(Exists x1; Auto with arith pts).

(Exists z; Auto with arith pts).

(Elim H1 with z0; Intros; Auto with arith pts).
(Elim H3 with x1; Intros; Auto with arith pts).
(Exists x2; Auto with arith pts).
Red.
(Apply rt_trans with x1; Auto with arith pts).
Save.

End Props_Confluence.

Section Tait_Martin_Lof.

  Variable R,R': red_rule.

  Hypothesis R'_confl: (confluent R').
  Hypothesis incl_R_R': (e:env)(inclusion term (R e) (R' e)).
  Hypothesis incl_R'_R_rt: (e:env)(inclusion term (R' e) (R_rt R e)).

  Lemma closures_are_equal: (e:env)(same_relation term (R_rt R' e) (R_rt R e)).
Unfold same_relation inclusion R_rt .
Split.
(Induction 1; Intros; Auto with arith pts).
(Apply (incl_R'_R_rt e x0 y0); Auto with arith pts).

(Apply rt_trans with y0; Auto with arith pts).

(Induction 1; Intros; Auto with arith pts).
Apply rt_step.
(Apply (incl_R_R' e x0 y0); Auto with arith pts).

(Apply rt_trans with y0; Auto with arith pts).
Save.

  Lemma confl_closure: (confluent (R_rt R)).
Apply confluent_is_ext with (R_rt R').
Exact closures_are_equal.

Apply strongly_confluent.
Trivial with arith pts.
Save.

  Lemma TML_Church_rosser: (church_rosser R).
Unfold church_rosser R_rt .
(Induction 1; Intros).
(Exists y; Auto with arith pts).

(Exists x; Auto with arith pts).

(Elim H1; Intros).
(Exists x0; Auto with arith pts).

(Elim H1; Intros).
(Elim H3; Intros).
(Elim confl_closure with e x0 y x1; Intros; Auto with arith pts).
Exists x2.
(Apply rt_trans with x0; Auto with arith pts).

(Apply rt_trans with x1; Auto with arith pts).
Save.

End Tait_Martin_Lof.

23/12/98, 14:29