From Undecidability.FOLP Require Export unscoped.

Class Signature := B_S { Funcs : Type; fun_ar : Funcs ;
              Preds : Type; pred_ar : Preds }.

Section fix_sig.

Context {Sigma : Signature}.

Inductive term : Type :=
  | var_term : () term
  | Func : (f : Funcs), Vector.t term (fun_ar f) term .

Definition congr_Func { f : Funcs } { s0 : Vector.t term (fun_ar f) } { t0 : Vector.t term (fun_ar f)} (H1 : = ) : Func f = Func f :=
  (eq_trans) (eq_refl) ((ap) ( x Func f x) ).

Fixpoint subst_term (sigmaterm : () term ) (s : term ) : _ :=
    match s with
    | var_term s sigmaterm s
    | Func f Func f (Vector.map (subst_term sigmaterm) )
    end.

Definition up_term_term (sigma : () term ) : _ :=
  (scons) ((var_term ) (var_zero)) ((funcomp) (subst_term ((funcomp) (var_term ) (shift))) ).

Definition upId_term_term (sigma : () term ) (Eq : x, x = (var_term ) x) : x, (up_term_term ) x = (var_term ) x :=
   n match n with
  | S fin_n (ap) (subst_term ((funcomp) (var_term ) (shift))) (Eq fin_n)
  | 0 eq_refl
  end.

Fixpoint idSubst_term (sigmaterm : () term ) (Eqterm : x, sigmaterm x = (var_term ) x) (s : term ) : subst_term sigmaterm s = s :=
    match s with
    | var_term s Eqterm s
    | Func f congr_Func ((vec_id (idSubst_term sigmaterm Eqterm)) )
    end.

Definition upExt_term_term (sigma : () term ) (tau : () term ) (Eq : x, x = x) : x, (up_term_term ) x = (up_term_term ) x :=
   n match n with
  | S fin_n (ap) (subst_term ((funcomp) (var_term) (shift))) (Eq fin_n)
  | 0 eq_refl
  end.

Fixpoint ext_term (sigmaterm : () term ) (tauterm : () term ) (Eqterm : x, sigmaterm x = tauterm x) (s : term ) : subst_term sigmaterm s = subst_term tauterm s :=
    match s with
    | var_term s Eqterm s
    | Func f congr_Func ((vec_ext (ext_term sigmaterm tauterm Eqterm)) )
    end.

Fixpoint compSubstSubst_term (sigmaterm : () term ) (tauterm : () term ) (thetaterm : () term ) (Eqterm : x, ((funcomp) (subst_term tauterm) sigmaterm) x = thetaterm x) (s : term ) : subst_term tauterm (subst_term sigmaterm s) = subst_term thetaterm s :=
    match s with
    | var_term s Eqterm s
    | Func f congr_Func ((vec_comp (compSubstSubst_term sigmaterm tauterm thetaterm Eqterm)) )
    end.

Definition up_subst_subst_term_term (sigma : () term ) (tauterm : () term ) (theta : () term ) (Eq : x, ((funcomp) (subst_term tauterm) ) x = x) : x, ((funcomp) (subst_term (up_term_term tauterm)) (up_term_term )) x = (up_term_term ) x :=
   n match n with
  | S fin_n (eq_trans) (compSubstSubst_term ((funcomp) (var_term) (shift)) (up_term_term tauterm) ((funcomp) (up_term_term tauterm) (shift)) ( x eq_refl) ( fin_n)) ((eq_trans) ((eq_sym) (compSubstSubst_term tauterm ((funcomp) (var_term) (shift)) ((funcomp) (subst_term ((funcomp) (var_term ) (shift))) tauterm) ( x eq_refl) ( fin_n))) ((ap) (subst_term ((funcomp) (var_term ) (shift))) (Eq fin_n)))
  | 0 eq_refl
  end.

Lemma instId_term : subst_term (var_term ) = (@id) (term ) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) ( x idSubst_term (var_term ) ( n eq_refl) (((@id) (term )) x))). Qed.

