(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA                        ENS-CNRS                *)
(*              Rocquencourt                        Lyon                    *)
(*                                                                          *)
(*                                Coq V5.10                                 *)
(*                              Nov 25th 1994                               *)
(*                                                                          *)
(****************************************************************************)
(*                               Confluence.v                               *)
(*                                                                          *)
(*                                Gerard Huet                               *)
(*                                                                          *)
(* Developed in V5.8  January 1993                                          *)
(* Ported    to V5.10 January 1995                                          *)
(****************************************************************************)

Require Import Arith.
Require Import Terms.
Require Import Reduction.
Require Import Redexes.
Require Import Test.
Require Import Marks.
Require Import Substitution.
Require Import Residuals.
Require Import Simulation.
Require Import Cube.

(* Confluence *)

Definition confluence (A : Set) (R : A -> A -> Prop) :=
  forall x y : A,
  R x y -> forall z : A, R x z -> exists u : A, R y u /\ R z u.


Lemma lemma1 : confluence lambda par_red -> confluence lambda red.
Proof.
(* Goal: forall _ : confluence lambda par_red, confluence lambda red *)
unfold all, confluence in |- *; intros.
(* Goal: @ex lambda (fun u : lambda => and (red y u) (red z u)) *)
cut (exists u : lambda, par_red y u /\ par_red z u).
(* Goal: forall _ : @ex lambda (fun u : lambda => and (par_red y u) (par_red z u)), @ex lambda (fun u : lambda => and (red y u) (red z u)) *)
(* Goal: @ex lambda (fun u : lambda => and (par_red y u) (par_red z u)) *)
simple induction 1.
intros u C; exists u; elim C; intros; split; apply par_red_red;
 trivial with arith.
(* Goal: @ex lambda (fun u : lambda => and (par_red y u) (par_red z u)) *)
apply H with x; apply red_par_red; trivial with arith.
Qed.


(* Strip lemmas *)

Definition strip :=
  forall x y : lambda,
  par_red x y ->
  forall z : lambda,
  par_red1 x z -> exists u : lambda, par_red1 y u /\ par_red z u.

Lemma strip_lemma_r : confluence lambda par_red1 -> strip.
Proof.
(* Goal: forall _ : confluence lambda par_red1, strip *)
unfold strip in |- *; simple induction 2; intros.
(* Goal: @ex lambda (fun u : lambda => and (par_red1 N u) (par_red z u)) *)
(* Goal: @ex lambda (fun u : lambda => and (par_red1 P u) (par_red z u)) *)
elim H with M N z; trivial with arith.
(* Goal: forall (x : lambda) (_ : and (par_red1 z x) (par_red N x)), @ex lambda (fun u : lambda => and (par_red N u) (par_red z u)) *)
(* Goal: @ex lambda (fun u : lambda => and (par_red P u) (par_red z u)) *)
intros u C; exists u; elim C; intros; split; trivial with arith.
(* Goal: par_red z u *)
(* Goal: @ex lambda (fun u : lambda => and (par_red P u) (par_red z u)) *)
apply one_step_par_red; trivial with arith.
(* Goal: @ex lambda (fun u : lambda => and (par_red P u) (par_red z u)) *)
elim (H2 z H5); intros.
(* Goal: @ex lambda (fun u : lambda => and (par_red P u) (par_red z u)) *)
elim H6; intros.
(* Goal: @ex lambda (fun u : lambda => and (par_red P u) (par_red z u)) *)
elim (H4 x0 H7); intros.
(* Goal: @ex lambda (fun u : lambda => and (par_red P u) (par_red z u)) *)
elim H9; intros.
(* Goal: @ex lambda (fun u : lambda => and (par_red P u) (par_red z u)) *)
exists x1; split; trivial with arith.
(* Goal: par_red z x1 *)
apply trans_par_red with x0; trivial with arith.
Qed.

