Mcltt.Core.Completeness.FunctionCases

From Coq Require Import Morphisms_Relations Relation_Definitions.

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

Lemma rel_exp_of_pi_inversion : forall {Γ M M' A B},
    {{ Γ M M' : Π A B }} ->
    exists env_rel (_ : {{ EF Γ Γ per_ctx_env env_rel }}) i,
    forall ρ ρ' (equiv_ρ_ρ' : {{ Dom ρ ρ' env_rel }}),
    exists in_rel out_rel,
      rel_typ i A ρ A ρ' in_rel /\
        (forall c c' (equiv_c_c' : {{ Dom c c' in_rel }}), rel_typ i B d{{{ ρ c }}} B d{{{ ρ' c' }}} (out_rel c c' equiv_c_c')) /\
        rel_exp M ρ M' ρ'
          (fun f f' : domain => forall (c c' : domain) (equiv_c_c' : in_rel c c'), rel_mod_app f c f' c' (out_rel c c' equiv_c_c')).
Proof.
  intros * [env_relΓ].
  destruct_conjs.
  eexists_rel_exp.
  intros.
  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
  destruct_by_head rel_typ.
  invert_rel_typ_body.
  do 2 eexists; repeat split; mauto.
Qed.

Lemma rel_exp_of_pi : forall {Γ M M' A B},
    (exists env_rel (_ : {{ EF Γ Γ per_ctx_env env_rel }}) i j,
      forall ρ ρ' (equiv_ρ_ρ' : {{ Dom ρ ρ' env_rel }}),
      exists in_rel out_rel,
        rel_typ i A ρ A ρ' in_rel /\
          (forall c c' (equiv_c_c' : {{ Dom c c' in_rel }}), rel_typ j B d{{{ ρ c }}} B d{{{ ρ' c' }}} (out_rel c c' equiv_c_c')) /\
          rel_exp M ρ M' ρ'
            (fun f f' : domain => forall (c c' : domain) (equiv_c_c' : in_rel c c'), rel_mod_app f c f' c' (out_rel c c' equiv_c_c'))) ->
    {{ Γ M M' : Π A B }}.
Proof.
  intros * [env_relΓ [? [i [j]]]].
  destruct_conjs.
  eexists_rel_exp_with (max i j).
  intros.
  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
  rename x0 into in_rel.
  destruct_by_head rel_typ.
  destruct_by_head rel_exp.
  eexists; split; econstructor; mauto.
  - per_univ_elem_econstructor; eauto using per_univ_elem_cumu_max_left.
    + intros.
      (on_all_hyp: destruct_rel_by_assumption in_rel).
      econstructor; eauto using per_univ_elem_cumu_max_right.
    + apply Equivalence_Reflexive.
  - mauto.
Qed.

Ltac eexists_rel_exp_of_pi :=
  apply rel_exp_of_pi;
  eexists_rel_exp;
  eexists.

#[local]
Ltac extract_output_info_with ρ c ρ' c' env_rel :=
  let Hequiv := fresh "equiv" in
  (assert (Hequiv : {{ Dom ρ c ρ' c' env_rel }}) by (apply_relation_equivalence; mauto 4);
   apply_relation_equivalence;
   (on_all_hyp: fun H => destruct (H _ _ Hequiv));
   destruct_conjs;
   destruct_by_head rel_typ;
   destruct_by_head rel_exp).

Lemma rel_exp_pi_core : forall {i o B o' B' R out_rel},
    (forall c c',
        R c c' ->
        rel_exp B d{{{ o c }}} B' d{{{ o' c' }}} (per_univ i)) ->
    
We use the next equality to make unification on `out_rel` works
    (out_rel = fun c c' (equiv_c_c' : R c c') m m' =>
                 forall R',
                   rel_typ i B d{{{ o c }}} B' d{{{ o' c' }}} R' ->
                   R' m m') ->
    (forall c c' (equiv_c_c' : R c c'), rel_typ i B d{{{ o c }}} B' d{{{ o' c' }}} (out_rel c c' equiv_c_c')).
Proof with intuition.
  intros.
  subst.
  (on_all_hyp: destruct_rel_by_assumption R).
  econstructor; mauto.
  destruct_by_head per_univ.
  apply -> per_univ_elem_morphism_iff; eauto.
  split; intros; destruct_by_head rel_typ; handle_per_univ_elem_irrel...
  exvar (relation domain) ltac:(fun R => assert (rel_typ i B d{{{ o c }}} B' d{{{ o' c' }}} R) by mauto).
  intuition.
Qed.

Lemma rel_exp_pi_cong : forall {i Γ A A' B B'},
    {{ Γ A A' : Type@i }} ->
    {{ Γ , A B B' : Type@i }} ->
    {{ Γ Π A B Π A' B' : Type@i }}.
Proof with mautosolve.
  intros * [env_relΓ]%rel_exp_of_typ_inversion [env_relΓA]%rel_exp_of_typ_inversion.
  destruct_conjs.
  pose env_relΓA.
  match_by_head (per_ctx_env env_relΓA) invert_per_ctx_env.
  eexists_rel_exp_of_typ.
  intros.
  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
  destruct_by_head per_univ.
  handle_per_univ_elem_irrel.
  econstructor; mauto.
  eexists.
  per_univ_elem_econstructor; eauto.
  - intros.
    eapply rel_exp_pi_core; eauto.
    reflexivity.
  - solve_refl.
Qed.

#[export]
Hint Resolve rel_exp_pi_cong : mcltt.

Lemma rel_exp_pi_sub : forall {i Γ σ Δ A B},
    {{ Γ s σ : Δ }} ->
    {{ Δ A : Type@i }} ->
    {{ Δ , A B : Type@i }} ->
    {{ Γ (Π A B)[σ] Π (A[σ]) (B[q σ]) : Type@i }}.
Proof with mautosolve.
  intros * [env_relΓ] [env_relΔ]%rel_exp_of_typ_inversion [env_relΔA]%rel_exp_of_typ_inversion.
  destruct_conjs.
  pose env_relΔ.
  pose env_relΔA.
  match_by_head (per_ctx_env env_relΔA) invert_per_ctx_env.
  handle_per_ctx_env_irrel.
  eexists_rel_exp_of_typ.
  intros.
  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
  assert {{ Dom ρ'σ' ρ'σ' env_relΔ }} by (etransitivity; [symmetry |]; eassumption).
  (on_all_hyp: destruct_rel_by_assumption env_relΔ).
  destruct_by_head per_univ.
  handle_per_univ_elem_irrel.
  econstructor; mauto.
  eexists.
  per_univ_elem_econstructor; eauto.
  - eapply rel_exp_pi_core; eauto; try reflexivity.
    intros.
    extract_output_info_with ρσ c ρ'σ' c' env_relΔA...
  - solve_refl.
Qed.

#[export]
Hint Resolve rel_exp_pi_sub : mcltt.

Lemma rel_exp_fn_cong : forall {i Γ A A' B M M'},
    {{ Γ A A' : Type@i }} ->
    {{ Γ , A M M' : B }} ->
    {{ Γ λ A M λ A' M' : Π A B }}.
Proof with mautosolve.
  intros * [env_relΓ]%rel_exp_of_typ_inversion [env_relΓA].
  destruct_conjs.
  pose env_relΓA.
  match_by_head (per_ctx_env env_relΓA) invert_per_ctx_env.
  handle_per_ctx_env_irrel.
  eexists_rel_exp_of_pi.
  intros.
  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
  destruct_by_head per_univ.
  functional_eval_rewrite_clear.
  do 2 eexists.
  repeat split; [econstructor | | econstructor]; mauto.
  - eapply rel_exp_pi_core; eauto; try reflexivity.
    intros.
    extract_output_info_with ρ c ρ' c' env_relΓA.
    econstructor; eauto.
    eexists...
  - intros.
    extract_output_info_with ρ c ρ' c' env_relΓA.
    econstructor; mauto.
    intros.
    destruct_by_head rel_typ.
    handle_per_univ_elem_irrel...
Qed.

#[export]
Hint Resolve rel_exp_fn_cong : mcltt.

Lemma rel_exp_fn_sub : forall {Γ σ Δ A M B},
    {{ Γ s σ : Δ }} ->
    {{ Δ , A M : B }} ->
    {{ Γ (λ A M)[σ] λ A[σ] M[q σ] : (Π A B)[σ] }}.
Proof with mautosolve.
  intros * [env_relΓ [? [env_relΔ]]] [env_relΔA].
  destruct_conjs.
  pose env_relΔA.
  match_by_head (per_ctx_env env_relΔA) invert_per_ctx_env.
  handle_per_ctx_env_irrel.
  eexists_rel_exp.
  intros.
  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
  (on_all_hyp: destruct_rel_by_assumption env_relΔ).
  eexists.
  split; econstructor; mauto 4.
  - per_univ_elem_econstructor; [apply per_univ_elem_cumu_max_right | | apply Equivalence_Reflexive]; eauto.
    intros.
    eapply rel_exp_pi_core; eauto; try reflexivity.
    clear dependent c.
    clear dependent c'.
    intros.
    extract_output_info_with ρσ c ρ'σ' c' env_relΔA.
    econstructor; eauto.
    eexists.
    eapply per_univ_elem_cumu_max_left...
  - intros ? **.
    extract_output_info_with ρσ c ρ'σ' c' env_relΔA.
    econstructor; mauto.
    intros.
    destruct_by_head rel_typ.
    handle_per_univ_elem_irrel...
Qed.

#[export]
Hint Resolve rel_exp_fn_sub : mcltt.

Lemma rel_exp_app_cong : forall {Γ M M' A B N N'},
    {{ Γ M M' : Π A B }} ->
    {{ Γ N N' : A }} ->
    {{ Γ M N M' N' : B[Id,,N] }}.
Proof with intuition.
  intros * [env_relΓ]%rel_exp_of_pi_inversion [].
  destruct_conjs.
  pose env_relΓ.
  handle_per_ctx_env_irrel.
  eexists_rel_exp.
  intros.
  assert (equiv_p'_p' : env_relΓ ρ' ρ') by (etransitivity; [symmetry |]; eassumption).
  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
  rename x2 into in_rel.
  destruct_by_head rel_typ.
  destruct_by_head rel_exp.
  handle_per_univ_elem_irrel.
  assert (in_rel m1 m2) by (etransitivity; [| symmetry]; eassumption).
  assert (in_rel m1 m'2) by intuition.
  (on_all_hyp: destruct_rel_by_assumption in_rel).
  handle_per_univ_elem_irrel.
  eexists.
  split; econstructor; mauto...
Qed.

#[export]
Hint Resolve rel_exp_app_cong : mcltt.

Lemma rel_exp_app_sub : forall {Γ σ Δ M A B N},
    {{ Γ s σ : Δ }} ->
    {{ Δ M : Π A B }} ->
    {{ Δ N : A }} ->
    {{ Γ (M N)[σ] M[σ] N[σ] : B[σ,,N[σ]] }}.
Proof with mautosolve.
  intros * [env_relΓ] [env_relΔ]%rel_exp_of_pi_inversion [].
  destruct_conjs.
  pose env_relΓ.
  pose env_relΔ.
  handle_per_ctx_env_irrel.
  eexists_rel_exp.
  intros.
  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
  (on_all_hyp: destruct_rel_by_assumption env_relΔ).
  rename x0 into in_rel.
  destruct_by_head rel_typ.
  handle_per_univ_elem_irrel.
  destruct_by_head rel_exp.
  (on_all_hyp_rev: destruct_rel_by_assumption in_rel).
  eexists.
  split; econstructor...
Qed.

#[export]
Hint Resolve rel_exp_app_sub : mcltt.

Lemma rel_exp_pi_beta : forall {Γ A M B N},
  {{ Γ , A M : B }} ->
  {{ Γ N : A }} ->
  {{ Γ (λ A M) N M[Id,,N] : B[Id,,N] }}.
Proof with mautosolve.
  intros * [env_relΓA] [env_relΓ].
  destruct_conjs.
  pose env_relΓA.
  match_by_head (per_ctx_env env_relΓA) invert_per_ctx_env.
  handle_per_ctx_env_irrel.
  eexists_rel_exp.
  intros.
  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
  destruct_by_head rel_typ.
  handle_per_univ_elem_irrel.
  destruct_by_head rel_exp.
  rename m into n.
  rename m' into n'.
  extract_output_info_with ρ n ρ' n' env_relΓA.
  eexists.
  split; econstructor...
Qed.

#[export]
Hint Resolve rel_exp_pi_beta : mcltt.

Lemma rel_exp_pi_eta : forall {Γ M A B},
  {{ Γ M : Π A B }} ->
  {{ Γ M λ A (M[Wk] #0) : Π A B }}.
Proof with mautosolve.
  intros * [env_relΓ]%rel_exp_of_pi_inversion.
  destruct_conjs.
  pose env_relΓ.
  eexists_rel_exp_of_pi.
  intros.
  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
  rename x into in_rel.
  destruct_by_head rel_typ.
  destruct_by_head rel_exp.
  do 2 eexists.
  repeat split; only 1,3: econstructor; mauto.
  intros.
  (on_all_hyp: destruct_rel_by_assumption in_rel)...
Qed.

#[export]
Hint Resolve rel_exp_pi_eta : mcltt.