Mcltt.Core.Semantic.Realizability

From Coq Require Import Lia Morphisms_Relations PeanoNat Relation_Definitions.
From Equations Require Import Equations.

From Mcltt Require Import LibTactics.
From Mcltt.Core Require Import Base.
From Mcltt.Core.Semantic Require Export NbE PER.
Import Domain_Notations.

Lemma per_nat_then_per_top : forall {n m},
    {{ Dom n m per_nat }} ->
    {{ Dom n m per_top }}.
Proof with solve [destruct_conjs; eexists; repeat econstructor; eauto].
  induction 1; simpl in *; intros s;
    try specialize (IHper_nat s);
    try specialize (H s)...
Qed.

#[export]
Hint Resolve per_nat_then_per_top : mcltt.

Lemma realize_per_univ_elem_gen : forall {i a a' R},
    {{ DF a a' per_univ_elem i R }} ->
    {{ Dom a a' per_top_typ }}
    /\ (forall {c c'}, {{ Dom c c' per_bot }} -> {{ Dom a c a' c' R }})
    /\ (forall {b b'}, {{ Dom b b' R }} -> {{ Dom a b a' b' per_top }}).
Proof with (solve [try (try (eexists; split); econstructor); mauto]).
  intros * Hunivelem. simpl in Hunivelem.
  induction Hunivelem using per_univ_elem_ind; repeat split; intros;
    apply_relation_equivalence; mauto.
  - subst; repeat econstructor.
  - subst.
    eexists.
    per_univ_elem_econstructor...
  - subst.
    destruct_by_head per_univ.
    specialize (H2 _ _ _ H0).
    destruct_conjs.
    intro s.
    specialize (H1 s) as [? []]...
  - destruct IHHunivelem as [? []].
    intro s.
    assert {{ Dom ⇑! a s ⇑! a' s in_rel }} by eauto using var_per_bot.
    destruct_rel_mod_eval.
    specialize (H9 (S s)) as [? []].
    specialize (H2 s) as [? []]...
  - intros c0 c0' equiv_c0_c0'.
    destruct_conjs.
    destruct_rel_mod_eval.
    econstructor; try solve [econstructor; eauto].
    enough ({{ Dom c a c0 c' a' c0' per_bot }}) by eauto.
    intro s.
    specialize (H3 s) as [? []].
    specialize (H5 _ _ equiv_c0_c0' s) as [? []]...
  - destruct_conjs.
    intro s.
    assert {{ Dom ⇑! a s ⇑! a' s in_rel }} by eauto using var_per_bot.
    destruct_rel_mod_eval.
    destruct_rel_mod_app.
    match goal with
    | _: {{ $| ^?f0 & ⇑! a s |↘ ^_ }},
        _: {{ $| ^?f0' & ⇑! a' s |↘ ^_ }},
          _: {{ B ρ ⇑! a s ^?b0 }},
            _: {{ B' ρ' ⇑! a' s ^?b0' }} |- _ =>
        rename f0 into f;
        rename f0' into f';
        rename b0 into b;
        rename b0' into b'
    end.
    assert {{ Dom b fa b' f'a' per_top }} by eauto.
    specialize (H2 s) as [? []].
    specialize (H16 (S s)) as [? []]...
  - intro s.
    (on_all_hyp: fun H => destruct (H s) as [? []])...
  - intro s.
    inversion_clear_by_head per_ne.
    (on_all_hyp: fun H => specialize (H s) as [? []])...
Qed.

Corollary per_univ_then_per_top_typ : forall {i a a' R},
    {{ DF a a' per_univ_elem i R }} ->
    {{ Dom a a' per_top_typ }}.
Proof.
  intros * ?%realize_per_univ_elem_gen; firstorder.
Qed.

#[export]
Hint Resolve per_univ_then_per_top_typ : mcltt.

Corollary per_bot_then_per_elem : forall {i a a' R c c'},
    {{ DF a a' per_univ_elem i R }} ->
    {{ Dom c c' per_bot }} -> {{ Dom a c a' c' R }}.
Proof.
  intros * ?%realize_per_univ_elem_gen; firstorder.
Qed.

We cannot add per_bot_then_per_elem as a hint because we don't know what "R" is (i.e. the pattern becomes higher-order.) In fact, Coq complains it cannot add one if we try.

Corollary per_elem_then_per_top : forall {i a a' R b b'},
    {{ DF a a' per_univ_elem i R }} ->
    {{ Dom b b' R }} -> {{ Dom a b a' b' per_top }}.
Proof.
  intros * ?%realize_per_univ_elem_gen; firstorder.
Qed.

#[export]
Hint Resolve per_elem_then_per_top : mcltt.

Lemma per_ctx_then_per_env_initial_env : forall {Γ Γ' env_rel},
    {{ EF Γ Γ' per_ctx_env env_rel }} ->
    exists ρ ρ', initial_env Γ ρ /\ initial_env Γ' ρ' /\ {{ Dom ρ ρ' env_rel }}.
Proof.
  induction 1.
  - do 2 eexists; intuition.
  - destruct_conjs.
    (on_all_hyp: destruct_rel_by_assumption tail_rel).
    do 2 eexists; repeat split; only 1-2: econstructor; eauto.
    apply_relation_equivalence.
    eexists.
    eapply per_bot_then_per_elem; eauto.
    erewrite per_ctx_respects_length; mauto.
    eexists; eauto.
Qed.

Lemma var_per_elem : forall {a b i R} n,
    {{ DF a b per_univ_elem i R }} ->
    {{ Dom ⇑! a n ⇑! b n R }}.
Proof.
  intros.
  eapply per_bot_then_per_elem; mauto.
Qed.