KM.Sequent.Sequents

Require Export Environments.

Open Scope stdpp_scope.

Sequent calculus G4KM

We implement the sequent calculus G4KM, a contraction-free calculus for KM analog to the caluclus G4iP' for intuitionistic propositional logic

The calculus is important because it allows for a terminating proof search, and in our proof of Pitts' theorem, it therefore lets us perform well-founded induction on proofs. Technically, this is thanks to the absence of a contraction rule. The left implication rule is refined into five separate proof rules.

Global Coercion Var : nat >-> form.
Global Instance Top : base.Top form := Top.

Definition of provability in G4KM

Reserved Notation "Γ ⊢ Δ" (at level 99, no associativity, Δ at level 90).
Inductive Provable : env -> env -> Type :=
| Atom : ∀ Γ Δ p, Γ • Var p ⊢ Δ • Var p
| ExFalso : ∀ Γ Δ, Γ • ⊥ ⊢ Δ
| AndR : ∀ Γ Δ φ ψ,
    Γ ⊢ Δ • φ -> Γ ⊢ Δ • ψ ->
      Γ ⊢ Δ • φ ∧ ψ
| AndL : ∀ Γ Δ φ ψ,
    Γ • φ • ψ ⊢ Δ ->
      Γ • φ ∧ ψ ⊢ Δ
| OrR : ∀ Γ Δ φ ψ,
    Γ ⊢ Δ • φ • ψ ->
      Γ ⊢ Δ • φ ∨ ψ
| OrL : ∀ Γ Δ φ ψ,
    Γ • φ ⊢ Δ -> Γ • ψ ⊢ Δ ->
      Γ • φ ∨ ψ ⊢ Δ
| ImpR : ∀ Γ Δ φ ψ,
    Γ • φ ⊢ Δ • ψ -> (⊗ Γ ) • φ ⊢ ∅ • ψ ->
      Γ ⊢ Δ • (φ → ψ )
| ImpLVar : ∀ Γ Δ p φ,
    Γ • Var p • φ ⊢ Δ ->
      Γ • Var p • (Var p → φ ) ⊢ Δ
| ImpLAnd : ∀ Γ Δ φ1 φ2 φ3,
    Γ • (φ1 → φ2 → φ3 ) ⊢ Δ ->
      Γ • ((φ1 ∧ φ2 ) → φ3 ) ⊢ Δ
| ImpLOr : ∀ Γ Δ φ1 φ2 φ3,
    Γ • (φ1 → φ3 ) • (φ2 → φ3 ) ⊢ Δ ->
      Γ • ((φ1 ∨ φ2 ) → φ3 ) ⊢ Δ
| ImpLImp : ∀ Γ Δ φ1 φ2 φ3,
    Γ • (φ2 → φ3 ) • φ1 ⊢ Δ • φ2 -> ⊗ Γ • (φ2 → φ3 ) • φ1 ⊢ ∅ • φ2 -> Γ • φ3 ⊢ Δ ->
      Γ • ((φ1 → φ2 ) → φ3 ) ⊢ Δ
| ImpLBox : ∀ Γ Δ φ1 φ2,
    (⊗ Γ ) • □ φ1 • φ2 ⊢ ∅ • φ1 ->
    Γ • φ2 ⊢ Δ ->
      Γ • ((□ φ1 ) → φ2 ) ⊢ Δ
| BoxR : ∀ Γ Δ φ, (⊗ Γ ) • □ φ ⊢ ∅ • φ -> Γ ⊢ Δ • □ φ
where "Γ ⊢ Δ" := (Provable Γ Δ).

Notation "Γ ⊢KM Δ" := (Provable Γ Δ) (at level 99, no associativity, Δ at level 90).

Global Hint Constructors Provable : proof.

We show that equivalent multisets prove the same things.

Global Instance proper_Provable : Proper ((≡@{env}) ==> (≡@{env}) ==> (=)) Provable.
Proof. intros Γ Γ' Heq Δ Δ' Heq'. ms. Qed.

Global Ltac equiv_tac :=
  repeat rewrite <- list_to_set_disj_rm;
  repeat rewrite <- list_to_set_disj_env_add;
  repeat (rewrite <- difference_singleton; trivial);
  try rewrite <- list_to_set_disj_rm;
  try (rewrite union_difference_L by trivial);
  try (rewrite union_difference_R by trivial);
  try ms.

We introduce a tactic "peapply" which allows for application of a G4ip rule even in case the left environment needs to be reordered. The tactic "rpeapply" does the same thing on the right.

Tactics

We introduce a few tactics that we will need to prove the admissibility of the weakening and exchange rules in the proof calculus.

The tactic "exchl" swaps the nth pair of formulas of the left-hand side of a sequent, counting from the right. The tactic "exchr" does the same thing but on the right.

The tactic "exhibit" exhibits an element that is in the environment on the left or right hand side.

The tactic "forwardl" tries to change a goal of the form :

