Typing and Reduction Relation in PCF2

From Coq Require Import Lia List Init.Nat PeanoNat.
Require Import PCF2.preliminaries.
From PCF2.external.Synthetic Require Import Definitions DecidabilityFacts.
From PCF2.Autosubst Require Import unscoped pcf_2.
Set Default Goal Selector "!".

Infix "⟶" := Fun (at level 30, right associativity).

Inductive step: tm -> tm -> Prop :=
| Beta e e': step (app (lam e) e') (Subst_tm (scons e' ids) e)
| AppL e1 e1' e2: step e1 e1' -> step (app e1 e2) (app e1' e2)
| AppR e1 e2 e2': step e2 e2' -> step (app e1 e2) (app e1 e2')
| Lam e e': step e e' -> step (lam e) (lam e')
| If1 e1 e1' e2 e3: step e1 e1' -> step (trny e1 e2 e3) (trny e1' e2 e3)
| If2 e1 e2 e2' e3: step e2 e2' -> step (trny e1 e2 e3) (trny e1 e2' e3)
| If3 e1 e2 e3 e3': step e3 e3' -> step (trny e1 e2 e3) (trny e1 e2 e3')
| IfT e1 e2: step (trny tt e1 e2) e1
| IfF e1 e2: step (trny ff e1 e2) e2
| IfB e1 e2: step (trny bot e1 e2) bot
| If_nested e1 e2 e3 e4 e5: step (trny (trny e1 e2 e3) e4 e5) (trny e1 (trny e2 e4 e5) (trny e3 e4 e5)).

Notation " s ≻ t" := (step s t) (at level 50, t at next level).

Definition context: Type := list(ty).

Inductive typed: context -> tm -> ty -> Prop :=
| tt_typed Γ: typed Γ tt Base
| ff_typed Γ: typed Γ ff Base
| bot_typed Γ: typed Γ bot Base
| var_typed n A Γ: nth_error Γ n = Some A -> typed Γ (var_tm n) A
| fun_typed e typ1 typ2 Γ: typed (cons typ1 Γ) e typ2 -> typed Γ (lam e) (Fun typ1 typ2)
| app_typed e1 e2 typ1 typ2 Γ: typed Γ e1 (Fun typ1 typ2) -> typed Γ e2 typ1 -> typed Γ (app e1 e2) typ2
| trny_typed e1 e2 e3 Γ: typed Γ e1 Base -> typed Γ e2 Base -> typed Γ e3 Base -> typed Γ (trny e1 e2 e3) Base.

Notation "Γ ⊢ s : A" := (typed Γ s A) (at level 50, s, A at next level).

Require Import Coq.Relations.Relation_Operators.
Hint Constructors clos_refl_trans typed step : core.

Definition steps := clos_refl_trans tm step.
Hint Unfold steps : core.

Notation " s ≻* t" := (steps s t) (at level 50, t at next level).

Definition is_bval e := match e with
                      |tt => true
                      |ff => true
                      |bot => true
                      |_ => false
                      end.

Definition evaluates_to_base s s' := s ≻* s' /\ is_bval s' = true.

Notation " s ⇓ t" := (evaluates_to_base s t) (at level 50, t at next level).

Definition subst_well_typed (Γ': context) (Γ: context) (σ: nat -> tm):=
    forall n T, nth_error Γ n = Some T -> Γ' ⊢ (σ n ): T.

Definition ren_well_typed (Γ': context) (Γ: context) (r: nat -> nat):=
  forall n T, nth_error Γ n = Some T -> nth_error Γ' (r n) = Some T.

Notation " Γ' ⊢ σ [ Γ ]" := (subst_well_typed Γ' Γ σ) (at level 50, Γ, σ at next level).

Axiom weak_normalisation_comp:
  forall e, nil ⊢ e : Base -> sig (fun v => e ⇓ v).

Axiom church_rosser:
  forall s t u, s ≻* t -> s ≻* u -> exists w , t ≻* w /\ u ≻* w.

Definition embed (b: bool) :=
  match b with
  |true => tt
  |false => ff
  end.

Require Import Setoid Morphisms.

Instance steps_PreOrder : PreOrder steps.
Proof.
  split.
  - intros x. eapply rt_refl.
  - intros x y z. eapply rt_trans.
Qed.

Lemma app_left s s' t:
  s ≻* s' -> app s t ≻* app s' t.
Proof.
  induction 1; eauto.
Qed.

Lemma app_right s t t':
  t ≻* t' -> app s t ≻* app s t'.
Proof.
  induction 1; eauto.
Qed.

Instance app_proper : Proper (steps ==> steps ==> steps) app.
Proof.
  intros a b H1 c d H2.
  eapply rt_trans.
  - eapply app_left; eauto.
  - now apply app_right.
Qed.

Lemma if_cond s s' t u:
  s ≻* s' -> trny s t u ≻* trny s' t u.
Proof.
  induction 1; eauto.
Qed.

Lemma if_trm1 s t t' u:
  t ≻* t' -> trny s t u ≻* trny s t' u.
Proof.
  induction 1; eauto.
Qed.

Lemma if_trm2 s t u u':
  u ≻* u' -> trny s t u ≻* trny s t u'.
Proof.
  induction 1; eauto.
Qed.

Instance if_proper : Proper (steps ==> steps ==> steps ==> steps) trny.
Proof.
  intros a b H1 c d H2 e f H3.
  eapply rt_trans.
  - eapply if_cond; eauto.
  - eapply rt_trans.
    + eapply if_trm1; eauto.
    + now apply if_trm2.
Qed.

Instance lam_proper : Proper (steps ==> steps) lam.
Proof.
  intros a b H.
  induction H; eauto.
Qed.

Instance step_steps : subrelation step (steps).
Proof.
  intros ? ? ?. econstructor.
  eauto.
Qed.

Instance evaluates_steps : subrelation evaluates_to_base (steps).
Proof.
  firstorder.
Qed.

Lemma steps_1n s t u:
  s ≻* t -> t ≻* u -> s ≻* u.
Proof.
  intros H1 H2. now rewrite H1.
Qed.

Lemma steps_n1 s t u:
  s ≻* t -> t ≻ u -> s ≻* u.
Proof.
  intros H1 H2. now rewrite <- H2.
Qed.

Lemma step_eval s t v:
  s ≻* t -> t ⇓ v -> s ⇓ v.
Proof.
  intros; firstorder; eauto.
Qed.

Lemma val_no_step v t:
  is_bval v = true -> ~ v ≻ t.
Proof.
  intros H H'. destruct v; try easy; inv H'.
Qed.

Lemma base_eval t:
  nil ⊢ t : Base -> (t ⇓ tt ) + (t ⇓ ff ) + (t ⇓ bot ).
Proof.
  intros typed_t. destruct (weak_normalisation_comp t typed_t).
  destruct x; try firstorder; discriminate.
Qed.

Lemma bval_steps_char v t:
  is_bval v = true -> v ≻* t -> t = v.
Proof.
  intros H H1. induction H1.
  2: easy.
  - destruct x; inv H0; discriminate.
  - rewrite IHclos_refl_trans2, IHclos_refl_trans1; try easy.
    now rewrite IHclos_refl_trans1.
Qed.

Lemma eval_step s t v:
  s ≻* t -> s ⇓ v -> t ⇓ v.
Proof.
  intros H H1; firstorder.
  destruct (church_rosser s t v); eauto.
  destruct H2. erewrite (bval_steps_char v x) in H2; eauto.
Qed.

Definition closed (s: tm) := allfv_tm (fun _ => False) s.

Lemma typed_free_var Γ s A:
  Γ ⊢ s : A -> allfv_tm (fun n => exists T , nth_error Γ n = Some T) s.
Proof.
  intros typed_s. induction typed_s; firstorder.
  apply (allfvImpl_tm (fun n : nat => exists T : ty , nth_error (typ1 :: Γ) n = Some T)); eauto.
  intros n H. destruct n; eauto.
  unfold upAllfv_tm_tm. unfold up_allfv; now cbn.
Qed.

Lemma typed_empty_closed s A:
  nil ⊢ s : A -> closed s.
Proof.
  intros typed_s.
  assert (H: allfv_tm (fun n => exists T , nth_error nil n = Some T) s) by exact (typed_free_var nil s A typed_s).
  unfold closed. apply (allfvImpl_tm (fun n : nat => exists T: ty , nth_error nil n = Some T)); eauto.
  intros n H1. destruct n, H1; discriminate.
Qed.

Lemma type_weakening Γ Γ' A s:
  Γ ⊢ s : A -> (Γ ++ Γ') ⊢ s : A.
Proof.
  intros typed_Γ. induction typed_Γ; eauto.
  econstructor. induction n in Γ, H |- *.
  - destruct Γ; cbn in *; try discriminate; eauto.
  - destruct Γ.
    + discriminate.
    + cbn in *. apply IHn; eauto.
Qed.

Lemma evaluates_to_same s v v':
  s ⇓ v -> s ⇓ v' -> v = v'.
Proof.
  intros [H1 H2] [H3 H4].
  assert (H5: exists w , v ≻* w /\ v' ≻* w).
  - apply (church_rosser s); eauto.
  - destruct H5 as [x [H5 H6]].
    assert (H7: x = v) by now apply bval_steps_char.
    assert (H8: x = v') by now apply bval_steps_char.
    now subst.
Qed.

Lemma ren_preserves' Γ Γ' r e A:
  ren_well_typed Γ' Γ r -> Γ ⊢ e : A -> Γ' ⊢ (Ren_tm r e ) : A.
Proof.
  intros ren_wt typed_e. induction typed_e in r, Γ', ren_wt |- *; cbn; eauto.
  econstructor. eapply IHtyped_e. intros n T H.
  destruct n; cbn in *.
  + assumption.
  + now eapply ren_wt in H.
Qed.

Lemma ren_preserves Γ Γ' r e A:
  Γ' ⊢ core.funcomp var_tm r [ Γ ] -> Γ ⊢ e : A -> Γ' ⊢ (Ren_tm r e ) : A.
Proof.
  intros subst_wt typed_e. induction typed_e in r, Γ', subst_wt |- *; cbn; eauto.
  econstructor. eapply IHtyped_e.
  econstructor. destruct n; cbn in *.
  + assumption.
  + eapply subst_wt in H. now inversion H.
Qed.

Lemma subst_preserves Γ Γ' σ e A:
  Γ' ⊢ σ [ Γ ] -> Γ ⊢ e : A -> Γ' ⊢ (Subst_tm σ e ) : A.
Proof.
  intros subst_wt typed_e. induction typed_e in σ, Γ', subst_wt |- *; cbn; eauto.
  econstructor. eapply IHtyped_e. unfold up_tm_tm.
  intros n T H. destruct n; cbn; eauto.
  unfold core.funcomp.
  eapply ren_preserves.
  2:{ eapply subst_wt. cbn in *. assumption. }
  econstructor. cbn. assumption.
Qed.
Hint Resolve subst_preserves : core.

Lemma type_preservation_step Γ A s s':
  Γ ⊢ s : A -> s ≻ s' -> Γ ⊢ s': A.
Proof.
  intros H step_s. induction step_s in A, Γ, H |-*; inv H; try firstorder.
  2, 3: econstructor; eauto.
  - inv H3. assert (H: Γ ⊢ (scons e' ids )[typ1 :: Γ]).
    + intros n T H. destruct n.
      * cbn in *. injection H. now intros ?; subst.
      * cbn in *. asimpl. now constructor.
    + eapply subst_preserves; eauto.
  - inv H4. econstructor; eauto.
Qed.

Lemma type_preservation Γ A s s':
  Γ ⊢ s : A -> s ≻* s' -> Γ ⊢ s': A.
Proof.
  intros typed_s steps.
  induction steps; eauto.
  eapply type_preservation_step; eauto.
Qed.

Lemma allfv_tm_dec:
  forall p, decidable p -> decidable (allfv_tm p).
Proof.
  intros p H. rewrite decidable_iff. rewrite decidable_iff in H. destruct H as [H]. constructor. intro trm.
  induction trm in p, H |- *; cbn; firstorder.
  destruct (IHtrm (upAllfv_tm_tm p)). 2,3: firstorder.
  intros []; firstorder.
Qed.

Lemma closed_dec:
  decidable closed.
Proof.
  unfold closed. eapply allfv_tm_dec. exists (fun _ => false).
  intros _. now firstorder.
Qed.

Lemma subst_charact_typed σ1 σ2 e Γ A:
  Γ ⊢ e : A -> (forall n T, nth_error Γ n = Some T -> σ1 n = σ2 n ) -> Subst_tm σ1 e = Subst_tm σ2 e.
Proof.
  intros typed_e eq.
  induction typed_e in σ1, σ2, eq |- *.
  1-4: eauto.
  - cbn. erewrite IHtyped_e. 1: reflexivity. intros n T H. destruct n; eauto. cbn. unfold core.funcomp.
    assert (σ1 n = σ2 n).
    + eapply eq. eauto.
    + rewrite H0; easy.
  - cbn. erewrite IHtyped_e1, IHtyped_e2. 1: reflexivity. all: eauto.
  - cbn. erewrite IHtyped_e1, IHtyped_e2, IHtyped_e3. 1: reflexivity. all: eauto.
Qed.

Require Import Lia.

Definition shifted_subst σ N :=
  fun n => match (S n - N) with
  |O => var_tm n
  |S _ => (iter N (fun s => up_tm_tm s) σ) n
  end.

Lemma subst_charact σ1 σ2 s:
  (forall n, σ1 n = σ2 n ) -> Subst_tm σ1 s = Subst_tm σ2 s.
Proof.
  intros H. induction s in σ1, σ2, H |- *; cbn; eauto.
  - erewrite IHs1, IHs2, IHs3; eauto.
  - erewrite IHs1, IHs2; eauto.
  - erewrite IHs; eauto. intros n. destruct n; eauto.
    cbn. unfold core.funcomp. now rewrite H.
Qed.

Lemma shifted_subst_char σ N e:
  Subst_tm (shifted_subst σ N) e = Subst_tm (iter N (fun s => up_tm_tm s) σ) e.
Proof.
  eapply subst_charact.
  intros n. induction N in σ, n |- *; eauto. rewrite iter_succ_l.
  unfold shifted_subst in *. destruct (S n - S N) eqn: eq.
  2: easy.
  unfold shifted_subst. destruct n; cbn; eauto. unfold core.funcomp.
  erewrite <- IHN. destruct (S n - N) eqn: eq'; eauto. lia.
Qed.

Lemma fv_subst e N σ:
  allfv_tm (fun n => n < N) e -> Subst_tm (shifted_subst σ N) e = e.
Proof.
  intros H. induction e in N, H |- *; firstorder.
  - cbn in *. unfold shifted_subst. destruct (S n - N) eqn: e; eauto. lia.
  - cbn in *. now rewrite IHe1, IHe2, IHe3.
  - cbn in *. now rewrite IHe1, IHe2.
  - erewrite shifted_subst_char. specialize (IHe (N + 1)). rewrite shifted_subst_char in IHe. cbn in *. enough (up_tm_tm (iter N (fun s => up_tm_tm s) σ) = iter (N + 1) (fun s => up_tm_tm s) σ).
    + rewrite H1, IHe.
      1: easy.
      eapply (allfvImpl_tm (upAllfv_tm_tm (fun n : nat => n < N))); eauto.
      * intros n H2. destruct n; cbn in H2; lia.
    + assert (eq: N + 1 = S N) by lia. now rewrite eq.
Qed.

Lemma closed_subst e σ:
  closed e -> Subst_tm σ e = e.
Proof.
  intros H. assert (allfv_tm (fun n => n < 0) e -> Subst_tm (shifted_subst σ 0) e = e) by apply fv_subst.
  enough (Subst_tm (shifted_subst σ 0) e = Subst_tm σ e).
  - rewrite <- H1. eapply H0.
    eapply (allfvImpl_tm (fun n => False)); firstorder.
  - eapply subst_charact. intros n. unfold shifted_subst.
    destruct (S n - 0) eqn: eq; eauto. lia.
Qed.

Lemma ren_subst e f:
  ren_tm f e = Subst_tm (fun n => var_tm (f n)) e.
Proof.
  induction e in f |- *; cbn; eauto.
  - now rewrite IHe1, IHe2, IHe3.
  - now rewrite IHe1, IHe2.
  - rewrite IHe. enough (H: Subst_tm (fun n : nat => var_tm (upRen_tm_tm f n)) e = Subst_tm (up_tm_tm (fun n : nat => var_tm (f n))) e) by now rewrite H.
    eapply subst_charact. intros [|n]; cbn; eauto.
Qed.

Lemma closed_ren e f:
  closed e -> ren_tm f e = e.
Proof.
  rewrite ren_subst.
  eapply closed_subst.
Qed.

Lemma subst_concat Γ T A a σ1 σ2 e:
  (cons T Γ ) ⊢ e : A -> nil ⊢ a : T -> nil ⊢ σ2 [Γ ] -> Subst_tm (scons a σ1) (Subst_tm (up_tm_tm σ2) e) = Subst_tm (scons a σ2) e.
Proof.
  intros. asimpl. eapply subst_charact_typed; eauto.
  intros [] ? ?; cbn in *; eauto.
  asimpl. unfold core.funcomp.
  erewrite closed_subst; eauto using typed_empty_closed.
Qed.

Lemma subst_shift T Γ A σ t:
(T :: Γ ) ⊢ t : A -> nil ⊢ σ [(T :: Γ )] -> Subst_tm (fun n => σ (S n)) (Subst_tm (scons (σ 0) (fun n => var_tm n)) t) = Subst_tm σ t.
Proof.
intros typed_t subst_wt. asimpl. eapply subst_charact.
intros n. destruct n; eauto. cbn. erewrite closed_subst; eauto. eapply typed_empty_closed; eapply subst_wt; now cbn.
Qed.

Lemma funcomp_charact X Y Z (f f': X -> Y) (g g': Y -> Z) (x: X):
  g (f x) = g' (f' x) -> core.funcomp g f x = core.funcomp g' f' x.
  firstorder.
Qed.

Lemma subst_preserves_step σ e e':
  e ≻ e' -> (Subst_tm σ e ) ≻ (Subst_tm σ e').
Proof.
  intros step_e.
  induction step_e in σ |- *; cbn.
   {enough (H: Subst_tm σ (Subst_tm (scons e' ids) e) = Subst_tm (scons (Subst_tm σ e') (fun n => var_tm n)) (Subst_tm (up_tm_tm σ) e)).
    + rewrite H. econstructor.
    + asimpl. eapply subst_charact. intros [ |n]; eauto. now asimpl. }
  all: now econstructor.
Qed.

Lemma subst_closes Γ σ e A:
  nil ⊢ σ [Γ ] -> Γ ⊢ e : A -> closed (Subst_tm σ e).
Proof.
  intros. eapply typed_empty_closed. eapply subst_preserves; eauto.
Qed.

Lemma subst_well_typed_nil_nil σ:
  nil ⊢ σ [nil ].
Proof.
  red. intros n T H. destruct n; easy.
Qed.

Lemma subst_well_typed_singleton T t Γ σ:
  Γ ⊢ t : T -> Γ ⊢ scons t σ [cons T nil ].
Proof.
  intros typed_t n A H.
  destruct n; cbn in *; eauto.
  - injection H. now intros ->.
  - destruct n; easy.
Qed.

Lemma subst_map_closed_list (σ: nat -> tm) (l: list tm):
  Forall (fun t => closed t) l -> map (Subst_tm σ) l = l.
Proof.
  intros H. induction l.
  1: easy.
  cbn. rewrite Forall_cons_iff in H. rewrite IHl. 2: easy.
  rewrite closed_subst; easy.
Qed.

Lemma iter_ren_closed f t n:
  closed t -> iter n (ren_tm f) t = t.
Proof.
  intros closed_t.
  induction n.
  1: easy. rewrite iter_succ_l.
  rewrite IHn. now rewrite closed_ren.
Qed.

Lemma up_tm_tm_iter1 n m σ:
  m < n -> iter n Up_tm_tm σ m = var_tm m.
Proof.
  intros H. induction n in σ, m, H |-*.
  1: easy.
  rewrite iter_succ_l. destruct m.
  1: easy. unfold Up_tm_tm at 1. unfold up_tm_tm. cbn.
  unfold core.funcomp. rewrite IHn. 2: lia. easy.
Qed.

Lemma up_tm_tm_iter2 n m σ:
  m >= n -> iter n Up_tm_tm σ m = iter n (ren_tm shift) (σ (m - n)).
Proof.
  intros H. induction n in σ, m, H |-*.
  1: now destruct m.
  rewrite iter_succ_l. destruct m.
  1: lia. unfold Up_tm_tm at 1. unfold up_tm_tm. cbn.
  unfold core.funcomp. rewrite IHn. 2: lia. easy.
Qed.

Lemma val_list_closed l:
    Forall (fun t : tm => is_bval t = true) l -> Forall (fun t : tm => closed t) l.
Proof.
    intros H. apply Forall_impl with (P := fun t => is_bval t = true); eauto.
    intros a. now destruct a.
Qed.