Require Import Arith.
Require Import nat_complements.
Require Import nat_term_eq_quasiterm.
Require Import is_in_quasiterm_term_subst.
Require Import listv_is_in_lv.
Require Import deb_term_unif.


Inductive Unification_s (t1 t2 : quasiterm) : Set :=
    Unif_succeed_def :
      ∀ f : quasisubst,
      unif f t1 t2 →
      idempotent f →
      over f (ConsArg t1 t2) →
      under f (ConsArg t1 t2) →
      min_unif f t1 t2
      
       →
      (∀ l : list_nat,
       L_TERM l t1 →
       L_TERM l t2
        → Length t1 = Length t2 → term_subst l f)
      
       → Unification_s t1 t2.

Inductive Unification_f (t1 t2 : quasiterm) : Prop :=
    Unif_fail_def :
      (∀ f : quasisubst, Subst f t1 ≠ Subst f t2) →
      Unification_f t1 t2.

Inductive Unification_or_fail (t1 t2 : quasiterm) : Set :=
  | Unification_or_fail_succeed :
      Unification_s t1 t2 → Unification_or_fail t1 t2
  | Unification_or_fail_fail :
      Unification_f t1 t2 → Unification_or_fail t1 t2.


Inductive head_diff : quasiterm → quasiterm → Prop :=
  | Fail_hd1 :
      ∀ (l : fun_) (t1 t2 : quasiterm), head_diff (C l) (ConsArg t1 t2)
  | Fail_hd2 :
      ∀ (l : fun_) (t1 t2 : quasiterm), head_diff (ConsArg t1 t2) (C l)
  | Fail_hd3 :
      ∀ (l l0 : fun_) (t : quasiterm), head_diff (C l) (Root l0 t)
  | Fail_hd4 :
      ∀ (l l0 : fun_) (t : quasiterm), head_diff (Root l0 t) (C l)
  | Fail_hd5 :
      ∀ (t1 t2 t3 : quasiterm) (l : fun_),
      head_diff (ConsArg t1 t2) (Root l t3)
  | Fail_hd6 :
      ∀ (t1 t2 t3 : quasiterm) (l : fun_),
      head_diff (Root l t3) (ConsArg t1 t2).

Require Import cps_Nx.

Section algorithmes.

Load "DeclareNx".

Definition Unification (t1 t2 : quasiterm) :=
  Unification_f t1 t2 \/+ Unification_s t1 t2.

Definition Unification_build (t1 t2 : quasiterm) :
  Unification t1 t2 →
  (Unification_f t1 t2 → P) → (Unification_s t1 t2 → X) → X :=
  Nx_handle (Unification_f t1 t2) (Unification_s t1 t2).

Definition Nxunif_unit (t1 t2 : quasiterm) :
  Unification_s t1 t2 → Unification t1 t2 :=
  Nx_unit (Unification_f t1 t2) (Unification_s t1 t2).

Definition Nxunif_raise (t1 t2 : quasiterm) :
  Unification_f t1 t2 → Unification t1 t2 :=
  Nx_raise (Unification_f t1 t2) (Unification_s t1 t2).

Definition Unif_succeed (t1 t2 : quasiterm) (f : quasisubst)
  (u : unif f t1 t2) (i : idempotent f) (o : over f (ConsArg t1 t2))
  (u0 : under f (ConsArg t1 t2)) (m : min_unif f t1 t2)
  (t : ∀ l : list_nat,
       L_TERM l t1 → L_TERM l t2 → Length t1 = Length t2 → term_subst l f) :=
  Nxunif_unit t1 t2 (Unif_succeed_def t1 t2 f u i o u0 m t).

Definition Unif_fail (t1 t2 : quasiterm)
  (e : ∀ f : quasisubst, Subst f t1 ≠ Subst f t2) :=
  Nxunif_raise t1 t2 (Unif_fail_def t1 t2 e).

Definition Unification_elim (t1 t2 t1' t2' : quasiterm) :
  (Unification_s t1 t2 → Unification t1' t2') →
  (Unification_f t1 t2 → Unification_f t1' t2') →
  Unification t1 t2 → Unification t1' t2' :=
  Nx_elim_Nx (Unification_s t1 t2) (Unification_s t1' t2')
    (Unification_f t1 t2) (Unification_f t1' t2').

