Library Continuations.FOUnify_cps.nat_term_eq_quasiterm



Require Import Arith.
Require Import nat_complements.


Section nat_sequence.

Inductive list_nat : Set :=
  | nil_nat : list_nat
  | cons_nat : natlist_natlist_nat.

Fixpoint At_last (x : nat) (l : list_nat) {struct l} : list_nat :=
  match l return list_nat with
  | nil_nat
       cons_nat x nil_nat
      
  | cons_nat c llcons_nat c (At_last x ll)
  end.

Fixpoint List_queue_nat (l : list_nat) : list_nat :=
  match l return list_nat with
  | nil_nat
       nil_nat
      
  | cons_nat c tailAt_last c (List_queue_nat tail)
  end.

Fixpoint Constr_f (l : list_nat) : natnat :=
  fun n : nat
  match l return nat with
  | nil_nat
       0
  | cons_nat m tail
      match n return nat with
      | O
           m
          
      | S pConstr_f tail p
      end
  end.


Inductive OK_Constr_f (f : list_natnatnat) : Prop :=
    OK_Constr_f_init :
      ( x : nat, 0 = f nil_nat x :>nat) →
      ( (val : nat) (l : list_nat), val = f (cons_nat val l) 0 :>nat) →
      ( (x val : nat) (l : list_nat),
       f l x = f (cons_nat val l) (S x) :>nat) → OK_Constr_f f.

Lemma Constr_f_OK : OK_Constr_f Constr_f.
apply OK_Constr_f_init; simpl in |- *; auto; simple induction x;
 simpl in |- *; auto.
Qed.

Inductive OK_At_last (f : natlist_natlist_nat) : Prop :=
    OK_At_last_init :
      ( x : nat, cons_nat x nil_nat = f x nil_nat :>list_nat) →
      ( x y : nat,
       cons_nat y (cons_nat x nil_nat) = f x (f y nil_nat) :>list_nat) →
      OK_At_last f.

Lemma At_last_OK : OK_At_last At_last.
apply OK_At_last_init; simpl in |- *; auto.
Qed.

Inductive OK_List_queue_nat (f : list_natlist_nat) : Prop :=
    OK_List_queue_nat_init :
      nil_nat = f nil_nat :>list_nat
      ( (x : nat) (l : list_nat),
       At_last x (f l) = f (cons_nat x l) :>list_nat) →
      OK_List_queue_nat f.

Lemma List_queue_nat_OK : OK_List_queue_nat List_queue_nat.
apply OK_List_queue_nat_init; simpl in |- *; auto.
Qed.

End nat_sequence.


Section terms.

Definition fun_ : Set := nat.

Definition var : Set := nat.

Lemma var_eq_decP : x x0 : var, x = x0 :>var x x0.
intros; elim (nat_eq_decP x x0); auto.
Qed.

Lemma var_eq_decS : x x0 : var, {x = x0 :>var} + {x x0}.
intros; elim (nat_eq_decS x x0); auto.
Qed.

Lemma fun_eq_decP : x x0 : fun_, x = x0 :>fun_ x x0.
intros; elim (nat_eq_decP x x0); auto.
Qed.

Lemma fun_eq_decS : x x0 : fun_, {x = x0 :>fun_} + {x x0}.
intros; elim (nat_eq_decS x x0); auto.
Qed.


Inductive quasiterm : Set :=
  | V : varquasiterm
  | C : fun_quasiterm
  | Root : fun_quasitermquasiterm
  | ConsArg : quasitermquasitermquasiterm.


Hypothesis list_arity : list_nat.

Definition arity : fun_nat := Constr_f (List_queue_nat list_arity).


Fixpoint Length (t : quasiterm) : nat :=
  match t return nat with
  | V x ⇒ 1
  | C f ⇒ 1
  | Root f u ⇒ 1
  | ConsArg t1 t2
      Length t1 + Length t2
      
  end.


Definition SIMPLE (t : quasiterm) : Prop :=
  match t return Prop with
  | V xTrue
  | C lTrue
  | Root l uTrue
  | ConsArg t1 t2False
  end.


Inductive l_term : quasitermProp :=
  | l_term_initV : x : var, l_term (V x)
  | l_term_initC : f : fun_, 0 = arity f :>natl_term (C f)
  | l_term_Root :
       (f : fun_) (t : quasiterm),
      l_term tarity f = Length t :>natl_term (Root f t)
  | l_term_ConsArg :
       t1 t2 : quasiterm,
      l_term t1l_term t2SIMPLE t1l_term (ConsArg t1 t2).

Fixpoint L_TERM (t : quasiterm) : Prop :=
  match t return Prop with
  | V xTrue
  | C c ⇒ 0 = arity c
  | Root l tL_TERM t arity l = Length t
  | ConsArg t1 t2SIMPLE t1 L_TERM t1 L_TERM t2
  end.


