Library Lambda.Conv_Dec


Require
 Import
 Peano_dec.

Require
 Import
 Transitive_Closure.

Require
 Import
 Union.

Require
 Import
 Lambda.Terms.

Require
 Import
 Lambda.Reduction.

Require
 Import
 Lambda.Conv.




  Definition
 ord_norm1 := union _
 subterm (transp _
 red1).

  Definition
 ord_norm := clos_trans _
 ord_norm1.




  Hint
 Unfold
 ord_norm1 ord_norm: coc
.




  Lemma
 subterm_ord_norm : ∀ a
 b
 : term, subterm a
 b
 → ord_norm a
 b
.




  Hint
 Resolve
 subterm_ord_norm: coc
.




  Lemma
 red_red1_ord_norm :

   ∀ a
 b
 : term, red a
 b
 → ∀ c
 : term, red1 b
 c
 → ord_norm c
 a
.




  Lemma
 wf_subterm : well_founded subterm.




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




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




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

    match
 a
 with


    | Srt s
 ⇒ Srt s


    | Ref n
 ⇒ Ref n


    | Abs T
 t
 ⇒ Abs (norm
 T
) (norm
 t
)

    | App u
 v
 ⇒

        match
 norm
 u
 return
 term with


        | Abs _
 b
 ⇒ norm
 (subst (norm
 v
) b
)

        | t
 ⇒ App t
 (norm
 v
)

        end


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

    | Prod T
 U
 ⇒ Prod (norm
 T
) (norm
 U
)

    | Sum T
 U
 ⇒ Sum (norm
 T
) (norm
 U
)

    | Subset T
 U
 ⇒ Subset (norm
 T
) (norm
 U
)

    | Pi1 t
 ⇒ match
 (norm
 t
) return
 term with


      | Pair _
 u
 _
 ⇒ u


      | t
 ⇒ Pi1 t


      end


    | Pi2 t
 ⇒ match
 norm
 t
 return
 term with


      | Pair _
 _
 v
 ⇒ v


      | t
 ⇒ Pi2 t


       end


    end
.




  Theorem
 compute_nf :

   ∀ t
 : term, sn t
 → {u
 : term | red t
 u
 &  normal u
}.




  Lemma
 eqterm : ∀ u
 v
 : term, {u
 = v
} + {u
 ≠ v
}.




  Theorem
 is_conv :

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