Natural Deduction for FOL


From Undecidability.FOLC Require Export FullFOL.

Inductive peirce := class | intu.
Inductive bottom := expl | lconst.
Existing Class peirce.
Existing Class bottom.

Section ND_def.
  Context {Sigma : Signature}.

  Definition form_shift : nat -> term :=
    fun n => var_term (S n).

  Notation "↑" := (form_shift).

  Reserved Notation "A ⊢ phi" (at level 61).

  (* ** Definition *)

  Implicit Type p : peirce.
  Implicit Type b : bottom.

  Inductive prv : forall (p : peirce) (b : bottom), list (form) -> form -> Prop :=
  | II {p b} A phi psi : phi::A psi -> A phi --> psi
  | IE {p b} A phi psi : A phi --> psi -> A phi -> A psi
  | AllI {p b} A phi : [psi[] | psi A] phi -> A phi
  | AllE {p b} A t phi : A phi -> A phi[t..]
  | ExI {p b} A t phi : A phi[t..] -> A phi
  | ExE {p b} A phi psi : A phi -> phi::[theta[] | theta A] psi[] -> A psi
  | Exp {p} A phi : prv p expl A -> prv p expl A phi
  | Ctx {p b} A phi : phi el A -> A phi
  | CI {p b} A phi psi : A phi -> A psi -> A phi psi
  | CE1 {p b} A phi psi : A phi psi -> A phi
  | CE2 {p b} A phi psi : A phi psi -> A psi
  | DI1 {p b} A phi psi : A phi -> A phi psi
  | DI2 {p b} A phi psi : A psi -> A phi psi
  | DE {p b} A phi psi theta : A phi psi -> phi::A theta -> psi::A theta -> A theta
  | Pc {b} A phi psi : prv class b A (((phi --> psi) --> phi) --> phi)
  where "A ⊢ phi" := (prv _ _ A phi).

  Arguments prv {_ _} _ _.

  Hint Constructors prv.

  Notation "A ⊢ phi" := (prv A phi) (at level 61).
  Notation "A '⊢(' p , b ')' phi" := (@prv p b A phi) (at level 30).
  Notation "A ⊢CE phi" := (@prv class expl A phi) (at level 30).
  Notation "A ⊢CL phi" := (@prv class lconst A phi) (at level 30).
  Notation "A ⊢IE phi" := (@prv intu expl A phi) (at level 30).

  Definition tprv p b T phi := (exists A, A T /\ @prv p b A phi).
  Arguments tprv {_ _} _ _.

  Notation "T ⊩ phi" := (tprv T phi) (at level 30).
  Notation "T '⊩(' s , b ')' phi" := (@tprv s b T phi) (at level 30).
  Notation "T ⊩CE phi" := (@tprv class expl T phi) (at level 30).
  Notation "T ⊩CL phi" := (@tprv class lconst T phi) (at level 30).
  Notation "T ⊩IE phi" := (@tprv intu expl T phi) (at level 30).

  Section Weakening.
    Context {p : peirce} {b : bottom}.

    Theorem Weak A B phi :
      A phi -> A <<= B -> B phi.
    Proof.
      intros H. revert B.
      induction H; intros B HB; try unshelve (solve [econstructor; intuition]); try now econstructor.
      - eapply AllI; eauto using incl_map.
      - eapply ExE; eauto using incl_map.
    Qed.

    Lemma up_term_term (t : term) xi :
      t[][up_term xi] = t[xi][].
    Proof.
      now asimpl.
    Qed.

    Lemma up_term_form xi psi :
      psi[][up_term xi] = psi[xi][].
    Proof.
      now asimpl.
    Qed.

    Theorem subst_Weak A phi xi :
      A phi -> [phi[xi] | phi A] phi[xi].
    Proof.
      induction 1 in xi |-*; comp.
      1-2,7-15: eauto using in_map.
      - apply AllI. setoid_rewrite map_map in IHprv. erewrite map_map, map_ext.
        apply IHprv. intros ?. comp. now apply ext_form.
      - specialize (IHprv xi). apply AllE with (t0 := t [xi]) in IHprv. comp. now asimpl in IHprv.
      - specialize (IHprv xi). eapply ExI with (t0 := t [xi]). asimpl. now asimpl in IHprv.
      - eapply ExE in IHprv1. eassumption. rewrite map_map.
        specialize (IHprv2 (up_term xi)). setoid_rewrite <- (up_term_form xi psi).
        erewrite map_map, map_ext in IHprv2. apply IHprv2.
        apply up_term_form.
    Qed.

    Lemma Weak_T T1 T2 phi :
      T1 phi -> T1 T2 -> T2 phi.
    Proof.
      intros (A & HA1 & HA2) HT2. exists A; firstorder.
    Qed.

    Definition cycle_shift n x :=
      if Dec (n = x) then var_term 0 else var_term (S x).

    Hint Unfold cycle_shift.

    Context {eq_dec_Funcs : eq_dec Funcs}.
    Context {eq_dec_Preds : eq_dec Preds}.

    Lemma cycle_shift_shift n phi :
      unused n phi -> phi[cycle_shift n] = phi[].
    Proof.
      intros H. apply (subst_unused_single H). intros m ?. unfold cycle_shift. now decide (n = m).
    Qed.

    Lemma cycle_shift_subject n phi :
      unused (S n) phi -> phi[(var_term n)..][cycle_shift n] = phi.
    Proof.
      intros H. asimpl. rewrite (@subst_unused_single _ _ _ _ ids _ _ H). 1: now asimpl.
      intros m H'; comp; decide (n = n); try congruence. destruct m; [reflexivity |].
        comp; decide (n = m); comp; congruence.
    Qed.

    Lemma nameless_equiv_all A phi n :
      unused_L n A -> unused (S n) phi -> ((A phi[(var_term n)..]) <-> [phi[] | phi A] phi).
    Proof.
      intros HL Hphi. split.
      - intros H % (subst_Weak (cycle_shift n)). rewrite cycle_shift_subject,
          (map_ext_in _ (subst_form form_shift)) in H. 1,3: assumption. intros ? ? % HL.
        now apply cycle_shift_shift.
      - intros H % (subst_Weak ((var_term n)..)). rewrite map_map in *. rewrite (map_ext _ id), map_id in H.
        assumption. intuition comp.
        erewrite ext_form. now asimpl. intros []; now asimpl.
    Qed.

    Lemma nameless_equiv_ex A phi psi n :
      unused_L n A -> unused n phi -> unused (S n) psi
      -> (psi[(var_term n)..]::A) phi <-> (psi::[p[] | p A]) phi[].
    Proof.
      intros HL Hphi Hpsi. split.
      - intros H % (subst_Weak (cycle_shift n)). cbn in *.
        rewrite (map_ext_in _ (subst_form form_shift)), cycle_shift_subject, cycle_shift_shift in H; trivial.
        intros a Ha. specialize (HL a Ha). now rewrite cycle_shift_shift.
      - intros H % (subst_Weak ((var_term n)..)). cbn in *.
        rewrite map_map, (map_ext _ id), map_id in H.
        + assert (phi[][(var_term n)..] = phi) as <-.
          asimpl. erewrite ext_form. now asimpl. intros []; now asimpl.
          eassumption.
        + intros. comp. erewrite ext_form. now asimpl. intros []; now asimpl.
    Qed.

    Lemma nameless_equiv_all' A phi :
      exists t, A phi[t..] <-> [p[] | p A] phi.
    Proof.
      destruct (find_unused_L (phi::A)) as [n HN].
      exists (var_term n). apply nameless_equiv_all.
      - intros psi H. apply HN; auto.
      - apply HN; auto.
    Qed.

    Lemma nameless_equiv_ex' A phi psi :
      exists t, (psi[t..]::A) phi <-> (psi::[p[] | p A]) phi[].
    Proof.
      destruct (find_unused_L (phi::psi::A)) as [n HN].
      exists (var_term n). apply nameless_equiv_ex.
      - intros theta H. apply HN; auto.
      - apply HN; auto.
      - apply HN; auto.
    Qed.

  End Weakening.

  Lemma prv_cut {p : peirce} {b : bottom} A phi psi :
    A phi -> (phi :: A) psi -> A psi.
  Proof.
    eauto.
  Qed.

  Lemma tprv_list_T {p : peirce} {b : bottom} A phi :
    list_T A phi -> A phi.
  Proof.
    intros (B & HB1 & HB2). apply (Weak HB2). firstorder.
  Qed.

  Definition capture_subs n x := var_term (x + n).

  Lemma capture_extract {p : peirce} {b : bottom} n A phi :
    A subst_form (capture_subs n) (capture n phi) -> A subst_form (capture_subs 0) phi.
  Proof.
    induction n; comp; intuition. apply IHn. apply (AllE (var_term n)) in H. asimpl in H.
    erewrite ext_form. 1: apply H. intros [| x]; unfold capture_subs; cbn; f_equal; omega.
  Qed.

  Context {eq_dec_Funcs : eq_dec Funcs}.
  Context {eq_dec_Preds : eq_dec Preds}.

  Lemma close_extract {p : peirce} {b : bottom} A phi :
    A close phi -> A phi.
  Proof.
    intros H. assert (Hclosed : closed (close phi)) by apply close_closed.
    unfold close in *. destruct (find_unused phi) as [n Hn]; cbn in *.
    rewrite <- subst_unused_closed' with (xi := capture_subs n) in H. 2: firstorder.
    apply capture_extract in H. rewrite idSubst_form in H; intuition.
    destruct x; unfold capture_subs; f_equal; omega.
  Qed.

  Lemma big_imp_extract {p : peirce} {b : bottom} A B phi :
    B (big_imp A phi) -> (rev A ++ B) phi.
  Proof.
    induction A in B |-*.
    - tauto.
    - cbn. intros Hprv. rewrite <- app_assoc. comp.
      apply IHA. eapply IE. 1: apply (Weak Hprv); intuition.
      now apply Ctx.
  Qed.

  Lemma prv_from_single {p : peirce} { b : bottom} A phi :
    nil close (A phi) -> A phi.
  Proof.
    intros Hprv % close_extract. apply big_imp_extract in Hprv.
    eapply Weak. apply Hprv. rewrite app_nil_r. now intros ? ? % in_rev.
  Qed.
