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.