Require Import Omega.
Require Export Setoid Morphisms Equivalence.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Require Import Coq.Program.Equality.
Require Export ARS.

Inductive exp := Zero
               | App : exp -> exp -> exp
               | Lam: exp -> exp
               | Inst : exp -> subst_exp -> exp
               | var_exp : nat -> exp
with subst_exp := I : subst_exp
                | Succ : subst_exp
                | Cons : exp -> subst_exp -> subst_exp
                | Comp : subst_exp -> subst_exp -> subst_exp
                | var_subst : nat -> subst_exp.

Scheme exp_ind' := Induction for exp Sort Prop
  with exp_s_ind' := Induction for subst_exp Sort Prop.

Combined Scheme comb_exp_ind from exp_ind', exp_s_ind'.

Inductive equiv_axiom : exp -> exp -> Prop :=
| equiv_App s t sigma : equiv_axiom (Inst (App s t) sigma) (App (Inst s sigma) (Inst t sigma))
| equiv_Lam s sigma : equiv_axiom (Inst (Lam s) sigma) (Lam (Inst s (Cons Zero (Comp sigma Succ))))
| equiv_Zero s sigma : equiv_axiom (Inst Zero (Cons s sigma)) s
| equiv_inst_I s : equiv_axiom (Inst s I) s
| equiv_inst_inst s sigma tau : equiv_axiom (Inst (Inst s sigma) tau) (Inst s (Comp sigma tau))

| equiv_appL s s' t: equiv_axiom s s' -> equiv_axiom (App s t) (App s' t)
| equiv_appR s t t': equiv_axiom t t' -> equiv_axiom (App s t) (App s t')
| equiv_lam s s' : equiv_axiom s s' -> equiv_axiom (Lam s) (Lam s')
| equiv_instL s s' sigma : equiv_axiom s s' -> equiv_axiom (Inst s sigma) (Inst s' sigma)
| equiv_instR s sigma sigma' : equiv_axiom_subst sigma sigma' -> equiv_axiom (Inst s sigma) (Inst s sigma')

with equiv_axiom_subst : subst_exp -> subst_exp -> Prop :=
| comp_S s sigma : equiv_axiom_subst (Comp Succ (Cons s sigma)) sigma
| comp_left sigma : equiv_axiom_subst (Comp I sigma) sigma
| comp_right sigma : equiv_axiom_subst (Comp sigma I) sigma
| comp_assoc sigma tau theta : equiv_axiom_subst (Comp (Comp sigma tau) theta) (Comp sigma (Comp tau theta))
| comp_cons s sigma tau : equiv_axiom_subst (Comp (Cons s sigma) tau) (Cons (Inst s tau) (Comp sigma tau))
| comp_I : equiv_axiom_subst (Cons Zero Succ) I
| cons_eta sigma: equiv_axiom_subst (Cons (Inst Zero sigma) (Comp Succ sigma)) sigma

| equiv_compL sigma sigma' tau : equiv_axiom_subst sigma sigma' -> equiv_axiom_subst (Comp sigma tau) (Comp sigma' tau)
| equiv_compR sigma tau tau' : equiv_axiom_subst tau tau' -> equiv_axiom_subst (Comp sigma tau) (Comp sigma tau')
| equiv_consL s s' sigma : equiv_axiom s s' -> equiv_axiom_subst (Cons s sigma) (Cons s' sigma)
| equiv_consR s sigma sigma' : equiv_axiom_subst sigma sigma' -> equiv_axiom_subst (Cons s sigma) (Cons s sigma').

Scheme equiv_ind' := Induction for equiv_axiom Sort Prop
with equiv_s_ind' := Induction for equiv_axiom_subst Sort Prop.

Combined Scheme comb_equiv_ind from equiv_ind', equiv_s_ind'.

Hint Constructors equiv_axiom equiv_axiom_subst.

Ltac auto_inv :=
  match goal with
  | [ H: equiv_axiom Zero _ |- _] => inv H
  | [ H : equiv_axiom (App _ _) _ |- _] => inv H
  | [ H : equiv_axiom (Lam _) _ |- _] => inv H
  | [ H : equiv_axiom (Inst _ _) _ |- _] => inv H
  | [ H : equiv_axiom (var_exp _) _ |- _] => inv H
  | [ H : equiv_axiom_subst (Succ) _ |- _] => inv H
  | [ H : equiv_axiom_subst I _ |- _] => inv H
  | [ H : equiv_axiom_subst (Cons _ _) _ |- _] => inv H
  | [ H : equiv_axiom_subst (Comp _ _) _ |- _] => inv H
  | [ H : equiv_axiom_subst (var_subst _) _ |- _] => inv H
  end.

Lemma star_AppL s s' t:
  star equiv_axiom s s' -> star equiv_axiom (App s t) (App s' t).
Proof. induction 1; eauto. Qed.

Lemma star_AppR s t t':
  star equiv_axiom t t' -> star equiv_axiom (App s t) (App s t').
Proof. induction 1; eauto. Qed.

Lemma star_Lam s s':
  star equiv_axiom s s' -> star equiv_axiom (Lam s) (Lam s').
Proof. induction 1; eauto. Qed.

Lemma star_InstL s s' sigma :
  star equiv_axiom s s' -> star equiv_axiom (Inst s sigma) (Inst s' sigma).
Proof. induction 1; eauto. Qed.

Lemma star_InstR s sigma sigma':
  star equiv_axiom_subst sigma sigma' -> star equiv_axiom (Inst s sigma) (Inst s sigma').
Proof. induction 1; eauto. Qed.

Lemma star_ConsL s s' sigma:
  star equiv_axiom s s' -> star equiv_axiom_subst (Cons s sigma) (Cons s' sigma).
Proof. induction 1; eauto. Qed.

Lemma star_ConsR s sigma sigma':
  star equiv_axiom_subst sigma sigma' -> star equiv_axiom_subst (Cons s sigma) (Cons s sigma').
Proof. induction 1; eauto. Qed.

Lemma star_CompL sigma sigma' tau :
  star equiv_axiom_subst sigma sigma' -> star equiv_axiom_subst (Comp sigma tau) (Comp sigma' tau).
Proof. induction 1; eauto. Qed.

Lemma star_CompR sigma tau tau' :
  star equiv_axiom_subst tau tau' -> star equiv_axiom_subst (Comp sigma tau) (Comp sigma tau').
Proof. induction 1; eauto. Qed.

Hint Resolve star_AppL star_AppR star_Lam star_InstL star_InstR star_ConsL star_ConsR star_CompL star_CompR.