Coral.RLogic: program logic for untyped λ-terms based on stable relations

Require Import Infrastructure.
Import Notations.
Require Import StepsFacts.
Require Import Env.
Require Import Rel.
Require Import Transp.
Require Import EquivarianceFacts.
Require Import RelExtra.
Require Import RelWf.
Require Import Rsem.
Require Import Interp.

Inductive RLogic : env (rel (env term) term) → term → rel (env term) term → Prop :=
| RLogicEquiv: ∀ E t R1 R2,
    RelEquiv R1 R2 →
    RLogic E t R1 →
    RLogic E t R2
| RLogicInter: ∀ E t R1 R2,
    RLogic E t R1 →
    RLogic E t R2 →
    RLogic E t (RelInter R1 R2)
| RLogicSub: ∀ E t R1 R2,
    wf_rel (dom E) R2 →
    RLogic E t R1 →
    RelIncl R1 R2 →
    RLogic E t R2
| RLogicSelf: ∀ E t R,
    RLogic E t R →
    is_extended_value t →
    RLogic E t (RelSelf t)
| RLogicGather: ∀ E t R,
    RLogic E t R →
    RLogic E t (RelGather E)
| RLogicVar: ∀ E x R,
    get x E = Some R →
    RLogic E (Var x) R
| RLogicLet: ∀ E t1 x t2 R1 R2,
    RLogic E t1 R1 →
    x `notin` dom E →
    RLogic (x ¬ R1 ++ E) t2 R2 →
    RLogic E (Let t1 (close x t2)) (RelLet (dom E) x R1 R2)
| RLogicLam: ∀ E x t R1 R2,
    x `notin` dom E →
    wf_rel (dom E) R1 →
    RLogic (x ¬ R1 ++ E) t R2 →
    RLogic E (Lam (close x t)) (RelLam (dom E) x R1 R2)
| RLogicApp: ∀ E t1 t2 R1 R2,
    RLogic E t1 R1 →
    RLogic E t2 R2 →
    RLogic E (App t1 t2) (APP R1 R2)
| RLogicUnit: ∀ E,
    RLogic E Unit RelUnitR
| RLogicPair: ∀ E t1 t2 R1 R2,
    RLogic E t1 R1 →
    RLogic E t2 R2 →
    RLogic E (Pair t1 t2) (RelPairR R1 R2)
| RLogicFst: ∀ E t R,
    RLogic E t R →
    RLogic E (Fst t) (RelCompose R (RelPairL RelEqVal RelTopVal))
| RLogicSnd: ∀ E t R,
    RLogic E t R →
    RLogic E (Snd t) (RelCompose R (RelPairL RelTopVal RelEqVal))
| RLogicInjL: ∀ E t R,
    RLogic E t R →
    RLogic E (InjL t) (RelSumR R RelBot)
| RLogicInjR: ∀ E t R,
    RLogic E t R →
    RLogic E (InjR t) (RelSumR RelBot R)
| RLogicMatch: ∀ E t x1 t1 x2 t2 R R1 R2,
    RLogic E t R →
    x1 `notin` dom E →
    RLogic (x1 ¬ (RelCompose R (RelSumL RelEqVal RelBot)) ++ E) t1 R1 →
    x2 `notin` dom E →
    RLogic (x2 ¬ (RelCompose R (RelSumL RelBot RelEqVal)) ++ E) t2 R2 →
    RLogic E (Match t (close x1 t1) (close x2 t2))
          (RelUnion
             (RelLet (dom E) x1 (RelCompose R (RelSumL RelEqVal RelBot)) R1)
             (RelLet (dom E) x2 (RelCompose R (RelSumL RelBot RelEqVal)) R2)
          )
.

Add Parametric Morphism: RLogic
    with signature env_rel_equiv ==> eq ==> RelEquiv ==> iff
      as RLogic_morphism_equiv.