Lemma L_TERM_l_term : t : quasiterm, L_TERM tl_term t.
intro; elim t; simpl in |- *; intros.
apply l_term_initV; auto.
apply l_term_initC; auto.
apply l_term_Root.
apply H; elim H0; auto.
elim H0; auto.
apply l_term_ConsArg.
apply H; elim H1; intros H2 H3; elim H3; intros; auto.
apply H0; elim H1; intros H2 H3; elim H3; intros; auto.
elim H1; auto.
Qed.

Lemma l_term_L_TERM : t : quasiterm, l_term tL_TERM t.
intros; elim H; simpl in |- *; auto.
Qed.


Inductive term (t : quasiterm) : Prop :=
    term_init : L_TERM tSIMPLE tterm t.


Lemma SIMPLE_decS : t : quasiterm, {SIMPLE t} + {¬ SIMPLE t}.
intros; elim t; simpl in |- *; auto.
Qed.

Lemma L_TERM_decS : t : quasiterm, {L_TERM t} + {¬ L_TERM t}.
simple induction t; simpl in |- *; auto.
intros f; elim (nat_eq_decS 0 (arity f)); intros; simpl in |- *; auto.
intros f y h0; elim (nat_eq_decS (arity f) (Length y)); intros h.
elim h; elim h0; intros; auto.
right; tauto.

right; tauto.

intros y h y0 h0; elim h; intros.
elim h0; intros.
elim (SIMPLE_decS y); intros h1.
auto.
right; tauto.
right; tauto.
right; tauto.
Qed.

Lemma term_decS : t : quasiterm, {term t} + {¬ term t}.
intro; elim (L_TERM_decS t); intros h1; elim (SIMPLE_decS t); intros h2.
left; apply term_init; auto.
right; unfold not in |- *; intros h3; elim h2; elim h3; intros; auto.
right; unfold not in |- *; intros h3; elim h1; elim h3; intros; auto.
right; unfold not in |- *; intros h3; elim h1; elim h3; intros; auto.
Qed.


Lemma Length_n_O : t : quasiterm, {x : nat | Length t = S x}.
simple induction t.
0; simpl in |- *; auto.
0; simpl in |- *; auto.
0; simpl in |- *; auto.
intros qx Hqx qy Hqy.
elim Hqy; elim Hqx; intros x Eqx y Eqy.
(x + Length qy).
simpl in |- ×.
rewrite Eqx; auto.
Qed.

Lemma n_SO_Length_ConsArg :
  t t0 : quasiterm, 1 Length (ConsArg t t0).
intros; elim (Length_n_O t); elim (Length_n_O t0); intros; simpl in |- ×.
replace (Length t) with (S x0); replace (Length t0) with (S x).
elim x0; simpl in |- ×.
discriminate.
intros; discriminate.
Qed.

Lemma SIMPLE_SO : t : quasiterm, SIMPLE t → 1 = Length t :>nat.
simple induction t; simpl in |- *; intros; auto.
absurd False; auto.
Qed.

Lemma Length_SO_term :
  t : quasiterm, L_TERM t → 1 = Length t :>natterm t.
simple induction t; intros; apply term_init; simpl in |- *; auto.
apply (n_SO_Length_ConsArg q q0); auto.
Qed.

Lemma term_L_TERM_Length :
  t : quasiterm, term tL_TERM t 1 = Length t :>nat.
simple induction t.
intros; simpl in |- *; auto.
intros; simpl in |- ×.
split; auto.
elim H; simpl in |- *; intros h; elim h; auto.
simpl in |- *; intros.
split; auto.
elim H0; simpl in |- *; intros h; elim h; intros; split; auto.
simpl in |- *; intros.
split.
elim H1; simpl in |- *; intros; auto.
elim H1; simpl in |- *; intros.
absurd False; auto.
Qed.

End terms.

Section eq_quasiterm.


Definition BC (t : quasiterm) : Prop :=
  match t return Prop with
  | V _False
  | C _True
  | Root _ _False
  | ConsArg _ t2False
  end.

Definition BV (t : quasiterm) : Prop :=
  match t return Prop with
  | V _True
  | C _False
  | Root _ _False
  | ConsArg _ t2False
  end.

Definition BRoot (t : quasiterm) : Prop :=
  match t return Prop with
  | V _False
  | C _False
  | Root _ _True
  | ConsArg _ t2False
  end.

Definition BConsArg (t : quasiterm) : Prop :=
  match t return Prop with
  | V _False
  | C _False
  | Root _ _False
  | ConsArg _ t2True
  end.

Definition Destr1 (t : quasiterm) :=
  match t return quasiterm with
  | V xV x
  | C xC x
  | Root _ pp
  | ConsArg p _p
  end.

Definition Destr2 (t : quasiterm) :=
  match t return quasiterm with
  | V xV x
  | C xC x
  | Root _ pp
  | ConsArg _ qq
  end.

Definition Destrvar (X : var) (t : quasiterm) :=
  match t return var with
  | V xx
  | C _X
  | Root _ _X
  | ConsArg _ _X
  end.

Definition Destrfun (F : fun_) (t : quasiterm) :=
  match t return fun_ with
  | V _F
  | C ll
  | Root l _l
  | ConsArg p qF
  end.


