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