Proof.
  assert (∀ E1 E2 t R,
             env_rel_equiv E1 E2 →
             RLogic E1 t R →
             RLogic E2 t R).
  { intros E1 E2 t R H12 H.
    generalize dependent E2.
    induction H; intros.
    - eapply RLogicEquiv; eauto.
    - apply RLogicInter; auto.
    - eapply RLogicSub; eauto. rewrite <- H12. assumption.
    - eapply RLogicSelf; eauto.
    - apply RLogicEquiv with (R1 := RelGather E2).
      + rewrite H12. reflexivity.
      + eapply RLogicGather; eauto.
    - case_eq (get x E2); intros.
      + eapply env_rel_equiv_get in H; [| symmetry |]; eauto.
        eapply RLogicEquiv with (R1 := r); auto.
        apply RLogicVar; auto.
      + exfalso. rewrite <- env_rel_equiv_get_None in H0; eauto. congruence.
    - eapply RLogicEquiv with (R1 := RelLet (dom E2) x R1 R2).
      + rewrite H12. reflexivity.
      + apply RLogicLet; auto.
        × rewrite <- H12. assumption.
        × apply IHRLogic2. simpl; split; [| split]; auto. reflexivity.
    - eapply RLogicEquiv with (R1 := RelLam (dom E2) x R1 R2).
      + rewrite H12. reflexivity.
      + apply RLogicLam; auto.
        × rewrite <- H12. assumption.
        × rewrite <- H12. assumption.
        × apply IHRLogic.
          simpl; split; [| split]; auto. reflexivity.
    - apply RLogicApp; auto.
    - apply RLogicUnit; auto.
    - apply RLogicPair; auto.
    - apply RLogicFst; auto.
    - apply RLogicSnd; auto.
    - apply RLogicInjL; auto.
    - apply RLogicInjR; auto.
    - apply RLogicEquiv with
          (R1 := RelUnion
                   (RelLet (dom E2) x1 (RelCompose R (RelSumL RelEqVal RelBot)) R1)
                   (RelLet (dom E2) x2 (RelCompose R (RelSumL RelBot RelEqVal)) R2)
          ).
      + rewrite H12. reflexivity.
      + apply RLogicMatch; auto.
        × rewrite <- H12. assumption.
        × apply IHRLogic2. simpl; split; [| split]; auto. reflexivity.
        × rewrite <- H12. assumption.
        × apply IHRLogic3. simpl; split; [| split]; auto. reflexivity.
  }
  intros E1 E2 HE t R1 R2 HR.
  split; intro HRLogic.
  - eapply RLogicEquiv; eauto.
  - symmetry in HR. symmetry in HE. eapply RLogicEquiv; eauto.
Qed.

Lemma RLogic_inhabited E t:
  lc t →
  fv t [<=] dom E →
  { R | RLogic E t R }.
