Names.v

Require Extraction.
Require MyList.
Require Ml.

  Axiom ml_x_int: ml_int -> ml_string.
  ML Import x_int: int -> string.
  Link ml_x_int := x_int.
  Axiom ml_x_int_inj: (m,n:ml_int)(ml_x_int m)=(ml_x_int n)->m=n.

  (* type des noms *)
  Definition name := ml_string.
  Definition prt_names:= (list name).

  Lemma name_dec: (x,y:name){x=y}+{~x=y}.
Proof ml_eq_string.

  Definition var_of_nat: nat -> name :=
    [n](ml_x_int (int_of_nat n)).

  Lemma inj_var_of_nat: (m,n:nat)(var_of_nat m)=(var_of_nat n)->m=n.
Unfold var_of_nat.
Intros.
Apply dangerous_int_injection.
(Apply ml_x_int_inj; Auto).
Save.

  Inductive ord_insert: (list name)->(list name)->Prop :=
    oi_intro: (x:name)(n:nat)(l1,l2:(list name))(insert ? x n l1 l2)
                ->(ord_insert l1 l2).

  Lemma wf_oi: (well_founded ? ord_insert).
Cut (n:nat)(l:(list name))(length ? l)=n->(Acc ? ord_insert l).
(Red; Intros).
(Apply H with (length ? a); Auto).

Induction n.
(Destruct l; Intros).
(Apply Acc_intro; Intros).
Inversion_clear H0.
Inversion_clear H1.

Discriminate H.

(Destruct l; Simpl; Intros).
Discriminate H0.

(Injection H0; Intros).
(Apply Acc_intro; Intros).
Inversion_clear H2.
Apply H.
(Cut (S (length ? y))=(length ? (cons ? n1 l0)); Intros).
Simpl in H2.
(Injection H2; Auto).
(Elim H1; Auto).

(Elim H3; Auto).
Intros.
Simpl.
(Elim H4; Auto).
Save.

  Lemma rmv: (x:name)(l:prt_names)
           { l1:prt_names | (Ex [n:nat](insert ? x n l1 l)) }
         + {~(In ? x l)}.
Realizer Fix rmv {rmv/2: name->(list name)->(sumor (list name)) :=
  [x,l]Cases l of
     nil => (inright ?)
   | (cons y l1) => Cases (name_dec x y) of
         left => (inleft ? l1)
       | right => Cases (rmv x l1) of
                    (inleft v) => (inleft ? (cons ? y v))
                  | inright => (inright ?)
                  end
       end
   end}.
Program_all.
(Red; Intros).
Inversion H.

Exists O.
(Elim e; Auto).

Inversion_clear e.
(Exists (S x0); Auto).

(Red; Intros; Apply n0).
(Inversion H; Auto).
(Elim n; Auto).
Save.

  Lemma find_free: (l: prt_names)(n:nat)
                            {m:nat| (le n m) & ~(In ? (var_of_nat m) l)}.
Realizer <nat->nat>rec ffv :: :: { ord_insert }
  [l:prt_names][n:nat]Cases (rmv (var_of_nat n) l) of
      (inleft l1) => (ffv l1 (S n))
    | inright => n
    end.
Program_all.
Exact wf_oi.

Inversion_clear e.
(Apply oi_intro with (var_of_nat n) x; Auto).

Inversion_clear e.
(Red; Intro).
Apply y0.
Generalize H0 .
Cut ~(var_of_nat n0)=(var_of_nat n).
Unfold var_of_nat.
(Elim H; Intros).
Generalize H1 .
(Inversion_clear H2; Auto).
(Induction 1; Auto).

(Inversion_clear H4; Auto).

(Red; Intros).
Apply (le_Sn_n n).
Pattern 2 n .
(Replace n with n0; Auto).
(Apply inj_var_of_nat; Auto).
Save.

  Lemma find_free_var: (l: prt_names){x:name| ~(In ? x l)}.
Realizer [l:prt_names](var_of_nat (find_free l O)).
Program_all.
Save.

  Definition name_unique := [l:prt_names](m,n:nat)(x:name)(item ? x l m)
                                                ->(item ? x l n)->m=n.

  Lemma fv_ext: (l:prt_names)(name_unique l)->(x:name)~(In ? x l)
                      ->(name_unique (cons ? x l)).
(Unfold name_unique; Intros).
Generalize H2 .
(Inversion_clear H1; Intros).
(Inversion_clear H1; Auto).
Elim H0.
(Elim H3; Auto).

Generalize H3 .
(Inversion_clear H1; Intros).
Elim H0.
(Elim H1; Auto).

(Elim H with n1 n0 x0; Auto).
Save.

  Lemma name_unique_first: (x:name)(l:prt_names)(n:nat)(item ? x l n)
                              ->(name_unique l)->(first_item ? x l n).
(Induction 1; Intros).
Auto.

(Apply fit_tl; Auto).
Apply H1.
(Red; Intros).
(Cut (S m)=(S n1); Intros).
(Injection H5; Auto).

(Elim H2 with (S m) (S n1) x0; Auto).

(Red; Intros).
(Cut O=(S n0); Intros).
Discriminate H4.

(Elim H2 with O (S n0) x; Auto).
(Rewrite -> H3; Auto).
Save.

(*   Inductive ord_ins [l:prt_names]: nat->nat->Prop :=     oi_int: (n:nat)(In ? (var_of_nat n) l)->(ord_ins l (S n) n).   Lemma Acc_cons: (l:prt_names)(n:nat)(Acc ? (ord_ins l) n)                     ->(m:nat)(lt m n)                       ->(Acc ? (ord_ins (cons ? (var_of_nat m) l)) n). (Induction 1; Intros). (Apply Acc_intro; Intros). Inversion H3. Elim H6. Rewrite -> H5. (Apply H1; Auto). Elim H5. Rewrite -> H6. Apply oi_int. (Inversion H4; Auto). ElimType False. Apply (le_Sn_n m). Red in H2. Pattern 2 m . (Elim inj_var_of_nat with x m; Auto). Red. (Apply le_trans with x; Auto). Elim H5. (Rewrite -> H6; Auto). Save.   Lemma wf_oi: (l:prt_names)(well_founded ? (ord_ins l)). Red. (Induction l; Intros). (Apply Acc_intro; Intros). Inversion_clear H. Inversion_clear H0. (Apply Acc_intro; Intros). *)

18/02/97, 15:57