End ND_def.

Hint Constructors prv.

Arguments prv {_ _ _} _ _.
Notation "A ⊢ phi" := (prv A phi) (at level 30).
Notation "A '⊢(' p , b ')' phi" := (@prv _ p b A phi) (at level 30).
Notation "A ⊢CE phi" := (@prv _ class expl A phi) (at level 30).
Notation "A ⊢CL phi" := (@prv _ class lconst A phi) (at level 30).
Notation "A ⊢IE phi" := (@prv _ intu expl A phi) (at level 30).

Arguments tprv {_ _ _} _ _.
Notation "T ⊩ phi" := (tprv T phi) (at level 30).
Notation "T '⊩(' s , b ')' phi" := (@tprv _ s b T phi) (at level 30).
Notation "T ⊩CE phi" := (@tprv _ class expl T phi) (at level 30).
Notation "T ⊩CL phi" := (@tprv _ class lconst T phi) (at level 30).
Notation "T ⊩IE phi" := (@tprv _ intu expl T phi) (at level 30).

(* ** Proof Tacticts *)

Ltac ointro_all :=
  match goal with
  | [ |- ?A ?phi] => apply AllI; cbn; asimpl
  end.

Ltac ointro_impl :=
  match goal with
  | [ |- _ (_ --> _)] => apply II
  | [ |- _ (¬ _)] => apply II
  end.