Goal
∀ t1 t2 t1' t2' : quasiterm,
(∀ (f : quasisubst) (u : unif f t1 t2) (i : idempotent f)
   (o : over f (ConsArg t1 t2)) (u0 : under f (ConsArg t1 t2))
   (m : min_unif f t1 t2)
   (t : ∀ l : list_nat,
        L_TERM l t1 → L_TERM l t2 → Length t1 = Length t2 → term_subst l f),
 Unification t1' t2') →
(∀ n : ∀ f : quasisubst, Subst f t1 ≠ Subst f t2,
 Unification_f t1' t2') → Unification t1 t2 → Unification t1' t2'.
  intros t1 t2 t1' t2' inh_s inh_f nu.
  apply Unification_elim with (3 := nu).
    intro u; elim u; exact inh_s.
    intro u; elim u; exact inh_f.
Defined Unif_elim.

Ltac Elimunif c := apply Unif_elim with (3 := c).

Goal ∀ t1 t2 : quasiterm, head_diff t1 t2 → Unification t1 t2.
intros; apply Unif_fail; elim H; intros.
apply Diff with BC; simpl in |- *; auto with v62.
apply Diff with BConsArg; simpl in |- *; auto with v62.
apply Diff with BC; simpl in |- *; auto with v62.
apply Diff with BRoot; simpl in |- *; auto with v62.
apply Diff with BConsArg; simpl in |- *; auto with v62.
apply Diff with BRoot; simpl in |- *; auto with v62.
Save Decomp_fail.

Hint Resolve Fail_hd1 Fail_hd2 Fail_hd3 Fail_hd4 Fail_hd5 Fail_hd6
  Decomp_fail.


Goal ∀ t1 t2 : quasiterm, Unification t1 t2 → Unification t2 t1.
intros; Elimunif ipattern:H;
 unfold idempotent, over, under, min_unif, unif in |- *;
 intros.
apply Unif_succeed with f;
 unfold idempotent, over, under, min_unif, unif in |- *;
 auto with v62; intros.
apply o; unfold not in |- *; intros h; elim H0; simpl in |- *; elim h;
 auto with v62.
simpl in |- *; elim (u0 x y); auto with v62.
apply Unif_fail_def; intros.
unfold not in |- *; intros; elim (n f); auto with v62.
Save sym_Unification.


Goal ∀ (n : var) (t : quasiterm), Unification (V n) t.
intros; elim (IS_IN_decS n t); intros.
elim (quasiterm_eq_decS (V n) t); intros.
elim a0; apply Unif_succeed with (fun x : var ⇒ V x);
 unfold unif, idempotent, over, under in |- *; simpl in |- *;
 auto with v62; intros.
absurd (V y = V y); auto with v62.
unfold min_unif, unif in |- *; intros.
apply less_subst_init with g; auto with v62.
apply term_subst_init; intros; apply term_init; simpl in |- *; auto with v62.
apply Unif_fail; intros; apply SUB_diff.
simpl in |- *; apply IS_IN_SUB; auto with v62.
elim (sig_elem_subst n t); intros.
apply Unif_succeed with x; unfold unif, idempotent, over, under in |- *;
 simpl in |- *; elim p; intros.
replace (x n) with t; auto with v62.
apply elem_subst_conserve with n; auto with v62.
elim (var_eq_decP n x0); intros.
elim (H0 x0); auto with v62.
apply elem_subst_conserve with n; auto with v62.
elim (H x0); simpl in |- *; auto with v62.
elim (var_eq_decP x0 n); intros.
elim H1; auto with v62.
elim (H x0); auto with v62.
elim (var_eq_decP n y); intros.
replace t with (x y); auto with v62.
symmetry in |- *; auto with v62.
absurd (V y = x y); auto with v62.
unfold min_unif, unif in |- *; intros.
apply less_subst_init with g.
intros; elim (var_eq_decP n x0); intros.
elim H2; elim (H0 n); auto with v62.
elim (H x0); auto with v62.
apply term_subst_init.
intros; elim (var_eq_decP x0 n); intros.
elim (H0 x0); auto with v62.
apply Length_SO_term; auto with v62.
elim (H x0).
apply term_init; simpl in |- *; auto with v62.
unfold not in |- *; intros; elim H4; auto with v62.
Save UnifV1.

