(* 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                               *)
(*                                                                          *)
(****************************************************************************)
(*                                Redexes.v                                 *)
(*                                                                          *)
(*                                Gerard Huet                               *)
(*                                                                          *)
(* Developed in V5.8  January 1993                                          *)
(* Ported    to V5.10 January 1995                                          *)
(****************************************************************************)

Require Import Arith.
Require Import Test.
Require Import Terms.
Require Import Reduction.

(************************************)
(* Lambda terms with marked redexes *)
(************************************)

Inductive redexes : Set :=
  | Var : nat -> redexes
  | Fun : redexes -> redexes
  | Ap : bool -> redexes -> redexes -> redexes.

(* A redex is marked as (Ap true (Fun M) N) *)

(* The Boolean algebra of sets of redexes *)

Inductive sub : redexes -> redexes -> Prop :=
  | Sub_Var : forall n : nat, sub (Var n) (Var n)
  | Sub_Fun : forall U V : redexes, sub U V -> sub (Fun U) (Fun V)
  | Sub_Ap1 :
      forall U1 V1 : redexes,
      sub U1 V1 ->
      forall U2 V2 : redexes,
      sub U2 V2 -> forall b : bool, sub (Ap false U1 U2) (Ap b V1 V2)
  | Sub_Ap2 :
      forall U1 V1 : redexes,
      sub U1 V1 ->
      forall U2 V2 : redexes,
      sub U2 V2 -> forall b : bool, sub (Ap true U1 U2) (Ap true V1 V2).

