Rules.v

Section Rule_Operators.

  Variable R,R': red_rule.

  Definition R_rst : red_rule := [e:env](clos_refl_sym_trans term (R e)).

  Definition reunion: red_rule := [e](union ? (R e) (R' e)).

(* passage au contexte *)

  Inductive ctxt : env->term->term->Prop :=
    ctx_rule: (e:env)(x,y:term)(R e x y) -> (ctxt e x y)
  | ctx_abs_l: (e:env)(M,M':term)(ctxt e M M')
                -> (N:term)(ctxt e (Abs M N) (Abs M' N))
  | ctx_abs_r: (e:env)(M,M',N:term)(ctxt (cons (Ax N) e) M M')
                -> (ctxt e (Abs N M) (Abs N M'))
  | ctx_app_l: (e:env)(M1,N1:term)(ctxt e M1 N1)
                ->(M2:term)(ctxt e (App M1 M2)(App N1 M2))
  | ctx_app_r: (e:env)(M2,N2:term)(ctxt e M2 N2)
                ->(M1:term)(ctxt e (App M1 M2)(App M1 N2))
  | ctx_prod_l: (e:env)(M1,N1:term)(ctxt e M1 N1)
                ->(M2:term)(ctxt e (Prod M1 M2)(Prod N1 M2))
  | ctx_prod_r: (e:env)(M2,N2,M1:term)(ctxt (cons (Ax M1) e) M2 N2)
                ->(ctxt e (Prod M1 M2)(Prod M1 N2)).

End Rule_Operators.

  Hints Unfold R_rst reunion : pts.
  Hints Resolve ctx_rule ctx_abs_l ctx_abs_r ctx_app_l ctx_app_r ctx_prod_l
                ctx_prod_r
   : pts.

Section Context_Closure.

  Variable R: red_rule.

  Definition red := (R_rt (ctxt R)).
  Definition conv := (R_rst (ctxt R)).

  Hints Unfold red conv : pts.

  Lemma red_trans: (e:env)(x,y,z:term)(red e x y)->(red e y z)
                      ->(red e x z).
Proof [e:env](rt_trans term (ctxt R e)).

  Lemma conv_trans: (e:env)(x,y,z:term)(conv e x y)->(conv e y z)
                      ->(conv e x z).
Proof [e:env](rst_trans term (ctxt R e)).

  Lemma conv_sym: (e:env)(x,y:term)(conv e x y)->(conv e y x).
Proof [e:env](rst_sym term (ctxt R e)).

  Lemma red_conv: (e:env)(x,y:term)(red e x y)->(conv e x y).
Proof [e:env](clos_rt_clos_rst term (ctxt R e)).

  Lemma red_sym_conv: (e:env)(x,y:term)(red e x y)->(conv e y x).
Intros.
Apply conv_sym;Apply red_conv;Auto with pts.
Save.

  Lemma red_red_abs: (e:env)(A,A',M,M':term)(red e A A')
          ->(red (cons (Ax A') e) M M')->(red e (Abs A M) (Abs A' M')).
Intros.
Apply red_trans with (Abs A' M).
(Elim H; Simpl; Intros; Auto with pts).
(Apply red_trans with (Abs y M); Auto with pts).

(Elim H0; Intros; Auto with pts).
(Apply red_trans with (Abs A' y); Auto with pts).
Save.

  Lemma red_red_app: (e:env)(u,u',v,v':term)(red e u u')
                  ->(red e v v')->(red e (App u v) (App u' v')).
Intros.
Apply red_trans with (App u' v).
(Elim H; Simpl; Intros; Auto with pts).
(Apply red_trans with (App y v); Auto with pts).

(Elim H0; Intros; Auto with pts).
(Apply red_trans with (App u' y); Auto with pts).
Save.

  Lemma red_red_prod: (e:env)(A,A',B,B':term)(red e A A')
        ->(red (cons (Ax A') e) B B')->(red e (Prod A B) (Prod A' B')).
Intros.
Apply red_trans with (Prod A' B).
(Elim H; Simpl; Intros; Auto with pts).
(Apply red_trans with (Prod y B); Auto with pts).

(Elim H0; Intros; Auto with pts).
(Apply red_trans with (Prod A' y); Auto with pts).
Save.

  Lemma conv_conv_abs: (e:env)(A,A',M,M':term)(conv e A A')
        ->(conv (cons (Ax A') e) M M')->(conv e (Abs A M) (Abs A' M')).
Intros.
Apply conv_trans with (Abs A' M).
(Elim H; Simpl; Intros; Auto with pts).
(Apply conv_trans with (Abs y M); Auto with pts).

(Elim H0; Intros; Auto with pts).
(Apply conv_trans with (Abs A' y); Auto with pts).
Save.

  Lemma conv_conv_app: (e:env)(u,u',v,v':term)(conv e u u')
                  ->(conv e v v')->(conv e (App u v) (App u' v')).
Intros.
Apply conv_trans with (App u' v).
(Elim H; Simpl; Intros; Auto with pts).
(Apply conv_trans with (App y v); Auto with pts).

(Elim H0; Intros; Auto with pts).
(Apply conv_trans with (App u' y); Auto with pts).
Save.

  Lemma conv_conv_prod: (e:env)(A,A',B,B':term)(conv e A A')
      ->(conv (cons (Ax A') e) B B')->(conv e (Prod A B) (Prod A' B')).
Intros.
Apply conv_trans with (Prod A' B).
(Elim H; Simpl; Intros; Auto with pts).
(Apply conv_trans with (Prod y B); Auto with pts).

(Elim H0; Intros; Auto with pts).
(Apply conv_trans with (Prod A' y); Auto with pts).
Save.

End Context_Closure.

  Hints Unfold red conv : pts.

  Hints Resolve red_conv red_sym_conv
       red_red_abs red_red_app red_red_prod
       conv_conv_abs conv_conv_app conv_conv_prod : pts.

  Hints Immediate conv_sym : pts.

Section Properties.

  Variable R,R': red_rule.

Section Prop_R_lift.

  Hypothesis R_lifts: (R_lift R).
  Hypothesis R_lifts': (R_lift R').

  Lemma reunion_lift: (R_lift (reunion R R')).
Proof.
Red.
(Destruct 1; EAuto with pts).
Save.

  Lemma ctxt_lift: (R_lift (ctxt R)).
Red.
(Induction 1; Simpl; Auto with pts; Intros).
Apply ctx_rule.
(Apply R_lifts with 2:=H1; Auto with pts).

Apply ctx_abs_r.
Apply H1.
(Replace (Ax (lift_rec (S O) N k)) with (lift_decl (S O) (Ax N) k); Auto with pts).

Apply ctx_prod_r.
Apply H1.
(Replace (Ax (lift_rec (S O) M1 k)) with (lift_decl (S O) (Ax M1) k);
Auto with pts).
Save.

  Lemma R_rt_lift: (R_lift (R_rt R)).
Unfold R_lift R_rt .
(Induction 1; Intros; Auto with pts).
Apply rt_step.
(Apply R_lifts with 2:=H1; Auto with pts).

(Apply rt_trans with (lift_rec (S O) y k); Auto with pts).
Save.

  Lemma R_rst_lift: (R_lift (R_rst R)).
Unfold R_lift R_rst .
(Induction 1; Intros; Auto with pts).
Apply rst_step.
(Apply R_lifts with 2:=H1; Auto with pts).

(Apply rst_sym; Auto with pts).

(Apply rst_trans with (lift_rec (S O) y k); Auto with pts).
Save.

End Prop_R_lift.

Section Prop_R_subst.

  Hypothesis R_substs: (R_subst R).
  Hypothesis R_substs': (R_subst R').

  Lemma reunion_subst: (R_subst (reunion R R')).
Proof.
Red.
Destruct 1; Intros.
(Elim R_substs with 1:=H0 2:=H1; Intros; Auto 10 with pts).
(Red; Apply rt_trans with y; Trivial with pts).

(Elim R_substs' with 1:=H0 2:=H1; Intros; Auto 10 with pts).
(Red; Apply rt_trans with y; Trivial with pts).
Save.

  Lemma ctxt_subst: (R_subst (ctxt R)).
Red;Red.
(Induction 1; Simpl; Auto with pts; Intros).
(Elim R_substs with 1:=H0 2:=H1; Intros; Auto with pts).
(Apply rt_trans with y0; Auto with pts).

(Elim H1 with n f; Intros; Auto with pts).
(Apply rt_trans with (Abs y (subst_rec s N (S n))); Auto with pts).

(Elim H1 with (S n) (cons (subst_decl s (Ax N) n) f); Intros; Auto with pts).
(Apply rt_trans with (Abs (subst_rec s N n) y); Auto with pts).

(Elim H1 with n f; Auto with pts; Intros).
(Apply rt_trans with (App y (subst_rec s M2 n)); Auto with pts).

(Elim H1 with n f; Auto with pts; Intros).
(Apply rt_trans with (App (subst_rec s M1 n) y); Auto with pts).

(Elim H1 with n f; Intros; Auto with pts).
(Apply rt_trans with (Prod y (subst_rec s M2 (S n))); Auto with pts).

(Elim H1 with (S n) (cons (subst_decl s (Ax M1) n) f); Auto with pts; Intros).
(Apply rt_trans with (Prod (subst_rec s M1 n) y); Auto with pts).
Save.

  Lemma R_rt_subst: (R_subst (R_rt R)).
Unfold R_subst 2 R_rt.
(Induction 1; Intros; Auto with pts).
Apply rt_step.
(Apply R_substs with 2:=H1; Auto with pts).

(Apply rt_trans with (subst_rec s y n); Auto with pts).
Save.

  Lemma R_rst_subst: (R_subst (R_rst R)).
Unfold R_subst R_rt .
(Induction 1; Intros; Auto with pts).
Apply rt_step.
Red.
Apply (clos_rt_clos_rst term (R f) (subst_rec s x n)).
Fold (R_rt R f).
(Apply R_substs with 2:=H1; Auto with pts).

(Elim H1 with 1:=H2; Auto with pts; Intros).
(Apply rt_trans with y0; Auto with pts).

(Apply rt_trans with (subst_rec s y n); Auto with pts).
Save.

End Prop_R_subst.

Section Prop_R_stable_env.

  Hypothesis R_stable: (R_stable_env R).
  Hypothesis R_stable': (R_stable_env R').

  Lemma reunion_stable: (R_stable_env (reunion R R')).
Proof.
Red.
(Destruct 1; EAuto with pts).
Save.

  Lemma ctxt_stable: (R_stable_env (ctxt R)).
Red.
(Induction 1; Intros; Auto with pts).
Apply ctx_rule.
(Apply R_stable with R'0 e0; Auto with pts).
Save.

  Lemma R_rt_stable: (R_stable_env (R_rt R)).
(Red; Red).
(Induction 1; Intros; Auto with pts).
Apply rt_step.
(Apply R_stable with R'0 e; Auto with pts).

(Apply rt_trans with y0; Auto with pts).
Save.

  Lemma R_rst_stable: (R_stable_env (R_rst R)).
(Red; Red).
(Induction 1; Intros; Auto with pts).
(Apply rst_step; Auto with pts).
(Apply R_stable with R'0 e; Auto with pts).

(Apply rst_sym; Auto with pts).

(Apply rst_trans with y0; Auto with pts).
Save.

End Prop_R_stable_env.

End Properties.

  Hints Resolve ctxt_lift R_rt_lift R_rst_lift ctxt_subst R_rt_subst
                R_rst_subst
   : pts.

Section Prop_R_lift_subst.

  Variable R: red_rule.

  Hypothesis R_lifts: (R_lift R).
  Hypothesis R_substs: (R_subst R).

(* amenes a disparaitre... *)
  Lemma red_lift: (R_lift (red R)).
Proof (R_rt_lift (ctxt R) (ctxt_lift R R_lifts)).

  Lemma conv_lift: (R_lift (conv R)).
Proof (R_rst_lift (ctxt R) (ctxt_lift R R_lifts)).

  Lemma red_subst: (R_subst (red R)).
Proof (R_rt_subst (ctxt R) (ctxt_subst R R_substs)).

  Lemma conv_subst: (R_subst (conv R)).
Proof (R_rst_subst (ctxt R) (ctxt_subst R R_substs)).

  Lemma red_subst_l: (g:env)(u,v:term)(ctxt R g u v)
              ->(t:term)(n:nat)(e:env)(trunc n e g)
               ->(red R e (subst_rec u t n) (subst_rec v t n)).
(Induction t; Simpl; Intros; Auto with pts).
(Red; Red).
(Elim (lt_eq_lt_dec n0 n); Intros; Auto with pts).
(Elim y; Intros; Auto with pts).
Apply rt_step.
(Apply iter_R_lift with g; Auto with pts).
Save.

  Lemma red_red_subst: (e:env)(x,y,t,u,T:term)
              (red R (cons (Ax T) e) t u)->(red R e x y)
                      ->(red R e (subst x t) (subst y u)).
Intros.
Unfold subst.
(Apply red_trans with (subst_rec x u O); Auto with pts).
(Elim red_subst
  with g:=e s:=x d1:=(Ax T) e:=(cons (Ax T) e) t:=t u:=u n:=O f:=e;
Intros; Auto with pts).
(Apply red_trans with y0; Auto with pts).

(Elim H0; Intros; Auto with pts).
(Apply red_subst_l with e; Auto with pts).

(Apply red_trans with (subst_rec y0 u O); Auto with pts).
Save.

End Prop_R_lift_subst.

  Hints Resolve red_lift conv_lift red_subst conv_subst : pts.

  Definition R_rt_basic_rule: Basic_rule -> Basic_rule.
Intros (R, Rlift, Rsubst, Rstable).
Constructor 1 with (R_rt R);Auto with pts.
Intros.
(Apply R_rt_stable; Auto with pts).
Defined.

  Definition R_rst_basic_rule: Basic_rule -> Basic_rule.
Intros (R, Rlift, Rsubst, Rstable).
Constructor 1 with (R_rst R);Auto with pts.
Intros.
(Apply R_rst_stable; Auto with pts).
Defined.

  Definition ctxt_basic_rule: Basic_rule -> Basic_rule.
Intros (R, Rlift, Rsubst, Rstable).
(Constructor 1 with (ctxt R); Auto with pts).
Intros.
(Apply ctxt_stable; Auto with pts).
Defined.

  Definition union_basic_rule: Basic_rule -> Basic_rule -> Basic_rule.
Intros (R0, Rlift0, Rsubst0, Rstable0) (R1, Rlift1, Rsubst1, Rstable1).
Constructor 1 with (reunion R0 R1).
(Red; Intros).
(Elim H; Intros).
Left.
(Apply Rlift0 with 2:=H0; Auto with pts).

Right.
(Apply Rlift1 with 2:=H0; Auto with pts).

(Red; Red; Intros).
(Elim H; Intros).
(Elim Rsubst0 with 1:=H1 2:=H0; Intros; Auto with pts).
(Apply rt_trans with y; Auto with pts).

(Elim Rsubst1 with 1:=H1 2:=H0; Intros; Auto with pts).
(Apply rt_trans with y; Auto with pts).

(Red; Intros).
(Elim H; Intros).
Left.
(Apply Rstable0 with R' e; Auto with pts).

Right.
(Apply Rstable1 with R' e; Auto with pts).
Defined.

(* Given a Basic_rule, the reflexive transitive closure is a * Subtyping_rule *)
  Definition canonical_subtyping: Basic_rule -> Subtyping_rule.
Intro.
Constructor 1 with (R_rt_basic_rule X).
(Generalize X; Intros (R, Rlift, Rsubst, Rstable) e; Simpl).
Unfold R_rt.
(Apply Build_preorder; Auto with pts).
(Red; Intros).
(Apply rt_trans with y; Auto with pts).
Defined.

23/12/98, 14:51