Lemma varL_term (sigmaterm : () term ) : (funcomp) (subst_term sigmaterm) (var_term ) = sigmaterm .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) ( x eq_refl)). Qed.

Lemma compComp_term (sigmaterm : () term ) (tauterm : () term ) (s : term ) : subst_term tauterm (subst_term sigmaterm s) = subst_term ((funcomp) (subst_term tauterm) sigmaterm) s .
Proof. exact (compSubstSubst_term sigmaterm tauterm (_) ( n eq_refl) s). Qed.

Lemma compComp'_term (sigmaterm : () term ) (tauterm : () term ) : (funcomp) (subst_term tauterm) (subst_term sigmaterm) = subst_term ((funcomp) (subst_term tauterm) sigmaterm) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) ( n compComp_term sigmaterm tauterm n)). Qed.

Inductive form : Type :=
  | Fal : form
  | Pred : (P : Preds), Vector.t term (pred_ar P) form
  | Impl : form form form
  | All : form form.

Definition congr_Fal : Fal = Fal :=
  eq_refl.

Definition congr_Pred { P : Preds } { s0 : Vector.t term (pred_ar P) } { t0 : Vector.t term (pred_ar P) } (H1 : = ) : Pred P = Pred P :=
  (eq_trans) (eq_refl) ((ap) ( x Pred P x) ).

Definition congr_Impl { s0 : form } { s1 : form } { t0 : form } { t1 : form } (H1 : = ) (H2 : = ) : Impl = Impl :=
  (eq_trans) ((eq_trans) (eq_refl) ((ap) ( x Impl x (_)) )) ((ap) ( x Impl (_) x) ).

Definition congr_All { s0 : form } { t0 : form } (H1 : = ) : All = All :=
  (eq_trans) (eq_refl) ((ap) ( x All x) ).

Fixpoint subst_form (sigmaterm : () term ) (s : form ) : _ :=
    match s with
    | Fal Fal
    | Pred P Pred P ((Vector.map (subst_term sigmaterm)) )
    | Impl Impl ((subst_form sigmaterm) ) ((subst_form sigmaterm) )
    | All All ((subst_form (up_term_term sigmaterm)) )
    end.

Fixpoint idSubst_form (sigmaterm : () term ) (Eqterm : x, sigmaterm x = (var_term ) x) (s : form ) : subst_form sigmaterm s = s :=
    match s with
    | Fal congr_Fal
    | Pred P congr_Pred ((vec_id (idSubst_term sigmaterm Eqterm)) )
    | Impl congr_Impl ((idSubst_form sigmaterm Eqterm) ) ((idSubst_form sigmaterm Eqterm) )
    | All congr_All ((idSubst_form (up_term_term sigmaterm) (upId_term_term (_) Eqterm)) )
    end.

Fixpoint ext_form (sigmaterm : () term ) (tauterm : () term ) (Eqterm : x, sigmaterm x = tauterm x) (s : form ) : subst_form sigmaterm s = subst_form tauterm s :=
    match s with
    | Fal congr_Fal
    | Pred P congr_Pred ((vec_ext (ext_term sigmaterm tauterm Eqterm)) )
    | Impl congr_Impl ((ext_form sigmaterm tauterm Eqterm) ) ((ext_form sigmaterm tauterm Eqterm) )
    | All congr_All ((ext_form (up_term_term sigmaterm) (up_term_term tauterm) (upExt_term_term (_) (_) Eqterm)) )
    end.

Fixpoint compSubstSubst_form (sigmaterm : () term ) (tauterm : () term ) (thetaterm : () term ) (Eqterm : x, ((funcomp) (subst_term tauterm) sigmaterm) x = thetaterm x) (s : form ) : subst_form tauterm (subst_form sigmaterm s) = subst_form thetaterm s :=
    match s with
    | Fal congr_Fal
    | Pred P congr_Pred ((vec_comp (compSubstSubst_term sigmaterm tauterm thetaterm Eqterm)) )
    | Impl congr_Impl ((compSubstSubst_form sigmaterm tauterm thetaterm Eqterm) ) ((compSubstSubst_form sigmaterm tauterm thetaterm Eqterm) )
    | All congr_All ((compSubstSubst_form (up_term_term sigmaterm) (up_term_term tauterm) (up_term_term thetaterm) (up_subst_subst_term_term (_) (_) (_) Eqterm)) )
    end.

