Library Lambda.Conv


Require
 Import
 Lambda.Terms.

Require
 Import
 Lambda.LiftSubst.

Require
 Import
 Lambda.Reduction.




Implicit
 Types
 i
 k
 m
 n
 p
 : nat.

Implicit
 Type
 s
 : sort.

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




Section
 Church_Rosser.




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

    commut _
 R
 (transp _
 R
).




  Lemma
 str_confluence_par_red1 : str_confluent par_red1.




  Lemma
 strip_lemma : commut _
 par_red (transp _
 par_red1).




  Lemma
 confluence_par_red : str_confluent par_red.




  Lemma
 confluence_red : str_confluent red.




  Theorem
 church_rosser :

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




  Lemma
 inv_conv_prod_l :

   ∀ a
 b
 c
 d
 : term, conv (Prod a
 c
) (Prod b
 d
) → conv a
 b
.




  Lemma
 inv_conv_prod_r :

   ∀ a
 b
 c
 d
 : term, conv (Prod a
 c
) (Prod b
 d
) → conv c
 d
.




  Lemma
 inv_conv_sum_l :

   ∀ a
 b
 c
 d
 : term, conv (Sum a
 c
) (Sum b
 d
) → conv a
 b
.




Lemma
 inv_conv_sum_r :

   ∀ a
 b
 c
 d
 : term, conv (Sum a
 c
) (Sum b
 d
) → conv c
 d
.




Lemma
 inv_conv_subset_l :

   ∀ a
 b
 c
 d
 : term, conv (Subset a
 c
) (Subset b
 d
) → conv a
 b
.




Lemma
 inv_conv_subset_r :

   ∀ a
 b
 c
 d
 : term, conv (Subset a
 c
) (Subset 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 s1
) (Srt s2
) → s1
 = s2
.




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




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




Lemma
 conv_sort_ref : ∀ s
 n
, ¬ conv (Srt s
) (Ref n
).




  Lemma
 conv_sort_prod : ∀ s
 t
 u
, ¬ conv (Srt s
) (Prod t
 u
).




  Lemma
 conv_sort_sum : ∀ s
 t
 u
, ¬ conv (Srt s
) (Sum t
 u
).




  Lemma
 conv_sort_subset : ∀ s
 t
 u
, ¬ conv (Srt s
) (Subset t
 u
).




  Lemma
 conv_ref_prod : ∀ n
 t
 u
, ¬ conv (Ref n
) (Prod t
 u
).




  Lemma
 conv_ref_sum : ∀ n
 t
 u
, ¬ conv (Ref n
) (Sum t
 u
).




  Lemma
 conv_ref_subset : ∀ n
 t
 u
, ¬ conv (Ref n
) (Subset t
 u
).




  Lemma
 conv_prod_abs : ∀ U
 V
 t
 u
, ¬ conv (Prod U
 V
) (Abs t
 u
).




  Lemma
 conv_prod_pair : ∀ U
 V
 t
 u
 v
, ¬ conv (Prod U
 V
) (Pair t
 u
 v
).




  Lemma
 conv_prod_subset : ∀ U
 V
 t
 u
, ¬ conv (Prod U
 V
) (Subset t
 u
).




  Lemma
 conv_prod_sum : ∀ U
 V
 t
 u
, ¬ conv (Prod U
 V
) (Sum t
 u
).




  Lemma
 conv_subset_sum : ∀ U
 V
 t
 u
, ¬ conv (Subset U
 V
) (Sum t
 u
).




  Lemma
 conv_sum_abs : ∀ U
 V
 t
 u
, ¬ conv (Sum U
 V
) (Abs t
 u
).




  Lemma
 conv_sum_pair : ∀ U
 V
 t
 u
 v
, ¬ conv (Sum U
 V
) (Pair t
 u
 v
).




  Lemma
 conv_subset_abs : ∀ U
 V
 t
 u
, ¬ conv (Subset U
 V
) (Abs t
 u
).




  Lemma
 conv_subset_pair : ∀ U
 V
 t
 u
 v
, ¬ conv (Subset U
 V
) (Pair t
 u
 v
).




End
 Church_Rosser.