Goal ∀ (t : quasiterm) (x : var), Unification t (V x).
intros; apply sym_Unification; apply UnifV1.
Save UnifV2.

Hint Resolve UnifV1 UnifV2.


Goal ∀ (t : quasiterm) (l : fun_), Unification (C l) t.
simple induction t; auto with v62.
intros; elim (fun_eq_decS l f); intros.
elim a; apply Unif_succeed with V;
 unfold unif, idempotent, over, under in |- *; simpl in |- *;
 auto with v62.
unfold min_unif, unif in |- *; intros.
apply less_subst_init with g; auto with v62.
intros; apply term_subst_init; intros; apply term_init; simpl in |- *;
 auto with v62.
apply Unif_fail; intros; simpl in |- ×.
apply C_diff_C; auto with v62.
Save UnifC1.

Goal ∀ (t : quasiterm) (l : fun_), Unification t (C l).
intros; apply sym_Unification; apply UnifC1.
Save UnifC2.

Hint Resolve UnifC1 UnifC2.


Goal
∀ (t1 t2 : quasiterm) (l1 l2 : fun_),
Unification t1 t2 → Unification (Root l1 t1) (Root l2 t2).
intros; elim (fun_eq_decS l1 l2); intros.
elim a; Elimunif H; unfold unif, idempotent, over, under in |- *; intros.
apply Unif_succeed with f; unfold unif, idempotent, over, under in |- *;
 simpl in |- *; auto with v62.
elim u; auto with v62.
unfold min_unif, unif in |- *; simpl in |- *; intros.
apply m; unfold unif in |- ×.
apply proj_Root2 with l1 l1; auto with v62.
intros.
elim H0; elim H1; intros; apply t; auto with v62.
elim H4; auto with v62.
apply Unif_fail_def; intros.
simpl in |- *; apply Root_diff_Root; auto with v62.
apply Unif_fail; intros.
simpl in |- *; apply Root_diff_Root; auto with v62.
Save UnifRoot.

Hint Resolve UnifRoot.


Goal
∀ t1 t2 t3 t4 : quasiterm,
(∀ f : quasisubst, Subst f t1 ≠ Subst f t3 :>quasiterm) →
Unification_f (ConsArg t1 t2) (ConsArg t3 t4).
intros; apply Unif_fail_def; intros.
simpl in |- *; apply ConsArg_diff_ConsArg; auto with v62.
Save UnifConsArgfail1.

Hint Resolve UnifConsArgfail1.


Goal
∀ t1 t2 : quasiterm,
DIFFELNB (list_var (ConsArg t1 t2)) 0 → Unification t1 t2.
intros; elim (quasiterm_eq_decS t1 t2); intros.
elim a.
apply Unif_succeed with V;
 unfold unif, idempotent, over, under, min_unif in |- *;
 auto with v62.
intros.
absurd (V y = V y); auto with v62.
intros; apply less_subst_init with g; auto with v62.
intros; apply term_subst_init; intros; apply term_init; simpl in |- *;
 auto with v62.
apply Unif_fail; intros.
elim (clossubst t1 f).
elim (clossubst t2 f); auto with v62.
apply closConsArg2 with t1; apply DIFFELNB_O_clos; auto with v62.
apply closConsArg1 with t2; apply DIFFELNB_O_clos; auto with v62.
Save Unif_DIFFELNB_O.


Goal
∀ (t1 t2 t3 t4 : quasiterm) (n : nat),
DIFFELNB (list_var (ConsArg (ConsArg t1 t2) (ConsArg t3 t4))) n →
∀ n0 : nat,
DIFFELNB (list_var (ConsArg t2 t4)) n0 → {S n0 ≤ n} + {n0 = n :>nat}.
intros; elim (le_decS n0 n); intros.
apply (le_S_eqS n0 n a).
absurd (n0 ≤ n); auto with v62.
apply
 inclv_le
  with
    (list_var (ConsArg t2 t4))
    (list_var (ConsArg (ConsArg t1 t2) (ConsArg t3 t4)));
 auto with v62.
