Library Can
Require Export Lambda.
Hint Unfold iff: core.
Definition CR := term -> Prop.
Record weak_cand (X : CR) : Prop :=
{wk_sn : ∀ t, X t -> sn t;
wk_red : ∀ t u, X t -> red t u -> X u;
wk_wit : exists w, X w}.
Definition weak_chain t : CR := fun u => red t u.
Lemma weakest_cands :
∀ t, sn t -> weak_cand (weak_chain t).
unfold weak_chain.
split; intros.
eauto using sn_red_sn.
transitivity t0; trivial.
eauto using refl_red.
Qed.
Record is_cand (X : CR) : Prop :=
{incl_sn : ∀ t, X t -> sn t;
clos_red : ∀ t u, X t -> red t u -> X u;
clos_exp : ∀ t, neutral t -> (∀ u, red1 t u -> X u) -> X t}.
Instance is_cand_morph : Proper (pointwise_relation _ iff ==> iff) is_cand.
Proof.
do 2 red; intros.
split; destruct 1; split; intros.
rewrite <- H in H0; auto.
rewrite <- H in H0 |-*; eauto.
rewrite <- H; apply clos_exp0; intros; trivial.
rewrite H; auto.
rewrite H in H0; auto.
rewrite H in H0 |-*; eauto.
rewrite H; apply clos_exp0; intros; trivial.
rewrite <- H; auto.
Qed.
Lemma cand_sn : is_cand sn.
constructor; intros; auto with coc.
apply sn_red_sn with t; auto with coc.
red in |- *; apply Acc_intro; auto with coc.
Qed.
Hint Resolve incl_sn cand_sn: coc.
Lemma var_in_cand : ∀ n X, is_cand X -> X (Ref n).
intros.
apply (clos_exp X); auto with coc.
exact I.
intros.
inversion H0.
Qed.
Lemma weaker_cand : ∀ X, is_cand X -> weak_cand X.
intros.
case H; split; trivial.
exists (Ref 0).
apply (var_in_cand _ X); trivial.
Qed.
Lemma sat1_in_cand : ∀ n X u,
is_cand X -> sn u -> X (App (Ref n) u).
induction 2; intros.
apply (clos_exp X); trivial.
exact I.
intros.
inversion_clear H2; auto.
inversion H3.
Qed.
Lemma cand_sat X m u :
is_cand X ->
boccur 0 m=true \/ sn u ->
X (subst u m) ->
X (App (Abs m) u).
Proof.
intros.
assert (snu : sn u).
destruct H0; trivial.
apply (incl_sn _ H) in H1.
apply sn_subst_inv_l in H1; trivial.
clear H0; revert m H1.
elim snu.
clear u snu; intros u _ IHu; unfold transp in *.
intros m m_in_X.
generalize m_in_X.
cut (sn m).
2: apply sn_subst with u; apply (incl_sn _ H); trivial.
simple induction 1.
clear m m_in_X H0; intros m _ IHm m_in_X; unfold transp in *.
apply (clos_exp _ H). exact I.
intros x red_redex.
inversion_clear red_redex; [idtac|inversion_clear H0|idtac].
trivial.
apply IHm; trivial.
apply clos_red with (subst u m); trivial.
unfold subst; auto with coc.
apply IHu; auto with coc.
apply clos_red with (subst u m); trivial.
unfold subst; auto with coc.
Qed.
Definition eq_cand (X Y:CR) := ∀ t : term, X t <-> Y t.
Hint Unfold eq_cand: coc.
Lemma eq_cand_incl : ∀ t X Y, eq_cand X Y -> X t -> Y t.
Proof.
intros.
elim H with t; auto with coc.
Qed.
Definition Inter (X:Type) (F:X->CR) t :=
sn t /\ ∀ x, F x t.
Lemma eq_can_Inter :
∀ X Y (F:X->term->Prop) (G:Y->term->Prop),
(∀ x, exists y, eq_cand (F x) (G y)) /\
(∀ y, exists x, eq_cand (F x) (G y)) ->
eq_cand (Inter _ F) (Inter _ G).
unfold eq_cand, Inter; intros.
destruct H.
split; intros.
destruct H1; split; trivial; intros.
destruct (H0 x).
rewrite <- H3; trivial.
destruct H1; split; trivial; intros.
destruct (H x).
rewrite H3; trivial.
Qed.
Lemma is_can_Inter :
∀ X F, (∀ x:X, is_cand (F x)) -> is_cand (Inter X F).
unfold Inter; intros.
constructor.
destruct 1; trivial.
intros.
destruct H0.
split; intros.
apply sn_red_sn with t; trivial.
apply (clos_red _ (H x)) with t; auto.
split; intros.
constructor; intros.
destruct (H1 y); trivial.
apply (clos_exp _ (H x)); intros; trivial.
destruct (H1 u); trivial.
Qed.
Lemma is_can_Inter' :
∀ X F, (∀ x:X, is_cand (fun t => sn t /\ F x t)) -> is_cand (Inter X F).
unfold Inter; intros.
constructor.
destruct 1; trivial.
intros.
destruct H0.
split; intros.
apply sn_red_sn with t; trivial.
apply (clos_red _ (H x)) with t; auto.
split; intros.
constructor; intros.
destruct (H1 y); trivial.
apply (clos_exp _ (H x)); intros; trivial.
destruct (H1 u); auto.
Qed.
Lemma is_can_weak : ∀ X,
is_cand X -> is_cand (fun t => sn t /\ X t).
intros.
generalize H.
apply is_cand_morph; red; intros.
split; intros.
apply H0.
split; trivial.
apply (incl_sn X); trivial.
Qed.
Definition Neu : CR := fun t =>
sn t /\ exists2 u, red t u & nf u /\ neutral u.
Lemma neutral_is_cand : is_cand Neu.
split; intros.
destruct H; trivial.
destruct H.
destruct H1.
split.
apply sn_red_sn with t; auto with coc.
exists x; trivial.
destruct H2.
elim confluence with (1:=H1) (2:=H0); intros.
replace x with x0; trivial.
revert H2; elim H4; trivial; intros.
rewrite H6 in H7; trivial.
elim nf_norm with (2:=H7); trivial.
assert (sn t).
constructor; intros.
destruct (H0 y); auto.
split; trivial.
destruct (red1_dec t).
destruct s.
specialize H0 with (1:=r).
destruct H0.
destruct H2.
exists x0; trivial.
transitivity x; auto with coc.
exists t; auto with *.
Qed.
Section Completion.
Variable P : term -> Prop.
Definition compl : CR :=
fun t => ∀ C, is_cand C -> (∀ u, sn u -> P u -> C u) -> C t.
Lemma is_can_compl : is_cand compl.
split.
intros.
apply (H sn); auto.
apply cand_sn.
red; intros.
apply (clos_red C) with t; auto.
apply (H C); trivial.
red; intros.
apply (clos_exp C); trivial; intros.
apply H0; trivial.
Qed.
Lemma compl_intro : ∀ t, sn t -> P t -> compl t.
red; intros; auto.
Qed.
Lemma compl_elim : ∀ t,
compl t ->
(exists2 u, conv t u & compl u /\ P u) \/ Neu t.
intros.
apply (@proj2 (sn t)).
apply H; intros.
split; intros.
destruct H0; trivial.
destruct H0.
split.
apply sn_red_sn with t0; trivial.
destruct H2.
left.
destruct H2.
exists x; trivial.
apply trans_conv_conv with t0; auto.
apply red_sym_conv; trivial.
right.
apply (clos_red Neu) with t0; trivial.
apply neutral_is_cand.
split.
constructor; intros.
destruct (H1 y); auto.
assert ((exists u, red1 t0 u) \/ normal t0).
destruct (red1_dec t0).
destruct s as (u,?); left; exists u; trivial.
right; red; intros; apply nf_norm; trivial.
destruct H2.
destruct H2.
destruct (H1 x); auto.
destruct H4.
left.
destruct H4.
exists x0; trivial.
apply trans_conv_conv with x; trivial.
apply red_conv; auto with coc.
right.
destruct H4.
destruct H5.
split.
constructor; intros; apply H1; trivial.
exists x0; trivial.
apply red_trans with x; auto.
apply one_step_red; auto.
right.
split.
constructor; intros.
elim (H2 y); trivial.
exists t0; auto with *.
split; trivial.
apply nf_sound; trivial.
split; trivial.
left.
exists u.
constructor.
split; trivial.
red; auto.
Qed.
End Completion.
Lemma eq_can_compl : ∀ X Y,
eq_cand X Y -> eq_cand (compl X) (compl Y).
unfold eq_cand; simpl; split; intros.
red; intros.
apply (H0 C); trivial; intros.
rewrite H in H4; auto.
red; intros.
apply (H0 C); trivial; intros.
rewrite <- H in H4; auto.
Qed.
Definition Arr (X Y:CR) : CR :=
fun t => ∀ u, X u -> Y (App t u).
Lemma eq_can_Arr :
∀ X1 Y1 X2 Y2,
eq_cand X1 X2 -> eq_cand Y1 Y2 -> eq_cand (Arr X1 Y1) (Arr X2 Y2).
unfold eq_cand, Arr; split; intros.
rewrite <- H0; rewrite <- H in H2; auto.
rewrite H0; rewrite H in H2; auto.
Qed.
Lemma weak_cand_Arr : ∀ (X Y:CR),
weak_cand X ->
is_cand Y ->
is_cand (Arr X Y).
unfold Arr in |- *; intros X Y Hne Y_cand.
constructor.
intros t app_in_can.
destruct (wk_wit _ Hne) as (w,?).
apply subterm_sn with (App t w); auto with coc.
apply (incl_sn Y); auto with coc.
intros.
apply (clos_red Y) with (App t u0); auto with coc.
intros t t_neutr clos_exp_t u u_in_X.
apply (clos_exp Y); auto with coc.
exact I.
generalize u_in_X.
assert (u_sn: sn u).
apply (wk_sn X); auto with coc.
clear u_in_X.
elim u_sn.
intros v _ v_Hrec v_in_X w red_w.
revert t_neutr.
inversion_clear red_w; intros; auto with coc.
destruct t_neutr.
apply (clos_exp Y); intros; auto with coc.
exact I.
apply v_Hrec with N2; auto with coc.
apply (wk_red X) with v; auto with coc.
Qed.
Lemma weak_Abs_sound_Arr :
∀ (X Y:CR) m,
(∀ t, X t -> sn t) ->
is_cand Y ->
(∀ n, X n -> Y (subst n m)) ->
Arr X Y (Abs m).
unfold Arr in |- *; intros.
apply (clos_exp Y); intros; auto with coc.
exact I.
apply clos_red with (App (Abs m) u); auto with coc.
apply (cand_sat Y); auto with coc.
Qed.
Lemma is_cand_Arr :
∀ X Y, is_cand X -> is_cand Y -> is_cand (Arr X Y).
intros.
apply weak_cand_Arr; trivial.
apply weaker_cand; trivial.
Qed.
Lemma Abs_sound_Arr :
∀ X Y m,
is_cand X ->
is_cand Y ->
(∀ n, X n -> Y (subst n m)) ->
Arr X Y (Abs m).
unfold Arr in |- *; intros.
apply (clos_exp Y); intros; auto with coc.
exact I.
apply clos_red with (App (Abs m) u); auto with coc.
apply (cand_sat Y); auto with coc.
right; apply (incl_sn X); auto with coc.
Qed.
Definition Pi (X:CR) (Y:term->CR) : CR :=
fun t => ∀ u u', conv u' u -> X u -> X u' -> Y u' (App t u).
Lemma eq_can_Pi :
∀ X1 X2 (Y1 Y2:term->CR),
eq_cand X1 X2 ->
(∀ u, eq_cand (Y1 u) (Y2 u)) ->
eq_cand (Pi X1 Y1) (Pi X2 Y2).
unfold eq_cand, Pi; split; intros.
rewrite <- H0; rewrite <- H in H3,H4; auto.
rewrite H0; rewrite H in H3,H4; auto.
Qed.
Lemma is_cand_Pi : ∀ X (Y:term->CR),
is_cand X ->
(∀ u, is_cand (Y u)) ->
is_cand (Pi X Y).
unfold Pi in |- *; intros X Y X_can Y_can.
constructor.
intros t app_in_can.
apply subterm_sn with (App t (Ref 0)); auto with coc.
apply (incl_sn (Y (Ref 0))); auto with coc.
apply app_in_can; auto with coc.
apply var_in_cand with (X:=X); auto with coc.
apply var_in_cand with (X:=X); auto with coc.
intros.
apply (clos_red (Y u')) with (App t u0); auto with coc.
intros t t_neutr clos_exp_t u u' redu u_in_X u'_in_X.
apply (clos_exp (Y u')); auto with coc.
exact I.
assert (u_sn: sn u).
apply (incl_sn X); auto with coc.
revert u' redu u_in_X u'_in_X.
elim u_sn.
intros v _ v_Hrec u' redu v_in_X u'_in_X w red_w.
revert t_neutr.
inversion_clear red_w; intros; auto with coc.
destruct t_neutr.
apply (clos_exp (Y u')); intros; auto with coc.
exact I.
apply v_Hrec with N2; eauto with coc.
apply (clos_red X) with v; auto with coc.
Qed.
Lemma Abs_sound_Pi :
∀ X Y m,
is_cand X ->
(∀ u, is_cand (Y u)) ->
(∀ n n', X n -> X n' -> conv n' n -> Y n' (subst n m)) ->
Pi X Y (Abs m).
unfold Pi in |- *; intros.
apply (clos_exp (Y u')); intros; auto with coc.
exact I.
apply clos_red with (App (Abs m) u); auto with coc.
apply (cand_sat (Y u')); auto with coc.
right; apply (incl_sn X); auto with coc.
Qed.
Definition Union (X Y:CR) : CR := compl (fun t => X t \/ Y t).
Lemma eq_can_union : ∀ X Y X' Y',
eq_cand X X' -> eq_cand Y Y' ->
eq_cand (Union X Y) (Union X' Y').
unfold Union; intros.
apply eq_can_compl.
red; intros.
red in H, H0.
rewrite H; rewrite H0; reflexivity.
Qed.
Lemma is_cand_union : ∀ X Y, is_cand (Union X Y).
unfold Union; intros.
apply is_can_compl.
Qed.
Lemma is_cand_union1 : ∀ (X Y:CR) t,
is_cand X -> X t -> Union X Y t.
red; red; intros.
apply H2; auto.
apply (incl_sn X); trivial.
Qed.
Lemma is_cand_union2 : ∀ (X Y:CR) t,
is_cand Y -> Y t -> Union X Y t.
red; red; intros.
apply H2; auto.
apply (incl_sn Y); trivial.
Qed.
Lemma cand_context : ∀ u u' v,
(∀ X, is_cand X -> X u -> X u') ->
∀ X, is_cand X -> X (App u v) -> X (App u' v).
intros.
assert (sn v).
apply subterm_sn with (App u v); auto.
apply (incl_sn X); trivial.
assert (Arr (weak_chain v) X u').
apply H.
apply weak_cand_Arr; trivial.
apply weakest_cands; trivial.
red; intros.
apply (clos_red X) with (App u v); auto with *.
red in H3.
apply H3; auto with *.
Qed.
Lemma cand_sat1 X m u v :
is_cand X ->
boccur 0 m = true \/ sn u ->
X (App (subst u m) v) ->
X (App2 (Abs m) u v).
intros.
apply cand_context with (X:=X) (u:=subst u m); intros; auto.
apply cand_sat with (X:=X0); trivial.
Qed.
Lemma cand_sat2 X m u v w :
is_cand X ->
boccur 0 m = true \/ sn u ->
X (App2 (subst u m) v w) ->
X (App2 (App (Abs m) u) v w).
intros.
apply cand_context with (X:=X) (u:=App (subst u m) v); intros; auto.
apply cand_sat1 with (X:=X0); trivial.
Qed.
Lemma cand_sat3 X m u v w x :
is_cand X ->
boccur 0 m = true \/ sn u ->
X (App2 (App (subst u m) v) w x) ->
X (App2 (App2 (Abs m) u v) w x).
intros.
apply cand_context with (X:=X) (u:=App2 (subst u m) v w); intros; auto.
apply cand_sat2 with (X:=X0); trivial.
Qed.