Lemma contra: forall (P Q:Prop), (P -> Q) -> (~ Q -> ~P). Proof. intros. intros hasP. apply H in hasP. contradiction. Qed. Lemma not_or_to_not_and: forall P Q: Prop, ~ P \/ ~ Q -> ~ (P /\ Q). Proof. intros. intros N. destruct N. destruct H. - contradiction. - contradiction. Qed. Definition ExcludedMiddle := (forall P: Prop, P \/ ~ P). (** To prove that from not (P and Q) implies not P or not Q is not provable in a constructive logic. *) Lemma not_and_to_or_not (XM: ExcludedMiddle): forall P Q: Prop, ~ (P /\ Q) -> ~P \/ ~ Q. Proof. intros. (* Our assumptions are: H : ~ (P /\ Q) and the excluded middle. The only way to reach a contradiction is to have P and Q, but we have neither! So, we need to fabricate P and Q by using the excluded middle. *) destruct (XM P), (XM Q). - contradict H. split. + assumption. + assumption. - right. assumption. - left. assumption. - left. assumption. Qed. (** Let us define a variable. *) Variable lang : Type. (** Let us define a predicate on context-freedom. *) Variable CtxFree : lang -> Prop. (** Let us define a predicate for regular languages. *) Variable Reg: lang -> Prop. (** Further, let us defined union of languages, which is a function that takes a language and another language and produces a language. *) Variable union: lang -> lang -> lang. Variable cat: lang -> lang -> lang. (** Let us assume that the union in closed under context-free languages, which we know to be the case. *) Axiom union_cf: forall L1 L2, CtxFree L1 -> CtxFree L2 -> CtxFree (union L1 L2). Axiom cat_cf: forall L1 L2, CtxFree L1 -> CtxFree L2 -> CtxFree (cat L1 L2). Axiom union_reg: forall L1 L2, Reg L1 -> Reg L2 -> Reg (union L1 L2). Axiom cat_reg: forall L1 L2, Reg L1 -> Reg L2 -> Reg (cat L1 L2). Variable reg_to_cf: forall L, Reg L -> CtxFree L. Lemma not_cf_to_reg: forall L, ~ CtxFree L -> ~ Reg L. Proof. intros L. apply contra. apply reg_to_cf. Qed. (** Our objective is to show that if the union of L1 and L2 is not context-free, then either L1 is not context free or L2 is not context free. This result requires the excluded middle. *) Lemma objective (XM:ExcludedMiddle) : forall L1 L2, ~ CtxFree (union L1 L2) -> ~ CtxFree L1 \/ ~ CtxFree L2. Proof. intros L1 L2. intros H. apply (not_and_to_or_not XM). intros N. destruct N as (H1, H2). contradict H. apply union_cf. - assumption. - assumption. Qed. Lemma cf_reg_union: forall L1 L2, CtxFree L1 -> Reg L2 -> CtxFree (union L1 L2). Proof. intros. apply reg_to_cf in H0. apply union_cf. - assumption. - assumption. Qed. Lemma cf_reg_union2: forall L1 L2, Reg L1 -> Reg L2 -> CtxFree (union L1 L2). Proof. intros. apply reg_to_cf in H. apply reg_to_cf in H0. apply union_cf. - assumption. - assumption. (* apply reg_to_cf. apply union_reg. - assumption. - assumption. *) Qed. Variable _0n1n : lang. Axiom _0n1n_not_reg: ~ Reg _0n1n. Axiom _0n1n_cf: CtxFree _0n1n. Lemma not_reg_to_not_cf: ~ (forall l, ~ Reg l -> ~ CtxFree l). Proof. intros N. assert (N := N _0n1n). assert (H := _0n1n_not_reg). apply N in H. contradict H. apply _0n1n_cf. Qed.