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