Definition bool_max (b b' : bool) :=
  match b return bool with
  | true => true
  | false => b'
  end.

Lemma max_false : forall b : bool, bool_max b false = b.
Proof.
(* Goal: forall b : bool, @eq bool (bool_max b false) b *)
simple induction b; simpl in |- *; trivial.
Qed.

Inductive union : redexes -> redexes -> redexes -> Prop :=
  | Union_Var : forall n : nat, union (Var n) (Var n) (Var n)
  | Union_Fun :
      forall U V W : redexes, union U V W -> union (Fun U) (Fun V) (Fun W)
  | Union_Ap :
      forall U1 V1 W1 : redexes,
      union U1 V1 W1 ->
      forall U2 V2 W2 : redexes,
      union U2 V2 W2 ->
      forall b1 b2 : bool,
      union (Ap b1 U1 U2) (Ap b2 V1 V2) (Ap (bool_max b1 b2) W1 W2).

Lemma union_l : forall U V W : redexes, union U V W -> sub U W.
Proof.
(* Goal: forall (U V W : redexes) (_ : union U V W), union V U W *)
simple induction 1; intros.
(* Goal: sub (Var n) (Var n) *)
(* Goal: sub (Fun V0) (Fun W0) *)
(* Goal: sub (Ap b2 V1 V2) (Ap (bool_max b1 b2) W1 W2) *)
apply Sub_Var.
(* Goal: sub (Fun V0) (Fun W0) *)
(* Goal: sub (Ap b2 V1 V2) (Ap (bool_max b1 b2) W1 W2) *)
apply Sub_Fun; trivial.
(* Goal: sub (Ap b1 U1 U2) (Ap (bool_max b1 b2) W1 W2) *)
elim b1.
(* Goal: sub (Ap true U1 U2) (Ap (bool_max true b2) W1 W2) *)
(* Goal: sub (Ap false U1 U2) (Ap (bool_max false b2) W1 W2) *)
elim b2; simpl in |- *; apply Sub_Ap2; trivial.
(* Goal: sub (Ap false U1 U2) (Ap (bool_max false b2) W1 W2) *)
elim b2; simpl in |- *; apply Sub_Ap1; trivial.
Qed.

Lemma union_r : forall U V W : redexes, union U V W -> sub V W.
Proof.
(* Goal: forall (U V W : redexes) (_ : union U V W), union V U W *)
simple induction 1; intros.
(* Goal: sub (Var n) (Var n) *)
(* Goal: sub (Fun V0) (Fun W0) *)
(* Goal: sub (Ap b2 V1 V2) (Ap (bool_max b1 b2) W1 W2) *)
apply Sub_Var.
(* Goal: sub (Fun V0) (Fun W0) *)
(* Goal: sub (Ap b2 V1 V2) (Ap (bool_max b1 b2) W1 W2) *)
apply Sub_Fun; trivial.
(* Goal: sub (Ap b2 V1 V2) (Ap (bool_max b1 b2) W1 W2) *)
elim b2.
(* Goal: sub (Ap true V1 V2) (Ap (bool_max b1 true) W1 W2) *)
(* Goal: sub (Ap false V1 V2) (Ap (bool_max b1 false) W1 W2) *)
elim b1; simpl in |- *; apply Sub_Ap2; trivial.
(* Goal: sub (Ap false V1 V2) (Ap (bool_max b1 false) W1 W2) *)
elim b1; simpl in |- *; apply Sub_Ap1; trivial.
Qed.

Lemma bool_max_Sym : forall b b' : bool, bool_max b b' = bool_max b' b.
Proof.
(* Goal: forall b b' : bool, @eq bool (bool_max b b') (bool_max b' b) *)
simple induction b; simple induction b'; simpl in |- *; trivial.
Qed.

Lemma union_sym : forall U V W : redexes, union U V W -> union V U W.
Proof.
(* Goal: forall (U V W : redexes) (_ : union U V W), union V U W *)
simple induction 1; intros.
(* Goal: union (Var n) (Var n) (Var n) *)
(* Goal: union (Fun V0) (Fun U0) (Fun W0) *)
(* Goal: union (Ap b2 V1 V2) (Ap b1 U1 U2) (Ap (bool_max b1 b2) W1 W2) *)
apply Union_Var; trivial.
(* Goal: union (Fun V0) (Fun U0) (Fun W0) *)
(* Goal: union (Ap b2 V1 V2) (Ap b1 U1 U2) (Ap (bool_max b1 b2) W1 W2) *)
apply Union_Fun; trivial.
(* Goal: union (Ap b2 V1 V2) (Ap b1 U1 U2) (Ap (bool_max b1 b2) W1 W2) *)
rewrite (bool_max_Sym b1 b2); apply Union_Ap; trivial.
Qed.

(* Compatibility *)
(* (comp U V) iff (unmark U)=(unmark V) *)

Inductive comp : redexes -> redexes -> Prop :=
  | Comp_Var : forall n : nat, comp (Var n) (Var n)
  | Comp_Fun : forall U V : redexes, comp U V -> comp (Fun U) (Fun V)
  | Comp_Ap :
      forall U1 V1 : redexes,
      comp U1 V1 ->
      forall U2 V2 : redexes,
      comp U2 V2 -> forall b1 b2 : bool, comp (Ap b1 U1 U2) (Ap b2 V1 V2).

Hint Resolve Comp_Var Comp_Fun Comp_Ap.

Lemma comp_refl : forall U : redexes, comp U U.
Proof.
(* Goal: forall U : redexes, comp U U *)
simple induction U; auto.
Qed.

Lemma comp_sym : forall U V : redexes, comp U V -> comp V U.
Proof.
(* Goal: forall (U V : redexes) (_ : comp U V), comp V U *)
simple induction 1; auto.
Qed.

Lemma comp_trans :
 forall U V : redexes,
 comp U V -> forall (W : redexes) (CVW : comp V W), comp U W.
(* Goal: forall (U V : redexes) (_ : comp U V) (W : redexes) (_ : comp V W), comp U W *)
simple induction 1; intros; inversion_clear CVW; auto.
Qed.

Lemma union_defined :
 forall U V : redexes, comp U V -> exists W : redexes, union U V W.
Proof.
(* Goal: forall (_ : and (regular U1) (regular U2)) (_ : match V1 with | Var n => False | Fun r => and (regular V1) (regular V2) | Ap b r r0 => False end), match W1 with | Var n => False | Fun r => and (regular W1) (regular W2) | Ap b r r0 => False end *)
(* Goal: forall (_ : and (regular U1) (regular U2)) (_ : and (regular V1) (regular V2)), and (regular W1) (regular W2) *)
simple induction 1.
(* Goal: forall n : nat, @ex redexes (fun W : redexes => union (Var n) (Var n) W) *)
(* Goal: forall (U V : redexes) (_ : comp U V) (_ : @ex redexes (fun W : redexes => union U V W)), @ex redexes (fun W : redexes => union (Fun U) (Fun V) W) *)
(* Goal: forall (U1 V1 : redexes) (_ : comp U1 V1) (_ : @ex redexes (fun W : redexes => union U1 V1 W)) (U2 V2 : redexes) (_ : comp U2 V2) (_ : @ex redexes (fun W : redexes => union U2 V2 W)) (b1 b2 : bool), @ex redexes (fun W : redexes => union (Ap b1 U1 U2) (Ap b2 V1 V2) W) *)
intro n; exists (Var n); apply Union_Var.
(* Goal: union (Fun V0) (Fun U0) (Fun W0) *)
(* Goal: union (Ap b2 V1 V2) (Ap b1 U1 U2) (Ap (bool_max b1 b2) W1 W2) *)
simple induction 2; intros W0 H2; exists (Fun W0); apply Union_Fun; trivial.
(* Goal: forall (U1 V1 : redexes) (_ : comp U1 V1) (_ : @ex redexes (fun W : redexes => union U1 V1 W)) (U2 V2 : redexes) (_ : comp U2 V2) (_ : @ex redexes (fun W : redexes => union U2 V2 W)) (b1 b2 : bool), @ex redexes (fun W : redexes => union (Ap b1 U1 U2) (Ap b2 V1 V2) W) *)
intros U1 V1 H1 E1 U2 V2 H2 E2; elim E1; elim E2.
(* Goal: forall (x : redexes) (_ : union U2 V2 x) (x0 : redexes) (_ : union U1 V1 x0) (b1 b2 : bool), @ex redexes (fun W : redexes => union (Ap b1 U1 U2) (Ap b2 V1 V2) W) *)
intros W2 A W1 B b1 b2; exists (Ap (bool_max b1 b2) W1 W2). 
(* Goal: union (Ap b1 U1 U2) (Ap b2 V1 V2) (Ap (bool_max b1 b2) W1 W2) *)
apply Union_Ap; trivial.
Qed.


(* A element of type redexes is said to be regular if its true marks label
   redexes *)


Fixpoint regular (U : redexes) : Prop :=
  match U with
  | Var n => True
  | Fun V => regular V
  | Ap true (Fun _ as V) W => regular V /\ regular W
  | Ap true _ W => False
  | Ap false V W => regular V /\ regular W
  end.

Lemma union_preserve_regular :
 forall U V W : redexes, union U V W -> regular U -> regular V -> regular W.
Proof.
(* Goal: forall (U V W : redexes) (_ : union U V W) (_ : regular U) (_ : regular V), regular W *)
simple induction 1; simpl in |- *; trivial.
(* Goal: forall (U1 V1 W1 : redexes) (_ : union U1 V1 W1) (_ : forall (_ : regular U1) (_ : regular V1), regular W1) (U2 V2 W2 : redexes) (_ : union U2 V2 W2) (_ : forall (_ : regular U2) (_ : regular V2), regular W2) (b1 b2 : bool) (_ : if b1 then match U1 with | Var n => False | Fun r => and (regular U1) (regular U2) | Ap b r r0 => False end else and (regular U1) (regular U2)) (_ : if b2 then match V1 with | Var n => False | Fun r => and (regular V1) (regular V2) | Ap b r r0 => False end else and (regular V1) (regular V2)), if bool_max b1 b2 then match W1 with | Var n => False | Fun r => and (regular W1) (regular W2) | Ap b r r0 => False end else and (regular W1) (regular W2) *)
simple induction b1; simple induction b2; simpl in |- *.
(* Goal: forall (_ : regular U1) (_ : regular U2) (_ : match V1 with | Var n => False | Fun r => and (regular V1) (regular V2) | Ap b r r0 => False end), match W1 with | Var n => False | Fun r => and (regular W1) (regular W2) | Ap b r r0 => False end *)
(* Goal: forall (_ : and (regular U1) (regular U2)) (_ : and (regular V1) (regular V2)), and (regular W1) (regular W2) *)
generalize H1.
(* Goal: forall (_ : forall (_ : regular U1) (_ : regular V1), regular W1) (_ : regular U1) (_ : regular U2) (_ : match V1 with | Var n => False | Fun r => and (regular V1) (regular V2) | Ap b r r0 => False end), match W1 with | Var n => False | Fun r => and (regular W1) (regular W2) | Ap b r r0 => False end *)
(* Goal: forall (_ : and (regular U1) (regular U2)) (_ : and (regular V1) (regular V2)), and (regular W1) (regular W2) *)
elim H0; try contradiction.
(* Goal: forall (U V W : redexes) (_ : union U V W) (_ : forall (_ : forall (_ : regular U) (_ : regular V), regular W) (_ : match U with | Var n => False | Fun r => and (regular U) (regular U2) | Ap b r r0 => False end) (_ : and (regular V) (regular V2)), match W with | Var n => False | Fun r => and (regular W) (regular W2) | Ap b r r0 => False end) (_ : forall (_ : regular (Fun U)) (_ : regular (Fun V)), regular (Fun W)) (_ : and (regular (Fun U)) (regular U2)) (_ : and (regular (Fun V)) (regular V2)), and (regular (Fun W)) (regular W2) *)
(* Goal: forall (_ : and (regular U1) (regular U2)) (_ : match V1 with | Var n => False | Fun r => and (regular V1) (regular V2) | Ap b r r0 => False end), match W1 with | Var n => False | Fun r => and (regular W1) (regular W2) | Ap b r r0 => False end *)
(* Goal: forall (_ : and (regular U1) (regular U2)) (_ : and (regular V1) (regular V2)), and (regular W1) (regular W2) *)
intros; elim H7; elim H8; auto.
(* Goal: forall (_ : regular U1) (_ : regular U2) (_ : match V1 with | Var n => False | Fun r => and (regular V1) (regular V2) | Ap b r r0 => False end), match W1 with | Var n => False | Fun r => and (regular W1) (regular W2) | Ap b r r0 => False end *)
(* Goal: forall (_ : and (regular U1) (regular U2)) (_ : and (regular V1) (regular V2)), and (regular W1) (regular W2) *)
generalize H1.
(* Goal: forall (_ : forall (_ : regular U1) (_ : regular V1), regular W1) (_ : regular U1) (_ : regular U2) (_ : match V1 with | Var n => False | Fun r => and (regular V1) (regular V2) | Ap b r r0 => False end), match W1 with | Var n => False | Fun r => and (regular W1) (regular W2) | Ap b r r0 => False end *)
(* Goal: forall (_ : and (regular U1) (regular U2)) (_ : and (regular V1) (regular V2)), and (regular W1) (regular W2) *)
elim H0; try contradiction.
(* Goal: forall (U V W : redexes) (_ : union U V W) (_ : forall (_ : forall (_ : regular U) (_ : regular V), regular W) (_ : match U with | Var n => False | Fun r => and (regular U) (regular U2) | Ap b r r0 => False end) (_ : and (regular V) (regular V2)), match W with | Var n => False | Fun r => and (regular W) (regular W2) | Ap b r r0 => False end) (_ : forall (_ : regular (Fun U)) (_ : regular (Fun V)), regular (Fun W)) (_ : and (regular (Fun U)) (regular U2)) (_ : and (regular (Fun V)) (regular V2)), and (regular (Fun W)) (regular W2) *)
(* Goal: forall (_ : and (regular U1) (regular U2)) (_ : match V1 with | Var n => False | Fun r => and (regular V1) (regular V2) | Ap b r r0 => False end), match W1 with | Var n => False | Fun r => and (regular W1) (regular W2) | Ap b r r0 => False end *)
(* Goal: forall (_ : and (regular U1) (regular U2)) (_ : and (regular V1) (regular V2)), and (regular W1) (regular W2) *)
intros; elim H7; elim H8; auto.
(* Goal: forall (_ : and (regular U1) (regular U2)) (_ : match V1 with | Var n => False | Fun r => and (regular V1) (regular V2) | Ap b r r0 => False end), match W1 with | Var n => False | Fun r => and (regular W1) (regular W2) | Ap b r r0 => False end *)
(* Goal: forall (_ : and (regular U1) (regular U2)) (_ : and (regular V1) (regular V2)), and (regular W1) (regular W2) *)
simple induction 1.
(* Goal: forall (_ : regular U1) (_ : regular U2) (_ : match V1 with | Var n => False | Fun r => and (regular V1) (regular V2) | Ap b r r0 => False end), match W1 with | Var n => False | Fun r => and (regular W1) (regular W2) | Ap b r r0 => False end *)
(* Goal: forall (_ : and (regular U1) (regular U2)) (_ : and (regular V1) (regular V2)), and (regular W1) (regular W2) *)
generalize H1.
(* Goal: forall (_ : forall (_ : regular U1) (_ : regular V1), regular W1) (_ : regular U1) (_ : regular U2) (_ : match V1 with | Var n => False | Fun r => and (regular V1) (regular V2) | Ap b r r0 => False end), match W1 with | Var n => False | Fun r => and (regular W1) (regular W2) | Ap b r r0 => False end *)
(* Goal: forall (_ : and (regular U1) (regular U2)) (_ : and (regular V1) (regular V2)), and (regular W1) (regular W2) *)
elim H0; try contradiction.
(* Goal: forall (U V W : redexes) (_ : union U V W) (_ : forall (_ : forall (_ : regular U) (_ : regular V), regular W) (_ : regular U) (_ : regular U2) (_ : match V with | Var n => False | Fun r => and (regular V) (regular V2) | Ap b r r0 => False end), match W with | Var n => False | Fun r => and (regular W) (regular W2) | Ap b r r0 => False end) (_ : forall (_ : regular (Fun U)) (_ : regular (Fun V)), regular (Fun W)) (_ : regular (Fun U)) (_ : regular U2) (_ : and (regular (Fun V)) (regular V2)), and (regular (Fun W)) (regular W2) *)
(* Goal: forall (_ : and (regular U1) (regular U2)) (_ : and (regular V1) (regular V2)), and (regular W1) (regular W2) *)
intros; elim H10; auto.
(* Goal: forall (U V : redexes) (_ : comp U V), comp V U *)
simple induction 1; intros O1 O2; simple induction 1; auto.
Qed.





