Require Export Base.

Definition var := nat.

Inductive ter : Type :=
| V : var → ter
| T : ter → ter → ter.

Definition eqn := prod ter ter.

Implicit Types x y z : var.
Implicit Types s t u v : ter.
Implicit Types sigma tau : ter → ter.
Implicit Types A B C : list eqn.
Implicit Type e : eqn.
Implicit Types m n k : nat.

Definition subst sigma : Prop :=
 ∀ s t, sigma (T s t) = T (sigma s) (sigma t).

Definition unif sigma A : Prop :=
 subst sigma ∧
 ∀ s t, (s,t) el A → sigma s = sigma t.

Definition unifiable A : Prop :=
  ∃ sigma, unif sigma A.

Definition principal_unifier sigma A : Prop :=
 unif sigma A ∧
 ∀ tau, unif tau A → ∀ s, tau (sigma s) = tau s.

Definition idempotent X (f : X → X) : Prop :=
 ∀ x : X, f (f x) = f x.

Lemma subst_id :
 subst (fun s ⇒ s).

Lemma principal_idempotent sigma A :
 principal_unifier sigma A → idempotent sigma.

Lemma unif_cons sigma s t A :
 unif sigma ((s,t)::A) ↔ sigma s = sigma t ∧ unif sigma A.

Lemma unif_app sigma A B :
  unif sigma (A ++ B) ↔ unif sigma A ∧ unif sigma B.

Fixpoint vart s : list var :=
 match s with
   | V x ⇒ [x]
   | T s1 s2 ⇒ vart s1 ++ vart s2
 end.

Fixpoint varl A : list var :=
 match A with
   | nil ⇒ nil
   | (s,t)::A' ⇒ vart s ++ vart t ++ varl A'
 end.

Fixpoint dom A : list var :=
 match A with
   | (V x, s) :: A' ⇒ x :: dom A'
   | _ ⇒ nil
 end.

Lemma dom_varl A :
 dom A <<= varl A.

Lemma varl_app A B :
 varl (A ++ B) = varl A ++ varl B.

Lemma vart_incl_varl s t A :
  (s,t) el A → vart s <<= varl A ∧ vart t <<= varl A.

Lemma varl_incl A B :
 A <<= B → varl A <<= varl B.

Fixpoint rep s x t : ter :=
 match s with
   | V y ⇒ if decision (x = y) then t else V y
   | T s1 s2 ⇒ T (rep s1 x t) (rep s2 x t)
 end.

Definition repe e x s : eqn :=
 let (u,v) := e in (rep u x s , rep v x s).

Definition repl A x s := map (fun e ⇒ repe e x s) A.

Lemma rep_xx x t :
 rep (V x) x t = t.

Lemma rep_id x s t :
 ¬ x el vart s → rep s x t = s.

Lemma rep_id_subst sigma x s t :
 subst sigma → sigma (V x) = sigma t → sigma (rep s x t) = sigma s.

Lemma rep_var s x t :
  vart (rep s x t) <<= vart s ++ vart t.

Lemma repl_var A x t :
  varl (repl A x t) <<= vart t ++ varl A.

Lemma rep_var_not_in x s t :
  ¬ x el vart s → ¬ x el vart (rep t x s).

Lemma repl_var_elim A x s :
  ¬ x el vart s → ¬ x el varl (repl A x s).

Inductive solved : list (ter × ter) → Prop :=
| solvedN :
   solved nil
| solvedC x s A :
   ¬ x el vart s → ¬ x el dom A → disjoint (vart s) (dom A) →
   solved A → solved ((V x, s) :: A).

Fixpoint phi A s : ter :=
 match A with
   | (V x, t) :: A' ⇒ (rep (phi A' s) x t)
   | _ ⇒ s
 end.

Lemma phi_subst A :
 subst (phi A).

Lemma phi_id A s :
 disjoint (dom A) (vart s) → phi A s = s.

Lemma phi_unif A :
 solved A → unif (phi A) A.

Lemma phi_principal sigma A s :
  unif sigma A → sigma (phi A s) = sigma s.

Theorem solved_principal A :
 solved A → principal_unifier (phi A) A.

