Require Export PropL. Inductive gen : context -> form -> Prop := | genV A x : Var x el A -> gen A (Var x) | genF A u : Fal el A -> gen A u | genIR A s t : gen (s::A) t -> gen A (Imp s t) | genIL A s t u : Imp s t el A -> gen A s -> gen (t::A) u -> gen A u. Lemma gen_nd A s : gen A s -> nd A s. Proof. induction 1; eauto using nd. Qed. (** Consistency *) Lemma gen_con : ~ gen nil Fal. Proof. intros B. inv B; intuition. Qed. (** Unprovability of DN *) Lemma gen_DN' A x s : A <<= [Var x; Not (Not (Var x))] -> gen A s -> s <> Fal /\ s <> Not (Var x). Proof. intros H D. induction D as [A y E|A v E|A s t E IHE|A s t v E F IHF G _ ]. - split; discriminate. - exfalso. apply H in E. unfold In in E; intuition; discriminate. - split; intros J; inv J. cut (Fal <> Fal). now auto. apply IHE; auto. - exfalso. apply H in E. destruct E as [E|[E|[]]]; inv E. apply IHF; auto. Qed. Lemma gen_DN x : ~ gen [Not (Not (Var x))] (Var x). Proof. intros E. inv E; unfold In in *; intuition; try discriminate. inv H2. apply gen_DN' with (x:=x) in H0; intuition. Qed. (** Assumption rule *) Lemma genA A s : s el A -> gen A s. Proof. revert A. induction s; eauto 6 using gen. Qed. (** Weakening rule *) Lemma genW A B s : gen A s -> A <<= B -> gen B s. Proof. intros C; revert B. induction C; eauto 7 using gen. Qed. (** Cut rule *) Lemma genC' A s B u : gen A s -> gen B u -> gen (A ++ rem B s) u. Proof with auto. intro C; revert A C B u. induction s as [x|s IHs t IHt|]; intros A C. - remember (Var x) as v. induction C as [A y E|A v E| |A s t v E F _ _ IHG]; intros B u D; subst; try inv Heqv. + apply (genW D)... + apply genF... + eapply genIL; eauto. apply (genW F)... - remember (Imp s t) as v. induction C as [ |A v E|A s' t' E _|A s' t' v E F _ _ IHG]; intros B u D; subst; try inv Heqv. + apply genF... + induction D as [B y F|B u F|B s' t' F IHF|B s' t' u F G IHG H IHH]. * apply genV. assert (Var y <> Imp s t) by congruence... * apply genF. assert (Fal <> Imp s t) by congruence... * apply genIR. apply (genW IHF)... * { decide (Imp s' t' = Imp s t) as [K|K]. - inv K. (* Imp s t is principal formula of both derivations *) specialize (IHs _ IHG _ _ E). specialize (IHt _ IHs _ _ IHH). apply (genW IHt). repeat apply incl_app... apply rem_app'... rewrite rem_comm... - clear IHs IHt. eapply genIL; eauto. apply (genW IHH)... } + eapply genIL; eauto. apply (genW F)... - remember Fal as v. induction C as [ |A v E| |A s t v E F _ _ IHG]; intros B u D; subst; try inv Heqv. + apply (genW D)... + eapply genIL; eauto. apply (genW F)... Qed. Lemma genC A s u : gen A s -> gen (s::A) u -> gen A u. Proof. intros E F. apply (genW (genC' E F)). auto. Qed. (** Completeness for ND *) Lemma nd_gen A s : nd A s -> gen A s. Proof. intros D. induction D as [A s D|A s t _ IHD|A s t _ IHD _ IHC|A s _ IHD]. - apply genA, D. - apply genIR, IHD. - apply (genC IHD). eapply genIL; eauto using genA. apply (genW IHC). auto. - apply (genC IHD). apply genF; auto. Qed. Theorem gen_iff_nd A s : gen A s <-> nd A s. Proof. split. apply gen_nd. apply nd_gen. Qed. (** Subformula Closure *) Definition sf_closed (A : context) : Prop := forall u, u el A -> match u with | Imp s t => s el A /\ t el A | _ => True end. Lemma sf_closed_app A B : sf_closed A -> sf_closed B -> sf_closed (A ++ B). Proof. intros E F [|s t|] G; auto. apply in_app_or in G as [G|G]. - apply E in G. intuition; eauto. - apply F in G. intuition; eauto. Qed. Lemma sf_closed_cons s t A : s el A -> t el A -> sf_closed A -> sf_closed (Imp s t :: A). Proof. intros D E F [|s' t'|] G; auto. destruct G as [G|G]. - inv G. auto. - apply (F _) in G. destruct G; auto. Qed. Fixpoint scl' (s : form) : context := s :: match s with | Imp u v => scl' u ++ scl' v | _ => nil end. Lemma scl'_in s : s el scl' s. Proof. destruct s; simpl; auto. Qed. Lemma scl'_closed s : sf_closed (scl' s). Proof. induction s; simpl; auto. - intros u [A|A]; inv A; auto. - apply sf_closed_cons; auto using scl'_in, sf_closed_app. - intros u [A|A]; inv A; auto. Qed. Fixpoint scl (A : context) : context := match A with | nil => nil | s :: A' => scl' s ++ scl A' end. Lemma scl_incl' A : A <<= scl A. Proof. induction A as [|s A]; simpl; auto using scl'_in. Qed. Lemma scl_incl A B : A <<= B -> A <<= scl B. Proof. intros E. setoid_rewrite E. apply scl_incl'. Qed. Lemma scl_closed A : sf_closed (scl A). Proof. induction A as [|s A]; simpl. now auto. auto using scl'_closed, sf_closed_app. Qed. (** Decidability *) Definition goal := prod (context) form. Instance goal_eq_dec gamma delta : dec (gamma = delta :> goal). Proof. unfold dec. repeat decide equality. Qed. Section Decidability. Variable A0 : context. Variable s0 : form. Definition U := scl (s0::A0). Definition U_sfc : sf_closed U := @scl_closed _. Definition Gamma := list_prod (power U) U. Definition step (Delta : list goal) (gamma : goal) : Prop := let (A,u) := gamma in match u with | Var _ => u el A | Imp s t => (rep (s::A) U, t) el Delta | _ => False end \/ exists v, v el A /\ match v with | Fal => True | Imp s t => (A, s) el Delta /\ (rep (t::A) U, u) el Delta | _ => False end. Instance step_dec Delta gamma : dec (step Delta gamma). Proof. destruct gamma as [A u]; simpl. apply or_dec. - destruct u as [x|s t|]; auto. - apply list_exists_dec. intros [x|s t|]; auto. Qed. Definition Lambda : list goal := FCI.C (step := step) Gamma. Lemma lambda_closure gamma : gamma el Gamma -> step Lambda gamma -> gamma el Lambda. Proof. apply FCI.closure. Qed. Lemma lambda_ind (p : goal -> Prop) : (forall Delta gamma, inclp Delta p -> gamma el Gamma -> step Delta gamma -> p gamma) -> inclp Lambda p. Proof. apply FCI.ind. Qed. Lemma gen_lambda A u : A <<= U -> u el U -> gen A u -> (rep A U,u) el Lambda. Proof. intros D1 D2 E. induction E as [A x F|A u F|A s t F IHF|A s t u F G IHG H IHH]; (apply lambda_closure; [now eauto using in_prod, rep_power|]); simpl. -left. auto using rep_in. - right. exists Fal. auto using rep_in. - apply U_sfc in D2 as [D2 D3]. left. rewrite rep_eq with (B := s::A). + auto. + setoid_rewrite rep_equi; auto. - assert (K := F). apply D1 in K. apply U_sfc in K as [K1 K2]. right. exists (Imp s t); repeat split; auto using rep_in. rewrite rep_eq with (B := t::A). + auto. + setoid_rewrite rep_equi; auto. Qed. Lemma lambda_gen A u : (A,u) el Lambda -> gen A u. Proof. revert A u. cut (inclp Lambda (fun gamma => gen (fst gamma) (snd gamma))). { intros E A u. apply E. } apply lambda_ind. intros Delta [A u] E F G; simpl. assert (E': forall B v, (B,v) el Delta -> gen B v). { intros B v. apply E. } clear E. destruct G as [G|[[x|s t|] [G H]]]. - destruct u; intuition; eauto using gen, genW, rep_incl. - contradiction H. - intuition; eauto using gen, genW, rep_incl. - eauto using gen. Qed. Theorem nd_dec : dec (nd A0 s0). Proof. apply (dec_prop_iff (gen_iff_nd _ _)). assert (A1: A0 <<= U). { apply scl_incl; auto. } assert (A2: s0 el U). { apply scl_incl'; auto. } apply dec_prop_iff with (X:= gen (rep A0 U) s0). - split; intros E; apply (genW E), rep_equi; auto. - decide ((rep A0 U, s0) el Lambda) as [E|E]. + left. apply lambda_gen, E. + right. intros F. apply E. apply gen_lambda; auto. apply genW with (A := rep A0 U); auto. apply rep_equi, A1. Qed. End Decidability.