apply inclv_init; intros; apply IS_IN_IS_IN_LV; simpl in |- ×.
elim (IS_IN_LV_IS_IN (ConsArg t2 t4) y H1); auto with v62.
Save DIFFELNB_ConsArg_ConsArg24_le.

Goal
∀ (t1 t2 t3 t4 : quasiterm) (n : nat),
DIFFELNB (list_var (ConsArg (ConsArg t1 t2) (ConsArg t3 t4))) n →
∀ n0 : nat,
DIFFELNB (list_var (ConsArg t1 t3)) n0 → {S n0 ≤ n} + {n0 = n :>nat}.
intros; elim (le_decS n0 n); intros h.
apply (le_S_eqS n0 n h).
absurd (n0 ≤ n); auto with v62.
apply
 inclv_le
  with
    (list_var (ConsArg t1 t3))
    (list_var (ConsArg (ConsArg t1 t2) (ConsArg t3 t4)));
 auto with v62.
apply inclv_init; intros; apply IS_IN_IS_IN_LV; simpl in |- ×.
elim (IS_IN_LV_IS_IN (ConsArg t1 t3) y H1); auto with v62.
Save DIFFELNB_ConsArg_ConsArg13_le.

Hint Resolve eq_V_stab.


Goal
∀ (t1 t2 u1 u2 : quasiterm) (f g : quasisubst),
unif f t1 u1 →
unif g (Subst f t2) (Subst f u2) →
unif (fun x : var ⇒ Subst g (f x)) (ConsArg t1 t2) (ConsArg u1 u2).
unfold unif in |- *; simpl in |- *; intros.
elim (comp_subst f g t2); elim (comp_subst f g u2); elim (comp_subst f g t1);
 elim (comp_subst f g u1).
elim H; elim H0; auto with v62.
Save unif_comp.

Hint Resolve unif_comp.


Goal
∀ (t1 t2 u1 u2 : quasiterm) (f g : quasisubst),
min_unif f t1 u1 →
min_unif g (Subst f t2) (Subst f u2) →
min_unif (fun x : var ⇒ Subst g (f x)) (ConsArg t1 t2) (ConsArg u1 u2).
unfold min_unif, unif in |- *; simpl in |- *; intros.
elim (H g0); intros.
elim (H0 h); intros.
apply less_subst_init with h0.
intros; elim (H2 x).
elim (exp_comp_subst g h0 (f x)).
apply eq_restriction_s_t; auto with v62.
elim (exp_comp_subst f h t2); elim (exp_comp_subst f h u2).
transitivity (Subst g0 t2).
apply eq_restriction_s_t; auto with v62.
transitivity (Subst g0 u2).
apply proj_ConsArg2 with (Subst g0 t1) (Subst g0 u1); auto with v62; intros.
apply eq_restriction_s_t; auto with v62.
apply proj_ConsArg1 with (Subst g0 t2) (Subst g0 u2); auto with v62; intros.
Save min_unif_comp.

Hint Resolve min_unif_comp.


Goal
∀ (t1 t2 t3 t4 : quasiterm) (f g : quasisubst) (l : list_nat),
L_TERM l (ConsArg t1 t2) →
L_TERM l (ConsArg t3 t4) →
Length (ConsArg t1 t2) = Length (ConsArg t3 t4) :>nat →
(∀ l : list_nat,
 L_TERM l t1 → L_TERM l t3 → Length t1 = Length t3 :>nat → term_subst l f) →
(∀ l : list_nat,
 L_TERM l (Subst f t2) →
 L_TERM l (Subst f t4) →
 Length (Subst f t2) = Length (Subst f t4) :>nat → term_subst l g) →
