Normal.v



  Hints Resolve left_sym right_sym sp_swap sp_noswap : pts.

Section Normalisation.

  Variable R: red_rule.


  Definition sn: env->term->Prop :=
              [e:env][t:term](Acc term (transp term (R e)) t).


  Definition
normal: env->term->Prop :=
              [e:env][t:term](u:term)~(R e t u).


  Definition
head_normal: env->term->Prop :=
              [e:env][t:term](u:term)(red R e t u)->(
normal e u).


  Definition confluent := (e:env)(commut term (R e) (transp term (R e))).


  Definition
church_rosser := (e:env)(u,v:term)(R_rst R e u v)
      ->(Ex2 [t:term](R_rt R e u t) [t:term](R_rt R e v t)).


  Lemma
sn_red_sn: (e:env)(a,b:term)(R_rt R e a b)->(sn e a)->(sn e b).
Proof.
(Induction 1; Intros; Auto with arith pts).
Red.
(Apply Acc_inv with x; Auto with arith pts).
Save.


  Lemma red_normal: (e:env)(u,v:term)(R_rt R e u v)->(normal e u)-> u=v.
Proof.
(Induction 1; Intros; Auto with arith pts).
(Absurd (R e x y); Auto with arith pts).

Generalize H3 .
(Elim H1; Auto with arith pts).
Save.


  Lemma hn_red_hn: (e:env)(t,u:term)(head_normal e t)
                          ->(red R e t u)->(head_normal e u).
Proof.
Unfold head_normal .
Intros.
Apply H.
(Apply red_trans with u; Auto with arith pts).
Save.


End Normalisation.


Section Normal_Terms.

  Variable R1,R2: red_rule.

  Lemma normal_union: (e:env)(x:term)(normal R1 e x) -> (normal R2 e x)
              -> (normal (reunion R1 R2) e x).
(Red; Red; Intros).
Inversion_clear H1.
(Elim H with u; Auto with arith pts).

(Elim H0 with u; Auto with arith pts).
Save.

End Normal_Terms.


Section Ordres.

  Variable R: red_rule.

  Hypothesis stable: (R_stable_env (ctxt R)).

Section Ordre_de_Normalisation.

  Definition value := env*term.

  Inductive