Proof.
  intros Hlc Hfv.
  apply lc_set_of_lc in Hlc.
  generalize dependent E. induction Hlc; intros.
  - case_eq (get x E); intros.
    + eexists. eapply RLogicVar; eauto.
    + simpl in Hfv. apply get_notin_dom in H. exfalso. fsetdec.
  - simpl in Hfv.
    pick fresh x for (fv t2 `union` dom E).
    rewrite <- (close_open t2 x); auto.
    destruct IHHlc with (E := E) as [R1 H1]; [fsetdec |].
    destruct (X x) with (E := x ¬ R1 ++ E) as [R2 H2];
      [ rewrite fv_open_upper; simpl; fsetdec | ].
    eexists. eapply RLogicLet; eauto.
  - simpl in Hfv.
    pick fresh x for (fv t `union` dom E).
    rewrite <- (close_open t x); auto.
    destruct (X x) with (E := x ¬ RelTopEnvVal ++ E) as [R1 H1];
      [ rewrite fv_open_upper; simpl; fsetdec | ].
    eexists.
    apply RLogicLam with (R1 := RelTopEnvVal) (R2 := R1); auto with wf_rel.
  - simpl in Hfv.
    destruct IHHlc1 with (E := E) as [R1 H1]; [fsetdec|].
    destruct IHHlc2 with (E := E) as [R2 H2]; [fsetdec|].
    eexists. apply RLogicApp; eauto.
  - eexists. apply RLogicUnit.
  - simpl in Hfv.
    destruct IHHlc1 with (E := E) as [R1 H1]; [fsetdec|].
    destruct IHHlc2 with (E := E) as [R2 H2]; [fsetdec|].
    eexists. eapply RLogicPair; eauto.
  - simpl in Hfv.
    destruct IHHlc with (E := E) as [R1 H1]; auto.
    eexists. eapply RLogicFst; eauto.
  - simpl in Hfv.
    destruct IHHlc with (E := E) as [R1 H1]; auto.
    eexists. eapply RLogicSnd; eauto.
  - simpl in Hfv.
    destruct IHHlc with (E := E) as [R1 H1]; auto.
    eexists. eapply RLogicInjL; eauto.
  - simpl in Hfv.
    destruct IHHlc with (E := E) as [R1 H1]; auto.
    eexists. eapply RLogicInjR; eauto.
  - simpl in Hfv.
    pick fresh x for (fv t1 `union` fv t2 `union` dom E).
    rewrite <- (close_open t1 x); auto.
    rewrite <- (close_open t2 x); auto.
    destruct IHHlc with (E := E) as [R0 Heval0]; [ fsetdec | ].
    destruct (X x) with (E := x ¬ RelCompose R0 (RelSumL RelEqVal RelBot) ++ E) as [R1 Heval1];
      [rewrite fv_open_upper; simpl; fsetdec | ].
    destruct (X0 x) with (E := x ¬ RelCompose R0 (RelSumL RelBot RelEqVal) ++ E) as [R2 Heval2];
      [rewrite fv_open_upper; simpl; fsetdec | ].
    eexists. apply RLogicMatch; eauto.
Qed.

Lemma RLogic_lc E t R:
  RLogic E t R →
  lc t.
Proof.
  intro H. induction H; auto with lngen.
Qed.

Lemma RLogic_fv E t R:
  RLogic E t R →
  fv t [<=] dom E.
Proof.
  intro H; induction H; simpl in *; try repeat rewrite fv_close; try fsetdec.
  apply get_in_dom in H. fsetdec.
Qed.

Lemma RLogic_equivariant x y E t R:
  RLogic E t R →
  RLogic (transp_env_rel x y E) (transp_term x y t) (transp_rel x y R).
