Library Conv_Dec


Require
 Import
 Transitive_Closure.

Require
 Import
 Union.

Require
 Export
 Peano_dec.




Require
 Export
 Conv.




Hint
 Unfold
 transp union: core
.

Hint
 Resolve
 t_step: core
.




  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 : forall
 a
 b
, subterm a
 b
 -> ord_norm a
 b
.

auto
 10 with
 coc
.

Qed
.




  Hint
 Resolve
 subterm_ord_norm: coc
.




  Lemma
 red_red1_ord_norm :

   forall
 a
 b
, red a
 b
 -> forall
 c
, red1 b
 c
 -> ord_norm c
 a
.

red
 in
 |- *.

simple
 induction
 1; intros
; auto
 with
 coc
.

apply
 t_trans with
 N
; auto
 with
 coc
.

Qed
.




  Lemma
 wf_subterm : well_founded subterm.

red
 in
 |- *.

simple
 induction
 a
; intros
; apply
 Acc_intro; intros
.

inversion_clear
 H
.




inversion_clear
 H
.




inversion_clear
 H1
; auto
 with
 coc
.




inversion_clear
 H1
; auto
 with
 coc
.




inversion_clear
 H1
; auto
 with
 coc
.

Qed
.




  Lemma
 wf_ord_norm1 : forall
 t
, sn t
 -> Acc ord_norm1 t
.

unfold
 ord_norm1
 in
 |- *.

intros
.

apply
 Acc_union; auto
 with
 coc
.

exact
 commut_red1_subterm.




intros
.

apply
 wf_subterm.

Qed
.




  Theorem
 wf_ord_norm : forall
 t
, sn t
 -> Acc ord_norm t
.

unfold
 ord_norm
 in
 |- *.

intros
.

apply
 Acc_clos_trans.

apply
 wf_ord_norm1; auto
 with
 coc
.

Qed
.




  Definition
 norm_body a
 norm
 :=

    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


    | Prod T
 U
 => Prod (norm
 T
) (norm
 U
)

    end
.




  Theorem
 compute_nf : forall
 t
, sn t
 -> {u
 : _
 | red t
 u
 &  normal u
}.

intros
.

elimtype
 (Acc ord_norm t
).

intros
 [s
| n
| T
 t0
| u
 v
| T
 U
] _
 norm
.

exists
 (Srt s
); auto
 with
 coc
.

red
 in
 |- *; red
 in
 |- *; intros
.

inversion_clear
 H0
.




exists
 (Ref n
); auto
 with
 coc
.

red
 in
 |- *; red
 in
 |- *; intros
.

inversion_clear
 H0
.




elim
 (norm
 T
); auto
 with
 coc
; intros
 nT
 T_red
 T_norm
.

elim
 (norm
 t0
); auto
 with
 coc
; intros
 nt0
 t0_red
 t0_norm
.

exists
 (Abs nT
 nt0
); auto
 with
 coc
.

red
 in
 |- *; red
 in
 |- *; intros
.

inversion_clear
 H0
.

apply
 (T_norm
 M'
); auto
 with
 coc
.




apply
 (t0_norm
 M'
); auto
 with
 coc
.




elim
 (norm
 v
); auto
 with
 coc
; intros
 nv
 v_red
 v_norm
.

elim
 (norm
 u
); auto
 with
 coc
; intros
 [s
| n
| T
 b
| u0
 v0
| T
 U
] u_red
 u_norm
.

exists
 (App (Srt s
) nv
); auto
 with
 coc
.

red
 in
 |- *; red
 in
 |- *; intros
.

inversion_clear
 H0
.

inversion_clear
 H1
.




apply
 (v_norm
 N2
); auto
 with
 coc
.




exists
 (App (Ref n
) nv
); auto
 with
 coc
.

red
 in
 |- *; red
 in
 |- *; intros
.

inversion_clear
 H0
.

inversion_clear
 H1
.




apply
 (v_norm
 N2
); auto
 with
 coc
.




elim
 (norm
 (subst nv
 b
)).

intros
 nt
 t_red
 t_norm
.

exists
 nt
; auto
 with
 coc
.

apply
 trans_red_red with
 (subst nv
 b
); auto
 with
 coc
.

apply
 trans_red with
 (App (Abs T
 b
) nv
); auto
 with
 coc
.




apply
 red_red1_ord_norm with
 (App (Abs T
 b
) nv
); auto
 with
 coc
.




exists
 (App (App u0
 v0
) nv
); auto
 with
 coc
.

red
 in
 |- *; red
 in
 |- *; intros
.

inversion_clear
 H0
.

elim
 u_norm
 with
 N1
; auto
 with
 coc
.




elim
 v_norm
 with
 N2
; auto
 with
 coc
.




exists
 (App (Prod T
 U
) nv
); auto
 with
 coc
.

red
 in
 |- *; red
 in
 |- *; intros
.

inversion_clear
 H0
.

elim
 u_norm
 with
 N1
; auto
 with
 coc
.




elim
 v_norm
 with
 N2
; auto
 with
 coc
.




elim
 (norm
 T
); auto
 with
 coc
; intros
 nT
 T_red
 T_norm
.

elim
 (norm
 U
); auto
 with
 coc
; intros
 nU
 U_red
 U_norm
.

exists
 (Prod nT
 nU
); auto
 with
 coc
.

red
 in
 |- *; red
 in
 |- *; intros
.

inversion_clear
 H0
.

apply
 (T_norm
 N1
); auto
 with
 coc
.




apply
 (U_norm
 N2
); auto
 with
 coc
.




apply
 wf_ord_norm; auto
 with
 coc
.

Qed
.




  Lemma
 eqterm : forall
 u
 v
 : term, {u
 = v
} + {u
 <> v
}.

Proof
.

decide
 equality
.

decide
 equality
 s
 s0
.




apply
 eq_nat_dec.

Qed
.




  Theorem
 is_conv : forall
 u
 v
, sn u
 -> sn v
 -> {conv u
 v
} + {~ conv u
 v
}.

intros
 u
 v
 sn_u
 sn_v
.

elim
 (compute_nf u
); auto
 with
 coc
; intros
 nu
 u_red
 u_norm
.

elim
 (compute_nf v
); auto
 with
 coc
; intros
 nv
 v_red
 v_norm
.

elim
 (eqterm nu
 nv
).

intros
 eq_nf
.

left
.

rewrite
 eq_nf
 in
 u_red
.

apply
 trans_conv_conv with
 nv
; auto
 with
 coc
.

apply
 sym_conv; auto
 with
 coc
.




intros
 diff_nf
.

right
; red
 in
 |- *; intro
; apply
 diff_nf
.

elim
 church_rosser with
 nu
 nv
; intros
.

rewrite
 red_normal with
 (1 := H0
); trivial
.

rewrite
 red_normal with
 (1 := H1
); trivial
.




apply
 trans_conv_conv with
 u
; auto
 with
 coc
.

apply
 sym_conv; auto
 with
 coc
.

apply
 trans_conv_conv with
 v
; auto
 with
 coc
.

Qed
.