### 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