Ltac ointro := ointro_impl + ointro_all + fail "Nothing to intro!".
Ltac ointros := repeat ointro.

Ltac ctx_index' n :=
  match n with
  | O => now left
  | S ?m => right; ctx_index' m
  end.
Ltac ctx_index n := apply Ctx; ctx_index' n.
Ltac ctx := apply Ctx; intuition.

Ltac oapply n := eapply IE; [ctx_index n|].

Ltac ospecialize n t :=
  eapply prv_cut; [eapply (@AllE _ _ _ _ t); ctx_index n|]; cbn; asimpl.

Ltac ouse H := eapply Weak; [apply H |]; intuition.
Ltac oimport H := eapply prv_cut; [ouse H |].
Ltac oassert form := eapply (@prv_cut _ _ _ _ form).
Ltac oexfalso := apply Exp.
Ltac opeirce form := eapply IE; [apply (@Pc _ _ _ _ form) | apply II].

Lemma DN {Sigma : Signature} A phi :
  A CE ¬ phi) -> A CE phi.
Proof.
  intros H. oimport H. opeirce Fal. oexfalso. oapply 1. ctx.
Qed.

Ltac oindirect := apply DN, II.

Notation "c∃ phi" := (¬ ¬ phi) (at level 56, right associativity).

Lemma ExE' {Sigma : Signature} A phi psi :
  A CE (c phi) -> (phi :: [phi[] | phi A]) CE psi[] -> A CE psi.
