Library Options
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.