Require Import List.

Variables T U : Type. (* T : clef, U : elmt *)
Hypothesis T_eq_dec : forall (x y : T), {x=y} + {~x=y}.

Definition empty := nil:(list (T*U)).

Fixpoint find2 (tabl : list (T*U)) (x : T) := match tabl with
  | nil => None
  | (k, v)::q => match T_eq_dec k x with
    | left _ => Some v
    | right _ => find2 q x
  end
end.

Inductive wf : list (T*U) -> Prop :=
  | wf_head : wf empty
  | wf_tail : forall (t : list (T*U)) (k:T) (v:U),
(*                wf t /\ find2 t k = None -> wf ((k,v)::t).*)
                wf t -> find2 t k = None -> wf ((k,v)::t).

Lemma osef_U : forall (t : list (T*U)) (k:T) (v u:U),
                wf ((k,v)::t) -> wf ((k,u)::t).
Proof.
intros. induction t.
+ apply wf_tail.
  - apply wf_head.
  - simpl. reflexivity.
+ apply wf_tail.
  - inversion H. exact H2.
  - unfold find2. destruct a. case T_eq_dec.
    * intro. inversion H. replace t0 in H4. inversion H4. case T_eq_dec.
      { trivial. }
      { contradiction. }
    * intro. destruct t.
      { reflexivity. }
      { destruct p. case T_eq_dec.
        { intro. inversion H. replace t1 in H4. inversion H4. case T_eq_dec.
          { contradiction. }
          { intro. case T_eq_dec. { trivial. } { contradiction. } } }
        { intro. destruct t.
          { reflexivity. }
          { destruct p. case T_eq_dec.
            { intro. inversion H. replace t2 in H4. inversion H4. case T_eq_dec.
              { contradiction. }
              { intro. case T_eq_dec. { contradiction. } { intro. case T_eq_dec.
                { trivial. } { contradiction. } } } }
            { intro. destruct t.
              { reflexivity. }
              { destruct p. case T_eq_dec.
                { intro. inversion H. replace t3 in H4. inversion H4. case T_eq_dec.
                  { contradiction. }
                  { intro. case T_eq_dec. { contradiction. } { intro. case T_eq_dec.
                    { contradiction. } { intro. case T_eq_dec. { trivial. } { contradiction. }}}}}
                { intro. destruct t.
Admitted.


Fixpoint include_table (t1 t2 :list(T*U)) := match t1 with
  | nil => True
  | (k1,_)::q1 => match t2 with
    | nil => False
    | (k2,_)::q2 => match T_eq_dec k1 k2 with (*test sur les clefs uniquement*)
      | left _ => include_table q1 q2
      | right _ => include_table t1 q2
    end
  end
end.

Lemma include_add_es : forall t1 t2 x,
  include_table t1 t2 -> include_table (x::t1) (x::t2).
Proof.
intros. simpl. destruct x.
case T_eq_dec.
+ intro. assumption.
+ contradiction.
Qed.

(*
Lemma add_eq : forall t k0 v0 k v, add2 ((k0,v0)::t) k v = (k0,v0)::(add2 t k v).
Proof.
intros.
simpl.
case T_eq_dec.
+ intros. rewrite e. induction t.
  - simpl.
*)

Lemma include_eq : forall t, include_table t t.
Proof.
intros. induction t.
+ simpl. trivial.
+ apply include_add_es. exact IHt.
Qed.

Lemma include_add : forall t x v, include_table t (add2 t x v).
Proof.
intros. induction t.
+ simpl. trivial.
+ simpl. destruct a. case T_eq_dec.
  - intros. rewrite e. simpl. case T_eq_dec.
    * intros. apply include_eq.
    * contradiction.
  - intros. simpl. case T_eq_dec.
    * intros. apply IHt.
    * intros. contradiction.
Qed.

Lemma couple_is_wf : forall (k:T) (v:U), wf (cons (k,v) nil).
Proof.
intros. apply wf_tail.
+ apply empty_is_wf.
+ simpl. reflexivity.
Qed.

Lemma xdptdr : forall t k v, wf ((k,v)::t) -> wf t.
Proof.
intros. induction t.
+ apply empty_is_wf.
+ inversion H. (* destruct H1. exact H1.*) exact H2.
Qed.

(*
Lemma plzzz : forall t k v, wf ((k,v)::t) -> find2 t k = None.
Proof.
intros. induction t.
+ trivial.
+ destruct a as (k0,u). unfold find2. case T_eq_dec.
  -

 unfold find2. destruct t.
+ trivial.
+ destruct p. case T_eq_dec.
  - intro. replace k in H. inversion H. destruct H1. inversion H4. case T_eq_dec.
    * trivial.
    * contradiction.
  - intro.
*)

Lemma add_is_wf : forall t x v, wf t -> wf (add2 t x v).
Proof.
intros. induction t.
+ simpl. apply couple_is_wf.
+ simpl. destruct a as (y,u). case T_eq_dec.
  - intros. rewrite <- e. apply wf_tail. (*split.*)
    * apply xdptdr with (k:=y) (v:=u). exact H.
    * unfold find2. destruct t.
      { trivial. }
      { destruct p. case T_eq_dec.
        { intros. inversion H. replace t0 in H4. inversion H4. case T_eq_dec.
          { trivial. } { easy. } }
        intros. destruct t.
          { trivial. } { destruct p. case T_eq_dec.
            { intro. inversion H. replace t1 in H4. inversion H4. case T_eq_dec.
              { contradiction. }
              { intros. case T_eq_dec. { trivial. } { contradiction. } } }
            { intro. destruct t. { trivial. } { destruct p. case T_eq_dec.
              { intro. inversion H. replace t2 in H4. inversion H4. case T_eq_dec.
                { contradiction. }
                { intros. case T_eq_dec. { contradiction. } { intro. case T_eq_dec.
                  { trivial. } { intro. unfold find2. destruct t.
                    { contradiction. } { destruct p. case T_eq_dec.
                      { contradiction. } { intro. destruct t. 
                        { contradiction. } { destruct p. case T_eq_dec.
                          { contradiction. }
(*
  - intros. apply wf_tail. (*split.*)
    * apply IHt. apply xdptdr with (k:=y) (v:=u). exact H.
    * 
*)
Admitted.