(*
 * This code was developped by IDEALX (http://IDEALX.org/) and
 * contributors (their names can be found in the CONTRIBUTORS file). It 
 * is released under the terms of the BSD license (see LICENCE file
 * for details). 
*)

(******************************************************************
 *                OPTION TYPE V0.1 (April 2001) 
 *
 *
 ******************************************************************
 *
 * The option type allows a function to have an error condition, a
 * way of making a partial function become total.
 *
 ******************************************************************)


Inductive option (A : Set) : Set :=
  | none : option A
  | some : A -> option A.

Lemma option_sum :
 forall (A : Set) (o : option A), {y : A | o = some A y} + {o = none A}.
Proof.
(* Goal: forall (A : Set) (o : option A), sumor (@sig A (fun y : A => @eq (option A) o (some A y))) (@eq (option A) o (none A)) *)
intro.
(* Goal: forall o : option A, sumor (@sig A (fun y : A => @eq (option A) o (some A y))) (@eq (option A) o (none A)) *)
simple induction o.
(* Goal: sumor (@sig A (fun y : A => @eq (option A) (none A) (some A y))) (@eq (option A) (none A) (none A)) *)
(* Goal: forall a : A, sumor (@sig A (fun y : A => @eq (option A) (some A a) (some A y))) (@eq (option A) (some A a) (none A)) *)
right.
(* Goal: @eq (option A) (some A a) (some A a) *)
auto.
(* Goal: forall a : A, sumor (@sig A (fun y : A => @eq (option A) (some A a) (some A y))) (@eq (option A) (some A a) (none A)) *)
left.
(* Goal: @sig A (fun y : A => @eq (option A) (some A a) (some A y)) *)
exists a.
(* Goal: @eq (option A) (some A a) (some A a) *)
auto.
Qed.
