(* File: ML_int.v    (last edited on 25/10/2000  (c) Klaus Weich  *)

(* Axiomisation of the ML type "int" *)

Axiom Int : Set.
Axiom Less : Int -> Int -> Prop.
Axiom Equal : Int -> Int -> Prop.
Axiom int_succ : forall x : Int, {y : Int | Less x y}.
Axiom int_null : Int.

Axiom equal_dec : forall x y : Int, {Equal x y} + {~ Equal x y}.
Axiom less_dec : forall x y : Int, {Less x y} + {~ Less x y}.


Axiom
  notequal_notless_greater :
    forall x y : Int, ~ Equal x y -> ~ Less x y -> Less y x.

Axiom less_trans : forall x y z : Int, Less x y -> Less y z -> Less x z.
Axiom equal_less_less : forall x y z : Int, Equal x y -> Less y z -> Less x z.
Axiom less_equal_less : forall x y z : Int, Less x y -> Equal y z -> Less x z.
Axiom equal_sym : forall x y : Int, Equal x y -> Equal y x.
Axiom equal_trans : forall x y z : Int, Equal x y -> Equal y z -> Equal x z.
Axiom equal_refl : forall x : Int, Equal x x.
Axiom equal_eq : forall x y : Int, Equal x y -> x = y.

Axiom less_irrefl : forall x : Int, Less x x -> False.


Lemma equal_dec_refl :
 forall (i : Int) (A : Set) (a b : A),
 match equal_dec i i with
 | left _ => a
 | right _ => b
 end = a.
(* Goal: forall (i : Int) (A : Set) (a b : A), @eq A (if equal_dec i i then a else b) a *)
intros i A a b.
(* Goal: @eq A (if equal_dec i i then a else b) a *)
elim (equal_dec i i).
(* Goal: forall _ : Equal i i, @eq A a a *)
(* Goal: forall _ : not (Equal i i), @eq A b a *)
intros; trivial.
(* Goal: forall _ : not (Equal i i), @eq A b a *)
intros notequal; elimtype False; apply notequal.
(* Goal: Equal i0 i0 *)
(* Goal: or (Less i1 i0) (Equal i1 i0) *)
apply equal_refl.
Qed.


Inductive max_int_spec (i0 i1 : Int) : Set :=
    Max_Int_Intro :
      forall j : Int,
      Less i0 j \/ Equal i0 j ->
      Less i1 j \/ Equal i1 j -> max_int_spec i0 i1.

Lemma max_int : forall i0 i1 : Int, max_int_spec i0 i1.
(* Goal: forall i0 i1 : Int, max_int_spec i0 i1 *)
intros i0 i1.
(* Goal: max_int_spec i0 i1 *)
elim (equal_dec i0 i1).
(* Goal: forall _ : Equal i0 i1, max_int_spec i0 i1 *)
(* Goal: forall _ : not (Equal i0 i1), max_int_spec i0 i1 *)
intros eq_i0_i1.
(* Goal: max_int_spec i0 i1 *)
exists i0.
(* Goal: or (Less i0 i0) (Equal i0 i0) *)
(* Goal: or (Less i1 i0) (Equal i1 i0) *)
right.
(* Goal: Equal i0 i0 *)
(* Goal: or (Less i1 i0) (Equal i1 i0) *)
apply equal_refl.
(* Goal: or (Less i0 i0) (Equal i0 i0) *)
(* Goal: or (Less i1 i0) (Equal i1 i0) *)
right.
(* Goal: Equal i1 i0 *)
(* Goal: forall _ : not (Equal i0 i1), max_int_spec i0 i1 *)
apply equal_sym; assumption.

(* Goal: forall _ : not (Equal i0 i1), max_int_spec i0 i1 *)
intros not_eq_i0_i1.
(* Goal: max_int_spec i0 i1 *)
elim (less_dec i0 i1).
(* Goal: forall _ : Less i0 i1, max_int_spec i0 i1 *)
(* Goal: forall _ : not (Less i0 i1), max_int_spec i0 i1 *)
intros less_i0_i1.
(* Goal: max_int_spec i0 i1 *)
(* Goal: forall _ : not (Less i0 i1), max_int_spec i0 i1 *)
exists i1.
(* Goal: or (Less i0 i1) (Equal i0 i1) *)
(* Goal: or (Less i1 i1) (Equal i1 i1) *)
(* Goal: forall _ : not (Less i0 i1), max_int_spec i0 i1 *)
left; assumption.
(* Goal: or (Less i0 i0) (Equal i0 i0) *)
(* Goal: or (Less i1 i0) (Equal i1 i0) *)
right.
(* Goal: Equal i0 i0 *)
(* Goal: or (Less i1 i0) (Equal i1 i0) *)
apply equal_refl.

(* Goal: forall _ : not (Less i0 i1), max_int_spec i0 i1 *)
intros ge_i0_i1.
(* Goal: max_int_spec i0 i1 *)
exists i0.
(* Goal: or (Less i0 i0) (Equal i0 i0) *)
(* Goal: or (Less i1 i0) (Equal i1 i0) *)
right.
(* Goal: Equal i0 i0 *)
(* Goal: or (Less i1 i0) (Equal i1 i0) *)
apply equal_refl.
(* Goal: or (Less i1 i0) (Equal i1 i0) *)
left.
(* Goal: Less i1 i0 *)
apply notequal_notless_greater; assumption.
Qed.




