cbneed.v

From mathcomp Require Import all_ssreflect.

Notation var := nat.
Notation pos := nat.

Inductive term :=
  | Var of var & pos
  | App of term & term
  | Lam of term
  | Let of seq term & term.

Definition term_rect'
  (P : term -> Type)
  (HVar : forall i j, P (Var i j))
  (HApp : forall t1, P t1 -> forall t2, P t2 -> P (App t1 t2))
  (HLam : forall t, P t -> P (Lam t))
  (HLet : forall ts, foldr (fun t => prod (P t)) unit ts -> forall t, P t -> P (Let ts t)) :=
  fix term_ind t :=
    match t as t0 return P t0 with
    | Var _ _ => HVar _ _
    | App t1 t2 => HApp _ (term_ind t1) _ (term_ind t2)
    | Lam t => HLam _ (term_ind t)
    | Let ts t => HLet _ ((fix term_ind' ts :=
        match ts as ts0 return foldr (fun t => prod (P t)) unit ts0 with
        | nil => tt
        | t :: ts => pair (term_ind t) (term_ind' ts)
        end) ts) _ (term_ind t)
    end.

Fixpoint encode t :=
  match t with
  | Var i j =>   GenTree.Leaf (i, j)
  | App t1 t2 => GenTree.Node 0 [:: encode t1; encode t2]
  | Lam t =>     GenTree.Node 1 [:: encode t]
  | Let ts t =>  GenTree.Node 2 (encode t :: map encode ts)
  end.

Fixpoint decode t :=
  match t with
  | GenTree.Leaf (i, j) => Some (Var i j)
  | GenTree.Node 0 [:: t1'; t2'] =>
      if decode t1' is Some t1 then omap (App t1) (decode t2')
      else None
  | GenTree.Node 1 [:: t'] => omap Lam (decode t')
  | GenTree.Node 2 (t' :: ts') => omap (Let (pmap decode ts')) (decode t')
  | GenTree.Node _ _ => None
  end.

Lemma codeK : pcancel encode decode.
Proof.
  elim /term_rect' => /= [ | ? -> ? -> | ? -> | ts IHts t -> ] //=.
  congr (Some (Let _ t)).
  elim: ts IHts => /= [ | ? ? IHIH [ -> ? ] ] //=.
  by rewrite IHIH.
Qed.

Definition term_eqMixin := PcanEqMixin codeK.
Canonical term_eqType := Eval hnf in EqType _ term_eqMixin.

Definition term_ind'
  (P : term -> Prop)
  (HVar : forall i j, P (Var i j))
  (HApp : forall t1, P t1 -> forall t2, P t2 -> P (App t1 t2))
  (HLam : forall t, P t -> P (Lam t))
  (HLet : forall ts, { in ts, forall t, P t } -> forall t, P t -> P (Let ts t))
  : forall t, P t.
Proof.
  elim /term_rect' => [ | | | ts IHts ] //=.
  apply: HLet.
  elim: ts IHts => /= [ ? ? | ? ? IHts [ ? ? ] ? ].
  - by rewrite in_nil.
  - rewrite in_cons.
    move /orP => [ /eqP -> // | ].
    by apply IHts.
Qed.

Definition upren r i :=
  if i is i.+1 then (r i).+1 else 0.

Lemma eq_upren r r' : r =1 r' -> upren r =1 upren r'.
Proof. move => ? [ | ? ] //=. by congr (_ .+1). Qed.
Hint Resolve eq_upren.

Fixpoint rename r t :=
  match t with
  | Var i j => Var (r i) j
  | App t1 t2 => App (rename r t1) (rename r t2)
  | Lam t => Lam (rename (upren r) t)
  | Let ts t => Let (map (rename (upren r)) ts) (rename (upren r) t)
  end.

Theorem eq_rename r r' : r =1 r' -> rename r =1 rename r'.
Proof.
  move => Heq t.
  elim /term_ind' : t r r' Heq => /=; intros; f_equal; eauto.
  apply /eq_in_map => ? ?. eauto.
Qed.

Definition up s i :=
  if i is i.+1 then rename succn \o s i else Var 0.

Lemma eq_up s s' : s =2 s' -> up s =2 up s'.
Proof.
  move => ? [ | ? ? ] //=.
  by congr (rename succn _).
Qed.
Hint Resolve eq_up.

Fixpoint subst s t :=
  match t with
  | Var i j => s i j
  | App t1 t2 => App (subst s t1) (subst s t2)
  | Lam t => Lam (subst (up s) t)
  | Let ts t => Let (map (subst (up s)) ts) (subst (up s) t)
  end.

Theorem eq_subst s s' : s =2 s' -> subst s =1 subst s'.
Proof.
  move => Heq t.
  elim /term_ind' : t s s' Heq => /=; intros; f_equal; eauto.
  apply /eq_in_map => ? ?. eauto.
Qed.

Theorem rename_subst : forall r, rename r =1 subst (Var \o r).
Proof.
  have ? : forall t,
    (forall r, rename r t = subst (Var \o r) t) ->
    (forall r, rename (upren r) t = subst (up (Var \o r)) t).
  { move => ? ? r.
    rewrite -(eq_subst (Var \o upren r)) => [ | [ | ? ] ? ] //=. }
  move => r t.
  elim /term_ind': t r => /=; intros; f_equal; eauto.
  apply /eq_in_map => ? ?. eauto.
Qed.

Theorem subst_id t : subst Var t = t.
  have ? : forall t, subst Var t = t -> subst (up Var) t = t.
  { move => ?.
    rewrite -(eq_subst (up Var)) => [ | [ | ? ] ? ] //=. }
  elim /term_ind': t => /=; intros; f_equal; eauto.
  apply: map_id_in => ? ?. eauto.
Qed.

Lemma subst_rename_comp : forall r s, subst s \o rename r =1 subst (s \o r).
Proof.
  have ? : forall t,
    (forall r s, subst s (rename r t) = subst (s \o r) t) ->
    (forall r s, subst (up s) (rename (upren r) t) = subst (up (s \o r)) t).
  { move => ? ? r s.
    rewrite (eq_subst (up (s \o r)) (up s \o upren r)) => [ | [ | ? ] ? ] //=. }
  move => r s t.
  elim /term_ind': t r s => /=; intros; f_equal; eauto.
  rewrite -map_comp.
  apply /eq_in_map => ? ?. eauto.
Qed.

Lemma rename_rename_comp : forall r r', rename r \o rename r' =1 rename (r \o r').
Proof.
  have ? : forall t,
    (forall r r', rename r (rename r' t) = rename (r \o r') t) ->
    (forall r r', rename (upren r) (rename (upren r') t) = rename (upren (r \o r')) t).
  { move => ? ? r r'.
    rewrite (eq_rename (upren (r \o r')) (upren r \o upren r')) => [ | [ | ? ] ] //=. }
  move => r r' t.
  elim /term_ind': t r r' => /=; intros; f_equal; eauto.
  rewrite -map_comp.
  apply /eq_in_map => ? ?. eauto.
Qed.

Lemma rename_subst_comp :
  forall r s, rename r \o subst s =1 subst (fun i j => rename r (s i j)).
Proof.
  have ? : forall t,
    (forall r s, rename r (subst s t) = subst (fun i j => rename r (s i j)) t) ->
    (forall r s, rename (upren r) (subst (up s) t) = subst (up (fun i j => rename r (s i j))) t).
  { move => ? ? r s.
    rewrite (eq_subst (up (fun i j => rename r (s i j))) (fun i j => rename (upren r) (up s i j))) => [ | [ | ? ] ? ] //=.
    by etransitivity; [ | symmetry ]; apply: rename_rename_comp. }
  move => r s t.
  elim /term_ind': t r s => /=; intros; f_equal; eauto.
  rewrite -map_comp.
  apply /eq_in_map => ? ?. eauto.
Qed.

Theorem subst_comp :
  forall s s', subst s \o subst s' =1 subst (fun i j => subst s (s' i j)).
Proof.
  have ? : forall t,
    (forall s s', subst s (subst s' t) = subst (fun i j => subst s (s' i j)) t) ->
    (forall s s', subst (up s) (subst (up s') t) = subst (up (fun i j => subst s (s' i j))) t).
  { move => ? ? s s'.
    rewrite (eq_subst (up (fun i j => subst s (s' i j))) (fun i j => subst (up s) (up s' i j))) => [ | [ | ? ] ? ] //=.
    etransitivity; [ apply rename_subst_comp | symmetry; apply subst_rename_comp ]. }
  move => s s' t /=.
  elim /term_ind': t s s' => /=; intros; f_equal; eauto.
  rewrite -map_comp.
  apply /eq_in_map => ? ?. eauto.
Qed.

Inductive value : term -> Prop := value_lam t : value (Lam t).

Inductive answer : term -> Prop :=
| answer_lam t : answer (Lam t)
| answer_let ts a :
    answer a ->
    answer (Let ts a).

Inductive demand : var -> pos -> term -> Prop :=
| demand_var i j : demand i j (Var i j)
| demand_app i j t1 t2 :
    demand i j t1 ->
    demand i j (App t1 t2)
| demand_letL i j k ts t :
    demand 0 i t ->
    demand_rec i j.+1 k ts ->
    demand j k (Let ts t)
| demand_letR i j ts t :
    demand i.+1 j t ->
    demand i j (Let ts t)
with demand_rec : pos -> var -> pos -> list term -> Prop :=
| demand_rec_fin i j k t ts :
    demand j k t ->
    nth (Var 0 i) ts i = t ->
    demand_rec i j k ts
| demand_rec_cont i j k l t ts :
    demand_rec i 0 j ts ->
    nth (Var 0 j) ts j = t ->
    demand k l t ->
    demand_rec i k l ts.

Definition subst_single i j t k l :=
  if (i == k) && (j == l) then t else Var k l.

Inductive reassoc : term -> term -> Prop :=
| reassoc_app t1 t1' t2 :
    reassoc t1 t1' ->
    reassoc (App t1 t2) (App t1' t2)
| reassoc_letL i t1 t1' t1s t1s' t2 :
    demand 0 i t2 ->
    nth (Var 0 i) t1s i = t1 ->
    reassoc t1 t1' ->
    set_nth (Var 0 i) t1s i t1' = t1s' ->
    reassoc (Let t1s t2) (Let t1s' t2)
| reassoc_letL_env i j t1 t1' t1s t1s' t2 :
    demand 0 i t2 ->
    demand_rec i 0 j t1s ->
    nth (Var 0 j) t1s j = t1 ->
    reassoc t1 t1' ->
    set_nth (Var 0 j) t1s j t1' = t1s' ->
    reassoc (Let t1s t2) (Let t1s' t2)
| reassoc_letR ts t t' :
    reassoc t t' ->
    reassoc (Let ts t) (Let ts t')
| reassoc_lift t11s t12 t2 :
    reassoc (App (Let t11s t12) t2) (Let t11s (App t12 t2))
| reassoc_deref i t1s v1 t2 t2' :
    value v1 ->
    demand 0 i t2 ->
    nth (Var 0 i) t1s i = v1 ->
    subst (subst_single 0 i v1) t2 = t2' ->
    reassoc (Let t1s t2) (Let t1s t2')
| reassoc_deref_env i j t1s t1s' t1 v1 t2 :
    value v1 ->
    demand 0 i t2 ->
    demand 0 j t1 ->
    nth (Var 0 i) t1s i = t1 ->
    nth (Var 0 j) t1s j = v1 ->
    set_nth (Var 0 i) t1s i v1 = t1s' ->
    reassoc (Let t1s t2) (Let t1s' t2)
| reassoc_deref_env' i j k t1s t1s' t1 v1 t2 :
    value v1 ->
    demand 0 i t2 ->
    demand 0 k t1 ->
    nth (Var 0 j) t1s j = t1 ->
    nth (Var 0 k) t1s k = v1 ->
    demand_rec i 0 j t1s ->
    set_nth (Var 0 j) t1s j v1 = t1s' ->
    reassoc (Let t1s t2) (Let t1s' t2)
| reassoc_assoc i t1s t1s' t2s a1 t2 :
    answer a1 ->
    demand 0 i t2 ->
    nth (Var 0 i) t1s i = Let t2s a1 ->
    set_nth (Var 0 i) t1s i a1 ++ map (subst (fun i j => if i is i'.+1 then Var i' j else Var 0 (size t1s + j))) t2s = t1s' ->
    reassoc (Let t1s t2) (Let t1s' t2)
| reassoc_assoc_env i j t1s t1s' t2s a1 t2 :
    answer a1 ->
    demand 0 i t2 ->
    demand_rec i 0 j t1s ->
    nth (Var 0 j) t1s j = Let t2s a1 ->
    set_nth (Var 0 i) t1s i a1 ++ map (subst (fun i j => if i is i'.+1 then Var i' j else Var 0 (size t1s + j))) t2s = t1s' ->
    reassoc (Let t1s t2) (Let t1s' t2).

Inductive reduce : term -> term -> Prop :=
| reduce_app t1 t1' t2 :
    reduce t1 t1' ->
    reduce (App t1 t2) (App t1' t2)
| reduce_letL i t1 t1' t1s t1s' t2 :
    demand 0 i t2 ->
    nth (Var 0 i) t1s i = t1 ->
    reduce t1 t1' ->
    set_nth (Var 0 i) t1s i t1' = t1s' ->
    reduce (Let t1s t2) (Let t1s' t2)
| reduce_letL_env i j t1 t1' t1s t1s' t2 :
    demand 0 i t2 ->
    demand_rec i 0 j t1s ->
    nth (Var 0 j) t1s j = t1 ->
    reduce t1 t1' ->
    set_nth (Var 0 j) t1s j t1' = t1s' ->
    reduce (Let t1s t2) (Let t1s' t2)
| reduce_letR ts t t' :
    reduce t t' ->
    reduce (Let ts t) (Let ts t')
| reduce_beta t1 t2 :
    reduce (App (Lam t1) t2) (Let [:: rename succn t2] t1).
      
Inductive blackhole : term -> Prop :=
| blackhole_app t1 t2 :
    blackhole t1 ->
    blackhole (App t1 t2)
| blackhole_letL i t1 t1s t2 :
    demand 0 i t2 ->
    nth (Var 0 i) t1s i = t1 ->
    blackhole t1 ->
    blackhole (Let t1s t2)
| blackhole_letL_env i j t1 t1s t2 :
    demand 0 i t2 ->
    demand_rec i 0 j t1s ->
    nth (Var 0 j) t1s j = t1 ->
    blackhole t1 ->
    blackhole (Let t1s t2)
| blackhole_letR ts t :
    blackhole t ->
    blackhole (Let ts t)
| blackhole_cycle i t1s t2 :
    demand 0 i t2 ->
    demand_rec i 0 i t1s ->
    blackhole (Let t1s t2)
| blackhole_cycle_env i j t1s t2 :
    demand 0 i t2 ->
    demand_rec i 0 j t1s ->
    demand_rec j 0 j t1s ->
    blackhole (Let t1s t2).

Hint Constructors value answer demand demand_rec reassoc reduce blackhole.

Lemma determinacy : forall t,
  answer t \/
  blackhole t \/
  (exists i j, demand i j t) \/
  (exists t', reassoc t t') \/
  (exists t', reduce t t').
Proof.
  elim /term_ind' =>
  [
  | ?
      [ Hanswer1
      | [ 
        | [ [ ? [ ] ]
          | [ [ ]
            | [ ] ] ] ] ] 
  |
  | ts IHts t
       [ ?
       | [ ?
         | [ [ [ | ? ] [ i ? ] ]
           | [ [ ? ? ]
             | [ ? ? ] ] ] ] ] ];
    try inversion Hanswer1; subst; eauto 7.
  case: (leqP (size ts) i) => [ ? | Hbound ].
  { suff : demand_rec i 0 i ts; eauto.
    apply: demand_rec_fin; [ | reflexivity ].
    by rewrite nth_default. }
  case: (IHts _ (mem_nth (Var 0 i) Hbound)) =>
  [ Hanswer
  | [ ?
    | [ [ [ | ? ] [ j ? ] ]
      | [ [ ] | [ ] ] ] ] ]; try inversion Hanswer; eauto 8.
  have determinacy_inner : forall n (A : { set 'I_(size ts) }) j k,
    #|A| = n ->
    { in ~: A , forall j : 'I_(size ts),
        (i = j \/ demand_rec i 0 j ts) /\ demand_rec j 0 k ts } ->
    i = j \/ demand_rec i 0 j ts ->
    demand 0 k (nth (Var 0 j) ts j) ->
    answer (Let ts t) \/
    blackhole (Let ts t) \/
    (exists i j, demand i j (Let ts t)) \/
    (exists t', reassoc (Let ts t) t') \/
    (exists t', reduce (Let ts t) t').
  { elim => [ | n IHn ] A j_ k /=;
      (case: (leqP (size ts) k) => [ ? | Hbound_ ];
        [ suff : demand_rec k 0 k ts;
          [ move => ? ? ? [ <- | ]; eauto 
          | by apply: demand_rec_fin; [ | reflexivity ]; rewrite nth_default ] | ]).
    - move /cards0_eq => ->.
      rewrite setC0 => HA.
      move: (HA (Ordinal Hbound_) (in_setT _)) => /= [ [ <- | ] ]; eauto.
    - move: (in_setT (Ordinal Hbound_)).
      rewrite -(setUCr A) in_setU.
      move /orP => [ Hin | Hnotin ] Hcard HA.
      + case: (IHts _ (mem_nth (Var 0 k) Hbound_)) =>
        [ Hanswer [ <- | ? ]
        | [ ? [ <- | ? ]
          | [ [ [ [ l ? ] | ? [ l ? ] [ <- | ? ] ] ]
            | [ [ ? ? ] [ <- | ? ]
              | [ ? ? ] [ <- | ? ] ] ] ] ]; try inversion Hanswer; eauto 9.
        move => Hdemand ?.
        apply (IHn (A :\ Ordinal Hbound_) k l); eauto.
        * move: Hcard. rewrite (cardsD1 (Ordinal Hbound_) A) Hin.
          by inversion 1.
        * rewrite setCD => x.
          move /setUP => [ Hin_ | /set1P -> /= ].
          -- case: (HA _ Hin_) => [ [ <- | ] ]; eauto.
          -- case: Hdemand => [ -> | ]; eauto.
        * case: Hdemand => [ -> | ]; eauto.
      + move: (HA _ Hnotin) => /= [ [ <- | ] ]; eauto. }
  apply (determinacy_inner (size ts) setT i j); eauto.
  - by rewrite cardsT card_ord.
  - move => ?. rewrite setCT in_set0. inversion 1.
Qed.