Require Export Apps.
Require Import Subst2.

Set Implicit Arguments.

Inductive WN : term -> term -> Prop :=
 | WN_var : forall n l l', WNs l l' -> WN ([n];;l) ([n];;l')
 | WN_abs : forall rho r s, WN r s -> WN (\rho,r) (\rho,s)
 | WN_beta : forall rho (r s:term) l t,
     WN ((sub r s);;l) t -> WN ((\rho,r);;(s::l)) t
with
WNs : list term -> list term -> Prop :=
 | WNs_nil : WNs nil nil
 | WNs_cons : forall r s l l', WN r s -> WNs l l' -> WNs (r::l) (s::l').

Hint Constructors WN.
Hint Constructors WNs.

Lemma WNs_app : forall l ll l' ll', WNs l l' -> WNs ll ll' ->
 WNs (l++ll) (l'++ll').
Proof.
induction l; simpl; intros; inversion_clear H; simpl; auto.
Qed.
Hint Resolve WNs_app.

Lemma WNs_rev : forall l l',
 WNs l l' -> WNs (rev l) (rev l').
Proof.
induction l; simpl; intros; inversion_clear H; simpl; auto.
Qed.

Lemma WNs_last: forall l l' r r',
 WNs (l++r::nil) (l'++r'::nil) -> WNs l l' /\ WN r r'.
Proof.
intros.
generalize (WNs_rev H).
simpl_list.
inversion_clear 1.
generalize (WNs_rev H2).
simpl_list; auto.
Qed.

Lemma WN_occurs :
  forall r r', WN r r' -> forall k, occurs k r = false -> occurs k r' = false.
 Proof.
 intros r r' w.
 set (P:= fun r r' => forall k, occurs k r = false -> occurs k r' = false).
 change (P r r').
 set (Q:= fun l l' => forall k, (existsb (occurs k) l = false) ->
                                           (existsb (occurs k) l' = false)).
 apply WN_WNs_ind with Q; unfold P, Q in *; clear P Q.

 intros.
 rewrite apps_occurs.
 rewrite apps_occurs in H1.
 destruct (orb_false_elim _ _ H1); clear H1.
 rewrite H0; auto with bool.

 intros.
 simpl in *.
 rewrite H0; auto.

 intros.
 simpl in H1.
 rewrite apps_occurs in H1.
 simpl in H1.
 destruct (orb_false_elim _ _ H1); clear H1.
 destruct (orb_false_elim _ _ H2); clear H2.
 apply H0.
 rewrite apps_occurs.
 rewrite H3.
 rewrite (orb_b_false).
 apply sub_occurs; simpl; auto with bool.
 simpl; simpl_arith; auto.

 simpl; auto.

 simpl; intros.
 destruct (orb_false_elim _ _ H3); clear H3.
 rewrite H0; auto.
 rewrite H2; auto.

 auto with bool.
Qed.


 Lemma WN_subk :
   forall r t, WN r t ->
   forall (lk:list nat) sk r',
     let rs := (map Var lk)#sk in
     r = sub r' rs -> exists t', t = sub t' rs /\ WN r' t'.