Proof.
  intro H. induction H; simpl.
  - eapply RLogicEquiv; eauto. rewrite H. reflexivity.
  - rewrite RelInter_rel_equivariant.
    apply RLogicInter; auto.
  - apply (RelIncl_rel_equivariant x y) in H1.
    rewrite (wf_rel_equivariant x y) in H.
    rewrite dom_equivariant_rel in H.
    eapply RLogicSub; eauto.
  - rewrite RelSelf_rel_equivariant.
    rewrite <- (is_extended_value_equivariant x y) in H0.
    eapply RLogicSelf; eauto.
  - rewrite RelGather_rel_equivariant.
    eapply RLogicGather; eauto.
  - apply RLogicVar with (R := transp_rel x y R).
    apply get_transp_env_rel_Some_equivariant. assumption.
  - rewrite RelLet_rel_equivariant.
    rewrite dom_equivariant_rel.
    rewrite close_equivariant.
    apply RLogicLet; auto.
    rewrite <- dom_equivariant_rel.
    apply notin_equivariant.
    assumption.
  - rewrite RelLam_rel_equivariant.
    rewrite dom_equivariant_rel.
    rewrite close_equivariant.
    eapply RLogicLam; eauto.
    + rewrite <- dom_equivariant_rel.
      apply notin_equivariant.
      assumption.
    + rewrite <- dom_equivariant_rel.
      apply wf_rel_equivariant.
      assumption.
  - rewrite APP_rel_equivariant.
    apply RLogicApp; auto.
  - rewrite RelUnitR_rel_equivariant.
    apply RLogicUnit.
  - rewrite RelPairR_rel_equivariant.
    apply RLogicPair; auto.
  - rewrite RelCompose_rel_equivariant.
    rewrite RelPairL_vrel_equivariant.
    rewrite RelTopVal_vrel_equivariant.
    rewrite RelEqVal_vrel_equivariant.
    apply RLogicFst; auto.
  - rewrite RelCompose_rel_equivariant.
    rewrite RelPairL_vrel_equivariant.
    rewrite RelTopVal_vrel_equivariant.
    rewrite RelEqVal_vrel_equivariant.
    apply RLogicSnd; auto.
  - rewrite RelSumR_rel_equivariant.
    rewrite RelBot_rel_equivariant.
    apply RLogicInjL; auto.
  - rewrite RelSumR_rel_equivariant.
    rewrite RelBot_rel_equivariant.
    apply RLogicInjR; auto.
  - rewrite RelUnion_rel_equivariant.
    repeat rewrite RelLet_rel_equivariant.
    repeat rewrite RelCompose_rel_equivariant.
    repeat rewrite RelSumL_vrel_equivariant.
    repeat rewrite RelBot_vrel_equivariant.
    repeat rewrite RelTopVal_vrel_equivariant.
    repeat rewrite RelEqVal_vrel_equivariant.
    repeat rewrite dom_equivariant_rel.
    repeat rewrite close_equivariant.
    apply RLogicMatch; auto.
    + rewrite <- dom_equivariant_rel.
      apply notin_equivariant.
      assumption.
    + rewrite transp_env_rel_app in IHRLogic2.
      rewrite transp_env_rel_one in IHRLogic2.
      assert (env_rel_equiv
                [(transp_atom x y x1, transp_rel x y (RelCompose R (RelSumL RelEqVal RelBot)))]
                [(transp_atom x y x1, RelCompose (transp_rel x y R) (RelSumL RelEqVal RelBot))]) as Heq.
      { simpl; split; [| split]; auto.
        rewrite RelCompose_rel_equivariant.
        rewrite RelSumL_vrel_equivariant.
        rewrite RelEqVal_vrel_equivariant.
        rewrite RelBot_vrel_equivariant.
        reflexivity.
      }
      rewrite Heq in IHRLogic2.
      assumption.
    + rewrite <- dom_equivariant_rel.
      apply notin_equivariant.
      assumption.
    + rewrite transp_env_rel_app in IHRLogic3.
      rewrite transp_env_rel_one in IHRLogic3.
      assert (env_rel_equiv
                [(transp_atom x y x2, transp_rel x y (RelCompose R (RelSumL RelBot RelEqVal)))]
                [(transp_atom x y x2, RelCompose (transp_rel x y R) (RelSumL RelBot RelEqVal))]) as Heq.
      { simpl; split; [| split]; auto.
        rewrite RelCompose_rel_equivariant.
        rewrite RelSumL_vrel_equivariant.
        rewrite RelEqVal_vrel_equivariant.
        rewrite RelBot_vrel_equivariant.
        reflexivity.
      }
      rewrite Heq in IHRLogic3.
      assumption.
Qed.

Lemma RLogic_wf E t R:
  wf_env_rel E →
  RLogic E t R →
  wf_rel (dom E) R.
Proof.
  intros Hwf H. induction H; auto with wf_rel.
  - rewrite <- H. auto.
  - apply wf_rel_RelSelf. apply RLogic_fv in H. assumption.
  - apply wf_rel_RelGather; auto. reflexivity.
  - eapply wf_env_rel_get; eauto.
  - apply wf_rel_RelUnion; apply wf_rel_RelLet; auto with wf_rel.
Qed.
Hint Resolve RLogic_wf : wf_rel.