Fixpoint size s : nat :=
  match s with
    | V _ ⇒ 1
    | T s1 s2 ⇒ 1 + size s1 + size s2
  end.

Lemma subst_size x s sigma :
  subst sigma → x el vart s → size (sigma (V x)) ≤ size (sigma s).

Lemma bad_eqn x s sigma :
  subst sigma → x el vart s → V x ≠ s → sigma (V x) ≠ sigma s.

Definition ueq A B : Prop :=
  ∀ sigma, unif sigma A ↔ unif sigma B.

Definition red A B : Prop :=
 varl B <<= varl A ∧ ueq A B.

Lemma ueq_sym A B :
  ueq A B → ueq B A.

Lemma ueq_principal_unifier A B sigma :
 ueq A B → principal_unifier sigma A → principal_unifier sigma B.

Instance red_preorder :
  PreOrder red.

Instance equi_red :
 subrelation (@equi eqn) red.

Instance cons_red_proper e :
  Proper (red ==> red) (cons e).

Instance app_red_proper :
 Proper (red ==> red ==> red) (@app eqn).

Instance unif_red_proper sigma :
 Proper (red ==> iff) (unif sigma).

Lemma red_delete s :
 red [(s,s)] nil.

Lemma red_swap s t:
 red [(s,t)] [(t,s)].

Lemma red_decompose s1 s2 t1 t2 :
 red [(T s1 s2, T t1 t2)] [(s1, t1); (s2, t2)].

(* The next 2 lemmas have smart proof scripts avoiding combinatorial explosion *)

Lemma repl_unif sigma x t A :
  sigma (V x) = sigma t → (unif sigma A ↔ unif sigma (repl A x t)).

Lemma repl_ueq x t A :
  ueq ((V x, t) :: A) ((V x, t) :: repl A x t).

Lemma red_repl x t A :
 red ((V x,t)::A) ((V x,t)::repl A x t).

Inductive presolved : list eqn → Prop :=
| presolvedN : presolved nil
| presolvedC x s A : V x ≠ s → presolved ((V x, s) :: A).

Instance ter_eq_dec :
 eq_dec ter.

Fixpoint pre' s t : list eqn :=
 if decision (s=t) then nil
 else match s, t with
        | V _, _ ⇒ [(s,t)]
        |_, V _ ⇒ [(t,s)]
        | T s1 s2, T t1 t2 ⇒ pre' s1 t1 ++ pre' s2 t2
      end.

Fixpoint pre A : list eqn :=
 match A with
   | nil ⇒ nil
   | (s,t) :: A' ⇒ pre' s t ++ pre A'
 end.

Lemma pre'_red s t :
 red [(s,t)] (pre' s t).

Lemma pre_red A :
 red A (pre A).

Lemma presolved_app A B :
 presolved A → presolved B → presolved (A ++ B).

Lemma pre'_presolved s t :
 presolved (pre' s t).

Lemma pre_presolved A :
 presolved (pre A).

Fixpoint solveN n A B : option (list eqn) :=
  match n, pre B with
    | O, _ ⇒ None
    | S n', (V x, t) :: C ⇒ if decision (x el vart t) then None
                             else solveN n' ((V x, t)::A) (repl C x t)
    | _, _ ⇒ Some A
 end.

Definition solve C : option (list eqn) :=
 solveN (S (card (varl C))) nil C.

Lemma solveN_correct A B C n :
 red C (A ++ B) →
 solved A →
 disjoint (dom A) (varl B) →
 card (varl B) < n →
 match solveN n A B with
   | Some A' ⇒ red C A' ∧ solved A'
   | None ⇒ ¬ unifiable C
 end.
 trivially unifiable *)
 nonunifiable *)
 eliminable variable *)

Theorem solve_correct C :
  match solve C with
    | Some A ⇒ red C A ∧ solved A
    | None ⇒ ¬ unifiable C
  end.

Theorem solved_form_exists A :
 { B | red A B ∧ solved B } + { ¬ unifiable A }.

Theorem principal_unifier_exists A :
  { sigma | principal_unifier sigma A } + { ¬ unifiable A }.