Lemma proj_C : l1 l2 : fun_, C l1 = C l2 :>quasiterml1 = l2 :>fun_.
intros; replace l1 with (Destrfun l1 (C l1)); auto.
replace l2 with (Destrfun l1 (C l2)); auto.
elim H; auto.
Qed.

Lemma proj_V : x1 x2 : var, V x1 = V x2 :>quasitermx1 = x2 :>var.
intros; replace x1 with (Destrvar x1 (V x1)); auto.
replace x2 with (Destrvar x1 (V x2)); auto.
elim H; auto.
Qed.

Lemma proj_Root1 :
  (t1 t2 : quasiterm) (l1 l2 : fun_),
 Root l1 t1 = Root l2 t2 :>quasiterml1 = l2 :>fun_.
intros; replace l1 with (Destrfun l1 (Root l1 t1)); auto.
replace l2 with (Destrfun l1 (Root l2 t2)); auto.
elim H; auto.
Qed.

Lemma proj_Root2 :
  (t1 t2 : quasiterm) (l1 l2 : fun_),
 Root l1 t1 = Root l2 t2 :>quasitermt1 = t2 :>quasiterm.
intros; replace t1 with (Destr1 (Root l1 t1)); auto.
replace t2 with (Destr2 (Root l2 t2)); auto.
elim H; auto.
Qed.

Lemma proj_ConsArg1 :
  t1 t2 t3 t4 : quasiterm,
 ConsArg t1 t2 = ConsArg t3 t4 :>quasitermt1 = t3 :>quasiterm.
intros; replace t1 with (Destr1 (ConsArg t1 t2)); auto.
replace t3 with (Destr1 (ConsArg t3 t4)); auto.
elim H; auto.
Qed.

Lemma proj_ConsArg2 :
  t1 t2 t3 t4 : quasiterm,
 ConsArg t1 t2 = ConsArg t3 t4 :>quasitermt2 = t4 :>quasiterm.
intros; replace t2 with (Destr2 (ConsArg t1 t2)); auto.
replace t4 with (Destr2 (ConsArg t3 t4)); auto.
elim H; auto.
Qed.

Lemma C_diff_C : l l0 : fun_, l l0C l C l0 :>quasiterm.
unfold not in |- *; intros; elim H; apply proj_C; auto.
Qed.

Lemma V_diff_V : x y : var, x y :>varV x V y :>quasiterm.
unfold not in |- *; intros; elim H; apply proj_V; auto.
Qed.

Lemma ConsArg_diff_ConsArg :
  t t0 t1 t2 : quasiterm,
 t t1 :>quasiterm t0 t2 :>quasiterm
 ConsArg t t0 ConsArg t1 t2 :>quasiterm.
unfold not in |- *; intros; elim H; intros; elim H1.
apply proj_ConsArg1 with t0 t2; auto.
apply proj_ConsArg2 with t t1; auto.
Qed.

Lemma Root_diff_Root :
  (l l0 : fun_) (t t0 : quasiterm),
 l l0 :>fun_ t t0 :>quasitermRoot l t Root l0 t0 :>quasiterm.
unfold not in |- *; intros; elim H; intros; elim H1.
apply proj_Root1 with t t0; auto.
apply proj_Root2 with l l0; auto.
Qed.

Lemma quasiterm_eq_decS :
  t t0 : quasiterm, {t = t0 :>quasiterm} + {t t0 :>quasiterm}.
simple induction t.
simple induction t0.
intros; elim (var_eq_decS v v0); intros H.
elim H; auto.
right; apply V_diff_V; auto.
intros; right; apply (Diff quasiterm BV); simpl in |- *; auto.
intros; right; apply (Diff quasiterm BV); simpl in |- *; auto.
intros; right; apply (Diff quasiterm BV); simpl in |- *; auto.
simple induction t0.
intros; right; apply (Diff quasiterm BC); simpl in |- *; auto.
intros; elim (fun_eq_decS f f0); intros H.
elim H; auto.
right; apply C_diff_C; auto.
intros; right; apply (Diff quasiterm BC); simpl in |- *; auto.
intros; right; apply (Diff quasiterm BC); simpl in |- *; auto.
simple induction t0.
intros; right; apply (Diff quasiterm BRoot); simpl in |- *; auto.
intros; right; apply (Diff quasiterm BRoot); simpl in |- *; auto.
intros.
elim (H q0); intros y.
rewrite y; elim (fun_eq_decS f f0); intros y0.
rewrite y0; auto.
right; simplify_eq; auto.
right; simplify_eq; auto.
intros; right; simplify_eq.
simple induction t0.
intros; right; simplify_eq.
intros; right; simplify_eq.
intros; right; simplify_eq.
intros y1 H1 y2 H2.
elim (H y1); intros E1.
elim (H0 y2); intros E2.
rewrite E1; rewrite E2; auto.
right; simplify_eq; tauto.
right; simplify_eq; tauto.
Qed.

Lemma quasiterm_eq_decP :
  t t0 : quasiterm, t = t0 :>quasiterm t t0.
intros; elim (quasiterm_eq_decS t t0); intros; auto.
Qed.


End eq_quasiterm.