Lemma RLogic_soundness E t R:
  wf_env_rel E →
  RLogic E t R →
  RelIncl (Rsem E t) R.
Proof.
  intros Hwf H. induction H.
  - rewrite <- H. auto.
  - apply RelInter_glb; auto.
  - rewrite IHRLogic; auto.
  - apply Rsem_RelIncl_RelSelf; auto.
    + eapply RLogic_lc; eauto.
    + eapply RLogic_fv; eauto.
  - apply Rsem_RelIncl_RelGather; auto.
    + eapply RLogic_lc; eauto.
    + eapply RLogic_fv; eauto.
  - eapply Rsem_RelIncl_Var_get; eauto.
  - rewrite <- IHRLogic1; auto.
    rewrite <- IHRLogic2; auto.
    + assert (env_rel_incl (x ¬ (Rsem E t1) ++ E) (x ¬ R1 ++ E)) as Hincl.
      { simpl. split; [| split]; auto. reflexivity. }
      rewrite <- Hincl.
      apply Rsem_RelIncl_Let; auto with wf_rel.
      × eapply RLogic_lc; eauto.
      × eapply RLogic_lc; eauto.
      × eapply RLogic_fv; eauto.
      × erewrite RLogic_fv; eauto. reflexivity.
    + apply wf_env_rel_cons; eauto using RLogic_wf.
  - rewrite <- IHRLogic; auto with wf_rel.
    apply Rsem_RelIncl_Lam_RelLam; auto with wf_rel.
    + eapply RLogic_lc; eauto.
    + erewrite RLogic_fv; eauto. reflexivity.
  - rewrite <- IHRLogic1; auto.
    rewrite <- IHRLogic2; auto.
    apply Rsem_RelIncl_App.
  - apply Rsem_RelIncl_Unit_UnitR; auto.
  - rewrite <- IHRLogic1; auto.
    rewrite <- IHRLogic2; auto.
    apply Rsem_RelIncl_Pair.
  - rewrite <- IHRLogic; auto.
    apply Rsem_RelIncl_Fst.
    + eapply RLogic_lc; eauto.
    + eapply RLogic_fv; eauto.
  - rewrite <- IHRLogic; auto.
    apply Rsem_RelIncl_Snd.
    + eapply RLogic_lc; eauto.
    + eapply RLogic_fv; eauto.
  - rewrite <- IHRLogic; auto.
    apply Rsem_RelIncl_InjL.
  - rewrite <- IHRLogic; auto.
    apply Rsem_RelIncl_InjR.
  - assert (wf_rel (dom E) R) by (eapply RLogic_wf; eauto).
    rewrite <- IHRLogic1; auto.
    rewrite <- IHRLogic2; auto with wf_rel.
    rewrite <- IHRLogic3; auto with wf_rel.
    assert (env_rel_incl (x1 ¬ (RelCompose (Rsem E t) (RelSumL RelEqVal RelBot)) ++ E)
                         (x1 ¬ (RelCompose R (RelSumL RelEqVal RelBot)) ++ E))
      as Hincl1.
    { simpl. split; [| split]; auto.
      - rewrite IHRLogic1; auto. reflexivity.
      - reflexivity.
    }
    rewrite <- Hincl1. clear Hincl1.
    assert (env_rel_incl (x2 ¬ (RelCompose (Rsem E t) (RelSumL RelBot RelEqVal)) ++ E)
                         (x2 ¬ (RelCompose R (RelSumL RelBot RelEqVal)) ++ E))
      as Hincl2.
    { simpl. split; [| split]; auto.
      - rewrite IHRLogic1; auto. reflexivity.
      - reflexivity.
    }
    rewrite <- Hincl2. clear Hincl2.
    apply Rsem_RelIncl_Match; auto.
    + eapply RLogic_lc; eauto.
    + eapply RLogic_lc; eauto.
    + eapply RLogic_lc; eauto.
    + eapply RLogic_fv; eauto.
    + erewrite RLogic_fv; eauto. reflexivity.
    + erewrite RLogic_fv; eauto. reflexivity.
