# Library Options

Require Export Encoding Seval.

# Inernalized Maybe type

Definition none : term := .\"s", "n"; "n".

Definition some : term := .\"t", "s", "n"; "s" "t".

Hint Unfold some none : cbv.

Definition oenc t :=
match t with
| Some t => lam(lam (#1 (tenc t)))
| None => none
end.

Lemma some_correct_enc s : some (tenc s) == oenc (Some s).

Proof.

crush.

Qed.

Lemma some_correct s t u: proc s -> proc t -> (some s) t (lam u) == t s.

Proof.

destruct 1 as [cls_s [x B]], 1 as [cls_t [y D]].

rewrite B.
reduction'. rewrite <- B.
rewrite D.
reduction'. rewrite <- D.
crush.

Qed.

Lemma none_correct s t : lambda s -> lambda t -> none s t == t.

Proof.

intros.
crush.
Qed.

Lemma some_inj s t : lambda s -> lambda t -> some s == some t -> s = t.

Proof.

intros.

eapply eqTrans with (s := lam(lam (#1 s))) in H1.

symmetry in H1.
eapply eqTrans with (s := lam(lam (#1 t))) in H1.
eapply eq_lam in H1.
congruence.
symmetry; now reduction'.

symmetry; now reduction'.

Qed.

Lemma oenc_correct_some (s v : term) : lambda v -> oenc (Some s) == some v -> v == tenc s.

Proof.

intros lam_v H.

symmetry in H.
eapply eqTrans with (s := lam(lam(#1 v))) in H. eapply eq_lam in H. inv H. reflexivity.
symmetry; clear H; crush.

Qed.

Lemma none_equiv_some v : ~ none == some v.

Proof.

intros H.
assert (converges (some v)) by (eexists; rewrite <- H; cbv; now unfold none). destruct (app_converges H0) as [_ ?]. destruct H1. rewrite H1 in H.
symmetry in H.
eapply eqTrans with (s := (lam (lam (#1 (lam x))))) in H.
eapply eq_lam in H.
inv H. symmetry. unfold some. clear H. crush.
Qed.