Section Basics.

Inductive maybe (A : Type) : Type :=
  | defined : A -> maybe A
  | undefined : maybe A.

Check maybe.
Print maybe.
Check maybe_ind.

Variables A B : Type.

Definition maybe_apply (f : A -> B) (ma : maybe A) : maybe B :=
  match ma with
  | defined a => defined _ (f a)
  | undefined => undefined B
  end.

Print bool.

Definition is_defined (ma : maybe A) : bool :=
  match ma with
  | defined _ => true
  | undefined => false
  end.

Lemma bool_elim : forall (b : bool),
  b = true \/ b = false.
Proof.
  intro b. destruct b as [ | ].
   left. reflexivity.
   right. reflexivity.
Qed.

Print bool_elim.

Lemma true_neq_false : ~ false = true.
Proof.
  discriminate.
Qed.

Lemma is_defined_exists_defined : forall (ma : maybe A),
  is_defined ma = true -> exists (a : A),
  ma = defined A a.
Proof.
  intros ma E. destruct ma as [a | ].
   exists a. reflexivity.
   simpl in E. apply true_neq_false in E. destruct E.
Qed.

Lemma equal_defined_is_defined : forall (ma : maybe A) a,
  ma = defined _ a -> is_defined ma = true.
Proof.
  intros ma a E. rewrite E.
  simpl. reflexivity.
Qed.

End Basics.

Check maybe_apply.