Qed.

Lemma RLogic_soundness_Interp E t R:
  ∀ (Huniq: uniq E)
    (HwfEnv: wf_env_rel E)
    (HLogic: RLogic E t R),
    RelIncl (Interp E t (RLogic_lc _ _ _ HLogic) (RLogic_fv _ _ _ HLogic)) R.
Proof.
  intros Huniq Hwf HLogic.
  rewrite Interp_completeness; auto.
  apply RLogic_soundness; auto.
Qed.

Lemma RLogic_completeness_Interp E t (Hlc: lc t) (Hfv: fv t [<=] dom E):
  wf_env_rel E →
  RLogic E t (Interp E t Hlc Hfv).
Proof.
  apply Interp_ind; clear E t Hlc Hfv; intros.
  - assert (RLogic E (Var x) R) by auto using RLogicVar.
    apply RLogicInter; auto.
    + eapply RLogicSelf; eauto. simpl. trivial.
    + eapply RLogicGather; eauto.
  - assert (wf_rel (dom E) R1) by (subst R1; auto using Interp_wf).
    apply RLogicLet; auto with wf_rel.
  - assert (RLogic E (Lam (close x t1)) (RelLam (dom E) x RelTopEnvVal R1)).
    { apply RLogicLam; auto with wf_rel. }
    apply RLogicInter; [| apply RLogicInter ]; auto.
    + eapply RLogicSelf; eauto. simpl. trivial.
    + eapply RLogicGather; eauto.
  - apply RLogicApp; auto.
  - assert (RLogic E Unit RelUnitR) by apply RLogicUnit.
    apply RLogicInter; auto.
    eapply RLogicGather; eauto.
  - apply RLogicPair; auto.
  - apply RLogicFst; auto.
  - apply RLogicSnd; auto.
  - apply RLogicInjL; auto.
  - apply RLogicInjR; auto.
  - assert (wf_rel (dom E) R1) by (subst R1; auto with wf_rel).
    apply RLogicMatch; auto with wf_rel.
Qed.

Lemma RLogic_completeness E t:
  lc t →
  fv t [<=] dom E →
  uniq E →
  wf_env_rel E →
  RLogic E t (Rsem E t).
Proof.
  intros Hlc Hfv Huniq Hwf.
  apply RLogicSub with (R1 := Interp E t Hlc Hfv).
  - apply (wf_rel_subset (dom E `union` fv t)); [ fsetdec |].
    apply Rsem_wf_rel; auto.
  - apply RLogic_completeness_Interp; auto.
  - apply Interp_completeness; auto.
Qed.

Lemma RLogic_preservation_steps E t1 t2 R:
  uniq E →
  wf_env_rel E →
  steps t1 t2 →
  RLogic E t1 R →
  RLogic E t2 R.
Proof.
  intros Huniq Hwf Hsteps H.
  assert (wf_rel (dom E) R) as HwfR by eauto with wf_rel.
  assert (lc t2) as Hlc.
  { apply steps_lc in Hsteps; auto. eapply RLogic_lc; eauto. }
  assert (fv t2 [<=] dom E) as Hfv.
  { apply steps_fv in Hsteps. apply RLogic_fv in H. fsetdec. }
  apply RLogic_soundness in H; auto.
  rewrite <- (Rsem_steps _ _ _ Hsteps) in H.
  apply RLogicSub with (R1 := Rsem E t2); auto.
  apply RLogic_completeness; auto.
Qed.

Lemma RLogic_preservation_eval E t v R:
  uniq E →
  wf_env_rel E →
  eval t v →
  RLogic E t R →
  RLogic E v R.
Proof.
  intros Huniq Hwf [Hsteps Hvalue] H.
  eapply RLogic_preservation_steps; eauto.
Qed.