Lemma instId_form : subst_form (var_term ) = (@id) (form ) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) ( x idSubst_form (var_term ) ( n eq_refl) (((@id) (form )) x))). Qed.

Lemma compComp_form (sigmaterm : () term ) (tauterm : () term ) (s : form ) : subst_form tauterm (subst_form sigmaterm s) = subst_form ((funcomp) (subst_term tauterm) sigmaterm) s .
Proof. exact (compSubstSubst_form sigmaterm tauterm (_) ( n eq_refl) s). Qed.

Lemma compComp'_form (sigmaterm : () term ) (tauterm : () term ) : (funcomp) (subst_form tauterm) (subst_form sigmaterm) = subst_form ((funcomp) (subst_term tauterm) sigmaterm) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) ( n compComp_form sigmaterm tauterm n)). Qed.

End fix_sig.

Instance Subst_term (Sigma : Signature) : Subst1 (() term ) (term ) (term ) := @subst_term .

Instance Subst_form (Sigma : Signature) : Subst1 (() term ) (form ) (form ) := @subst_form .

Instance VarInstance_term (Sigma : Signature) : Var (() ) (term ) := @var_term .

Notation "x '__term'" := (var_term x) (at level 5, format "x __term") : subst_scope.

Notation "x '__term'" := (@ids (_) (_) VarInstance_term x) (at level 5, only printing, format "x __term") : subst_scope.

Notation "'var'" := (var_term) (only printing, at level 1) : subst_scope.

Class Up_term X Y := up_term : X Y.

Notation "↑__term" := (up_term) (only printing) : subst_scope.

Notation "↑__term" := (up_term_term) (only printing) : subst_scope.

Instance Up_term_term (Sigma : Signature) : Up_term (_) (_) := @up_term_term .

Notation "s [ sigmaterm ]" := (subst_term sigmaterm s) (at level 7, left associativity, format "s '/' [ sigmaterm ]", only printing) : subst_scope.


Notation "s [ sigmaterm ]" := (subst_form sigmaterm s) (at level 7, left associativity, format "s '/' [ sigmaterm ]", only printing) : subst_scope.

Notation "[ sigmaterm ]" := (subst_form sigmaterm) (at level 0, left associativity, only printing) : fscope.

Ltac auto_unfold := repeat unfold , , Subst1, Subst2, ids, Subst_term, Subst_form, VarInstance_term.

Tactic Notation "auto_unfold" "in" "*" := repeat unfold , , Subst1, Subst2, ids, Subst_term, Subst_form, VarInstance_term in *.

Ltac asimpl' := repeat first [progress rewrite ?instId_term| progress rewrite ?term| progress rewrite ?compComp_term| progress rewrite ?compComp'_term| progress rewrite ?instId_form| progress rewrite ?form| progress rewrite ?compComp_form| progress rewrite ?compComp'_form| progress rewrite ?varL_term| progress (unfold up_ren, up_term_term)| progress (cbn [subst_term subst_form])| fsimpl].

Ltac asimpl := repeat try unfold_funcomp; auto_unfold in *; asimpl'; repeat try unfold_funcomp.

Tactic Notation "asimpl" "in" hyp(J) := revert J; asimpl; intros J.

Tactic Notation "auto_case" := auto_case (asimpl; cbn; eauto).

Tactic Notation "asimpl" "in" "*" := auto_unfold in *; repeat first [progress rewrite ?instId_term in *| progress rewrite ?term in *| progress rewrite ?compComp_term in *| progress rewrite ?compComp'_term in *| progress rewrite ?instId_form in *| progress rewrite ?form in *| progress rewrite ?compComp_form in *| progress rewrite ?compComp'_form in *| progress rewrite ?varL_term in *| progress (unfold up_ren, up_term_term)| progress (cbn [subst_term subst_form] in *)| fsimpl in *].