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).

  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.

  Lemma cand_sn : is_cand sn.

  Hint Resolve incl_sn cand_sn: coc.

  Lemma var_in_cand : ∀ n X, is_cand X -> X (Ref n).

  Lemma weaker_cand : ∀ X, is_cand X -> weak_cand X.

  Lemma sat1_in_cand : ∀ n X u,
    is_cand X -> sn u -> X (App (Ref n) u).

  Lemma cand_sat X m u :
    is_cand X ->
    boccur 0 m=true \/ sn u ->
    X (subst u m) ->
    X (App (Abs m) u).


  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.


  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).

  Lemma is_can_Inter :
    ∀ X F, (∀ x:X, is_cand (F x)) -> is_cand (Inter X F).

  Lemma is_can_Inter' :
    ∀ X F, (∀ x:X, is_cand (fun t => sn t /\ F x t)) -> is_cand (Inter X F).

  Lemma is_can_weak : ∀ X,
    is_cand X -> is_cand (fun t => sn t /\ X t).


  Definition Neu : CR := fun t =>
    sn t /\ exists2 u, red t u & nf u /\ neutral u.

Lemma neutral_is_cand : is_cand Neu.


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.

  Lemma compl_intro : ∀ t, sn t -> P t -> compl t.

  Lemma compl_elim : ∀ t,
    compl t ->
    (exists2 u, conv t u & compl u /\ P u) \/ Neu t.

End Completion.

  Lemma eq_can_compl : ∀ X Y,
    eq_cand X Y -> eq_cand (compl X) (compl Y).


  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).

  Lemma weak_cand_Arr : ∀ (X Y:CR),
    weak_cand X ->
    is_cand Y ->
    is_cand (Arr X Y).

  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).

  Lemma is_cand_Arr :
   ∀ X Y, is_cand X -> is_cand Y -> is_cand (Arr X Y).

  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).


  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).

  Lemma is_cand_Pi : ∀ X (Y:term->CR),
   is_cand X ->
   (∀ u, is_cand (Y u)) ->
   is_cand (Pi X Y).

  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).


  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').

  Lemma is_cand_union : ∀ X Y, is_cand (Union X Y).

 Lemma is_cand_union1 : ∀ (X Y:CR) t,
   is_cand X -> X t -> Union X Y t.

 Lemma is_cand_union2 : ∀ (X Y:CR) t,
   is_cand Y -> Y t -> Union X Y t.


  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).

  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).

  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).

  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).