Require Import List Lia.
Import ListNotations.
Require Import ssreflect ssrbool ssrfun.

Require Import Undecidability.HilbertCalculi.HSC.

Set Default Goal Selector "!".

Lemma ForallE {T : Type} {P : T -> Prop} {l} :
  Forall P l -> if l is x :: l then P x /\ Forall P l else True.
Proof. by case. Qed.

Fixpoint size s :=
  match s with
  | var _ => 1
  | arr s t => S (size s + size t)
  end.

Fixpoint arguments (k: nat) (t: formula) :=
  match k with
  | 0 => []
  | S k =>
    match t with
    | var _ => []
    | arr s t => s :: (arguments k t)
    end
  end.

Fixpoint target (k: nat) (t: formula) :=
  match k with
  | 0 => t
  | S k =>
    match t with
    | var _ => t
    | arr _ t => target k t
    end
  end.

Inductive der (Gamma: list formula) : nat -> formula -> Prop :=
  | der_var {ζ: nat -> formula} {s t: formula} {k n: nat} :
      In s Gamma ->
      Forall (der Gamma n) (arguments k (substitute ζ s)) ->
      target k (substitute ζ s) = t ->
      der Gamma (S n) t.

Lemma der_0E {n Gamma t} : der Gamma n t -> n = S (Nat.pred n).
Proof. move=> H. by inversion H. Qed.

Lemma derE {n Gamma t} : der Gamma n t ->
  exists (ζ: nat -> formula) (s: formula) (k: nat),
    n = S (Nat.pred n) /\
    In s Gamma /\
    Forall (der Gamma (Nat.pred n)) (arguments k (substitute ζ s)) /\
    target k (substitute ζ s) = t.
Proof. move=> H. inversion H. do 3 eexists. by eauto. Qed.

Lemma der_mon {n m t Gamma} : der Gamma n t -> n <= m -> der Gamma m t.
Proof.
  elim: n m Gamma t; first by move=> > /der_0E.
  move=> n IH m Gamma t.
  move /derE => [ζ [s' [k']]].
  move=> [_ [? [? ?]]] ?.
  have -> : m = S (Nat.pred m) by lia.
  apply: der_var; try eassumption.
  apply: Forall_impl; last by eassumption.
  move=> ? /IH. apply. by lia.
Qed.

Lemma target_S {r s t k} : target k r = arr s t -> target (S k) r = t.
Proof.
  elim: k r s t; first by move=> > /= ->.
  by move=> k IH [> /= | > /= /IH <-].
Qed.

Lemma arguments_S {r s t k} : target k r = arr s t -> arguments (S k) r = (arguments k r) ++ [s].
Proof.
  elim: k r s t; first by move=> > /= ->.
  by move=> k IH [> /= | > /= /IH <-].
Qed.

Lemma hsc_der {Gamma t} : hsc Gamma t -> exists n, der Gamma n t.
Proof.
  elim.
  - move=> ζ s /der_var => /(_ ζ (substitute ζ s) 0 0).
    move /(_ ltac:(by constructor)). move /(_ ltac:(done)).
    move=> ?. by exists 1.
  - move=> s' t' _ [n1 /derE +] _ [n2 /derE].
    move=> [ζ1 [s1 [k1 [-> [Hs1 [? Hk1]]]]]].
    move=> [ζ2 [s2 [k2 [-> [? [? ?]]]]]].
    exists (S (S (n1+n2))). apply: (der_var _ (ζ := ζ1) (s := s1) (k := S k1)).
      + done.
      + rewrite (arguments_S ltac:(eassumption)). apply /Forall_app. constructor.
        * apply: Forall_impl; last eassumption.
          move=> ? /der_mon. apply. by lia.
        * constructor; last done.
          apply: der_var; last eassumption; first done.
          apply: Forall_impl; last eassumption.
          move=> ? /der_mon. apply. by lia.
      + apply: target_S. by eassumption.
Qed.

Lemma der_hsc {Gamma t n} : der Gamma n t -> hsc Gamma t.
Proof.
  elim: n Gamma t; first by move=> > /der_0E.
  move=> n IH Gamma t /derE.
  move=> [ζ [s [k [-> [? [+ +]]]]]].
  have : hsc Gamma (substitute ζ s) by apply: hsc_var.
  move: IH. clear. move: (substitute ζ s) => {}s. clear.
  move=> IH. elim: k s.
  { move=> s /= *. by subst t. }
  move=> k IHk. case.
  { move=> ? /= *. by subst t. }
  move=> s1 s2 /= /hsc_arr + /ForallE [/IH H].
  by move=> /(_ H){H} /IHk.
Qed.