Library Lambda.TPOSR.Conv


Require
 Import
 Lambda.TPOSR.Terms.

Require
 Import
 Lambda.TPOSR.LiftSubst.

Require
 Import
 Lambda.TPOSR.Reduction.




Implicit
 Types
 i
 k
 m
 n
 p
 : nat.

Implicit
 Type
 s
 : sort.

Implicit
 Types
 A
 B
 M
 N
 T
 t
 u
 v
 : lterm.




Section
 Church_Rosser.




  Definition
 str_confluent (R
 : lterm → lterm → Prop
) :=

    commut _
 R
 (transp _
 R
).




  Lemma
 str_confluence_par_lred1 : str_confluent par_lred1.




  Lemma
 strip_lemma : commut _
 par_lred (transp _
 par_lred1).




  Lemma
 confluence_par_lred : str_confluent par_lred.




  Lemma
 confluence_lred : str_confluent lred.




  Theorem
 church_rosser :

   ∀ u
 v
, conv u
 v
 → ex2 (fun
 t
 ⇒ lred u
 t
) (fun
 t
 ⇒ lred v
 t
).




  Lemma
 inv_conv_prod_l :

   ∀ a
 b
 c
 d
 : lterm, conv (Prod_l a
 c
) (Prod_l b
 d
) → conv a
 b
.




  Lemma
 inv_conv_prod_r :

   ∀ a
 b
 c
 d
 : lterm, conv (Prod_l a
 c
) (Prod_l b
 d
) → conv c
 d
.




  Lemma
 inv_conv_sum_l :

   ∀ a
 b
 c
 d
 : lterm, conv (Sum_l a
 c
) (Sum_l b
 d
) → conv a
 b
.




Lemma
 inv_conv_sum_r :

   ∀ a
 b
 c
 d
 : lterm, conv (Sum_l a
 c
) (Sum_l b
 d
) → conv c
 d
.




Lemma
 inv_conv_subset_l :

   ∀ a
 b
 c
 d
 : lterm, conv (Subset_l a
 c
) (Subset_l b
 d
) → conv a
 b
.




Lemma
 inv_conv_subset_r :

   ∀ a
 b
 c
 d
 : lterm, conv (Subset_l a
 c
) (Subset_l b
 d
) → conv c
 d
.




  Lemma
 nf_uniqueness : ∀ u
 v
, conv u
 v
 → normal u
 → normal v
 → u
 = v
.




  Lemma
 conv_sort : ∀ s1
 s2
, conv (Srt_l s1
) (Srt_l s2
) → s1
 = s2
.




  Lemma
 conv_kind_prop : ¬ conv (Srt_l kind) (Srt_l prop).




  Lemma
 conv_kind_set : ¬ conv (Srt_l kind) (Srt_l set).




Lemma
 conv_sort_ref : ∀ s
 n
, ¬ conv (Srt_l s
) (Ref_l n
).




  Lemma
 conv_sort_prod : ∀ s
 t
 u
, ¬ conv (Srt_l s
) (Prod_l t
 u
).




  Lemma
 conv_sort_sum : ∀ s
 t
 u
, ¬ conv (Srt_l s
) (Sum_l t
 u
).




  Lemma
 conv_sort_subset : ∀ s
 t
 u
, ¬ conv (Srt_l s
) (Subset_l t
 u
).




  Lemma
 conv_prod_subset : ∀ U
 V
 t
 u
, ¬ conv (Prod_l U
 V
) (Subset_l t
 u
).




  Lemma
 conv_prod_sum : ∀ U
 V
 t
 u
, ¬ conv (Prod_l U
 V
) (Sum_l t
 u
).




  Lemma
 conv_subset_sum : ∀ U
 V
 t
 u
, ¬ conv (Subset_l U
 V
) (Sum_l t
 u
).




End
 Church_Rosser.