Require Import List.
Require Import Arith.
Require Import Wf_nat.
Require Import Relations.

Require Import MatchCompNat.
Require Import Util.


Require Syntax.
Module SetProgram(My_Program: Syntax.Program).
Import My_Program.

Require Auxiliary_proofs.
Module My_Auxiliary_proofs := Auxiliary_proofs.SetProgram(My_Program).
Import My_Auxiliary_proofs.

Import My_Substitutions_proofs.
Import My_Binders_proofs.
Import My_Semantics.
Import My_WellFormedness.
Import My_Typing.
Import My_Auxiliary.
Import My_Substitutions.
Import My_Binders.

Inductive RedTypePar: TypeS -> TypeS -> Prop :=

  

  | RTP_class:
    forall (C: ClassSym),
      (RedTypePar (Type_class C) (Type_class C))

  | RTP_var:
    forall (X: TypeVar),
      (RedTypePar (Type_var X) (Type_var X))

  | RTP_none:
    (RedTypePar Type_none Type_none)

  | RTP_nil:
    (RedTypePar Type_nil Type_nil)

  

  | RTP_proj_sub:
    forall (R R': TypeS) (i: nat),
      (RedTypePar R R') ->
      (RedTypePar (Type_proj R i) (Type_proj R' i))

  | RTP_proj_redex:
    forall (Ks Ks' Ki: TypeS) (i: nat),
      (RedTypePar Ks Ks') ->
      (TypeS_at Ks' i Ki ) ->
      (RedTypePar (Type_proj (Type_tuple Ks) i) Ki)

  | RTP_fun_left_right:
    forall (Pi Pi' T T': TypeS),
      (RedTypePar Pi Pi') ->
      (RedTypePar T T') ->
      (RedTypePar (Type_fun Pi T) (Type_fun Pi' T'))

  

  | RTP_apply_redex:
    forall (Pi Pi' T T' R R': TypeS),
      (RedTypePar Pi Pi') ->
      (RedTypePar T T') ->
      (RedTypePar R R') ->
      (RedTypePar (Type_apply (Type_fun Pi T) R) (typeSubst_in_type T' 0 R'))

  | RTP_apply_left_right:
    forall (K K': TypeS) (R R': TypeS),
      (RedTypePar K K') ->
      (RedTypePar R R') ->
      (RedTypePar (Type_apply K R) (Type_apply K' R'))

  

  | RTP_tuple:
    forall (Ks Ks': TypeS),
    (RedTypePar Ks Ks') ->
    (RedTypePar (Type_tuple Ks) (Type_tuple Ks'))

  

  | RTP_param_left_right:
    forall (Pi Pi' T T': TypeS),
      (RedTypePar Pi Pi') ->
      (RedTypePar T T') ->
      (RedTypePar (Type_param Pi T) (Type_param Pi' T'))

  

  | RTP_section:
    forall (Ps Ps': TypeS),
      (RedTypePar Ps Ps') ->
      (RedTypePar (Type_section Ps) (Type_section Ps'))

  

  | RTP_some:
    forall (T T': TypeS),
    (RedTypePar T T') ->
    (RedTypePar (Type_some T) (Type_some T'))

  

  | RTP_cons_head_tail:
    forall (t t' ts ts': TypeS),
      (RedTypePar t t') ->
      (RedTypePar ts ts') ->
      (RedTypePar (Type_cons t ts) (Type_cons t' ts'))
.

Lemma RTP_refl:
  forall (t: TypeS),
    (RedTypePar t t)
.

Lemma RedType_included_in_RedTypePar:
  forall (t t': TypeS),
    (RedType t t') ->
    (RedTypePar t t')
.

Lemma Parallel_reduction_in_lifting:
  forall (t t': TypeS) (n: nat),
    (RedTypePar t t') ->
    forall (k: nat),
      (RedTypePar (lift_at_depth_in_type t n k) (lift_at_depth_in_type t' n k))
.

Lemma Reduction_and_substitution_par:
  forall (t t' R R': TypeS) (k: nat),
    (RedTypePar t t') ->
    (RedTypePar R R') ->
    (RedTypePar (typeSubst_in_type t k R) (typeSubst_in_type t' k R'))
.

Lemma RedTypePar_included_in_RedTypeStar:
  forall (t t': TypeS),
    (RedTypePar t t') ->
    (RedTypeStar t t')
.

Lemma Parallel_reduction_and_list_lookup:
  forall (ts: TypeS) (i: nat) (t: TypeS),
    (TypeS_at ts i t) ->
    forall (ts': TypeS),
      (RedTypePar ts ts') ->
      exists t': TypeS,
        (TypeS_at ts' i t') /\
        (RedTypePar t t')
.

Fixpoint size (t: TypeS): nat :=
  match t with
    | (Type_proj R i) => 1 + (size R)
    | (Type_class C) => 1
    | (Type_fun Pi T) => 1 + ((size Pi) + (size T))
    | (Type_apply K R) => 1 + ((size K) + (size R))
    | (Type_var X) => 1
    | (Type_tuple Ks) => 1 + (size Ks)
    | (Type_param Pi T) => 1 + ((size Pi) + (size T))
    | (Type_section Ps) => 1 + (size Ps)
    | (Type_none) => 1
    | (Type_some T) => 1 + (size T)
    | (Type_nil) => 1
    | (Type_cons u us) => 1 + ((size u) + (size us))
  end
.

Lemma Parallel_reduction_is_confluent:
  forall (t u1 u2: TypeS),
    (RedTypePar t u1) ->
    (RedTypePar t u2) ->
    exists s: TypeS,
      (RedTypePar u1 s) /\
      (RedTypePar u2 s)
.


























































Definition SubRelation (A: Set) (R1 R2: A -> A -> Prop): Prop :=
  forall (x y: A), (R1 x y) -> (R2 x y)
.

Lemma Transitive_closure_preserves_inclusion:
  forall (A: Set) (R1 R2: A -> A -> Prop),
    (SubRelation _ R1 R2) ->
    (SubRelation _ (clos_trans _ R1) (clos_trans _ R2))
.





Definition DiamondProperty (A: Set) (R: A -> A -> Prop): Prop :=
  forall (x y1 y2: A), (R x y1) -> (R x y2) ->
    exists z: A, (R y1 z) /\ (R y2 z)
.

Definition DiamondProperty_aux (A: Set) (R: A -> A -> Prop): Prop :=
  forall (x y1 y2: A), (clos_trans _ R x y1) -> (R x y2) ->
    exists z: A, (R y1 z) /\ (clos_trans _ R y2 z)
.

Lemma Transitive_closure_preserves_diamond_property_aux:
  forall (A: Set) (R: A -> A -> Prop),
    (DiamondProperty _ R) ->
    (DiamondProperty_aux _ R)
.







Lemma Transitive_closure_preserves_diamond_property:
  forall (A: Set) (R: A -> A -> Prop),
    (DiamondProperty _ R) ->
    (DiamondProperty _ (clos_trans _ R))
.






Lemma Equality_preserves_diamond_property:
  forall (A: Set) (R1 R2: A -> A -> Prop),
    (DiamondProperty _ R1) ->
    (SubRelation _ R1 R2) ->
    (SubRelation _ R2 R1) ->
    (DiamondProperty _ R2)
.

Definition RedTypeParTrans: TypeS -> TypeS -> Prop :=
  (clos_trans _ RedTypePar).

Lemma RedTypeParTrans_has_diamond_property:
  (DiamondProperty _ RedTypeParTrans)
.


Lemma RedTypeStar_included_in_RedTypeParTrans:
  forall (t t': TypeS),
    (RedTypeStar t t') ->
    (RedTypeParTrans t t')
.





Lemma RedTypeParTrans_included_in_RedTypeStar:
  forall (t t': TypeS),
    (RedTypeParTrans t t') ->
    (RedTypeStar t t')
.

Theorem Type_reduction_is_confluent:
  forall (t u1 u2: TypeS),
    (RedTypeStar t u1) ->
    (RedTypeStar t u2) ->
    exists s: TypeS,
      (RedTypeStar u1 s) /\
      (RedTypeStar u2 s)
.



End SetProgram.