term_subst l (fun x : var ⇒ Subst g (f x)).
simpl in |- *; intros.
elim H; elim H0; intros.
elim H5; elim H7; intros.
cut (term_subst l f).
intros hyp; apply term_subst_init.
intros; simpl in |- *; apply term_term_subst.
elim hyp; auto with v62.
apply H3; try apply L_TERM_term_subst; auto with v62.
elim (term_subst_eq_Length l f t2); elim (term_subst_eq_Length l f t4);
 auto with v62.
cut (Length t1 + Length t2 = Length t3 + Length t4); auto with v62.
replace (Length t1) with 1; try apply SIMPLE_SO; auto with v62.
replace (Length t3) with 1; try apply SIMPLE_SO; auto with v62.
apply (H2 l H8 H10).
replace (Length t1) with 1; try apply SIMPLE_SO; auto with v62.
Save term_subst_comp.


Hint Resolve over_comp under_comp.

Goal
∀ (t1 t2 t3 t4 : quasiterm) (f g : quasisubst),
unif f t1 t3 →
idempotent f →
over f (ConsArg t1 t3) →
under f (ConsArg t1 t3) →
min_unif f t1 t3 →
(∀ l : list_nat,
 L_TERM l t1 → L_TERM l t3 → Length t1 = Length t3 :>nat → term_subst l f) →
unif g (Subst f t2) (Subst f t4) →
idempotent g →
over g (ConsArg (Subst f t2) (Subst f t4)) →
under g (ConsArg (Subst f t2) (Subst f t4)) →
min_unif g (Subst f t2) (Subst f t4) →
(∀ l : list_nat,
 L_TERM l (Subst f t2) →
 L_TERM l (Subst f t4) →
 Length (Subst f t2) = Length (Subst f t4) :>nat → term_subst l g) →
Unification (ConsArg t1 t2) (ConsArg t3 t4).
intros; apply Unif_succeed with (fun x : var ⇒ Subst g (f x)); intros;
 auto with v62.
apply (idempotent_Fondamental (ConsArg t2 t4)); auto with v62.
apply term_subst_comp with t1 t2 t3 t4; auto with v62.
Save two_succes.


Goal
∀ (t1 t2 t3 t4 : quasiterm) (f : quasisubst),
unif f t1 t3 →
idempotent f →
min_unif f t1 t3 →
(∀ g : quasisubst,
 Subst g (Subst f t2) ≠ Subst g (Subst f t4) :>quasiterm)
 → Unification_f (ConsArg t1 t2) (ConsArg t3 t4).
unfold unif, idempotent, over, under, min_unif in |- *; intros;
 apply Unif_fail_def; intros.
unfold not in |- *; simpl in |- *; intros.
elim (H2 f0).
elim (H1 f0); unfold unif in |- *; intros.
elim (exp_comp_subst f f0 t2); elim (exp_comp_subst f f0 t4).
replace (Subst (fun x : var ⇒ Subst f0 (f x)) t2) with (Subst f0 t2).
replace (Subst (fun x : var ⇒ Subst f0 (f x)) t4) with (Subst f0 t4).
apply proj_ConsArg2 with (Subst f0 t1) (Subst f0 t3); auto with v62.
apply eq_restriction_s_t; intros.
elim (H4 x).
replace (Subst h (f x)) with (Subst h (Subst f (f x))).
elim (exp_comp_subst f h (f x)); apply eq_restriction_s_t; auto with v62.
elim H0; auto with v62.
apply eq_restriction_s_t; intros.
elim (H4 x).
replace (Subst h (f x)) with (Subst h (Subst f (f x))).
elim (exp_comp_subst f h (f x)); apply eq_restriction_s_t; auto with v62.
elim H0; auto with v62.
apply proj_ConsArg1 with (Subst f0 t2) (Subst f0 t4); auto with v62.
Save one_only_succes.


Goal
∀ (t1 t2 t3 t4 : quasiterm) (f : quasisubst),
(∀ x : var, V x = f x :>quasiterm) →
unif f t1 t3 →
Unification t2 t4 → Unification (ConsArg t1 t2) (ConsArg t3 t4).
unfold unif in |- *; intros.
Elimunif H1; unfold unif, over, under, idempotent, min_unif in |- *; intros.
apply two_succes with f f0; replace (Subst f t2) with t2;
 replace (Subst f t4) with t4;
 unfold unif, over, under, idempotent, dom in |- *;
 simpl in |- *; auto with v62.