Lemma strip_lemma_l : strip -> confluence lambda par_red.
Proof.
(* Goal: forall _ : strip, confluence lambda par_red *)
unfold confluence in |- *; simple induction 2; intros.
(* Goal: @ex lambda (fun u : lambda => and (par_red N u) (par_red z u)) *)
(* Goal: @ex lambda (fun u : lambda => and (par_red P u) (par_red z u)) *)
elim (H M z H2 N H1).
(* Goal: forall (x : lambda) (_ : and (par_red1 z x) (par_red N x)), @ex lambda (fun u : lambda => and (par_red N u) (par_red z u)) *)
(* Goal: @ex lambda (fun u : lambda => and (par_red P u) (par_red z u)) *)
intros u C; exists u; elim C; intros; split; trivial with arith.
(* Goal: par_red z u *)
(* Goal: @ex lambda (fun u : lambda => and (par_red P u) (par_red z u)) *)
apply one_step_par_red; trivial with arith.
(* Goal: @ex lambda (fun u : lambda => and (par_red P u) (par_red z u)) *)
elim (H2 z H5); intros.
(* Goal: @ex lambda (fun u : lambda => and (par_red P u) (par_red z u)) *)
elim H6; intros.
(* Goal: @ex lambda (fun u : lambda => and (par_red P u) (par_red z u)) *)
elim (H4 x0 H7); intros.
(* Goal: @ex lambda (fun u : lambda => and (par_red P u) (par_red z u)) *)
elim H9; intros.
(* Goal: @ex lambda (fun u : lambda => and (par_red P u) (par_red z u)) *)
exists x1; split; trivial with arith.
(* Goal: par_red z x1 *)
apply trans_par_red with x0; trivial with arith.
Qed.

Lemma lemma2 : confluence lambda par_red1 -> confluence lambda par_red.
Proof.
(* Goal: forall _ : confluence lambda par_red1, confluence lambda par_red *)
intro C; unfold confluence in |- *; intros.
(* Goal: @ex lambda (fun u : lambda => and (par_red y u) (par_red z u)) *)
apply (strip_lemma_l (strip_lemma_r C) x); trivial with arith.
Qed.

(***************************************)
(* Parallel moves lemma and confluence *)
(***************************************)

Lemma parallel_moves : confluence lambda par_red1.
Proof.
(* Goal: confluence lambda par_red1 *)
red in |- *; intros M N R1 P R2.
(* Goal: @ex lambda (fun u : lambda => and (par_red1 N u) (par_red1 P u)) *)
elim (simulation M N); trivial with arith.
(* Goal: forall (x : redexes) (_ : residuals (mark M) x (mark N)), @ex lambda (fun u : lambda => and (par_red1 N u) (par_red1 P u)) *)
elim (simulation M P); trivial with arith.
(* Goal: forall (x : redexes) (_ : residuals (mark M) x (mark P)) (x0 : redexes) (_ : residuals (mark M) x0 (mark N)), @ex lambda (fun u : lambda => and (par_red1 N u) (par_red1 P u)) *)
intros V RV U RU.  
(* Goal: @ex lambda (fun u : lambda => and (par_red1 N u) (par_red1 P u)) *)
elim (paving U V (mark M) (mark N) (mark P)); trivial with arith.
(* Goal: forall (x : redexes) (_ : @ex redexes (fun VU : redexes => @ex redexes (fun WUV : redexes => and (residuals (mark N) VU WUV) (residuals (mark P) x WUV)))), @ex lambda (fun u : lambda => and (par_red1 N u) (par_red1 P u)) *)
intros UV C1; elim C1.
(* Goal: forall (x : redexes) (_ : @ex redexes (fun WUV : redexes => and (residuals (mark N) x WUV) (residuals (mark P) UV WUV))), @ex lambda (fun u : lambda => and (par_red1 N u) (par_red1 P u)) *)
intros VU C2; elim C2.
(* Goal: forall (x : redexes) (_ : and (residuals (mark N) VU x) (residuals (mark P) UV x)), @ex lambda (fun u : lambda => and (par_red1 N u) (par_red1 P u)) *)
intros UVW C3; elim C3; intros P1 P2.
(* Goal: @ex lambda (fun u : lambda => and (par_red1 N u) (par_red1 P u)) *)
exists (unmark UVW); split.
(* Goal: par_red1 N (unmark UVW) *)
(* Goal: par_red1 P (unmark UVW) *)
rewrite (inverse N).
(* Goal: par_red1 (unmark (mark N)) (unmark UVW) *)
(* Goal: par_red1 P (unmark UVW) *)
apply Simulation.completeness with VU; trivial with arith.
(* Goal: par_red1 P (unmark UVW) *)
rewrite (inverse P).
(* Goal: par_red1 (unmark (mark P)) (unmark UVW) *)
apply Simulation.completeness with UV; trivial with arith.
Qed.

Lemma confluence_parallel_reduction : confluence lambda par_red.
Proof.
(* Goal: confluence lambda par_red *)
apply lemma2; exact parallel_moves.
Qed.

Theorem confluence_beta_reduction : confluence lambda red.
Proof.
(* Goal: confluence lambda red *)
apply lemma1; exact confluence_parallel_reduction.
Qed.