Library Can
Require Export Lambda.
Hint Unfold iff: core.
Definition neutral t := forall v, t <> Abs v.
Definition CR := term -> Prop.
Record is_cand (X : CR) : Prop :=
{incl_sn : forall t, X t -> sn t;
clos_red : forall t u, X t -> red t u -> X u;
clos_exp : forall t, neutral t -> (forall u, red1 t u -> X u) -> X t}.
Lemma cand_sn : is_cand sn.
Hint Resolve cand_sn: coc.
Lemma var_in_cand : forall n X, is_cand X -> X (Ref n).
Lemma cand_sat :
forall X, is_cand X ->
forall u, sn u ->
forall m, X (subst u m) ->
X (App (Abs m) u).
Definition eq_cand (X Y:CR) := forall t : term, X t <-> Y t.
Hint Unfold eq_cand: coc.
Lemma eq_cand_incl : forall t X Y, eq_cand X Y -> X t -> Y t.
Section Completion.
Variable P : term -> Prop.
Definition compl : CR :=
fun t => forall C, is_cand C -> (forall u, sn u -> P u -> C u) -> C t.
Lemma is_can_compl : is_cand compl.
Lemma compl_intro : forall t, sn t -> P t -> compl t.
Lemma compl_elim : forall t,
compl t ->
(exists2 u, conv t u & compl u /\ P u) \/
(forall C, is_cand C -> C t).
End Completion.
Lemma eq_can_compl : forall X Y,
eq_cand X Y -> eq_cand (compl X) (compl Y).
Definition Inter (X:Type) (F:X->CR) t :=
sn t /\ forall x, F x t.
Lemma eq_can_Inter :
forall X Y (F:X->term->Prop) (G:Y->term->Prop),
(forall x, exists y, eq_cand (F x) (G y)) /\
(forall y, exists x, eq_cand (F x) (G y)) ->
eq_cand (Inter _ F) (Inter _ G).
Lemma is_can_Inter :
forall X F, (forall x:X, is_cand (F x)) -> is_cand (Inter X F).
Definition Arr (X Y:CR) : CR :=
fun t => forall u, X u -> Y (App t u).
Lemma eq_can_Arr :
forall X1 Y1 X2 Y2,
eq_cand X1 X2 -> eq_cand Y1 Y2 -> eq_cand (Arr X1 Y1) (Arr X2 Y2).
Lemma is_cand_Arr :
forall X Y, is_cand X -> is_cand Y -> is_cand (Arr X Y).
Lemma Abs_sound_Arr :
forall X Y m,
is_cand X ->
is_cand Y ->
(forall n, X n -> Y (subst n m)) ->
Arr X Y (Abs m).
Definition Pi (X:CR) (Y:term->CR) : CR :=
fun t => forall u u', conv u' u -> X u -> X u' -> Y u' (App t u).
Lemma eq_can_Pi :
forall X1 X2 (Y1 Y2:term->CR),
eq_cand X1 X2 ->
(forall u, eq_cand (Y1 u) (Y2 u)) ->
eq_cand (Pi X1 Y1) (Pi X2 Y2).
Lemma is_cand_Pi : forall X (Y:term->CR),
is_cand X ->
(forall u, is_cand (Y u)) ->
is_cand (Pi X Y).
Lemma Abs_sound_Pi :
forall X Y m,
is_cand X ->
(forall u, is_cand (Y u)) ->
(forall n n', X n -> X n' -> conv n' n -> Y n' (subst n m)) ->
Pi X Y (Abs m).
Definition Union (X Y:CR) : CR := compl (fun t => X t \/ Y t).
Lemma eq_can_union : forall X Y X' Y',
eq_cand X X' -> eq_cand Y Y' ->
eq_cand (Union X Y) (Union X' Y').
Lemma is_cand_union : forall X Y, is_cand (Union X Y).
Lemma is_cand_union1 : forall (X Y:CR) t,
is_cand X -> X t -> Union X Y t.
Lemma is_cand_union2 : forall (X Y:CR) t,
is_cand Y -> Y t -> Union X Y t.