((Γ•φ ∖ {ψ}•…) ⊢ …

into

((Γ ∖ {ψ}•…•φ) ⊢ … ,

by first proving that ψ ∈ Γ. The tactic "forwardr" does the same thing on the right.

Ltac forwardl := match goal with
| |- (?Γ•?φ) ∖ {[?ψ]} ⊢ _ =>
  let Hin := fresh "Hin" in
  assert(Hin : ψ ∈ Γ) by ms;
  rewrite (proper_Provable _ _ (env_replace φ Hin) _ _ (env_refl _))
| |- (?Γ•?φ) ∖ {[?ψ]}•_ ⊢ _ =>
  let Hin := fresh "Hin" in
  assert(Hin : ψ ∈ Γ) by ms;
  rewrite (proper_Provable _ _ (equiv_disj_union_compat_r (env_replace φ Hin)) _ _ (env_refl _));
  exchl 0
| |- (?Γ•?φ) ∖ {[?ψ]}•_•_ ⊢ _ =>
  let Hin := fresh "Hin" in
  assert(Hin : ψ ∈ Γ) by ms;
  rewrite (proper_Provable _ _ (equiv_disj_union_compat_r
    (equiv_disj_union_compat_r (env_replace φ Hin))) _ _ (env_refl _));
  exchl 1; exchl 0
| |- (?Γ•?φ) ∖ {[?ψ]}•_•_•_ ⊢ _ =>
  let Hin := fresh "Hin" in
  assert(Hin : ψ ∈ Γ) by ms;
  rewrite (proper_Provable _ _ (equiv_disj_union_compat_r
    (equiv_disj_union_compat_r(equiv_disj_union_compat_r (env_replace φ Hin)))) _ _ (env_refl _));
  exchl 2; exchl 1; exchl 0
| |- (?Γ•?φ) ∖ {[?ψ]}•_•_•_•_ ⊢ _ =>
  let Hin := fresh "Hin" in
  assert(Hin : ψ ∈ Γ) by ms;
  rewrite (proper_Provable _ _ (equiv_disj_union_compat_r
    (equiv_disj_union_compat_r(equiv_disj_union_compat_r(equiv_disj_union_compat_r
      (env_replace φ Hin))))) _ _ (env_refl _));
  exchl 3; exchl 2; exchl 1; exchl 0
end.

Ltac forwardr := match goal with
| |- _ ⊢ ((?Δ•?φ) ∖ {[?ψ]}) =>
  let Hin := fresh "Hin" in
  assert(Hin : ψ ∈ Δ) by ms;
  rewrite (proper_Provable _ _ (env_refl _) _ _ (env_replace φ Hin))
| |- _ ⊢ ((?Δ•?φ) ∖ {[?ψ]}•_) =>
  let Hin := fresh "Hin" in
  assert(Hin : ψ ∈ Δ) by ms;
  rewrite (proper_Provable _ _ (env_refl _) _ _
    (equiv_disj_union_compat_r (env_replace φ Hin)));
  exchr 0
| |- _ ⊢ ((?Δ•?φ) ∖ {[?ψ]}•_•_) =>
  let Hin := fresh "Hin" in
  assert(Hin : ψ ∈ Δ) by ms;
  rewrite (proper_Provable _ _ (env_refl _) _ _
    (equiv_disj_union_compat_r(equiv_disj_union_compat_r (env_replace φ Hin))));
  exchr 1; exchr 0
| |- _ ⊢ ((?Δ•?φ) ∖ {[?ψ]}•_•_•_) =>
  let Hin := fresh "Hin" in
  assert(Hin : ψ ∈ Δ) by ms;
  rewrite (proper_Provable _ _ (env_refl _) _ _
    (equiv_disj_union_compat_r(equiv_disj_union_compat_r(equiv_disj_union_compat_r (env_replace φ Hin)))));
  exchr 2; exchr 1; exchr 0
| |- _ ⊢ ((?Δ•?φ) ∖ {[?ψ]}•_•_•_•_) =>
  let Hin := fresh "Hin" in
  assert(Hin : ψ ∈ Δ) by ms;
  rewrite (proper_Provable _ _ (env_refl _) _ _ (equiv_disj_union_compat_r
    (equiv_disj_union_compat_r(equiv_disj_union_compat_r *
      (equiv_disj_union_compat_r (env_replace φ Hin))))));
  exchr 3; exchr 2; exchr 1; exchr 0
end.

The tactic "backwardl" changes a goal of the form :

((Γ ∖ {ψ}•…•φ) ⊢ …

into

((Γ•φ ∖ {ψ}•…) ⊢ …,

by first proving that ψ ∈ Γ. The tactic "backwardr" does the same thing on the right.

Ltac backwardl := match goal with
| |- ?Γ ∖ {[?ψ]}•?φ ⊢ _ =>
  let Hin := fresh "Hin" in
  assert(Hin : ψ ∈ Γ) by (eauto with proof || ms);
  rewrite (proper_Provable _ _ (symmetry(env_replace _ Hin)) _ _ (env_refl _))
| |- ?Γ ∖ {[?ψ]}•_•?φ ⊢ _ =>
  let Hin := fresh "Hin" in
  assert(Hin : ψ ∈ Γ) by (eauto with proof || ms); try exchl 0;
  rewrite (proper_Provable _ _ (symmetry(equiv_disj_union_compat_r
    (env_replace _ Hin))) _ _ (env_refl _))
| |- ?Γ ∖ {[?ψ]}•_•_•?φ ⊢ _ =>
  let Hin := fresh "Hin" in
  assert(Hin : ψ ∈ Γ) by (eauto with proof || ms); try exchl 0; exchl 1;
  rewrite (proper_Provable _ _ (symmetry(equiv_disj_union_compat_r
    (equiv_disj_union_compat_r (env_replace φ Hin)))) _ _ (env_refl _))
| |- ?Γ ∖ {[?ψ]}•_•_•_•?φ ⊢ _ =>
  let Hin := fresh "Hin" in
  assert(Hin : ψ ∈ Γ) by (eauto with proof || ms); try exchl 0; exchl 1; exchl 2;
  rewrite (proper_Provable _ _ (symmetry(equiv_disj_union_compat_r
    (equiv_disj_union_compat_r(equiv_disj_union_compat_r (env_replace φ Hin))))) _ _ (env_refl _))
| |- ?Γ ∖ {[?ψ]}•_•_•_•_•?φ ⊢ _ =>
  let Hin := fresh "Hin" in
  assert(Hin : ψ ∈ Γ) by (eauto with proof || ms); try exchl 0; exchl 1; exchl 2; exchl 3;
  rewrite (proper_Provable _ _ (symmetry(equiv_disj_union_compat_r
    (equiv_disj_union_compat_r(equiv_disj_union_compat_r(equiv_disj_union_compat_r (env_replace φ Hin)))))) _ _ (env_refl _))
end.

Ltac backwardr := match goal with
| |- _ ⊢ (?Δ ∖ {[?ψ]}•?φ) =>
  let Hin := fresh "Hin" in
  assert(Hin : ψ ∈ Δ) by (eauto with proof || ms);
  rewrite (proper_Provable _ _ (env_refl _) _ _ (symmetry(env_replace _ Hin)))
| |- _ ⊢ (?Δ ∖ {[?ψ]}•_•?φ) =>
  let Hin := fresh "Hin" in
  assert(Hin : ψ ∈ Δ) by (eauto with proof || ms); try exchr 0;
  rewrite (proper_Provable _ _ (env_refl _) _ _
    (symmetry(equiv_disj_union_compat_r (env_replace _ Hin))))
| |- _ ⊢ (?Δ ∖ {[?ψ]}•_•_•?φ) =>
  let Hin := fresh "Hin" in
  assert(Hin : ψ ∈ Δ) by (eauto with proof || ms); try exchr 0; exchr 1;
  rewrite (proper_Provable _ _ (env_refl _) _ _ (symmetry(equiv_disj_union_compat_r
    (equiv_disj_union_compat_r (env_replace φ Hin)))))
| |- _ ⊢ (?Δ ∖ {[?ψ]}•_•_•_•?φ) =>
  let Hin := fresh "Hin" in
  assert(Hin : ψ ∈ Δ) by (eauto with proof || ms); try exchr 0; exchr 1; exchr 2;
  rewrite (proper_Provable _ _ (env_refl _) _ _ (symmetry(equiv_disj_union_compat_r
    (equiv_disj_union_compat_r(equiv_disj_union_compat_r (env_replace φ Hin))))))
| |- _ ⊢ (?Δ ∖ {[?ψ]}•_•_•_•_•?φ) =>
  let Hin := fresh "Hin" in
  assert(Hin : ψ ∈ Δ) by (eauto with proof || ms); try exchr 0; exchr 1; exchr 2; exchr 3;
  rewrite (proper_Provable _ _ (env_refl _) _ _ (symmetry(equiv_disj_union_compat_r
    (equiv_disj_union_compat_r(equiv_disj_union_compat_r
      (equiv_disj_union_compat_r (env_replace φ Hin)))))))
end.

The tactic "rwl" rewrites the left environment equivalence Heq in the premise. The tactic "rwr" does the same thing on the conclusion.

Ltac rwl Heq :=
  erewrite proper_Provable; [|now rewrite Heq| reflexivity].

Ltac rwr Heq :=
  erewrite proper_Provable; [|reflexivity|now rewrite Heq].

Ltac box_tac :=
       let rec box_tac_aux Γ n := lazymatch Γ with
  |⊗(?Γ'' • ?φ) => rewrite (open_boxes_add Γ'' φ)
  |⊗(?Γ' ∖ {[?ψ]}) => match goal with |H: ψ ∈ Γ' |- _ => rwl (open_boxes_remove Γ' ψ H) end
  | ?Γ'' • ?φ => box_tac_aux Γ'' (S n) end
  in
    try match goal with | |- ?Γ ⊢ _ => box_tac_aux Γ 0 end; simpl.

Ltac lazy_apply th:=
((erewrite proper_Provable; [| |reflexivity]); [eapply th|]) ||
((erewrite proper_Provable; [|reflexivity|]); [eapply th|]).