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