Can.v

Require Termes.
Require Conv.
Require Types.
Require Class.

  (* schemes of reducibility: functions on sets of terms *)

  Fixpoint Can [K:skel]: Type :=
      Cases K of
        PROP => (term->Prop)
      | (PROD s1 s2) => ((Can s1)->(Can s2))
      end.

  (* equality on schemes *)

  Definition eq_cand: (term->Prop)->(term->Prop)->Prop :=
      [X,Y:term->Prop](t:term)(X t)<->(Y t).

  Hint Unfold eq_cand.

  Fixpoint eq_can [s:skel]: (Can s)->(Can s)->Prop :=
    <[s0:skel](Can s0)->(Can s0)->Prop>Case s of
         eq_cand
         [s1,s2:skel][C1,C2:(Can (PROD s1 s2))]
                        (X1,X2:(Can s1))(eq_can s1 X1 X2)
                           ->(eq_can s1 X1 X1)->(eq_can s1 X2 X2)
                             ->(eq_can s2 (C1 X1) (C2 X2))
      end.

  Hint Unfold iff.

  Lemma eq_can_sym: (s:skel)(X,Y:(Can s))(eq_can s X Y)->(eq_can s Y X).
Induction s;Simpl;Intros;Auto.
(Unfold eq_cand ;Intros).
(Elim H with t ;Auto).
Save.

  Lemma eq_can_trans: (s:skel)(a,b,c:(Can s))
                 (eq_can s a b)->(eq_can s b b)->(eq_can s b c)
                  ->(eq_can s a c).
(Induction s;Simpl;Intros).
(Unfold eq_cand ;Intros).
(Elim H with t ;Elim H1 with t ;Auto).

Apply H0 with (b X1) ;Auto.
Save.

  Lemma eq_cand_incl: (t:term)(X,Y:(Can PROP))(eq_can PROP X Y)->(X t)->(Y t).
Intros.
(Elim H with t; Auto).
Save.

  (* Higher order candidates of reducibility *)

  Definition neutral: term->Prop := [t:term](u,v:term)~(t=(Abs u v)).

  Record is_cand [X:term->Prop]: Prop := {
     incl_sn: (t:term)(X t)->(sn t);
     clos_red: (t:term)(X t)->(u:term)(red1 t u)->(X u);
     clos_exp: (t:term)(neutral t)->((u:term)(red1 t u)->(X u))->(X t)}.

  Lemma var_in_cand: (n:nat)(X:term->Prop)(is_cand X)->(X (Ref n)).
Intros.
(Apply (clos_exp X); Auto).
(Unfold neutral; Intros; Discriminate).

Intros.
Inversion H0.
Save.

  Lemma clos_red_star: (R:term->Prop)(is_cand R)
                           ->(a,b:term)(R a)->(red a b)->(R b).
(Induction 3; Intros; Auto).
(Apply (clos_red R) with P; Auto).
Save.

  Lemma cand_sat: (X:term->Prop)(is_cand X)
              ->(T:term)(sn T)
               ->(u:term)(sn u)
                ->(m:term)(X (subst u m))
                 ->(X (App (Abs T m) u)).
Unfold sn.
Induction 2.
Induction 3.
Intros.
Generalize H6 .
(ElimType (sn m); Intros).
(Apply (clos_exp X); Intros; Auto).
(Red; Intros; Discriminate).

(Inversion_clear H10; Auto).
Inversion_clear H11.
(Apply H2; Auto).
(Apply Acc_intro; Auto).

(Apply H8; Auto).
(Apply (clos_red X) with (subst x0 x1); Auto).
(Unfold subst; Auto).

(Apply H5; Auto).
(Apply clos_red_star with (subst x0 x1); Auto).
(Unfold subst; Auto).

