Require Import Omega.
Require Export Setoid Morphisms Equivalence.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
From Chapter3 Require Export utlc_pure.
From Chapter4 Require Export sigmacalculus.

Open Scope equiv_scope.
Hint Extern 0 (_ === _) => reflexivity.

Lemma setoid_crutch A (R : relation A) (c : Equivalence R) x y :
  R x y -> @Equivalence.equiv A R c x y.
Proof. auto. Qed.

Fixpoint den (alpha : nat -> tm) (alpha' : nat -> (nat -> tm)) (s : exp) : tm :=
  match s with
  | Zero => var_tm 0
  | App s t => app (den alpha alpha' s) (den alpha alpha' t)
  | Lam s => lam (den alpha alpha' s)
  | Inst s sigma => (den alpha alpha' s)[den_subst alpha alpha' sigma]
  | var_exp n => alpha n
  end
with den_subst (alpha : nat -> tm) (alpha' : nat -> (nat -> tm)) (sigma : subst_exp) : nat -> tm :=
  match sigma with
  | Succ => fun n => var_tm (S n)
  | I => var_tm
  | Cons s sigma => (den alpha alpha' s) .: (den_subst alpha alpha' sigma)
  | Comp sigma tau => fun s => (den_subst alpha alpha' sigma s)[den_subst alpha alpha' tau]
  | var_subst n => alpha' n
  end.

Definition equiv_den (s t : exp) : Prop :=
  forall alpha alpha', den alpha alpha' s = den alpha alpha' t.

Definition equiv_den_subst (sigma tau : subst_exp) : Prop :=
  forall alpha alpha' x, den_subst alpha alpha' sigma x = den_subst alpha alpha' tau x.

Fixpoint soundness s t (H : equiv_axiom s t) {struct H}:
   equiv_den s t
with soundness_subst sigma tau (H : equiv_axiom_subst sigma tau) {struct H}:
  equiv_den_subst sigma tau.
Proof.
  - induction H; unfold equiv_den; intros; cbn; asimpl; eauto.
    all: try (now rewrite IHequiv_axiom).
    + repeat f_equal. fext. intros []; cbn. unfold funcomp. now substify.
      unfold funcomp. now substify.
    + apply ext_tm. intros x. now rewrite (soundness_subst _ _ H).
  - induction H; unfold equiv_den_subst; intros; cbn; asimpl; eauto.
    + destruct x; asimpl; f_equal.
    + f_equal. apply IHequiv_axiom_subst.
    + apply ext_tm; eauto.
    + destruct x; cbn; eauto. apply soundness; eauto.
    + destruct x; cbn; eauto.
Qed.