subterm: value->value->Prop :=
    sbtrm_abs_l: (e:env)(A,M:term)(subterm (e,A) (e,(Abs A M)))
  | sbtrm_abs_r: (e:env)(A,A',M:term)
                    (subterm ((cons (Ax A') e),M) (e,(Abs A M)))
  | sbtrm_app_l: (e:env)(u,v:term)(subterm (e,u) (e,(App u v)))
  | sbtrm_app_r: (e:env)(u,v:term)(subterm (e,v) (e,(App u v)))
  | sbtrm_prod_l: (e:env)(A,B:term)(subterm (e,A) (e,(Prod A B)))
  | sbtrm_prod_r: (e:env)(A,A',B:term)
                    (subterm ((cons (Ax A') e),B) (e,(Prod A B))).

  Hints Resolve sbtrm_abs_l sbtrm_abs_r sbtrm_app_l sbtrm_app_r
         sbtrm_prod_l sbtrm_prod_r : pts.


  Lemma wf_subterm: (well_founded value subterm).
Red.
Destruct a.
Intros.
Generalize e .
(Elim t; Intros; Apply Acc_intro; Intros).
Inversion_clear H.

Inversion_clear H.

(Inversion_clear H1; Auto with arith pts).

(Inversion_clear H1; Auto with arith pts).

(Inversion_clear H1; Auto with arith pts).
Save.


  Inductive R_exp: value->value->Prop :=
    Rex_intro: (e:env)(x,y:term)(ctxt R e x y)->(R_exp (e,y) (e,x)).

  Hints Resolve Rex_intro : pts.


  Lemma commut_subterm_R_exp: (commut value subterm R_exp).
Red.
(Induction 1; Intros; (Inversion_clear H1) Orelse Inversion_clear H0).
(Exists (e,(Abs y0 M)); Auto with arith pts).

(Exists (e,(Abs A y0)); Auto with arith pts).
Apply Rex_intro.
Apply ctx_abs_r.
(Apply stable with [_:env][x,y:term](eq ? y A) (cons (Ax A') e); Auto with arith pts).

(Exists (e,(App y0 v)); Auto with arith pts).

(Exists (e,(App u y0)); Auto with arith pts).

(Exists (e,(Prod y0 B)); Auto with arith pts).

(Exists (e,(Prod A y0)); Auto with arith pts).
Apply Rex_intro.
Apply ctx_prod_r.
(Apply stable with [_:env][x,y:term](eq ? y A) (cons (Ax A') e); Auto with arith pts).
Save.


  Lemma subterm_sn: (e:env)(t:term)(sn (ctxt R) e t)
        ->(f:env)(u:term)(subterm (f,u) (e,t))
          ->(sn (ctxt R) f u).
Unfold sn transp .
(Induction 1; Intros).
(Apply Acc_intro; Intros).
(Elim commut_subterm_R_exp with (e,x) (f,u) (f,y); Intros; Auto with arith pts).
Inversion_clear H4 in H5.
(Apply H1 with y0; Auto with arith pts).
Save.



  Definition ord_norm1: (relation value) :=
                               (union value subterm R_exp).
  Definition ord_norm: (relation value) :=
                               (clos_trans value ord_norm1).

  Lemma sn_acc_ord_norm1: (e:env)(t:term)(sn (ctxt R) e t)
                                ->(Acc value ord_norm1 (e,t)).
Unfold ord_norm1 .
Intros.
(Apply Acc_union; Intros).
Exact commut_subterm_R_exp.

Apply wf_subterm.

(Elim H; Intros).
(Apply Acc_intro; Intros).
(Inversion_clear H2; Auto with arith pts).
Save.

End Ordre_de_Normalisation.

  Hints Resolve Rex_intro : pts.
  Hints Unfold ord_norm1 : pts.

Section Ordre_de_Sous_typage.


  Definition ord_conv: (relation value*value) :=
                   (clos_trans value*value (swapprod value ord_norm1)).

  Lemma ord_cv_no_swap: (e:env)(u,ru:term)(red R e ru u)
            ->(v,rv:term)(red R e rv v)
              ->(su,sv:
value)(ord_norm1 (e,ru) su)->(ord_norm1 (e,rv) sv)
                ->(ord_conv ((e,u),(e,v)) (su,sv)).
Red;Intros.
Apply t_trans with (((e,u)),sv).
(Elim H0 using clos_refl_trans_ind_left; Intros; Auto with arith pts).
(Apply t_trans with (((e,u)),((e,P0))); Auto 10 with arith pts).

(Elim H using clos_refl_trans_ind_left; Intros; Auto with arith pts).
(Apply t_trans with (((e,P0)),sv); Auto 10 with arith pts).
Save.


  Lemma ord_cv_swap: (e:env)(u,ru:term)(red R e ru u)
            ->(v,rv:term)(red R e rv v)
              ->(su,sv:
value)(ord_norm1 (e,ru) su)->(ord_norm1 (e,rv) sv)
                ->(ord_conv ((e,u),(e,v)) (sv,su)).
Red;Intros.
Apply t_trans with (((e,u)),sv).
(Elim H0 using clos_refl_trans_ind_left; Intros; Auto with arith pts).
(Apply t_trans with (((e,u)),((e,P0))); Auto 10 with arith pts).

(Elim H using clos_refl_trans_ind_left; Intros; Auto with arith pts).
(Apply t_trans with (((e,P0)),sv); Auto 10 with arith pts).
Save.

End Ordre_de_Sous_typage.

End Ordres.

  Hints Resolve Rex_intro sbtrm_abs_l sbtrm_abs_r sbtrm_app_l sbtrm_app_r
         sbtrm_prod_l sbtrm_prod_r : pts.
  Hints Unfold ord_norm1 ord_norm ord_conv : pts.


23/12/98, 14:30