From Coq Require Import Arith Lia Compare_dec Relations
  Wellfounded Wf_nat List Bool Eqdep_dec Ensembles ArithRing Logic.

From hydras Require Import More_Arith Restriction
     DecPreOrder rpo.term rpo.rpo Epsilon0.T1.

Set Implicit Arguments.

Create HintDb rpo.

Module Alt.

Module Eps0_sig <: Signature.

  Inductive symb0 : Set := nat_0 | nat_S | ord_zero | ord_cons.
  Definition symb := symb0.

  Lemma eq_symbol_dec : ∀ f1 f2 : symb, {f1 = f2} + {f1 ≠ f2}.

  Inductive arity_type : Set :=
  | AC : arity_type
  | C : arity_type
  | Free : nat → arity_type.

  Definition arity : symb → arity_type :=
    fun f ⇒ match f with
             | nat_0 ⇒ Free 0
             | ord_zero ⇒ Free 0
             | nat_S ⇒ Free 1
             | ord_cons ⇒ Free 3
             end.
End Eps0_sig.

Module Vars <: Variables.

  Inductive empty_set : Set := .
  Definition var := empty_set.

  Lemma eq_variable_dec : ∀ v1 v2 : var, {v1 = v2} + {v1 ≠ v2}.

End Vars.

Module Eps0_prec <: Precedence.

  Definition A : Set := Eps0_sig.symb.
  Import Eps0_sig.

  Definition prec : relation A :=
    fun f g ⇒ match f, g with
               | nat_0, nat_S ⇒ True
               | nat_0, ord_zero ⇒ True
               | nat_0, ord_cons ⇒ True
               | ord_zero, nat_S ⇒ True
               | ord_zero, ord_cons ⇒ True
               | nat_S, ord_cons ⇒ True
               | _, _ ⇒ False
               end.

  Inductive status_type : Set :=
  | Lex : status_type
  | Mul : status_type.

  Definition status : A → status_type := fun f ⇒ Lex.

  Lemma prec_dec : ∀ a1 a2 : A, {prec a1 a2} + {¬ prec a1 a2}.

  Lemma prec_antisym : ∀ s, prec s s → False.

  Lemma prec_transitive : transitive A prec.

End Eps0_prec.

Module Eps0_alg <: Term := term.Make (Eps0_sig) (Vars).
Module Eps0_rpo <: RPO := rpo.Make (Eps0_alg) (Eps0_prec).

Import Eps0_alg Eps0_rpo Eps0_sig.

Fixpoint nat_2_term (n:nat) : term :=
  match n with 0 ⇒ (Term nat_0 nil)
             | S p ⇒ Term nat_S ((nat_2_term p)::nil)
  end.

Lemma nat_lt_cons : ∀ (n:nat) a p b ,
    rpo (nat_2_term n) (Term ord_cons (a::p::b::nil)).

Theorem rpo_trans (t t1 t2: term): rpo t t1 → rpo t1 t2 → rpo t t2.

Fixpoint T1_2_term (a:T1) : term :=
match a with
| zero ⇒ Term ord_zero nil
| cons a n b ⇒
    Term ord_cons (T1_2_term a :: nat_2_term n ::T1_2_term b::nil)
end.

Fixpoint T1_size (o:T1):nat :=
 match o with zero ⇒ 0
            | cons a n b ⇒ S (T1_size a + n + T1_size b)%nat
         end.

Lemma T1_size1 a n b: T1_size zero < T1_size (cons a n b).

Lemma T1_size2 a n b: T1_size a < T1_size (cons a n b).

Lemma T1_size3 a n b: T1_size b < T1_size (cons a n b).

#[global] Hint Resolve T1_size2 T1_size3 : rpo.

Lemma lt_subterm1 a a' n' b': lt a a' → lt a (cons a' n' b').

Lemma lt_subterm2 a a' n n' b b':
  lt a a' →
  nf (cons a n b) →
  nf (cons a' n' b') →
  lt b (cons a' n' b').

#[global] Hint Resolve nat_lt_cons : rpo.
#[global] Hint Resolve lt_subterm2 lt_subterm1 : rpo.
#[global] Hint Resolve T1_size3 T1_size2 T1_size1 : rpo.

Lemma nat_2_term_mono (n n': nat):
  n < n' → rpo (nat_2_term n) (nat_2_term n').


Theorem lt_inc_rpo_0 : ∀ n,
    ∀ o' o, (T1_size o + T1_size o' ≤ n)%nat→
                 lt o o' → nf o → nf o' →
                 rpo (T1_2_term o) (T1_2_term o').

Remark R1 : Acc P.prec nat_0.

#[global] Hint Resolve R1 : rpo.

Remark R2 : Acc P.prec ord_zero.

#[global] Hint Resolve R2 : rpo.

Remark R3 : Acc P.prec nat_S.

#[global] Hint Resolve R3 : rpo.

Remark R4 : Acc P.prec ord_cons.

#[global] Hint Resolve R4 : rpo.

Theorem well_founded_rpo : well_founded rpo.

Section well_founded.

  Let R := restrict nf lt.

  #[local] Hint Unfold restrict R : rpo.

  Lemma R_inc_rpo (o o':T1) :
    R o o' → rpo (T1_2_term o) (T1_2_term o').


  Lemma nf_Wf : well_founded_restriction _ nf lt.

  Lemma nf_Acc : ∀ alpha, nf alpha → Acc LT alpha.

End well_founded.

Definition transfinite_recursor_lt :
  ∀ (P:T1 → Type),
    (∀ x:T1, nf x →
                  (∀ y:T1, nf y → lt y x → P y) → P x) →
    ∀ a, nf a → P a.

Definition transfinite_recursor :
  ∀ (P:T1 → Type),
    (∀ x:T1, nf x →
                  (∀ y:T1, y t1< x → P y) → P x) →
    ∀ a, nf a → P a.

Ltac transfinite_induction_lt a :=
  pattern a; apply transfinite_recursor_lt ;[ | try assumption].

Ltac transfinite_induction a :=
  pattern a; apply transfinite_recursor;[ | try assumption].

End Alt.