Can.v

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

  (* reducibility schemes *)

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

  (* extensional 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.

  (* higher order reducibilty candidates *)

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

  Definition is_cand: (term->Prop)->Prop :=
      [CR:term->Prop]
         ((t:term)(CR t)->(sn t))
       /\((t:term)(CR t)->(u:term)(red1 t u)->(CR u))
       /\((t:term)(neutral t)->((u:term)(red1 t u)->(CR u))->(CR t)).

  Lemma int_var: (n:nat)(CR:term->Prop)(is_cand CR)->(CR (Ref n)).
Induction 1;Intros.
(Elim H1;Intros).
Apply H3.
(Unfold neutral ;Intros;Discriminate).

Intros.
Inversion_clear H4.
Save.

  Lemma cr_red: (R:term->Prop)(is_cand R)->(a,b:term)(R a)->(red a b)->(R b).
(Induction 3;Intros;Auto).
(Elim H;Intros).
(Elim H6;Intros).
(Apply H7 with P ;Auto).
Save.

  Fixpoint is_can [s:skel]: (Can s)->Prop :=
     <[s0:skel](Can s0)->Prop>Case s of
          [CR:term->Prop](is_cand CR)
          [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.

  (* Canonical 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 CR_sn: (is_cand sn).
(Split;Intros).
Auto.

(Split;Intros).
(Apply sn_red_sn with t ;Auto).

(Red;Apply Acc_intro;Auto).
Save.

  Hint CR_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)(Can (PROD s PROP))->(term->Prop)->(term->Prop) :=
       [s:skel][F:(Can (PROD s PROP))][CR:term->Prop][t:term]
          (u:term)(CR u)->(C:(Can s))(is_can s C)->(eq_can s C C)
                    ->(F C (App t u)).

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

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

  Lemma CR_pi: (s:skel)(F:(Can (PROD s PROP)))(is_can (PROD s PROP) F)
                      ->(CR:term->Prop)(is_cand CR)->(is_cand (Pi s F CR)).
(Simpl;Unfold Pi ; Intros).
(Elim H0; Intros).
(Elim H2; Intros).
Clear H2.
(Split; Intros).
(Elim H with (default_can s); Auto; Intros).
(Apply subterm_sn with (App t (Ref O)); Auto).
Apply H5.
(Apply H2; Auto).
(Apply int_var; Auto).

(Split; Intros).
(Elim H with C; Intros; Auto).
(Elim H10; Intros).
(Apply H11 with (App t u0); Auto).

(Elim H with C; Intros; Auto).
(Elim H10; Intros).
Clear H10.
(Apply H12; Intros).
(Red; Intros; Discriminate).

Generalize H6 u0 H10 .
(Cut (sn u); Auto).
(Induction 1; Intros).
Generalize H2 .
(Inversion_clear H17; Intros; Auto).
(Elim H17 with T M; Auto).

(Apply H12; Intros).
(Red; Intros; Discriminate).

(Apply H15 with N2; Auto).
(Apply H3 with x; Auto).
Save.

  Lemma red1_subst_cand: (CR:term->Prop)(is_cand CR)->(T:term)(sn T)
                    ->(m:term)(sn m)->(u:term)(sn u)->(CR (subst u m))
                     ->(v:term)(red1 (App (Abs T m) u) v)->(CR v).
Unfold sn.
Induction 2.
Inversion_clear H.
Inversion_clear H2.
Induction 3.
(Induction 3;Intros).
(Inversion_clear H12;Auto).
Inversion_clear H13.
(Apply H3;Intros).
Unfold neutral ;Intros;Discriminate.

Apply H4 with M' x0 x1 ;Auto.
Apply Acc_intro;Auto.

Apply Acc_intro;Auto.

(Apply H3;Intros).
Unfold neutral ;Intros;Discriminate.

(Apply H7 with M' x1 ;Auto).
Apply Acc_intro;Auto.

(Apply H with (subst x1 x0) ;Auto).
Unfold subst .
Apply red1_subst_r;Auto.

(Apply H3;Intros).
Unfold neutral ;Intros;Discriminate.

(Apply H10 with N2 ;Auto).
Apply (cr_red CR) with (subst x1 x0) ;Auto.
Unfold is_cand ;Auto.

Unfold subst .
Apply red1_subst_l;Auto.
Save.

  Lemma Pi_sound: (A:term->Prop)(s:skel)(F:(Can s)->(term->Prop))(T,m:term)
            (is_cand 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 F A (Abs T m)).
(Unfold Pi ;Simpl;Intros).
Cut (is_cand (F C));Intros;Auto.
Inversion_clear H6.
Inversion_clear H8.
Apply H9;Intros.
(Unfold neutral ;Intros;Discriminate).

Apply (red1_subst_cand (F C)) with T m u ;Auto.
Apply sn_subst with (Ref O).
Apply H7.
Apply H1;Auto.
Apply int_var;Auto.

Inversion_clear H.
Inversion_clear H11.
Auto.
Save.

  (* interpretation of type variables *)

  Inductive Int_K: Type :=
      iK: (s:skel)(Can s)->Int_K.

  Definition intP:=(TList Int_K).

  Definition def_cons: cls->term->intP->intP :=
    [e:cls][K:term](TCs ? (iK (cv_skel K e) (default_can (cv_skel K e)))).

  Definition extract_CR: (s:skel)Int_K->(Can s) :=
   [s:skel][i:Int_K]Cases i of
     (iK si Ci) =>
          Case (EQ_skel si s) of
            [y:(si===s)]<[s0:skel][_:(si===s0)](Can s0)>Case y of
                                  Ci
                                  end
            [_:(notT (si===s))](default_can s)
            end
     end.

  (* dependent types lemmas *)

  Lemma extr_eq: (P:(s:skel)(Can s)->Prop)(s:skel)(c:(Can s))(i:Int_K)
    (i==(iK s c))->(P s c)->
    (P s (extract_CR s i)).
Intros.
Unfold extract_CR.
Rewrite -> H.
Elim (EQ_skel s s).
Intro.
Change ([s0:skel]
         [e:s===s0](P s0 <[s1:skel][_:s===s1](Can s1)>Case e of c
                                                              end) s y).
(Elim y; Auto).

(Induction 1; Auto).
Save.

  Lemma eq_can_extr: (s,si:skel)(X,Y:(Can s))(eq_can s X Y)
           ->(eq_can si (extract_CR si (iK s X)) (extract_CR si (iK s Y))).
Unfold extract_CR .
Intros.
Elim (EQ_skel s si);Auto.
(Induction y;Auto).
Save.

  Hint eq_can_extr.

  Lemma simpl_eq_extr: (s:skel)(X,Y:(Can s))
    (eq_can s X Y)==(eq_can s (extract_CR s (iK s X)) (extract_CR s (iK s Y))).
Intros.
Unfold extract_CR.
Elim (EQ_skel s s).
Intros.
Change ([s0:skel]
         [e:s===s0]
          (eq_can s X Y)
           ==(eq_can s0 <[s0:skel][_:s===s0](Can s0)>Case e of X
                                                              end
               <[s0:skel][_:s===s0](Can s0)>Case e of Y
                                                      end) s y).
(Elim y; Auto).

(Induction 1; Auto).
Save.

  Lemma inv_eq_int: (sx,sy:skel)(X,X1:(Can sx))(Y,Y1:(Can sy))
         (iK sx X)==(iK sy Y)->(iK sx X1)==(iK sy Y1)
           ->(eq_can sx X X1)==(eq_can sy Y Y1).
Intros.
Rewrite -> simpl_eq_extr.
(Rewrite -> H; Rewrite -> H0).
Replace sx with sy.
(Elim simpl_eq_extr; Auto).

Change (<skel>Case (iK sy Y) of [s:skel][_:(Can s)]s
                                end)
        ==(<skel>Case (iK sx X) of [s:skel][_:(Can s)]s
                                   end).
(Elim H; Auto).
Save.

  Inductive int_inv: intP->Prop :=
    iv_nl: (int_inv (TNl ?))
  | iv_cs: (i:intP)(s:skel)(C:(Can s))(int_inv i)->(eq_can s C C)
             ->(int_inv (TCs ? (iK s C) i)).

  Hint iv_nl iv_cs.

  Lemma ins_int_inv: (e,f:intP)(k:nat)(y:Int_K)(TIns ? y k e f)
                      ->(int_inv f)->(int_inv e).
(Induction 1; Intros).
(Inversion H0; Auto).

(Inversion H2; Auto).
Save.

  Inductive int_eq_can: intP->intP->Prop :=
    ieq_nl: (int_eq_can (TNl ?) (TNl ?))
  | ieq_cs: (i,i':intP)(s:skel)(X,Y:(Can s))(int_eq_can i i')
             ->(eq_can s X Y)->(eq_can s X X)->(eq_can s Y Y)
              ->(int_eq_can (TCs ? (iK s X) i) (TCs ? (iK s Y) i')).

  Hint ieq_nl ieq_cs.

  Lemma int_inv_int_eq_can: (i:intP)(int_inv i)->(int_eq_can i i).
(Induction 1;Auto).
Save.

  Hint int_inv_int_eq_can.

20/01/97, 15:32