intros; absurd (V y = f y :>quasiterm); auto with v62.
unfold min_unif in |- *; intros.
apply less_subst_init with g.
intros; elim (H x); auto with v62.
intros; apply term_subst_init; intros; apply term_init;
     elim H; simpl in |- *; auto with v62.
apply Unif_fail_def.
simpl in |- *; intros; unfold not in |- *; intros.
elim (n f0); apply proj_ConsArg2 with (Subst f0 t1) (Subst f0 t3);
 auto with v62.
Save eq_V_stab3.


Goal
∀ (n : nat) (u1 u2 : quasiterm),
DIFFELNB (list_var (ConsArg u1 u2)) n → Unification u1 u2.
intros n; pattern n in |- *; apply (ind_leS n).

intros; apply Unif_DIFFELNB_O; auto with v62.
simple induction u1; auto with v62. simple induction u2; auto with v62. simple induction u2; auto with v62. intros.

elim (DIFFELNBor (list_var (ConsArg q q1))); intros p0 H5.

elim (DIFFELNB_ConsArg_ConsArg13_le q q0 q1 q2 (S p) H4 p0 H5); intros.


Elimunif (H p0 (le_S_n p0 p a) q q1 H5); intros.
2: auto with v62.

elim (ident_or_notS (ConsArg q q1) f o); intros.

elim a0; intros x H6.

cut (Unification (Subst f q0) (Subst f q2)).
intros H7; Elimunif H7; intros.
apply two_succes with f f0; auto with v62.
apply one_only_succes with f; auto with v62.

elim (DIFFELNBor (list_var (ConsArg (Subst f q0) (Subst f q2))));
 intros p1 H7.
apply (H p1); auto with v62.
apply le_S_n; apply (f_n_id_minus q q0 q1 q2 (S p)) with f; auto with v62.
∃ x; auto with v62.

apply eq_V_stab3 with f; auto with v62.
elim (DIFFELNBor (list_var (ConsArg q0 q2))); intros p1 H6.
elim (DIFFELNB_ConsArg_ConsArg24_le q q0 q1 q2 (S p) H4 p1 H6); intros.
apply (H p1 (le_S_n p1 p a0) q0 q2); auto with v62.
apply (H1 q2); elim b0; auto with v62.


cut (Unification q q1); [ intro H0' | apply (H0 q1); elim b; auto with v62 ].
Elimunif H0'; auto with v62; intros. elim (ident_or_notS (ConsArg q q1) f o); intros.
elim a; intros x H6.

cut (Unification (Subst f q0) (Subst f q2)).
intros H7; Elimunif H7; intros.
apply two_succes with f f0; auto with v62.
apply one_only_succes with f; auto with v62.

elim (DIFFELNBor (list_var (ConsArg (Subst f q0) (Subst f q2))));
 intros p1 H7.
apply (H p1); auto with v62.
apply le_S_n; apply (f_n_id_minus q q0 q1 q2 (S p)) with f; auto with v62.
∃ x; auto with v62.

apply eq_V_stab3 with f; auto with v62.
elim (DIFFELNBor (list_var (ConsArg q0 q2))); intros p1 H6.
elim (DIFFELNB_ConsArg_ConsArg24_le q q0 q1 q2 (S p) H4 p1 H6); intros.
apply (H p1); auto with v62. apply (H1 q2); elim b1; auto with v62.
Save proof_unif.

Goal ∀ t u : quasiterm, Unification t u.
intros; elim (DIFFELNBor (list_var (ConsArg t u))); intros n0 p;
 apply proof_unif with n0; auto with v62.
Save unif_proof.

End algorithmes.

Goal ∀ t u : quasiterm, Unification_or_fail t u.
  intros; apply Unification_build with (Unification_f t u) t u.
    apply unif_proof. intro c; apply Unification_or_fail_fail; exact c.
    intro c; exact c.
    intro res; apply Unification_or_fail_succeed; exact res.
Save unif_call.