Mcltt.Core.Completeness.SubstitutionCases

From Coq Require Import Morphisms_Relations RelationClasses.

From Mcltt Require Import LibTactics.
From Mcltt.Core Require Import Base.
From Mcltt.Core.Completeness Require Import ContextCases LogicalRelation UniverseCases.
Import Domain_Notations.

Lemma rel_sub_id : forall {Γ},
    {{ Γ }} ->
    {{ Γ s Id Id : Γ }}.
Proof with mautosolve.
  intros * [].
  eexists_rel_sub...
Qed.

#[export]
Hint Resolve rel_sub_id : mcltt.

Lemma rel_sub_weaken : forall {Γ A},
    {{ Γ, A }} ->
    {{ Γ, A s Wk Wk : Γ }}.
Proof with mautosolve.
  intros * [env_relΓA].
  inversion_by_head (per_ctx_env env_relΓA); subst.
  eexists_rel_sub.
  intros.
  apply_relation_equivalence.
  destruct_conjs...
Qed.

#[export]
Hint Resolve rel_sub_weaken : mcltt.

Lemma rel_sub_compose_cong : forall {Γ τ τ' Γ' σ σ' Γ''},
    {{ Γ s τ τ' : Γ' }} ->
    {{ Γ' s σ σ' : Γ'' }} ->
    {{ Γ s σ τ σ' τ' : Γ'' }}.
Proof with mautosolve.
  intros * [env_relΓ [? [env_relΓ']]] [].
  destruct_conjs.
  pose env_relΓ'.
  handle_per_ctx_env_irrel.
  eexists_rel_sub.
  intros.
  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
  (on_all_hyp: destruct_rel_by_assumption env_relΓ')...
Qed.

#[export]
Hint Resolve rel_sub_compose_cong : mcltt.

Lemma rel_sub_extend_cong : forall {i Γ M M' σ σ' Δ A},
    {{ Γ s σ σ' : Δ }} ->
    {{ Δ A : Type@i }} ->
    {{ Γ M M' : A[σ] }} ->
    {{ Γ s σ ,, M σ' ,, M' : Δ, A }}.
Proof with mautosolve.
  intros * [env_relΓ [? [env_relΔ]]] HA [].
  destruct_conjs.
  pose env_relΓ.
  pose env_relΔ.
  assert {{ Δ, A }} as [env_relΔA] by (eapply rel_ctx_extend; eauto; eexists; mauto).
  destruct_conjs.
  handle_per_ctx_env_irrel.
  eexists_rel_sub.
  match_by_head (per_ctx_env env_relΔA) invert_per_ctx_env.
  destruct_conjs.
  handle_per_ctx_env_irrel.
  intros.
  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
  (on_all_hyp: destruct_rel_by_assumption env_relΔ).
  destruct_by_head rel_typ.
  invert_rel_typ_body.
  destruct_by_head rel_exp...
Qed.

#[export]
Hint Resolve rel_sub_extend_cong : mcltt.

Lemma rel_sub_id_compose_right : forall {Γ σ Δ},
    {{ Γ s σ : Δ }} ->
    {{ Γ s Id σ σ : Δ }}.
Proof with mautosolve.
  intros * [env_relΓ].
  destruct_conjs.
  eexists_rel_sub.
  intros.
  (on_all_hyp: destruct_rel_by_assumption env_relΓ)...
Qed.

#[export]
Hint Resolve rel_sub_id_compose_right : mcltt.

Lemma rel_sub_id_compose_left : forall {Γ σ Δ},
    {{ Γ s σ : Δ }} ->
    {{ Γ s σ Id σ : Δ }}.
Proof with mautosolve.
  intros * [env_relΓ].
  destruct_conjs.
  eexists_rel_sub.
  intros.
  (on_all_hyp: destruct_rel_by_assumption env_relΓ)...
Qed.

#[export]
Hint Resolve rel_sub_id_compose_left : mcltt.

Lemma rel_sub_compose_assoc : forall {Γ σ Γ' σ' Γ'' σ'' Γ'''},
    {{ Γ' s σ : Γ }} ->
    {{ Γ'' s σ' : Γ' }} ->
    {{ Γ''' s σ'' : Γ'' }} ->
    {{ Γ''' s (σ σ') σ'' σ (σ' σ'') : Γ }}.
Proof with mautosolve.
  intros * [env_relΓ'] [env_relΓ'' [? []]] [env_relΓ'''].
  destruct_conjs.
  pose env_relΓ'.
  pose env_relΓ''.
  handle_per_ctx_env_irrel.
  eexists_rel_sub.
  intros.
  (on_all_hyp: destruct_rel_by_assumption env_relΓ''').
  (on_all_hyp: destruct_rel_by_assumption env_relΓ'').
  (on_all_hyp: destruct_rel_by_assumption env_relΓ').
  econstructor...
Qed.

#[export]
Hint Resolve rel_sub_compose_assoc : mcltt.

Lemma rel_sub_extend_compose : forall {Γ τ Γ' M σ Γ'' A i},
    {{ Γ' s σ : Γ'' }} ->
    {{ Γ'' A : Type@i }} ->
    {{ Γ' M : A[σ] }} ->
    {{ Γ s τ : Γ' }} ->
    {{ Γ s (σ ,, M) τ (σ τ) ,, M[τ] : Γ'', A }}.
Proof with mautosolve.
  intros * [env_relΓ' [? [env_relΓ'']]] HA [] [env_relΓ].
  destruct_conjs.
  pose env_relΓ'.
  pose env_relΓ''.
  handle_per_ctx_env_irrel.
  assert {{ Γ'', A }} as [env_relΓ''A] by (eapply rel_ctx_extend; eauto; eexists; eassumption).
  destruct_conjs.
  eexists_rel_sub.
  match_by_head (per_ctx_env env_relΓ''A) invert_per_ctx_env.
  handle_per_ctx_env_irrel.
  intros.
  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
  (on_all_hyp: destruct_rel_by_assumption env_relΓ').
  (on_all_hyp: destruct_rel_by_assumption env_relΓ'').
  destruct_by_head rel_typ.
  invert_rel_typ_body.
  destruct_by_head rel_exp.
  econstructor...
Qed.

#[export]
Hint Resolve rel_sub_extend_compose : mcltt.

Lemma rel_sub_p_extend : forall {Γ' M σ Γ A},
    {{ Γ' s σ : Γ }} ->
    {{ Γ' M : A[σ] }} ->
    {{ Γ' s Wk (σ ,, M) σ : Γ }}.
Proof with mautosolve.
  intros * [env_relΓ'] [].
  destruct_conjs.
  pose env_relΓ'.
  handle_per_ctx_env_irrel.
  eexists_rel_sub.
  intros.
  (on_all_hyp: destruct_rel_by_assumption env_relΓ').
  destruct_by_head rel_typ.
  invert_rel_typ_body.
  destruct_by_head rel_exp.
  econstructor...
Qed.

#[export]
Hint Resolve rel_sub_p_extend : mcltt.

Lemma rel_sub_extend : forall {Γ' σ Γ A},
    {{ Γ' s σ : Γ, A }} ->
    {{ Γ' s σ (Wk σ) ,, #0[σ] : Γ, A }}.
Proof with mautosolve.
  intros * [env_relΓ' [? [env_relΓA]]].
  destruct_conjs.
  pose env_relΓ'.
  inversion_by_head (per_ctx_env env_relΓA); subst.
  rename tail_rel into env_relΓ.
  handle_per_ctx_env_irrel.
  eexists_rel_sub.
  intros.
  (on_all_hyp: destruct_rel_by_assumption env_relΓ').
  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
  econstructor...
Qed.

#[export]
Hint Resolve rel_sub_extend : mcltt.

Lemma rel_sub_sym : forall {Γ σ σ' Δ},
    {{ Γ s σ σ' : Δ }} ->
    {{ Γ s σ' σ : Δ }}.
Proof with mautosolve.
  intros * [env_relΓ].
  destruct_conjs.
  eexists_rel_sub.
  intros.
  assert (env_relΓ ρ' ρ) by (symmetry; eassumption).
  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
  econstructor; mauto; symmetry...
Qed.

#[export]
Hint Resolve rel_sub_sym : mcltt.

Lemma rel_sub_trans : forall {Γ σ σ' σ'' Δ},
    {{ Γ s σ σ' : Δ }} ->
    {{ Γ s σ' σ'' : Δ }} ->
    {{ Γ s σ σ'' : Δ }}.
Proof with mautosolve.
  intros * [env_relΓ] [].
  destruct_conjs.
  pose env_relΓ.
  handle_per_ctx_env_irrel.
  eexists_rel_sub.
  intros.
  assert (env_relΓ ρ' ρ') by (etransitivity; [symmetry |]; eassumption).
  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
  functional_eval_rewrite_clear.
  econstructor; mauto; etransitivity...
Qed.

#[export]
Hint Resolve rel_sub_trans : mcltt.

#[export]
Instance rel_sub_PER {Γ A} : PER (rel_sub_under_ctx Γ A).
Proof.
  split; mauto.
Qed.

Lemma rel_sub_conv : forall {Γ σ σ' Δ Δ'},
    {{ Γ s σ σ' : Δ }} ->
    {{ Δ Δ' }} ->
    {{ Γ s σ σ' : Δ' }}.
Proof with mautosolve.
  intros * [? [? [env_relΔ]]] [].
  destruct_conjs.
  pose env_relΔ.
  handle_per_ctx_env_irrel.
  assert {{ EF Δ' Δ' per_ctx_env env_relΔ }} by (etransitivity; [symmetry |]; eassumption).
  eexists_rel_sub...
Qed.

#[export]
Hint Resolve rel_sub_conv : mcltt.

Lemma presup_rel_sub : forall {Γ σ σ' Δ},
    {{ Γ s σ σ' : Δ }} ->
    {{ Γ }} /\ {{ Γ s σ : Δ }} /\ {{ Γ s σ' : Δ }} /\ {{ Δ }}.
Proof with mautosolve.
  intros * [].
  destruct_conjs.
  repeat split; try solve [eexists; eauto];
    unfold valid_sub_under_ctx;
    etransitivity; only 2,3: symmetry;
    econstructor...
Qed.

Lemma rel_sub_eq_subtyp : forall Γ σ σ' Δ Δ',
    {{ Γ s σ σ' : Δ }} ->
    {{ SubE Δ <: Δ' }} ->
    {{ Γ s σ σ' : Δ' }}.
Proof.
  intros * [env_relΓ] HSub.
  pose proof (per_ctx_subtyp_to_env _ _ HSub).
  destruct_conjs.
  handle_per_ctx_env_irrel.
  eexists_rel_sub.
  intros.
  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
  econstructor; eauto.
  eapply per_ctx_env_subtyping; eauto.
Qed.

#[export]
Hint Resolve rel_sub_eq_subtyp : mcltt.