Proof.
  intros Hex Hinst.
  oindirect. oimport Hex. oapply 0.
  ointros. oapply 2. ouse Hinst.
Qed.

Ltac odestruct n := eapply ExE'; [ctx_index n|]; cbn; asimpl.

Lemma ExI' {Sigma : Signature} {p : peirce} {b : bottom} A t phi :
  A phi [t..] -> A c phi.
Proof.
  intros Hc. apply II. ospecialize 0 t. oapply 0. ouse Hc.
Qed.

Ltac oexists t :=
  eapply (@ExI' _ _ _ _ t); cbn; asimpl.

Ltac osplit := eapply CI.
Ltac oleft := eapply DI1.
Ltac oright := eapply DI2.

Lemma AXM {Sigma : Signature} A phi psi :
  (phi :: A) CE psi -> (¬ phi :: A) CE psi -> A CE psi.
Proof.
  intros Ht Hf. oindirect. oassert (¬ phi). ointros. oapply 1.
  ouse Ht. oapply 1. ouse Hf.
Qed.

Ltac oxm form :=
  apply (@AXM _ _ form).

Lemma DP {Sigma : Signature} phi :
  [] CE c (phi --> ( phi)[]).
Proof.
  oxm (c ¬ phi).
  - odestruct 0. oexists (var_term 0). ointros. oexfalso. oapply 1. ctx.
  - oexists (var_term 0). ointros. oindirect. oapply 2. oexists (var_term 0). ctx.
Qed.

(* ** Theory manipulation *)

Section TheoryManipulation.
  Context {Sigma : Signature}.
  Context {p : peirce} {b : bottom}.
  Context {HF : eq_dec Funcs} {HP : eq_dec Preds}.

  Lemma prv_T_impl T phi psi :
    (T phi) psi -> T (phi --> psi).
  Proof.
    intros (A & HA1 & HA2). exists (rem A phi); split.
    - intros f [[] % HA1 Hf2] % in_rem_iff; subst; intuition.
    - eapply II, Weak. 1: apply HA2. transitivity (phi :: A). 1: eauto. apply rem_equi.
  Qed.

  Lemma prv_T_remove T phi psi :
    T phi -> T phi psi -> T psi.
  Proof.
    intros (A & HA1 & HA2) (B & HB1 & HB2) % prv_T_impl.
    use_theory (A ++ B). oimport HA2. oimport HB2. oapply 0. ctx.
  Qed.

  Lemma prv_T_comp T phi psi xi :
    T phi xi -> T psi phi -> T psi xi.
  Proof.
    intros (A & HA1 & HA2) % prv_T_impl (B & HB1 & HB2) % prv_T_impl.
    use_theory (psi :: A ++ B). oimport HA2. oimport HB2. oapply 1. oapply 0. ctx.
  Qed.

  Lemma elem_prv T phi :
    phi T -> T phi.
  Proof.
    intros ?. use_theory [phi]. ctx.
  Qed.
End TheoryManipulation.

(* ** Refutation completeness *)

Section RefutationComp.
  Context {Sigma : Signature}.
  Context {HF : eq_dec Funcs} {HP : eq_dec Preds}.

  Lemma refutation_prv T phi :
    T CE phi <-> (T ¬ phi) CE .
  Proof.
    split.
    - intros (A & HA1 & HA2). use_theory (¬ phi :: A). oimport HA2. oapply 1. ctx.
    - intros (A & HA1 & HA2) % prv_T_impl. use_theory A. now apply DN.
  Qed.
End RefutationComp.

(* ** Double Negation Translation *)

Section DNT.
  Context {Sigma : Signature}.

  Fixpoint dnt phi :=
    match phi with
    | =>
    | Pred P v => ¬ ¬ Pred P v
    | phi --> psi => dnt phi --> dnt psi
    | phi psi => dnt phi dnt psi
    | phi psi => ¬ dnt phi ¬ dnt psi)
    | phi => dnt phi
    | phi => ¬ ¬ dnt phi
    end.

  Lemma dnt_subst phi sigma :
    dnt (phi[sigma]) = (dnt phi)[sigma].
  Proof.
    induction phi in sigma |-*; comp; congruence.
  Qed.

  Lemma form_ind_subst' (P : form -> Prop) :
    P -> (forall p v, P (Pred p v)) ->
    (forall phi psi, P phi -> P psi -> P (phi --> psi)) ->
    (forall phi psi, P phi -> P psi -> P (phi psi)) ->
    (forall phi psi, P phi -> P psi -> P (phi psi)) ->
    (forall phi, P phi -> P ( phi)) ->
    (forall phi, (forall sigma, P phi[sigma]) -> P ( phi)) ->
    forall phi, P phi.
  Proof.
    intros H1 H2 H3 H4 H5 H6 H7 phi.
    induction phi using (@size_induction _ size).
    destruct phi; trivial.
    - apply H3; apply H; cbn; lia.
    - apply H4; apply H; cbn; lia.
    - apply H5; apply H; cbn; lia.
    - apply H6. eauto.
    - apply H7. intros t. apply H.
      cbn. setoid_rewrite subst_size. lia.
  Qed.

  Lemma dnt_float A phi :
    A IE (¬ ¬ dnt phi) -> A IE dnt phi.
  Proof.
    intros Hprv. revert A Hprv. induction phi using form_ind_subst'; intros A Hprv. 1-7:comp.
    - eauto.
    - oimport Hprv. ointros. oapply 1. ointros. oapply 0. ctx.
    - oimport Hprv. ointros. apply IHphi2. ointros. oapply 2. ointros. oapply 1.
      oapply 0. ctx.
    - oimport Hprv. eapply CI.
      + eapply IHphi1. ointros.
        oapply 1. ointros. oapply 1. eapply CE1. ctx.
      + eapply IHphi2. ointros.
        oapply 1. ointros. oapply 1. eapply CE2. ctx.
    - oimport Hprv. ointros. oapply 1. ointros.
      oapply 0. ctx.
    - oimport Hprv. ointros. comp. apply IHphi. ointros. oapply 1.
      ointros. ospecialize 0 (var_term 0). oapply 2. ctx.
    - oimport Hprv. cbn. ointros. oapply 1. ointros.
      oapply 0. ctx.
  Qed.

  Ltac clean_dnt_correct :=
    repeat (match goal with
            | [ H : ?x = ?x -> _ |- _ ] => specialize (H eq_refl)
            end).

  Lemma dnt_to_IE A phi :
    A CE phi -> map dnt A IE dnt phi.
  Proof.
    remember expl; remember class. induction 1; subst; comp.
    - eauto 3 using in_map; clean_dnt_correct.
    - eauto using in_map; clean_dnt_correct.
    - apply AllI. rewrite map_map in *. erewrite map_ext. apply IHprv; try reflexivity. now setoid_rewrite <- dnt_subst.
    - apply AllE with (t0 := t) in IHprv. now setoid_rewrite dnt_subst. all:reflexivity.
    - ointros. ospecialize 0 t. oapply 0. setoid_rewrite dnt_subst in IHprv. ouse IHprv.
    - oimport IHprv1. eapply dnt_float. ointros.
      oapply 1. ointros. oapply 1. setoid_rewrite dnt_subst in IHprv2. ouse IHprv2.
      intros ? [-> | (? & <- & ?) % in_map_iff]; eauto.
      eapply in_map_iff in H2 as (? & <- & ?).
      repeat right. eapply in_map_iff. exists (dnt x0). setoid_rewrite dnt_subst; eauto.
    - eauto using in_map; clean_dnt_correct.
    - eauto using in_map; clean_dnt_correct.
    - eauto using in_map; clean_dnt_correct.
    - eauto using in_map; clean_dnt_correct.
    - eauto using in_map; clean_dnt_correct.
    - ointros. eapply IE. eapply CE1. ctx. eapply Weak. eapply IHprv; try reflexivity. firstorder.
    - ointros. eapply IE. eapply CE2. ctx. eapply Weak. eapply IHprv; try reflexivity. firstorder.
    - oimport IHprv1. eapply dnt_float. ointros.
      oapply 1. osplit.
      + ointros. oapply 1. eapply Weak. eapply IHprv2. reflexivity. reflexivity. firstorder.
      + ointros. oapply 1. eapply Weak. eapply IHprv3. reflexivity. reflexivity. firstorder.
    - change (((dnt phi --> dnt psi) --> dnt phi) --> dnt phi) with (dnt (((phi --> psi) --> phi) --> phi)).
      apply dnt_float. comp. ointros. oapply 0. ointros. oapply 0. ointros. oexfalso. oapply 2.
      ointros. ctx.
  Qed.

  Lemma IE_to_CE A phi :
    A IE phi -> A CE phi.
  Proof.
    induction 1; eauto.
  Qed.

  Lemma dnt_CE A phi :
    A CE dnt phi <-> A CE phi.
  Proof.
    induction phi in A |-*; cbn in *.
    - reflexivity.
    - split. 1: eauto using DN. intros Hprv. ointros. oapply 0. ouse Hprv.
    - split; intros Hprv; oimport Hprv. all: ointros; apply IHphi2; oapply 1; apply IHphi1; ctx.
    - split; intros Hprv; oimport Hprv. all: osplit. 1,3: eapply IHphi1, CE1. 3,4: eapply IHphi2, CE2.
      all:ctx.
    - split; intros Hprv; oimport Hprv.
      + oindirect. oapply 1. osplit.
        * ointros. oapply 1. oleft. eapply IHphi1. ctx.
        * ointros. oapply 1. oright. eapply IHphi2. ctx.
      + ointros. eapply DE.
        * ctx.
        * eapply IE with (phi := dnt phi1). eapply CE1. ctx. eapply IHphi1. ctx.
        * eapply IE with (phi := dnt phi2). eapply CE2. ctx. eapply IHphi2. ctx.
    - split; intros Hprv; oimport Hprv. all: ointros; apply IHphi; ospecialize 0 (var_term 0); ctx.
    - split; intros Hprv; oimport Hprv.
      + oindirect. oapply 1. ointros. oapply 1.
        eapply ExI with (t := var_term 0). asimpl. eapply IHphi. ctx.
      + ointros. eapply ExE. ctx. cbn.
        ospecialize 1 (var_term 0). oapply 0. eapply IHphi. ctx.
  Qed.

  Lemma dnt_remove_ctx A B phi :
    (A ++ map dnt B) CE phi -> (A ++ B) CE phi.
  Proof.
    induction B in A |-*; cbn.
    - now rewrite app_nil_r.
    - intros H. specialize (IHB (A ++ [a])). do 2 rewrite <- app_assoc in IHB. apply IHB.
      apply prv_cut with (dnt a). 1: apply dnt_CE; ctx; intuition. apply (Weak H).
      intros ? [| []] % in_app_or; subst; intuition. repeat (right; apply in_or_app). now right.
  Qed.

  Lemma dnt_to_CE A phi :
    map dnt A IE dnt phi -> A CE phi.
  Proof.
    intros H % IE_to_CE. now apply dnt_remove_ctx with (A := nil), dnt_CE.
  Qed.
End DNT.