Apply sn_subst with x0.
(Apply (incl_sn X); Auto).
Save.

  Fixpoint is_can [s:skel]: (Can s)->Prop :=
     <[s0:skel](Can s0)->Prop>Case s of
          [X:term->Prop](is_cand X)
          [s1,s2:skel][C:(Can s1)->(Can s2)]
            (X:(Can s1))(is_can s1 X)->(eq_can s1 X X)->(is_can s2 (C X))
          end.

  Lemma is_can_prop: (X:term->Prop)(is_can PROP X)->(is_cand X).
Auto.
Save.

  Hint is_can_prop.

  (* Default Candidates *)

  Fixpoint default_can [s:skel]: (Can s) :=
     <[ss:skel](Can ss)>Case s of
         sn
         [s1,s2:skel][_:(Can s1)](default_can s2)
         end.

  Lemma cand_sn: (is_cand sn).
Apply Build_is_cand;Intros;Auto.

(Apply sn_red_sn with t; Auto).

(Red;Apply Acc_intro;Auto).
Save.

  Hint cand_sn.

  Lemma def_can_cr: (s:skel)(is_can s (default_can s)).
(Induction s;Simpl;Intros;Auto).
Save.

  Lemma def_inv: (s:skel)(eq_can s (default_can s) (default_can s)).
(Induction s;Simpl;Intros;Auto).
Save.

  Hint def_inv def_can_cr.

  Definition Pi: (s:skel)(term->Prop)->(Can (PROD s PROP))->(term->Prop) :=
       [s:skel][X:term->Prop][F:(Can (PROD s PROP))][t:term]
          (u:term)(X u)->(C:(Can s))(is_can s C)->(eq_can s C C)
                    ->(F C (App t u)).

  Lemma eq_can_Pi: (s:skel)(X,Y:term->Prop)(F1,F2:(Can (PROD s PROP)))
                   (eq_can PROP X Y)->(eq_can (PROD s PROP) F1 F2)
                      ->(eq_can PROP (Pi s X F1) (Pi s Y F2)).
(Simpl;Intros;Unfold iff Pi ).
(Split;Intros).
(Elim H0 with C C (App t u) ;Elim H with u ;Auto).

(Elim H0 with C C (App t u) ;Elim H with u ;Auto).
Save.

  Lemma is_can_Pi: (s:skel)(X:term->Prop)(is_cand X)
                  ->(F:(Can (PROD s PROP)))(is_can (PROD s PROP) F)
                      ->(is_cand (Pi s X F)).
(Simpl; Unfold Pi; Intros).
(Apply Build_is_cand; Intros).
(Apply subterm_sn with (App t (Ref O)); Auto).
(Apply (incl_sn (F (default_can s))); Auto).
(Apply H1; Auto).
(Apply (var_in_cand O X); Auto).

(Apply (clos_red (F C)) with (App t u0); Auto).

(Apply (clos_exp (F C)); Auto).
(Red; Intros; Discriminate).

Generalize H3 .
Cut (sn u).
(Induction 1; Intros).
Generalize H1 .
(Inversion_clear H10; Intros; Auto).
(Elim H10 with T M; Auto).

(Apply (clos_exp (F C)); Intros; Auto).
(Red; Intros; Discriminate).

(Apply H8 with N2; Auto).
(Apply (clos_red X) with x; Auto).

(Apply (incl_sn X); Auto).
Save.

  Lemma Abs_sound: (A:term->Prop)(s:skel)(F:(Can s)->(term->Prop))(T,m:term)
            (is_can PROP A)->(is_can (PROD s PROP) F)
             ->((n:term)(A n)->(C:(Can s))(is_can s C)
                 ->(eq_can s C C)->(F C (subst n m)))
              ->(sn T)->(Pi s A F (Abs T m)).
(Unfold Pi; Simpl; Intros).
(Cut (is_cand (F C)); Intros; Auto).
(Apply (clos_exp (F C)); Intros; Auto).
(Red; Intros; Discriminate).

(Apply clos_red with (App (Abs T m) u); Auto).
(Apply (cand_sat (F C)); Auto).
(Apply (incl_sn A); Auto).
Save.

13/02/97, 13:19