Ml.v
Require Extraction.
ML Inductive
bool [true false] ==
Inductive
BOOL: Set := TRUE:BOOL | FALSE:BOOL.
ML Inductive
option [Some None] ==
Inductive
OPTION [A:Set]: Set := SOME: A->(OPTION A) | NONE: (OPTION A).
ML Import int: Set.
ML Import eq_int: int -> int -> BOOL.
ML Import zero: int.
ML Import succ: int -> int.
ML Import int_case: int -> (OPTION int).
ML Import string: Set.
ML Import eq_string: string -> string -> BOOL.
Parameter ml_int: Set.
Link ml_int := int.
Parameter ml_eq_int: (m,n:ml_int){m=n}+{~m=n}.
Link ml_eq_int :=
[s1,s2:int]Case (eq_int s1 s2) of left right end.
Parameter ml_zero: ml_int.
Link ml_zero := zero.
Parameter ml_succ: ml_int -> ml_int.
Link ml_succ := succ.
Parameter ml_int_pred: (m,n:ml_int)(ml_succ m)=(ml_succ n)->m=n.
Axiom dangerous_discr: (n:ml_int)~ml_zero=(ml_succ n).
Parameter ml_int_case: (n:ml_int){ m:ml_int | n=(ml_succ m) }+{ n=ml_zero }.
Link ml_int_case :=
[n:ml_int]Case (int_case n) of
[m:ml_int](inleft ml_int m)
(inright ml_int)
end.
Fixpoint
int_of_nat [n:nat]: ml_int :=
Cases n of
O => ml_zero
| (S k) => (ml_succ (int_of_nat k))
end.
Lemma
dangerous_int_injection: (i,j:nat)(int_of_nat i)=(int_of_nat j)->i=j.
(Induction i; Destruct j; Simpl; Intros; Auto).
(Elim dangerous_discr with (int_of_nat n); Auto).
(Elim dangerous_discr with (int_of_nat n); Auto).
(Elim H with n0; Auto).
(Apply ml_int_pred; Auto).
Save.
Parameter ml_string: Set.
Link ml_string := string.
Parameter ml_eq_string: (s1,s2:ml_string){s1=s2}+{~s1=s2}.
Link ml_eq_string :=
[s1,s2:string]Case (eq_string s1 s2) of left right end.
18/02/97, 15:26