Library Lambda.TPOSR.Conv_Dec


Require
 Import
 Peano_dec.

Require
 Import
 Transitive_Closure.

Require
 Import
 Union.

Require
 Import
 Lambda.TPOSR.Terms.

Require
 Import
 Lambda.TPOSR.Reduction.

Require
 Import
 Lambda.TPOSR.Conv.




  Definition
 ord_norm1 := union _
 sublterm (transp _
 lred1).

  Definition
 ord_norm := clos_trans _
 ord_norm1.




  Hint
 Unfold
 ord_norm1 ord_norm: coc
.




  Lemma
 sublterm_ord_norm : ∀ a
 b
 : lterm, sublterm a
 b
 → ord_norm a
 b
.




  Hint
 Resolve
 sublterm_ord_norm: coc
.




  Lemma
 lred_lred1_ord_norm :

   ∀ a
 b
 : lterm, lred a
 b
 → ∀ c
 : lterm, lred1 b
 c
 → ord_norm c
 a
.




  Lemma
 wf_sublterm : well_founded sublterm.




  Lemma
 wf_ord_norm1 : ∀ t
 : lterm, sn t
 → Acc ord_norm1 t
.




  Theorem
 wf_ord_norm : ∀ t
 : lterm, sn t
 → Acc ord_norm t
.




  Definition
 norm_body (a
 : lterm) (norm
 : lterm → lterm) :=

    match
 a
 with


    | Srt_l s
 ⇒ Srt_l s


    | Ref_l n
 ⇒ Ref_l n


    | Abs_l T
 t
 ⇒ Abs_l (norm
 T
) (norm
 t
)

    | App_l T
 u
 v
 ⇒

        match
 norm
 u
 return
 lterm with


        | Abs_l _
 b
 ⇒ norm
 (lsubst (norm
 v
) b
)

        | t
 ⇒ App_l (norm
 T
) t
 (norm
 v
)

        end


    | Pair_l T
 u
 v
 ⇒ Pair_l (norm
 T
) (norm
 u
) (norm
 v
)

    | Prod_l T
 U
 ⇒ Prod_l (norm
 T
) (norm
 U
)

    | Sum_l T
 U
 ⇒ Sum_l (norm
 T
) (norm
 U
)

    | Subset_l T
 U
 ⇒ Subset_l (norm
 T
) (norm
 U
)

    | Pi1_l T
 t
 ⇒ match
 (norm
 t
) return
 lterm with


      | Pair_l _
 u
 _
 ⇒ u


      | t
 ⇒ Pi1_l (norm
 T
) t


      end


    | Pi2_l T
 t
 ⇒ match
 norm
 t
 return
 lterm with


      | Pair_l _
 _
 v
 ⇒ v


      | t
 ⇒ Pi2_l (norm
 T
) t


       end


    end
.




  Theorem
 compute_nf :

   ∀ t
 : lterm, sn t
 → {u
 : lterm | lred t
 u
 &  normal u
}.




  Lemma
 eqlterm : ∀ u
 v
 : lterm, {u
 = v
} + {u
 ≠ v
}.




  Theorem
 is_conv :

   ∀ u
 v
 : lterm, sn u
 → sn v
 → {conv u
 v
} + {¬ conv u
 v
}.