KM.Sequent.SequentProps
Require Import Sequents Order.
(* Required for dependent induction. *)
From Stdlib Require Import Program.Equality.
(* Required for dependent induction. *)
From Stdlib Require Import Program.Equality.
Admissible rules in G4KM sequent calculus
Weakening
Theorem weakeningl φ' Γ Δ : Γ ⊢ Δ -> Γ• φ' ⊢ Δ.
Proof with (auto with proof).
intro H. revert φ'. induction H; intro φ'; auto with proof;
try (exchl 0; auto with proof).
- apply AndL. exchl 1 ; exchl 0...
- apply OrL; exchl 0...
- apply ImpR. exchl 0... box_tac ; exchl 0...
- exchl 1; apply ImpLVar; exchl 1; exchl 0...
- apply ImpLAnd; exchl 0...
- apply ImpLOr. exchl 1; exchl 0...
- apply ImpLImp.
+ exchl 1; exchl 0...
+ box_tac. exchl 1; exchl 0...
+ exchl 0...
- apply ImpLBox ; box_tac.
+ peapply (IHProvable1 (open_box φ')).
+ exchl 0...
- apply BoxR. box_tac. exchl 0...
Qed.
Theorem weakeningr φ' Γ Δ : Γ ⊢ Δ -> Γ ⊢ (Δ • φ').
Proof with (auto with proof).
intro H. revert φ'. induction H; intro φ'; auto with proof ;
try (exchr 0; auto with proof).
- apply AndR ; exchr 0...
- apply OrR; exchr 1... exchr 0...
- apply ImpR ; auto. exchr 0...
- apply ImpLImp; auto. exchr 0...
Qed.
Global Hint Resolve weakeningl : proof.
Global Hint Resolve weakeningr : proof.
Theorem generalised_weakeninglL (Γ Γ' Δ: env) : Γ ⊢ Δ -> Γ' ⊎ Γ ⊢ Δ.
Proof.
intro Hp.
induction Γ' as [| x Γ' IHΓ'] using gmultiset_rec.
- peapply Hp.
- peapply (weakeningl x). exact IHΓ'. ms.
Qed.
Theorem generalised_weakeninglR (Γ Γ' Δ : env) : Γ' ⊢ Δ -> Γ' ⊎ Γ ⊢ Δ.
Proof.
intro Hp.
induction Γ as [| x Γ IHΓ] using gmultiset_rec.
- peapply Hp.
- peapply (weakeningl x). exact IHΓ. ms.
Qed.
Theorem generalised_weakeningrL (Δ Δ' Γ : env) : Γ ⊢ Δ -> Γ ⊢ (Δ' ⊎ Δ).
Proof.
intro Hp.
induction Δ' as [| x Δ' IHΔ'] using gmultiset_rec.
- rpeapply Hp.
- rpeapply (weakeningr x). exact IHΔ'. ms.
Qed.
Theorem generalised_weakeningrL_form (Δ Γ : env) (φ : form): Γ ⊢ ∅ • φ -> Γ ⊢ (Δ • φ).
Proof.
intro Hp.
induction Δ as [| x Δ' IHΔ'] using gmultiset_rec.
- rpeapply Hp.
- rpeapply (weakeningr x). exact IHΔ'. ms.
Qed.
Theorem generalised_weakeningrR (Δ Δ' Γ : env) : Γ ⊢ Δ -> Γ ⊢ (Δ ⊎ Δ').
Proof.
intro Hp.
induction Δ' as [| x Δ' IHΔ'] using gmultiset_rec.
- rpeapply Hp.
- rpeapply (weakeningr x). exact IHΔ'. ms.
Qed.
Global Hint Extern 5 (?a <= ?b) => simpl in *; lia : proof.
Inversion rules
Lemma ImpR_revl Γ Δ φ ψ :
(Γ ⊢ (Δ • (φ → ψ)))
-> (Γ • φ ⊢ (Δ • ψ)).
Proof with (auto with proof).
intro Hp.
remember (Δ • (φ → ψ)) as Δ0 eqn:Heq0.
assert(HeqΔ : Δ ≡ Δ0 ∖ {[φ → ψ]}) by ms.
rwr HeqΔ.
assert(Hin : (φ → ψ) ∈ Δ0) by (subst Δ0; ms).
clear Δ HeqΔ Heq0.
dependent induction Hp generalizing Δ0 Hp; auto with proof; try exchl 0 ; try exchr 0.
- forwardr. constructor.
- forwardr. apply AndR; backwardr; [apply IHHp1 | apply IHHp2]; ms.
- apply AndL. exchl 1 ; exchl 0. apply IHHp ; auto.
- forwardr. apply OrR. exchr 0. do 2 backwardr. apply IHHp. ms.
- apply OrL; exchl 0; [apply IHHp1 | apply IHHp2]; ms.
- case (decide ((φ0 → ψ0) = (φ → ψ))).
+ intro Heq ; dependent destruction Heq ; subst. rpeapply Hp1.
+ intro Hneq. forwardr. apply ImpR.
* backwardr. exchl 0. apply IHHp1. ms.
* rewrite open_boxes_add. exchl 0 ; apply weakeningl ; auto.
- exchl 1. apply ImpLVar. exchl 1 ; exchl 0. apply IHHp ; auto.
- apply ImpLAnd. exchl 0 ; apply IHHp ; auto.
- apply ImpLOr. exchl 1 ; exchl 0 ; apply IHHp ; auto.
- apply ImpLImp.
+ exchl 1. exchl 0. backwardr. apply IHHp1. ms.
+ box_tac. exchl 1; exchl 0 ; apply weakeningl, Hp2.
+ exchl 0. apply IHHp3. ms.
- apply ImpLBox.
+ rewrite open_boxes_add. exchl 1 ; exchl 0 ; apply weakeningl ; auto.
+ exchl 0 ; apply IHHp2 ; auto.
- forwardr. apply BoxR. rewrite open_boxes_add ; exchl 0 ; apply weakeningl ; auto.
Qed.
Theorem generalised_axiom Γ Δ φ : Γ • φ ⊢ Δ • φ.
Proof with (auto with proof).
remember (weight φ) as w.
assert(Hle : weight φ ≤ w) by lia.
clear Heqw. revert Γ Δ φ Hle.
induction w; intros Γ Δ φ Hle.
- assert (Hφ := weight_pos φ). lia.
- destruct φ; simpl in Hle...
+ dependent destruction φ1.
* apply ImpR.
-- exchl 0. apply ImpLVar. exchl 0...
-- box_tac. exchl 0. apply ImpLVar, IHw...
* auto with proof.
* apply ImpR.
-- apply AndL. exchl 1; exchl 0. apply ImpLAnd.
exchl 0. apply ImpR_revl. exchl 0.
apply ImpR_revl. apply IHw...
-- box_tac. apply AndL. exchl 1. exchl 0. apply ImpLAnd.
exchl 0. exchl 1. apply ImpR_revl, ImpR_revl, IHw...
* apply ImpLOr. apply ImpR; apply OrL.
-- exchl 1. apply ImpR_revl, IHw...
-- apply ImpR_revl, IHw...
-- repeat box_tac. exchl 1. apply ImpR_revl, IHw...
-- repeat box_tac. apply ImpR_revl, IHw...
* apply ImpR.
-- exchl 0. apply ImpLImp.
++ apply ImpR_revl. exchl 0. apply IHw. lia.
++ repeat box_tac. apply ImpR_revl. exchl 0. apply IHw. lia.
++ apply IHw. lia.
-- repeat box_tac; exchl 0. apply ImpLImp.
++ apply ImpR_revl. exchl 0. apply IHw. lia.
++ repeat box_tac. apply ImpR_revl. exchl 0. apply IHw. lia.
++ apply IHw. lia.
* apply ImpR; box_tac; exchl 0; apply ImpLBox; box_tac...
+ apply BoxR. box_tac. exchl 0. apply IHw. lia.
Qed.
Global Hint Resolve generalised_axiom : proof.
Lemma open_box_L Γ φ ψ : Γ • φ ⊢ ψ -> Γ • ⊙ φ ⊢ ψ.
Proof.
intro Hp.
remember (Γ•φ) as Γ' eqn:HH.
assert (Heq: Γ ≡ Γ' ∖ {[ φ ]}) by ms.
assert(Hin : φ ∈ Γ')by ms.
rwl Heq. clear Γ HH Heq. revert φ Hin.
dependent induction Hp generalizing Γ' Hp; intros φ0 Hin.
- case (decide (φ0 = Var p)).
+ intro; subst. simpl. auto with proof.
+ intro. forwardl. auto with proof.
- case (decide (φ0 = ⊥)).
+ intro; subst. simpl. auto with proof.
+ intro. forwardl. auto with proof.
- apply AndR; auto.
- case (decide (φ0 = (φ ∧ ψ))).
+ intro; subst. simpl. apply AndL. peapply Hp.
+ intro. forwardl. apply AndL. exchl 0. do 2 backwardl.
peapply (IHHp φ0). ms.
- apply OrR; auto.
- case (decide (φ0 = (φ ∨ ψ))).
+ intro; subst. simpl. apply OrL.
* peapply Hp1.
* peapply Hp2.
+ intro. forwardl. apply OrL.
* backwardl. peapply IHHp1. ms.
* backwardl. peapply IHHp2. ms.
- apply ImpR.
+ backwardl. apply IHHp1. ms.
+ repeat box_tac. backwardl. apply IHHp2. ms.
- case (decide (φ0 = Var p)).
+ intro; subst; simpl. forwardl. apply ImpLVar. peapply Hp.
+ intro. case (decide (φ0 = (Var p → φ))).
* intro; subst; simpl. peapply (ImpLVar Γ). exact Hp.
* intro. do 2 forwardl. exchl 0. apply ImpLVar. exchl 0. do 2 backwardl.
apply IHHp. ms.
- case (decide (φ0 = (φ1 ∧ φ2 → φ3))).
+ intro; subst; simpl. apply ImpLAnd. peapply Hp.
+ intro. forwardl. apply ImpLAnd. backwardl. apply IHHp. ms.
- case (decide (φ0 = (φ1 ∨ φ2 → φ3))).
+ intro; subst; simpl. apply ImpLOr. peapply Hp.
+ intro. forwardl. apply ImpLOr. exchl 0. do 2 backwardl. apply IHHp. ms.
- case (decide (φ0 = ((φ1 → φ2) → φ3))).
+ intro; subst; simpl. rewrite env_add_remove. now apply ImpLImp.
+ intro. forwardl. apply ImpLImp.
* exchl 0. do 2 backwardl. apply IHHp1. ms.
* repeat box_tac. exchl 0. do 2 backwardl. apply IHHp2. ms.
* backwardl. apply IHHp3. ms.
- case (decide (φ0 = (□ φ1 → φ2))).
+ intro; subst; simpl. apply ImpLBox.
* box_tac. lazy_apply Hp1. autorewrite with proof. ms.
* peapply Hp2.
+ intro. forwardl.
case (decide (open_box φ0 = □ φ1)).
* intro Heq. repeat rewrite Heq. apply ImpLBox; box_tac.
-- exchl 1; exchl 0. apply generalised_axiom.
-- backwardl. rewrite <- Heq. apply IHHp2. auto with *.
* intro Hneq. case (decide (open_box φ0 = φ2)).
-- intro Heq. subst φ2. apply ImpLBox; box_tac.
++ box_tac. backwardl. rewrite env_add_remove.
exchl 0. peapply (IHHp1 (⊙ φ0)). ms.
++ box_tac. backwardl. apply IHHp2. auto with *.
-- intro Hneq'. apply ImpLBox; repeat box_tac.
++ exchl 0. box_tac. backwardl. backwardl. eapply IHHp1. ms.
++ backwardl. apply IHHp2. apply env_in_add. now right.
- case (decide (open_box φ0 = □ φ)).
+ intro Heq; rewrite Heq. apply generalised_axiom.
+ intro. backwardl. apply BoxR. box_tac.
case (decide (φ0 = open_box φ0)).
* intro Heq. rewrite <- Heq. autorewrite with proof. exact Hp.
* intro. assert( open_box φ0 ∈ open_boxes Γ) by (now apply In_open_boxes).
rwl (env_replace (⊙φ0) Hin0). box_tac. exchl 0.
lazy_apply (IHHp (open_box φ0)); [ms|].
rewrite open_boxes_remove, env_replace by trivial. ms.
Qed.
Local Hint Resolve env_in_add : proof.
Lemma AndL_rev Γ φ ψ θ: (Γ•φ ∧ ψ) ⊢ θ → (Γ•φ•ψ) ⊢ θ.
Proof.
intro Hp.
remember (Γ•φ ∧ ψ) as Γ' eqn:HH.
assert (Heq: Γ ≡ Γ' ∖ {[ φ ∧ ψ ]}) by ms.
assert(Hin : (φ ∧ ψ) ∈ Γ')by ms.
rwl Heq. clear Γ HH Heq. revert φ ψ Hin.
(* we massaged the goal so that the environment of the derivation on which we do
the induction is not composite anymore *)
induction Hp; intros φ0 ψ0 Hin.
(* auto takes care of the right rules easily *)
- forwardl. auto with proof.
- forwardl. auto with proof.
- apply AndR; auto with proof.
(* the main case *)
- case(decide ((φ ∧ ψ) = (φ0 ∧ ψ0))); intro Heq0.
+ dependent destruction Heq0; subst. peapply Hp.
+ forwardl. constructor 4. exchl 0. backwardl. backwardl. apply IHHp. ms.
(* only left rules remain. Now it's all a matter of putting the right principal
formula at the front, apply the rule; and put back the front formula at the back
before applying the induction hypothesis *)
- apply OrR. auto with proof.
- forwardl. apply OrL; backwardl; [apply IHHp1 | apply IHHp2]; ms.
- apply ImpR.
+ backwardl. apply IHHp1. ms.
+ repeat box_tac. backwardl. apply open_box_L. exchl 0. apply open_box_L.
exchl 0. apply IHHp2. ms.
- forwardl. forwardl. exchl 0. apply ImpLVar. exchl 0. do 2 backwardl. apply IHHp. ms.
- forwardl. apply ImpLAnd. backwardl. apply IHHp. ms.
- forwardl. apply ImpLOr. exchl 0. do 2 backwardl. apply IHHp. ms.
- forwardl. apply ImpLImp.
+ exchl 0. do 2 backwardl. apply IHHp1. ms.
+ repeat box_tac. exchl 0. do 2 backwardl.
do 2 (apply open_box_L; exchl 0). apply IHHp2. ms.
+ backwardl. apply IHHp3. ms.
- forwardl. apply ImpLBox; repeat box_tac.
+ exchl 0. box_tac.
apply In_open_boxes in Hin0. backwardl. backwardl. apply open_box_L. exchl 0.
apply open_box_L. exchl 0.
apply IHHp1. ms.
+ backwardl. apply IHHp2. ms.
- apply BoxR. repeat box_tac. backwardl. apply open_box_L.
exchl 0. apply open_box_L. exchl 0. peapply (IHHp φ0 ψ0). ms.
Qed.
Lemma open_boxes_R (Γ : env) Γ' Δ: (Γ ⊎ Γ') ⊢ Δ → (⊗Γ) ⊎ Γ' ⊢ Δ.
Proof.
revert Δ Γ'.
induction Γ using gmultiset_rec; intros Δ Γ'.
- rewrite open_boxes_empty. trivial.
- intro HP. lazy_apply (open_box_L ((⊗ Γ) ⊎ Γ') x Δ).
+ replace ((⊗ Γ) ⊎ Γ' • x) with ((⊗ Γ) ⊎ (Γ' • x)) by ms.
apply IHΓ. peapply HP.
+ rewrite open_boxes_disj_union, open_boxes_singleton; ms.
Qed.
Lemma open_boxes_R2 (Γ : env) φ ψ Δ: (Γ • φ • ψ) ⊢ Δ → (⊗Γ) • φ • ψ ⊢ Δ.
Proof.
revert Δ φ ψ.
induction Γ using gmultiset_rec; intros Δ φ ψ.
- rewrite open_boxes_empty. trivial.
- intro HP. lazy_apply (open_box_L (⊗ Γ • φ • ψ) x Δ).
+ apply AndL_rev, IHΓ, AndL. peapply HP.
+ rewrite open_boxes_disj_union, open_boxes_singleton; ms.
Qed.
Lemma open_boxes_R3 (Γ : env) φ ψ χ Δ: (Γ • φ • ψ • χ) ⊢ Δ → (⊗Γ) • φ • ψ • χ ⊢ Δ.
Proof.
revert Δ φ ψ χ.
induction Γ using gmultiset_rec; intros Δ φ ψ χ.
- rewrite open_boxes_empty. trivial.
- intro HP. lazy_apply (open_box_L (⊗ Γ • φ • ψ • χ) x Δ).
+ apply AndL_rev, IHΓ, AndL. peapply HP.
+ rewrite open_boxes_disj_union, open_boxes_singleton; ms.
Qed.
Lemma open_boxes_weakening_L (Γ : env) Δ: Γ ⊢ Δ → (⊗Γ) ⊢ Δ.
Proof.
revert Δ.
destruct Γ using gmultiset_rec; intros Δ.
- rewrite open_boxes_empty. trivial.
- intro HP. lazy_apply (open_box_L (⊗ Γ) x Δ).
+ apply open_boxes_R. peapply HP.
+ rewrite open_boxes_disj_union, open_boxes_singleton; ms.
Qed.
(* We can get back the (non-modal) right implication rule from G4iP when the
conclusion is a singleton *)
Lemma ImpR_singleton Γ φ ψ : Γ • φ ⊢ ∅ • ψ -> Γ ⊢ ∅ • (φ → ψ).
Proof.
intro Hp. apply ImpR; [|apply open_boxes_R]; exact Hp.
Qed.
(* Or more generally, the intuitionistic right-implication rule. *)
Lemma Int_ImpR Γ Δ φ ψ :
(Γ • φ ⊢ ∅ • ψ) ->
(Γ ⊢ (Δ • (φ → ψ))).
Proof with (auto with proof).
intro Hp.
apply ImpR.
- rpeapply (generalised_weakeningrL (∅ • ψ) Δ) ; exact Hp.
- apply open_boxes_R ; auto.
Qed.
Lemma OrL_rev Γ φ ψ θ: (Γ • φ ∨ ψ) ⊢ θ → (Γ • φ ⊢ θ) * (Γ • ψ ⊢ θ).
Proof.
intro Hp.
remember (Γ•φ ∨ ψ) as Γ' eqn:HH.
assert (Heq: Γ ≡ Γ' ∖ {[ φ ∨ ψ ]}) by ms.
assert(Hin : (φ ∨ ψ) ∈ Γ')by ms.
assert(Heq' : ((Γ' ∖ {[φ ∨ ψ]}•φ) ⊢ θ) * ((Γ' ∖ {[φ ∨ ψ]}•ψ) ⊢ θ));
[| split; rwl Heq; tauto].
clear Γ HH Heq.
induction Hp.
- split; forwardl; auto with proof.
- split; forwardl; auto with proof.
- split; constructor 3; now (apply IHHp1 || apply IHHp2).
- split; forwardl; constructor 4; exchl 0; do 2 backwardl; apply IHHp; ms.
- split; constructor 5; now apply IHHp.
- case (decide ((φ0 ∨ ψ0) = (φ ∨ ψ))); intro Heq0.
+ dependent destruction Heq0; subst. split; [peapply Hp1| peapply Hp2].
+ split; forwardl; apply OrL; backwardl; (apply IHHp1||apply IHHp2); ms.
- split; (apply ImpR; repeat box_tac;
backwardl; [apply IHHp1; ms| apply open_box_L, IHHp2; ms]).
- split; do 2 forwardl; exchl 0; apply ImpLVar;
exchl 0; do 2 backwardl; apply IHHp; ms.
- split; forwardl; apply ImpLAnd; backwardl; apply IHHp; ms.
- split; forwardl; apply ImpLOr; exchl 0; do 2 backwardl; apply IHHp; ms.
- split;forwardl; apply ImpLImp.
+ exchl 0. do 2 backwardl. apply IHHp1. ms.
+ repeat box_tac. exchl 0. do 2 backwardl.
apply open_box_L. apply IHHp2. ms.
+ backwardl. apply IHHp3. ms.
+ exchl 0. do 2 backwardl. apply IHHp1. ms.
+ repeat box_tac. exchl 0. do 2 backwardl.
apply open_box_L. apply IHHp2. ms.
+ backwardl. apply IHHp3. ms.
- split; forwardl; (apply ImpLBox; repeat box_tac; exchl 0;
[do 2 backwardl; apply open_box_L; apply IHHp1|exchl 0; backwardl; apply IHHp2];ms).
- split; apply BoxR; repeat box_tac; backwardl; apply open_box_L; apply IHHp; ms.
Qed.
Lemma OrR_rev Γ φ ψ Δ: Γ ⊢ (Δ • φ ∨ ψ) → (Γ ⊢ (Δ • φ • ψ)).
Proof.
intro Hp.
remember (Δ • φ ∨ ψ) as Δ0 eqn:Heq0.
assert(HeqΔ : Δ ≡ Δ0 ∖ {[φ ∨ ψ]}) by ms.
rwr HeqΔ.
assert(Hin : (φ ∨ ψ) ∈ Δ0) by (subst Δ0; ms).
clear Δ HeqΔ Heq0.
dependent induction Hp generalizing φ ψ Hp ;
try specialize (IHHp _ _ eq_refl);
try specialize (IHHp1 _ _ eq_refl);
try specialize (IHHp2 _ _ eq_refl);
intuition ; repeat forwardr ; auto with proof.
- apply AndR.
+ backwardr. apply IHHp1 ; ms.
+ backwardr. apply IHHp2 ; ms.
- case (decide ((φ0 ∨ ψ0) = (φ ∨ ψ))).
+ intro H ; inversion H ; subst. rpeapply Hp.
+ intro H. forwardr. apply OrR ; exchr 0 ; do 2 backwardr ; apply IHHp ; ms.
- apply ImpR ; auto. backwardr. apply IHHp1 ; ms.
- apply ImpLImp.
+ backwardr. apply IHHp1. ms.
+ apply Hp2.
+ apply H.
Qed.
Lemma TopL_rev Γ φ θ: Γ•(⊥ → φ) ⊢ θ -> Γ ⊢ θ.
Proof.
remember (Γ•(⊥ → φ)) as Γ' eqn:HH.
assert (Heq: Γ ≡ Γ' ∖ {[ ⊥ → φ ]}) by ms.
assert(Hin : (⊥ → φ) ∈ Γ')by ms. clear HH.
intro Hp. rwl Heq. clear Γ Heq. induction Hp;
try forwardl.
- auto with proof.
- auto with proof.
- auto with proof.
- apply AndL. exchl 0. do 2 backwardl. apply IHHp. ms.
- auto with proof.
- apply OrL; backwardl; [apply IHHp1 | apply IHHp2]; ms.
- apply ImpR; repeat box_tac; backwardl;
[apply IHHp1| apply IHHp2]; ms.
- forwardl. exchl 0. apply ImpLVar. exchl 0. do 2 backwardl. apply IHHp. ms.
- apply ImpLAnd. backwardl. apply IHHp. ms.
- apply ImpLOr. exchl 0. do 2 backwardl. apply IHHp. ms.
- apply ImpLImp.
+ exchl 0. do 2 backwardl; apply IHHp1. ms.
+ box_tac. exchl 0. do 2 backwardl. apply IHHp2. ms.
+ backwardl. apply IHHp3. ms.
- apply ImpLBox; box_tac.
+ exchl 0. do 2 backwardl. apply IHHp1. ms.
+ backwardl. apply IHHp2. ms.
- apply BoxR. box_tac. backwardl. apply IHHp. ms.
Qed.
Local Hint Immediate TopL_rev : proof.
Lemma ImpLVar_rev Γ p φ ψ: (Γ•Var p•(p → φ)) ⊢ ψ → (Γ•Var p•φ) ⊢ ψ.
Proof.
intro Hp.
remember (Γ•Var p•(p → φ)) as Γ' eqn:HH.
assert (Heq: (Γ•Var p) ≡ Γ' ∖ {[Var p → φ]}) by ms.
assert(Hin : (p → φ) ∈ Γ')by ms.
rwl Heq. clear Γ HH Heq.
induction Hp.
- forwardl; auto with proof.
- forwardl; auto with proof.
- apply AndR; auto with proof.
- forwardl; apply AndL. exchl 0. do 2 backwardl. apply IHHp. ms.
- apply OrR. auto with proof.
- forwardl; apply OrL; backwardl; apply IHHp1 || apply IHHp2; ms.
- apply ImpR; repeat box_tac; backwardl;
[apply IHHp1| apply open_box_L, IHHp2]; ms.
- case (decide ((Var p0 → φ0) = (Var p → φ))); intro Heq0.
+ dependent destruction Heq0; subst. peapply Hp.
+ do 2 forwardl. exchl 0. apply ImpLVar. exchl 0; do 2 backwardl. apply IHHp. ms.
- forwardl; apply ImpLAnd. backwardl. apply IHHp. ms.
- forwardl; apply ImpLOr. exchl 0; do 2 backwardl. apply IHHp. ms.
- forwardl; apply ImpLImp.
+ exchl 0; do 2 backwardl; apply IHHp1; ms.
+ repeat box_tac. exchl 0; do 2 backwardl; apply open_box_L, IHHp2; ms.
+ backwardl; apply IHHp3; ms.
- forwardl; apply ImpLBox; repeat box_tac.
+ exchl 0; do 2 backwardl. apply open_box_L. apply IHHp1. ms.
+ backwardl. apply IHHp2. ms.
- apply BoxR. repeat box_tac. backwardl. apply open_box_L. apply IHHp. ms.
Qed.
(* inversion for ImpLImp is only partial *)
Lemma ImpLImp_prev Γ φ1 φ2 φ3 ψ: (Γ•((φ1 → φ2) → φ3)) ⊢ ψ -> (Γ•φ3) ⊢ ψ.
Proof.
intro Hp.
remember (Γ •((φ1 → φ2) → φ3)) as Γ' eqn:HH.
assert (Heq: Γ ≡ Γ' ∖ {[ ((φ1 → φ2) → φ3) ]}) by ms.
assert(Hin :((φ1 → φ2) → φ3) ∈ Γ')by ms.
rwl Heq. clear Γ HH Heq.
induction Hp.
- forwardl; auto with proof.
- forwardl; auto with proof.
- apply AndR; auto with proof.
- forwardl; apply AndL. exchl 0; do 2 backwardl. apply IHHp. ms.
- apply OrR. auto with proof.
- forwardl; apply OrL; backwardl; [apply IHHp1 | apply IHHp2]; ms.
- apply ImpR; repeat box_tac; backwardl;
[apply IHHp1| apply open_box_L, IHHp2]; ms.
- do 2 forwardl. exchl 0. apply ImpLVar. exchl 0. do 2 backwardl. apply IHHp. ms.
- forwardl; apply ImpLAnd. backwardl. apply IHHp. ms.
- forwardl; apply ImpLOr. exchl 0. do 2 backwardl. apply IHHp. ms.
- case (decide (((φ0 → φ4) → φ5) = ((φ1 → φ2) → φ3))); intro Heq0.
+ dependent destruction Heq0; subst. rewrite env_add_remove. apply Hp3.
+ forwardl. apply ImpLImp.
* exchl 0; do 2 backwardl; apply IHHp1; ms.
* repeat box_tac. exchl 0; do 2 backwardl. apply open_box_L, IHHp2; ms.
* backwardl. apply IHHp3; ms.
- forwardl; apply ImpLBox; repeat box_tac.
+ exchl 0; do 2 backwardl. apply open_box_L. apply IHHp1. ms.
+ backwardl. apply IHHp2. ms.
- apply BoxR. repeat box_tac. backwardl. apply open_box_L. apply IHHp. ms.
Qed.
(* Inversion for ImpLbox is only partial too *)
Lemma ImpLBox_prev Γ φ1 φ2 ψ: (Γ•((□φ1) → φ2)) ⊢ ψ -> (Γ•φ2) ⊢ ψ.
Proof.
intro Hp.
remember (Γ •((□φ1) → φ2)) as Γ' eqn:HH.
assert (Heq: Γ ≡ Γ' ∖ {[ ((□φ1) → φ2) ]}) by ms.
assert(Hin :((□φ1) → φ2) ∈ Γ')by ms.
rwl Heq. clear Γ HH Heq.
dependent induction Hp.
- forwardl; auto with proof.
- forwardl; auto with proof.
- apply AndR; auto with proof.
- forwardl; apply AndL. exchl 0; do 2 backwardl. apply IHHp; trivial. ms.
- apply OrR. auto with proof.
- forwardl; apply OrL; backwardl; [apply IHHp1 | apply IHHp2]; ms.
- apply ImpR; repeat box_tac; backwardl;
[apply IHHp1| apply open_box_L, IHHp2]; ms.
- do 2 forwardl. exchl 0. apply ImpLVar. exchl 0. do 2 backwardl.
apply IHHp; trivial. ms.
- forwardl; apply ImpLAnd. backwardl. apply IHHp; trivial. ms.
- forwardl; apply ImpLOr. exchl 0. do 2 backwardl. apply IHHp; trivial. ms.
- forwardl; apply ImpLImp.
+ exchl 0; do 2 backwardl; apply IHHp1; trivial. ms.
+ repeat box_tac. exchl 0; do 2 backwardl; apply open_box_L, IHHp2; ms.
+ backwardl; apply IHHp3; trivial. ms.
- case (decide((□φ0 → φ3) = (□φ1 → φ2))).
+ intro Heq; dependent destruction Heq; subst. peapply Hp2.
+ intro Hneq. forwardl. apply ImpLBox; repeat box_tac.
* exchl 0; do 2 backwardl. apply open_box_L; apply IHHp1; trivial. ms.
* backwardl. apply IHHp2; trivial. ms.
- apply BoxR. repeat box_tac. backwardl. apply open_box_L. apply IHHp; trivial. ms.
Qed.
Lemma ImpLOr_rev Γ φ1 φ2 φ3 ψ:
Γ•((φ1 ∨ φ2) → φ3) ⊢ ψ -> Γ•(φ1 → φ3)•(φ2 → φ3) ⊢ ψ.
Proof.
intro Hp.
remember (Γ •((φ1 ∨ φ2) → φ3)) as Γ' eqn:HH.
assert (Heq: Γ ≡ Γ' ∖ {[ ((φ1 ∨ φ2) → φ3) ]}) by ms.
assert(Hin :((φ1 ∨ φ2) → φ3) ∈ Γ')by ms.
rwl Heq. clear Γ HH Heq.
induction Hp.
- forwardl; auto with proof.
- forwardl; auto with proof.
- apply AndR; auto with proof.
- forwardl; constructor 4. exchl 0; do 2 backwardl. apply IHHp. ms.
- apply OrR. auto with proof.
- forwardl. apply OrL; backwardl; [apply IHHp1 | apply IHHp2]; ms.
- apply ImpR; repeat box_tac; backwardl; [apply IHHp1 | apply IHHp2]; ms.
- do 2 forwardl. exchl 0. apply ImpLVar. exchl 0. do 2 backwardl. apply IHHp. ms.
- forwardl; apply ImpLAnd. backwardl. apply IHHp. ms.
- case (decide (((φ0 ∨ φ4) → φ5) = ((φ1 ∨ φ2) → φ3))); intro Heq0.
+ dependent destruction Heq0; subst. peapply Hp.
+ forwardl. apply ImpLOr; exchl 0; do 2 backwardl; apply IHHp; ms.
- forwardl; apply ImpLImp.
+ exchl 0; do 2 backwardl; apply IHHp1; trivial. ms.
+ repeat box_tac. exchl 0; do 2 backwardl; apply IHHp2; ms.
+ backwardl; apply IHHp3; trivial. ms.
- forwardl; apply ImpLBox; repeat box_tac.
+ exchl 0; do 2 backwardl. apply IHHp1. ms.
+ backwardl. apply IHHp2. ms.
- apply BoxR. repeat box_tac. backwardl. apply IHHp. ms.
Qed.
Lemma ImpLAnd_rev Γ φ1 φ2 φ3 ψ: (Γ•(φ1 ∧ φ2 → φ3)) ⊢ ψ -> (Γ•(φ1 → φ2 → φ3)) ⊢ ψ .
Proof.
intro Hp.
remember (Γ •((φ1 ∧ φ2) → φ3)) as Γ' eqn:HH.
assert (Heq: Γ ≡ Γ' ∖ {[ ((φ1 ∧ φ2) → φ3) ]}) by ms.
assert(Hin :((φ1 ∧ φ2) → φ3) ∈ Γ')by ms.
rwl Heq. clear Γ HH Heq.
induction Hp.
- forwardl; auto with proof.
- forwardl; auto with proof.
- apply AndR; auto with proof.
- forwardl; constructor 4. exchl 0; do 2 backwardl. apply IHHp. ms.
- apply OrR. auto with proof.
- forwardl. apply OrL; backwardl; [apply IHHp1 | apply IHHp2]; ms.
- apply ImpR; repeat box_tac; backwardl; [apply IHHp1 | apply IHHp2]; ms.
- do 2 forwardl. exchl 0. apply ImpLVar. exchl 0. do 2 backwardl. apply IHHp. ms.
- case (decide (((φ0 ∧ φ4) → φ5) = ((φ1 ∧ φ2) → φ3))); intro Heq0.
+ dependent destruction Heq0; subst. peapply Hp.
+ forwardl. apply ImpLAnd. backwardl. apply IHHp. ms.
- forwardl; apply ImpLOr; exchl 0; do 2 backwardl; apply IHHp; ms.
- forwardl; apply ImpLImp.
+ exchl 0; do 2 backwardl; apply IHHp1; trivial. ms.
+ repeat box_tac. exchl 0; do 2 backwardl; apply IHHp2; ms.
+ backwardl; apply IHHp3; trivial. ms.
- forwardl; apply ImpLBox; repeat box_tac.
+ exchl 0; do 2 backwardl. apply IHHp1. ms.
+ backwardl. apply IHHp2. ms.
- apply BoxR. repeat box_tac. backwardl. apply IHHp. ms.
Qed.
Global Hint Resolve AndL_rev : proof.
Global Hint Resolve OrL_rev : proof.
Global Hint Resolve ImpLVar_rev : proof.
Global Hint Resolve ImpLOr_rev : proof.
Global Hint Resolve ImpLAnd_rev : proof.
Global Hint Resolve ImpLBox_prev : proof.
A general inversion rule for disjunction is not admissible.
However, inversion holds if one of the formulas is ⊥.
Lemma OrR_Bot_rev Γ Δ : Γ ⊢ Δ • ⊥ -> Γ ⊢ Δ.
Proof. intro Hd.
remember (Δ • ⊥) as Δ0 eqn:Heq0.
assert(HeqΔ : Δ ≡ Δ0 ∖ {[⊥]}) by ms.
rwr HeqΔ.
assert(Hin : ⊥ ∈ Δ0) by (subst Δ0; ms).
clear Δ HeqΔ Heq0.
dependent induction Hd; repeat forwardr; auto with proof.
- apply AndR; backwardr.
+ apply IHHd1. ms.
+ apply IHHd2. ms.
- apply OrR; exchr 0; do 2 backwardr. apply IHHd. ms.
- apply ImpR.
+ backwardr. apply IHHd1. ms.
+ apply Hd2.
- apply ImpLImp; auto with proof. backwardr. apply IHHd1. ms.
Qed.
Lemma exfalso Γ Δ: Γ ⊢ ∅ • ⊥ -> Γ ⊢ Δ.
Proof.
intro Hp. apply OrR_Bot_rev in Hp.
apply generalised_weakeningrR with (Δ':=Δ) in Hp.
rpeapply Hp.
Qed.
Global Hint Immediate exfalso : proof.
Lemma AndR_rev {Γ Δ} φ1 φ2 : Γ ⊢ Δ • (φ1 ∧ φ2) -> (Γ ⊢ Δ • φ1) * (Γ ⊢ Δ • φ2).
Proof.
intro Hp.
remember (Δ • φ1 ∧ φ2) as Δ0 eqn:Heq0.
assert(HeqΔ : Δ ≡ Δ0 ∖ {[φ1 ∧ φ2]}) by ms.
enough ((Γ ⊢KM Δ0 ∖ {[φ1 ∧ φ2]} • φ1) * (Γ ⊢KM Δ0 ∖ {[φ1 ∧ φ2]} • φ2)).
- split ; rwr HeqΔ ; destruct H ; auto.
- assert(Hin : (φ1 ∧ φ2) ∈ Δ0) by (subst Δ0; ms).
clear Δ HeqΔ Heq0.
dependent induction Hp generalizing φ1 φ2 Hp ;
try specialize (IHHp _ _ eq_refl);
try specialize (IHHp1 _ _ eq_refl);
try specialize (IHHp2 _ _ eq_refl);
intuition ; repeat forwardr ; auto with proof.
+ case (decide ((φ1 ∧ φ2) = (φ ∧ ψ))).
* intro H ; inversion H ; subst.
rpeapply Hp1.
* intro H. forwardr. apply
AndR ; [ backwardr ; apply IHHp1 ; ms | backwardr ; apply IHHp2 ; ms].
+ case (decide ((φ1 ∧ φ2) = (φ ∧ ψ))).
* intro H ; inversion H ; subst.
rpeapply Hp2.
* intro H. forwardr.
apply AndR ; [ backwardr ; apply IHHp1 ; ms | backwardr ; apply IHHp2 ; ms].
+ apply OrR. exchr 0. do 2 backwardr. apply IHHp ; ms.
+ apply OrR. exchr 0. do 2 backwardr. apply IHHp ; ms.
+ apply ImpR ; auto. backwardr. apply IHHp1 ; ms.
+ apply ImpR ; auto. backwardr. apply IHHp1 ; ms.
+ apply ImpLImp; auto with proof. backwardr. apply IHHp1 ; ms.
+ apply ImpLImp; auto with proof. backwardr. apply IHHp1 ; ms.
Qed.
Contraction on the left and on the right.
Fixpoint height {Γ Δ} (Hp : Γ ⊢ Δ) := match Hp with
| Atom Γ Δ p => 1
| ExFalso Γ Δ => 1
| AndR Γ Δ φ ψ H1 H2 => 1 + height H1 + height H2
| AndL Γ φ ψ θ H => 1 + height H
| OrR Γ Δ φ ψ H => 1 + height H
| OrL Γ Δ φ ψ H1 H2 => 1 + height H1 + height H2
| ImpR Γ Δ φ ψ H1 H2 => 1 + height H1 + height H2
| ImpLVar Γ Δ p φ H => 1 + height H
| ImpLAnd Γ Δ φ1 φ2 φ3 H => 1 + height H
| ImpLOr Γ Δ φ1 φ2 φ3 H => 1 + height H
| ImpLImp Γ Δ φ1 φ2 φ3 H1 H2 H3 => 1 + max(height H1) (max (height H2) (height H3))
| ImpLBox Γ Δ φ1 φ2 H1 H2 => 1 + height H1 + height H2
| BoxR Γ Δ φ H => 1 + height H
end.
Lemma height_0 {Γ Δ} (Hp : Γ ⊢ Δ) : height Hp <> 0.
Proof. destruct Hp; simpl; lia. Qed.
Lemma ImpLBox_dup Γ φ1 φ2 θ:
Γ•(□ φ1 → φ2) ⊢ θ ->
Γ • □ φ1 • □ φ1 • φ2 ⊢ θ.
Proof.
intro Hp.
remember (Γ• (□ φ1 → φ2)) as Γ0 eqn:Heq0.
assert(HeqΓ : Γ ≡ Γ0 ∖ {[(□ φ1 → φ2)]}) by ms.
rwl HeqΓ.
assert(Hin : (□ φ1 → φ2) ∈ Γ0) by (subst Γ0; ms).
clear Γ HeqΓ Heq0.
(* by induction on the height of the derivation *)
remember (height Hp) as h.
assert(Hleh : height Hp ≤ h) by lia. clear Heqh.
revert Γ0 θ Hp Hleh Hin. induction h as [|h]; intros Γ θ Hp Hleh Hin;
[pose (height_0 Hp); lia|].
dependent destruction Hp; simpl in Hleh.
- forwardl. auto with proof.
- forwardl. auto with proof.
- apply AndR.
+ apply IHh with Hp1. lia. ms.
+ apply IHh with Hp2. lia. ms.
- forwardl. apply AndL. exchl 0. do 2 backwardl. apply IHh with Hp. lia. ms.
- apply OrR. apply IHh with Hp. lia. ms.
- forwardl. apply OrL; backwardl.
+ apply IHh with Hp1. lia. ms.
+ apply IHh with Hp2. lia. ms.
- apply ImpR.
+ backwardl. apply IHh with Hp1; [lia|ms].
+ repeat box_tac. backwardl. apply open_box_L.
change φ1 with (⊙ (□ φ1)) at 2 3. exchl 0. apply open_box_L.
exchl 1; exchl 0. apply open_box_L. exchl 1; exchl 0.
apply IHh with Hp2; [lia|ms].
- do 2 forwardl. exchl 0. apply ImpLVar. exchl 0. do 2 backwardl.
apply IHh with Hp. lia. ms.
- forwardl. apply ImpLAnd. backwardl. apply IHh with Hp. lia. ms.
- forwardl. apply ImpLOr. exchl 0. do 2 backwardl. apply IHh with Hp. lia. ms.
- forwardl. apply ImpLImp.
+ exchl 0; do 2 backwardl. apply IHh with Hp1. lia. ms.
+ repeat rewrite open_boxes_add.
do 3 (exchl 2; exchl 1; exchl 0; apply open_box_L; exchl 3).
box_tac. do 2 (exchl 2; exchl 1; exchl 0; backwardl).
apply IHh with Hp2. lia. ms.
+ backwardl. apply IHh with Hp3. lia. ms.
- case (decide ((□ φ0 → φ3) = □ φ1 → φ2)); intro Heq.
+ dependent destruction Heq; subst.
exchl 0. apply weakeningl. exchl 0. apply weakeningl. peapply Hp2.
+ forwardl. apply ImpLBox; repeat box_tac.
* exchl 0. do 2 backwardl.
replace (φ1) with (⊙ (□ φ1)) by trivial.
apply open_box_L; exchl 0. apply open_box_L; exchl 1; exchl 0.
apply open_box_L. exchl 1; exchl 0. simpl.
apply IHh with Hp1. lia. ms.
* backwardl. apply IHh with Hp2. lia. ms.
- apply BoxR. repeat box_tac. backwardl.
replace (φ1) with (⊙ (□ φ1)) by trivial.
apply open_box_L; exchl 0. apply open_box_L; exchl 1; exchl 0.
apply open_box_L. exchl 1; exchl 0. simpl.
apply IHh with Hp. lia. ms.
Qed.
Definition pair_env_equiv (p q : env * env):= (fst p ≡ fst q) /\ (snd p ≡ snd q).
Global Instance Proper_pair_env :
Proper ((≡) ==> (≡) ==> pair_env_equiv) pair.
Proof. intros x y Hxy z t Hzt. unfold pair_env_equiv; tauto. Qed.
(* Crucial lemma : simultaneous proof of left-right contraction
and left-implication. *)
Lemma ImpL_dup_contr (s : env * env):
(∀ Γ Δ φ ψ, s = (Γ • (φ → ψ), Δ) ->
Γ ⊢ Δ • φ -> Γ • ψ ⊢ Δ -> Γ • (φ → ψ) ⊢ Δ) * (* ImpL *)
(∀ Γ Δ φ1 φ2 φ3, s = (Γ• φ1 • (φ2 → φ3) • (φ2 → φ3), Δ) ->
Γ • ((φ1 → φ2) → φ3) ⊢ Δ ->
Γ • φ1 • (φ2 → φ3) •(φ2 → φ3) ⊢ Δ) * (* ImpLImp_dup *)
(∀ Γ Δ ψ, s = (Γ, Δ • ψ) ->
Γ ⊢ Δ • ψ • ψ -> Γ ⊢ Δ • ψ) * (* contractionr *)
(∀ Γ Δ ψ, s = (Γ • ψ, Δ) ->
Γ • ψ • ψ ⊢ Δ -> Γ • ψ ⊢ Δ). (* contractionl *)
Proof.
(* By well-founded induction on the conclusion sequent using the sequent ordering. *)
induction s using (well_founded_induction wf_env_pair_ms_order).
Local Ltac ImpLtac H :=
unshelve eapply ((H (_ , _) _).1.1.1); simpl; try reflexivity; trivial;
[repeat order_tac | ..].
Local Ltac ImpLImp_duptac H :=
unshelve eapply ((H (_ , _) _).1.1.2); simpl; try reflexivity; trivial;
[repeat order_tac | ..];
try (rewrite Permutation_swap; order_tac).
Local Ltac contrrtac H:=
unshelve (eapply ((H (_ , _) _).1.2); simpl; try reflexivity; trivial);
[ repeat order_tac | ..];
try (rewrite Permutation_swap; order_tac).
Local Ltac contrltac H :=
unshelve eapply ((H (_ , _) _).2); simpl; try reflexivity; trivial;
[repeat order_tac | ..];
try (rewrite Permutation_swap; order_tac).
Local Ltac intac x := apply env_equiv_eq, env_add_inv, env_add_inv' in x; auto;
try setoid_rewrite x; try apply in_difference; ms.
(* Do not split right away to be able to reuse the current ImpL in the
ImpLImp case *)
assert(HImpL : ∀ (Γ Δ : env) (φ ψ : form),
s = (Γ • (φ → ψ), Δ) → (Γ ⊢KM Δ • φ) → (Γ • ψ ⊢KM Δ) → Γ • (φ → ψ) ⊢KM Δ).
(* ImpL *) {
destruct s as [Γ Δ].
intros Γ0 Δ' φ0 ψ0 Hs Hp Hp'. inversion Hs. subst Γ Δ. clear Hs.
dependent destruction Hp generalizing Γ0 Δ' Hp H.
- case (decide (# p = φ0)); intro; subst.
+ apply ImpLVar. peapply Hp'.
+ assert (# p ∈ Δ').
{ assert (# p ∈ (Δ' • φ0)) by (rewrite <- x ; ms).
apply env_in_add in H0 ; destruct H0 ; [ contradiction | auto]. }
exhibit H0 0. exchl 0. apply Atom.
- auto with proof.
- case (decide ((φ ∧ ψ) = φ0)); intro; subst.
+ apply ImpLAnd. replace Δ' with Δ in * by ms. do 2 ImpLtac H.
+ assert ((φ ∧ ψ) ∈ Δ').
{ assert ((φ ∧ ψ) ∈ (Δ' • φ0)) by (rewrite <- x ; ms).
apply env_in_add in H0 ; destruct H0 ; [ contradiction | auto]. }
assert (HeqΔ' := x).
apply env_equiv_eq, env_add_inv in x; [|assumption].
apply symmetry, env_equiv_eq, env_add_inv in HeqΔ'; [|auto].
exhibit H0 0. apply AndR.
* ImpLtac H. repeat rewrite env_replace by ms.
repeat rewrite env_add_remove. repeat order_tac.
-- rpeapply Hp1.
-- assert (H1 : Γ • ψ0 ⊢KM Δ' ∖ {[φ ∧ ψ]} • φ ∧ ψ) by rpeapply Hp'.
apply AndR_rev in H1 ; destruct H1 ; auto.
* ImpLtac H.
-- rpeapply Hp2.
-- assert (Γ • ψ0 ⊢KM Δ' ∖ {[φ ∧ ψ]} • φ ∧ ψ) by rpeapply Hp'.
apply AndR_rev in H1 ; destruct H1 ; auto.
- exchl 0; apply AndL; exchl 1; exchl 0. ImpLtac H.
exchl 0; exchl 1. apply AndL_rev ; exchl 0 ; auto.
- case (decide ((φ ∨ ψ) = φ0)) ; intro Heq ; subst.
+ assert (Heq : Δ ≡ Δ') by ms. clear x.
apply ImpLOr. ImpLtac H.
* ImpLtac H.
-- rpeapply Hp.
-- auto with proof.
* exchl 0. apply weakeningl, Hp'.
+ assert ((φ ∨ ψ) ∈ Δ').
{ assert ((φ ∨ ψ) ∈ (Δ' • φ0)) by (rewrite <- x ; ms).
apply env_in_add in H0 ; destruct H0 ; [ contradiction | auto]. }
exhibit H0 0. apply OrR. ImpLtac H.
* apply symmetry, env_equiv_eq, env_add_inv in x; [|auto].
rpeapply Hp.
* apply OrR_rev. backwardr. rpeapply Hp'.
- exchl 0. apply OrL.
+ exchl 0. ImpLtac H. exchl 0. apply (OrL_rev _ φ ψ). peapply Hp'.
+ exchl 0. ImpLtac H. exchl 0. apply (OrL_rev _ φ ψ). peapply Hp'.
- case (decide ((φ → ψ) = φ0)) ; intro Heq ; subst.
+ apply ImpLImp.
* exchl 0. apply weakeningl. lazy_apply Hp1. ms.
* exchl 0. apply weakeningl. peapply Hp2.
* peapply Hp'.
+ assert(HeqΔ := x).
apply env_equiv_eq, env_add_inv in x; trivial.
assert (Hin'' : (φ → ψ) ∈ Δ') by ms.
exhibit Hin'' 0. apply ImpR.
* exchl 0. ImpLtac H.
-- rpeapply Hp1.
-- exchl 0. apply ImpR_revl. backwardr. rewrite env_add_remove. peapply Hp'.
* box_tac. exchl 0. apply weakeningl, Hp2.
- exchl 0; exchl 1. apply ImpLVar. exchl 1; exchl 0.
ImpLtac H. exchl 0. exchl 1; apply ImpLVar_rev. peapply Hp'.
- exchl 0. apply ImpLAnd. exchl 0. ImpLtac H.
exchl 0. apply ImpLAnd_rev. peapply Hp'.
- exchl 0. apply ImpLOr. exchl 1. exchl 0. ImpLtac H.
exchl 0. exchl 1. apply ImpLOr_rev. exchl 0. peapply Hp'.
- exchl 0. apply ImpLImp; exchl 0.
+ exchl 1. exchl 0. exchl 1. ImpLtac H.
* rpeapply Hp1.
* exchl 1; exchl 0. contrltac H.
exchl 2. ImpLImp_duptac H. (* technical : order proved manually *)
repeat rewrite (Permutation_swap ψ0). order_tac.
exchl 0. apply weakeningr, Hp'.
+ repeat box_tac. exchl 1; exchl 0. apply weakeningl. exchl 0. exact Hp2.
+ ImpLtac H. exchl 0. eapply ImpLImp_prev with φ1 φ2. peapply Hp'.
- exchl 0. apply ImpLBox; box_tac.
+ exchl 1; exchl 0. apply weakeningl, Hp1.
+ exchl 0. ImpLtac H. exchl 0. apply ImpLBox_prev with φ1. exchl 0. peapply Hp'.
- case (decide ((□ φ) = φ0)).
+ intro. subst. apply ImpLBox.
* apply weakeningl, Hp.
* peapply Hp'.
+ intro Hneq.
apply env_equiv_eq, env_add_inv in x; trivial. rwr x.
apply BoxR. box_tac. exchl 0. apply weakeningl, Hp.
}
repeat split. { exact HImpL. }
(* ImpLImp_dup *)
{
destruct s as [Γ' Δ'].
intros Γ Δ φ1 φ2 φ3 Hs Hp.
inversion Hs. subst Γ' Δ'. clear Hs.
remember (Γ•((φ1 → φ2) → φ3)) as Γ0 eqn:Heq0.
assert(HeqΓ : Γ ≡ Γ0 ∖ {[((φ1 → φ2) → φ3)]}) by ms.
rwl HeqΓ.
assert(Hin : ((φ1 → φ2) → φ3) ∈ Γ0) by (subst Γ0; ms).
dependent destruction Hp.
- forwardl. auto with proof.
- forwardl. auto with proof.
- rwl (symmetry HeqΓ). apply AndR; ImpLImp_duptac H; now rewrite <- Heq0.
- forwardl. apply AndL. exchl 0.
do 2 (exchl 1; exchl 2; exchl 3; try exchl 0).
assert((φ ∧ ψ) ∈ Γ) by (rewrite HeqΓ, env_replace; ms).
replace (Γ0 ∖ {[(φ1 → φ2) → φ3]}) with (Γ ∖ {[φ ∧ ψ]}) by ms.
ImpLImp_duptac H.
rwl HeqΓ. exchl 0; exchl 1. lazy_apply Hp.
rewrite (env_replace (φ ∧ ψ) Hin0), env_add_remove.
rewrite difference_singleton. ms. ms.
- apply OrR. ImpLImp_duptac H. peapply Hp.
- forwardl.
assert((φ ∨ ψ) ∈ Γ) by (rewrite HeqΓ, env_replace; ms).
replace (Γ0 ∖ {[(φ1 → φ2) → φ3]}) with (Γ ∖ {[φ ∨ ψ]}) by ms.
apply OrL; backwardl.
+ ImpLImp_duptac H. backwardl. peapply Hp1.
+ ImpLImp_duptac H. backwardl. peapply Hp2.
- subst Γ0. rewrite env_add_remove. apply ImpR.
+ exchl 0; exchl 1; exchl 2. ImpLImp_duptac H. exchl 0. peapply Hp1.
+ repeat box_tac. exchl 0; exchl 1; exchl 2. exchl 1; exchl 0. apply open_box_L.
exchl 0; exchl 1. ImpLImp_duptac H. exchl 0. peapply Hp2.
- do 2 forwardl. exchl 0. apply ImpLVar. exchl 0.
assert((# p) ∈ Γ) by (rewrite HeqΓ; repeat rewrite env_replace; ms).
assert(((# p) → φ) ∈ Γ) by (rewrite HeqΓ; repeat rewrite env_replace; ms).
backwardl.
replace ((Γ0 • (# p)) ∖ {[(φ1 → φ2) → φ3]}) with (Γ ∖ {[(# p) → φ]}) by ms.
backwardl.
ImpLImp_duptac H. backwardl. peapply Hp.
- forwardl. apply ImpLAnd.
assert(((φ0 ∧ φ4) → φ5) ∈ Γ) by (rewrite HeqΓ, env_replace; ms).
replace (Γ0 ∖ {[(φ1 → φ2) → φ3]}) with (Γ ∖ {[(φ0 ∧ φ4) → φ5]}) by ms.
backwardl. ImpLImp_duptac H. backwardl. peapply Hp.
- forwardl. apply ImpLOr. exchl 0.
assert(((φ0 ∨ φ4) → φ5) ∈ Γ) by (rewrite HeqΓ, env_replace; ms).
replace (Γ0 ∖ {[(φ1 → φ2) → φ3]}) with (Γ ∖ {[(φ0 ∨ φ4) → φ5]}) by ms.
do 2 backwardl. ImpLImp_duptac H. backwardl. peapply Hp.
- case (decide (((φ0 → φ4) → φ5) = ((φ1 → φ2) → φ3))); intro Heq.
+ dependent destruction Heq; subst. rewrite env_add_remove.
replace Γ0 with Γ in * by ms. apply HImpL; trivial.
(* use the ImpL case we just proved *)
* exchl 0. exact Hp1.
* do 2 (exchl 0; apply weakeningl). peapply Hp3.
+ forwardl.
assert(((φ0 → φ4) → φ5) ∈ Γ) by (rewrite HeqΓ, env_replace; ms).
replace (Γ0 ∖ {[(φ1 → φ2) → φ3]}) with (Γ ∖ {[(φ0 → φ4) → φ5]}) by ms.
apply ImpLImp.
* exchl 0; do 2 backwardl.
ImpLImp_duptac H. backwardl. peapply Hp1.
* repeat box_tac. exchl 0; exchl 1; exchl 2; exchl 3.
exchl 2; exchl 1; exchl 0. apply open_box_L.
exchl 1; exchl 0; exchl 2; exchl 1.
assert(Ho := open_boxes_remove Γ ((φ0 → φ4) → φ5) H0).
replace ((⊗ Γ) ∖ ({[(φ0 → φ4) → φ5]})) with (⊗ (Γ ∖ ({[(φ0 → φ4) → φ5]})))
by ms.
ImpLImp_duptac H.
replace ((⊗ (Γ ∖ ({[(φ0 → φ4) → φ5]})))) with (⊗ (Γ0 ∖ ({[(φ1 → φ2) → φ3]})))
by(f_equal; ms).
box_tac. backwardl. rewrite env_add_remove. peapply Hp2.
* backwardl. ImpLImp_duptac H. backwardl. peapply Hp3.
- forwardl.
assert((□ φ0 → φ4) ∈ Γ) by (rewrite HeqΓ, env_replace; ms).
replace (Γ0 ∖ {[(φ1 → φ2) → φ3]}) with (Γ ∖ {[□ φ0 → φ4]}) by ms.
apply ImpLBox; repeat box_tac.
+ exchl 0.
assert(Ho := open_boxes_remove Γ ((□ φ0) → φ4) H0).
replace ((⊗ Γ) ∖ ({[(□ φ0) → φ4]})) with (⊗ (Γ ∖ ({[(□ φ0) → φ4]})))
by ms.
exchl 3; exchl 2; exchl 1; exchl 0. apply open_box_L; exchl 0; exchl 1.
exchl 2; exchl 1; exchl 0. exchl 3; exchl 2; exchl 1. exchl 3; exchl 2.
ImpLImp_duptac H.
replace ((⊗ (Γ ∖ ({[(□ φ0) → φ4]})))) with (⊗ (Γ0 ∖ ({[(φ1 → φ2) → φ3]})))
by(f_equal; ms).
box_tac. backwardl. rewrite env_add_remove. peapply Hp1.
+ backwardl. ImpLImp_duptac H. backwardl. peapply Hp2.
- apply BoxR. repeat box_tac. backwardl.
exchl 1; exchl 0; apply open_box_L; exchl 0; exchl 1.
ImpLImp_duptac H. backwardl. peapply Hp.
}
(* contractionr *)
{
destruct s as [Γ' Δ']. intros Γ Δ ψ Hs Hp.
inversion Hs. subst Γ' Δ'. clear HImpL Hs.
dependent destruction Hp generalizing Δ H.
- case(decide (ψ = Var p)); intro; subst.
+ apply Atom.
+ apply env_equiv_eq, env_add_inv in x; [|auto]. rwr x. apply Atom.
- auto with proof.
- case (decide (ψ = (φ ∧ ψ0))); intro Heq ; subst.
+ apply AndR.
* contrrtac H. apply (AndR_rev φ ψ0). rpeapply Hp1.
* contrrtac H. apply (AndR_rev φ ψ0). rpeapply Hp2.
+ assert(HeqΔ := x).
assert(Hin' : (φ ∧ ψ0) ∈ ((Δ • ψ) • ψ)) by (rewrite <- HeqΔ; ms).
apply env_equiv_eq, env_add_inv in x; [|auto]. rwr x.
assert(Heqψ : ((Δ0 ∖ ({[ψ]})) ≡ ((Δ ∖ {[φ ∧ ψ0]}) • ψ)))
by (apply env_add_inv in x; ms).
assert((φ ∧ ψ0) ∈ Δ) by ms.
apply AndR.
* rwr Heqψ. exchr 0. contrrtac H. exchr 1. rwr (symmetry Heqψ). rpeapply Hp1.
* rwr Heqψ. exchr 0. contrrtac H. exchr 1. rwr (symmetry Heqψ). rpeapply Hp2.
- apply AndL. contrrtac H.
- case (decide (ψ = (φ ∨ ψ0))); intro Heq ; subst.
+ apply OrR. contrrtac H. exchr 1; exchr 0. contrrtac H. exchr 1. exchr 0.
apply OrR_rev. rpeapply Hp.
+ assert(Hin : (φ ∨ ψ0) ∈ Δ) by intac x.
exhibit Hin 1.
exchr 0. apply OrR. exchr 1; exchr 0. contrrtac H. do 2 backwardr.
rwr (symmetry x). rewrite env_add_remove. exact Hp.
- apply OrL; contrrtac H.
- case (decide (ψ = (φ → ψ0))); intro Heq ; subst.
(* Here we need to do the contraction on the left at the same time *)
+ apply ImpR ; auto. contrltac H. contrrtac H.
apply ImpR_revl. rpeapply Hp1.
+ assert(Hin : (φ → ψ0) ∈ Δ) by intac x.
exhibit Hin 1. exchr 0. apply ImpR; auto.
exchr 0. contrrtac H. do 2 backwardr. rewrite <- x, env_add_remove. exact Hp1.
- apply ImpLVar. contrrtac H.
- apply ImpLAnd. contrrtac H.
- apply ImpLOr. contrrtac H.
- apply ImpLImp.
+ exchr 0. contrrtac H; [|rpeapply Hp1].
repeat setoid_rewrite (Permutation_swap ψ). order_tac.
+ assumption.
+ contrrtac H.
- apply ImpLBox; trivial. contrrtac H.
- case (decide (ψ = □ φ)).
+ intro Heq; subst; apply BoxR, Hp.
+ intro Hneq. assert(Hin : (□ φ) ∈ Δ) by intac x.
exhibit Hin 1. exchr 0. now apply BoxR.
}
{
(* contractionl *)
destruct s as [Γ' Δ']. intros Γ Δ ψ Hs Hp.
inversion Hs. subst Γ' Δ'. clear HImpL Hs.
dependent destruction Hp generalizing Γ H.
- case (decide(#p = ψ)); intro Heq; subst.
+ apply Atom.
+ assert(Hin : (#p) ∈ Γ) by intac x. exhibit Hin 1. exchl 0. apply Atom.
- case (decide(⊥ = ψ)); intro Heq; subst.
+ apply ExFalso.
+ assert(Hin : ⊥ ∈ Γ) by intac x. exhibit Hin 1. exchl 0. apply ExFalso.
- apply AndR; contrltac H.
- case (decide((φ ∧ ψ0) = ψ)); intro Heq; subst.
+ apply AndL. contrltac H. exchl 1; exchl 0. contrltac H. exchl 1.
exchl 0. apply AndL_rev. peapply Hp.
+ assert(Hin : (φ ∧ ψ0) ∈ Γ) by intac x.
exhibit Hin 1. exchl 0. apply AndL. exchl 1; exchl 0.
contrltac H. do 2 backwardl. peapply Hp.
- apply OrR. contrltac H.
- case (decide((φ ∨ ψ0) = ψ)); intro Heq; subst.
+ apply OrL.
* contrltac H. apply OrL_rev with (ψ := ψ0). peapply Hp1.
* contrltac H. apply OrL_rev with (φ := φ). peapply Hp2.
+ assert(Hin : (φ ∨ ψ0) ∈ Γ) by intac x.
exhibit Hin 1. exchl 0. apply OrL.
* exchl 0. contrltac H. do 2 backwardl. peapply Hp1.
* exchl 0. contrltac H. do 2 backwardl. peapply Hp2.
- apply ImpR.
+ exchl 0. contrltac H. peapply Hp1.
+ box_tac. exchl 0. assert(Hψ := weight_open_box ψ).
contrltac H. exchl 1; exchl 0. peapply Hp2.
- case (decide (ψ = (p → φ))); intro Heq.
+ subst. assert(Hin : (#p) ∈ Γ). {
apply env_equiv_eq, symmetry, env_add_inv', env_add_inv' in x; auto.
rewrite x, env_add_remove. apply in_difference; auto; ms. }
exhibit Hin 1. apply ImpLVar. contrltac H.
exchl 1. apply ImpLVar_rev. backwardl. peapply Hp.
+ case (decide (ψ = #p)).
* intro; subst. assert(Hin : ((# p) → φ) ∈ Γ) by intac x.
exhibit Hin 1. exchl 0. apply ImpLVar. exchl 0. contrltac H.
do 2 backwardl. peapply Hp.
* intro. assert(Hin : ((# p) → φ) ∈ Γ) by intac x.
assert(Hin' : (# p) ∈ (Γ ∖ ({[(# p) → φ]}))). {
apply env_equiv_eq, env_add_inv, env_add_inv' in x; auto; try setoid_rewrite x.
apply in_difference, in_difference, env_in_add, or_intror, in_difference; ms.
}
lazy_apply(ImpLVar (Γ ∖ {[(# p) → φ]} ∖ {[# p]} • ψ) Δ p φ).
-- exchl 1. exchl 0. contrltac H.
rwl difference_singleton. do 2 backwardl. peapply Hp.
-- do 2 rewrite (env_add_comm _ ψ).
now do 2 (rewrite difference_singleton by ms).
- case (decide (ψ = (φ1 ∧ φ2 → φ3))); intro Heq.
+ subst. apply ImpLAnd. contrltac H. apply ImpLAnd_rev. exchl 0. peapply Hp.
+ assert(Hin : ((φ1 ∧ φ2) → φ3) ∈ Γ) by intac x.
exhibit Hin 1. exchl 0. apply ImpLAnd. backwardl.
contrltac H. do 2 backwardl. peapply Hp.
- case (decide (ψ = (φ1 ∨ φ2 → φ3))); intro Heq.
+ subst. apply ImpLOr. contrltac H. exchl 1; exchl 0. contrltac H.
exchl 1. exchl 0. apply ImpLOr_rev. exchl 0; exchl 1; exchl 0. peapply Hp.
+ assert(Hin : ((φ1 ∨ φ2) → φ3) ∈ Γ) by intac x.
exhibit Hin 1. exchl 0. apply ImpLOr. exchl 1; exchl 0. contrltac H.
do 2 backwardl. peapply Hp.
- case (decide (ψ = ((φ1 → φ2) → φ3))); intro Heq.
+ subst. apply ImpLImp.
* contrltac H. exchl 1; exchl 0. contrltac H. contrltac H.
exchl 2. ImpLImp_duptac H. (* mutual induction hypothesis *)
(* This seems to be where the high constant in the order comes from *)
peapply Hp1.
* contrltac H. exchl 1; exchl 0. do 2 contrltac H. exchl 2. ImpLImp_duptac H.
exchl 0; exchl 1; exchl 0.
assert(Heq0 : Γ0 ≡ (Γ• ((φ1 → φ2) → φ3))) by ms.
replace ((⊗ Γ) • ((φ1 → φ2) → φ3)) with (⊗(Γ • ((φ1 → φ2) → φ3))) by ms.
lazy_apply Hp2. rewrite Heq0. ms.
* contrltac H. apply (ImpLImp_prev _ φ1 φ2 φ3). exchl 0. peapply Hp3.
+ assert(Hin : ((φ1 → φ2) → φ3) ∈ Γ) by intac x.
exhibit Hin 1. exchl 0. apply ImpLImp.
* exchl 1; exchl 0. contrltac H. do 2 backwardl. peapply Hp1.
* box_tac. exchl 1; exchl 0.
assert(Hw := weight_open_box ψ). contrltac H.
box_tac. do 2 backwardl. apply env_equiv_eq, env_add_inv' in x; auto.
lazy_apply Hp2. rewrite x. ms.
* backwardl. contrltac H. do 2 backwardl. peapply Hp3.
- case (decide (ψ = (□ φ1 → φ2))); intro Heq.
+ subst. apply ImpLBox.
* exchl 0. do 2 contrltac H. exchl 2; exchl 1; exchl 0. contrltac H.
exchl 1; exchl 2. apply ImpLBox_dup. exchl 0; exchl 1.
assert(Hin : ((□ φ1) → φ2) ∈ Γ0). {
apply env_equiv_eq, env_add_inv' in x.
rewrite x, env_add_remove. ms. }
lazy_apply Hp1.
apply env_equiv_eq, env_add_inv' in x; auto; try setoid_rewrite x. ms.
* contrltac H. apply (ImpLBox_prev _ φ1 φ2). exchl 0. peapply Hp2.
+ assert(Hin : ((□ φ1) → φ2) ∈ Γ) by intac x.
exhibit Hin 1. exchl 0. apply ImpLBox.
* box_tac. exchl 1; exchl 0.
assert(Hψ := weight_open_box ψ).
contrltac H. box_tac. do 2 backwardl.
apply (f_equal open_boxes), env_equiv_eq in x.
repeat rewrite open_boxes_add in x.
peapply Hp1.
* exchl 0. contrltac H. do 2 backwardl. peapply Hp2.
- apply BoxR. box_tac. exchl 0. assert(Hψ := weight_open_box ψ). contrltac H.
exchl 1; exchl 0. peapply Hp.
}
Qed.
| Atom Γ Δ p => 1
| ExFalso Γ Δ => 1
| AndR Γ Δ φ ψ H1 H2 => 1 + height H1 + height H2
| AndL Γ φ ψ θ H => 1 + height H
| OrR Γ Δ φ ψ H => 1 + height H
| OrL Γ Δ φ ψ H1 H2 => 1 + height H1 + height H2
| ImpR Γ Δ φ ψ H1 H2 => 1 + height H1 + height H2
| ImpLVar Γ Δ p φ H => 1 + height H
| ImpLAnd Γ Δ φ1 φ2 φ3 H => 1 + height H
| ImpLOr Γ Δ φ1 φ2 φ3 H => 1 + height H
| ImpLImp Γ Δ φ1 φ2 φ3 H1 H2 H3 => 1 + max(height H1) (max (height H2) (height H3))
| ImpLBox Γ Δ φ1 φ2 H1 H2 => 1 + height H1 + height H2
| BoxR Γ Δ φ H => 1 + height H
end.
Lemma height_0 {Γ Δ} (Hp : Γ ⊢ Δ) : height Hp <> 0.
Proof. destruct Hp; simpl; lia. Qed.
Lemma ImpLBox_dup Γ φ1 φ2 θ:
Γ•(□ φ1 → φ2) ⊢ θ ->
Γ • □ φ1 • □ φ1 • φ2 ⊢ θ.
Proof.
intro Hp.
remember (Γ• (□ φ1 → φ2)) as Γ0 eqn:Heq0.
assert(HeqΓ : Γ ≡ Γ0 ∖ {[(□ φ1 → φ2)]}) by ms.
rwl HeqΓ.
assert(Hin : (□ φ1 → φ2) ∈ Γ0) by (subst Γ0; ms).
clear Γ HeqΓ Heq0.
(* by induction on the height of the derivation *)
remember (height Hp) as h.
assert(Hleh : height Hp ≤ h) by lia. clear Heqh.
revert Γ0 θ Hp Hleh Hin. induction h as [|h]; intros Γ θ Hp Hleh Hin;
[pose (height_0 Hp); lia|].
dependent destruction Hp; simpl in Hleh.
- forwardl. auto with proof.
- forwardl. auto with proof.
- apply AndR.
+ apply IHh with Hp1. lia. ms.
+ apply IHh with Hp2. lia. ms.
- forwardl. apply AndL. exchl 0. do 2 backwardl. apply IHh with Hp. lia. ms.
- apply OrR. apply IHh with Hp. lia. ms.
- forwardl. apply OrL; backwardl.
+ apply IHh with Hp1. lia. ms.
+ apply IHh with Hp2. lia. ms.
- apply ImpR.
+ backwardl. apply IHh with Hp1; [lia|ms].
+ repeat box_tac. backwardl. apply open_box_L.
change φ1 with (⊙ (□ φ1)) at 2 3. exchl 0. apply open_box_L.
exchl 1; exchl 0. apply open_box_L. exchl 1; exchl 0.
apply IHh with Hp2; [lia|ms].
- do 2 forwardl. exchl 0. apply ImpLVar. exchl 0. do 2 backwardl.
apply IHh with Hp. lia. ms.
- forwardl. apply ImpLAnd. backwardl. apply IHh with Hp. lia. ms.
- forwardl. apply ImpLOr. exchl 0. do 2 backwardl. apply IHh with Hp. lia. ms.
- forwardl. apply ImpLImp.
+ exchl 0; do 2 backwardl. apply IHh with Hp1. lia. ms.
+ repeat rewrite open_boxes_add.
do 3 (exchl 2; exchl 1; exchl 0; apply open_box_L; exchl 3).
box_tac. do 2 (exchl 2; exchl 1; exchl 0; backwardl).
apply IHh with Hp2. lia. ms.
+ backwardl. apply IHh with Hp3. lia. ms.
- case (decide ((□ φ0 → φ3) = □ φ1 → φ2)); intro Heq.
+ dependent destruction Heq; subst.
exchl 0. apply weakeningl. exchl 0. apply weakeningl. peapply Hp2.
+ forwardl. apply ImpLBox; repeat box_tac.
* exchl 0. do 2 backwardl.
replace (φ1) with (⊙ (□ φ1)) by trivial.
apply open_box_L; exchl 0. apply open_box_L; exchl 1; exchl 0.
apply open_box_L. exchl 1; exchl 0. simpl.
apply IHh with Hp1. lia. ms.
* backwardl. apply IHh with Hp2. lia. ms.
- apply BoxR. repeat box_tac. backwardl.
replace (φ1) with (⊙ (□ φ1)) by trivial.
apply open_box_L; exchl 0. apply open_box_L; exchl 1; exchl 0.
apply open_box_L. exchl 1; exchl 0. simpl.
apply IHh with Hp. lia. ms.
Qed.
Definition pair_env_equiv (p q : env * env):= (fst p ≡ fst q) /\ (snd p ≡ snd q).
Global Instance Proper_pair_env :
Proper ((≡) ==> (≡) ==> pair_env_equiv) pair.
Proof. intros x y Hxy z t Hzt. unfold pair_env_equiv; tauto. Qed.
(* Crucial lemma : simultaneous proof of left-right contraction
and left-implication. *)
Lemma ImpL_dup_contr (s : env * env):
(∀ Γ Δ φ ψ, s = (Γ • (φ → ψ), Δ) ->
Γ ⊢ Δ • φ -> Γ • ψ ⊢ Δ -> Γ • (φ → ψ) ⊢ Δ) * (* ImpL *)
(∀ Γ Δ φ1 φ2 φ3, s = (Γ• φ1 • (φ2 → φ3) • (φ2 → φ3), Δ) ->
Γ • ((φ1 → φ2) → φ3) ⊢ Δ ->
Γ • φ1 • (φ2 → φ3) •(φ2 → φ3) ⊢ Δ) * (* ImpLImp_dup *)
(∀ Γ Δ ψ, s = (Γ, Δ • ψ) ->
Γ ⊢ Δ • ψ • ψ -> Γ ⊢ Δ • ψ) * (* contractionr *)
(∀ Γ Δ ψ, s = (Γ • ψ, Δ) ->
Γ • ψ • ψ ⊢ Δ -> Γ • ψ ⊢ Δ). (* contractionl *)
Proof.
(* By well-founded induction on the conclusion sequent using the sequent ordering. *)
induction s using (well_founded_induction wf_env_pair_ms_order).
Local Ltac ImpLtac H :=
unshelve eapply ((H (_ , _) _).1.1.1); simpl; try reflexivity; trivial;
[repeat order_tac | ..].
Local Ltac ImpLImp_duptac H :=
unshelve eapply ((H (_ , _) _).1.1.2); simpl; try reflexivity; trivial;
[repeat order_tac | ..];
try (rewrite Permutation_swap; order_tac).
Local Ltac contrrtac H:=
unshelve (eapply ((H (_ , _) _).1.2); simpl; try reflexivity; trivial);
[ repeat order_tac | ..];
try (rewrite Permutation_swap; order_tac).
Local Ltac contrltac H :=
unshelve eapply ((H (_ , _) _).2); simpl; try reflexivity; trivial;
[repeat order_tac | ..];
try (rewrite Permutation_swap; order_tac).
Local Ltac intac x := apply env_equiv_eq, env_add_inv, env_add_inv' in x; auto;
try setoid_rewrite x; try apply in_difference; ms.
(* Do not split right away to be able to reuse the current ImpL in the
ImpLImp case *)
assert(HImpL : ∀ (Γ Δ : env) (φ ψ : form),
s = (Γ • (φ → ψ), Δ) → (Γ ⊢KM Δ • φ) → (Γ • ψ ⊢KM Δ) → Γ • (φ → ψ) ⊢KM Δ).
(* ImpL *) {
destruct s as [Γ Δ].
intros Γ0 Δ' φ0 ψ0 Hs Hp Hp'. inversion Hs. subst Γ Δ. clear Hs.
dependent destruction Hp generalizing Γ0 Δ' Hp H.
- case (decide (# p = φ0)); intro; subst.
+ apply ImpLVar. peapply Hp'.
+ assert (# p ∈ Δ').
{ assert (# p ∈ (Δ' • φ0)) by (rewrite <- x ; ms).
apply env_in_add in H0 ; destruct H0 ; [ contradiction | auto]. }
exhibit H0 0. exchl 0. apply Atom.
- auto with proof.
- case (decide ((φ ∧ ψ) = φ0)); intro; subst.
+ apply ImpLAnd. replace Δ' with Δ in * by ms. do 2 ImpLtac H.
+ assert ((φ ∧ ψ) ∈ Δ').
{ assert ((φ ∧ ψ) ∈ (Δ' • φ0)) by (rewrite <- x ; ms).
apply env_in_add in H0 ; destruct H0 ; [ contradiction | auto]. }
assert (HeqΔ' := x).
apply env_equiv_eq, env_add_inv in x; [|assumption].
apply symmetry, env_equiv_eq, env_add_inv in HeqΔ'; [|auto].
exhibit H0 0. apply AndR.
* ImpLtac H. repeat rewrite env_replace by ms.
repeat rewrite env_add_remove. repeat order_tac.
-- rpeapply Hp1.
-- assert (H1 : Γ • ψ0 ⊢KM Δ' ∖ {[φ ∧ ψ]} • φ ∧ ψ) by rpeapply Hp'.
apply AndR_rev in H1 ; destruct H1 ; auto.
* ImpLtac H.
-- rpeapply Hp2.
-- assert (Γ • ψ0 ⊢KM Δ' ∖ {[φ ∧ ψ]} • φ ∧ ψ) by rpeapply Hp'.
apply AndR_rev in H1 ; destruct H1 ; auto.
- exchl 0; apply AndL; exchl 1; exchl 0. ImpLtac H.
exchl 0; exchl 1. apply AndL_rev ; exchl 0 ; auto.
- case (decide ((φ ∨ ψ) = φ0)) ; intro Heq ; subst.
+ assert (Heq : Δ ≡ Δ') by ms. clear x.
apply ImpLOr. ImpLtac H.
* ImpLtac H.
-- rpeapply Hp.
-- auto with proof.
* exchl 0. apply weakeningl, Hp'.
+ assert ((φ ∨ ψ) ∈ Δ').
{ assert ((φ ∨ ψ) ∈ (Δ' • φ0)) by (rewrite <- x ; ms).
apply env_in_add in H0 ; destruct H0 ; [ contradiction | auto]. }
exhibit H0 0. apply OrR. ImpLtac H.
* apply symmetry, env_equiv_eq, env_add_inv in x; [|auto].
rpeapply Hp.
* apply OrR_rev. backwardr. rpeapply Hp'.
- exchl 0. apply OrL.
+ exchl 0. ImpLtac H. exchl 0. apply (OrL_rev _ φ ψ). peapply Hp'.
+ exchl 0. ImpLtac H. exchl 0. apply (OrL_rev _ φ ψ). peapply Hp'.
- case (decide ((φ → ψ) = φ0)) ; intro Heq ; subst.
+ apply ImpLImp.
* exchl 0. apply weakeningl. lazy_apply Hp1. ms.
* exchl 0. apply weakeningl. peapply Hp2.
* peapply Hp'.
+ assert(HeqΔ := x).
apply env_equiv_eq, env_add_inv in x; trivial.
assert (Hin'' : (φ → ψ) ∈ Δ') by ms.
exhibit Hin'' 0. apply ImpR.
* exchl 0. ImpLtac H.
-- rpeapply Hp1.
-- exchl 0. apply ImpR_revl. backwardr. rewrite env_add_remove. peapply Hp'.
* box_tac. exchl 0. apply weakeningl, Hp2.
- exchl 0; exchl 1. apply ImpLVar. exchl 1; exchl 0.
ImpLtac H. exchl 0. exchl 1; apply ImpLVar_rev. peapply Hp'.
- exchl 0. apply ImpLAnd. exchl 0. ImpLtac H.
exchl 0. apply ImpLAnd_rev. peapply Hp'.
- exchl 0. apply ImpLOr. exchl 1. exchl 0. ImpLtac H.
exchl 0. exchl 1. apply ImpLOr_rev. exchl 0. peapply Hp'.
- exchl 0. apply ImpLImp; exchl 0.
+ exchl 1. exchl 0. exchl 1. ImpLtac H.
* rpeapply Hp1.
* exchl 1; exchl 0. contrltac H.
exchl 2. ImpLImp_duptac H. (* technical : order proved manually *)
repeat rewrite (Permutation_swap ψ0). order_tac.
exchl 0. apply weakeningr, Hp'.
+ repeat box_tac. exchl 1; exchl 0. apply weakeningl. exchl 0. exact Hp2.
+ ImpLtac H. exchl 0. eapply ImpLImp_prev with φ1 φ2. peapply Hp'.
- exchl 0. apply ImpLBox; box_tac.
+ exchl 1; exchl 0. apply weakeningl, Hp1.
+ exchl 0. ImpLtac H. exchl 0. apply ImpLBox_prev with φ1. exchl 0. peapply Hp'.
- case (decide ((□ φ) = φ0)).
+ intro. subst. apply ImpLBox.
* apply weakeningl, Hp.
* peapply Hp'.
+ intro Hneq.
apply env_equiv_eq, env_add_inv in x; trivial. rwr x.
apply BoxR. box_tac. exchl 0. apply weakeningl, Hp.
}
repeat split. { exact HImpL. }
(* ImpLImp_dup *)
{
destruct s as [Γ' Δ'].
intros Γ Δ φ1 φ2 φ3 Hs Hp.
inversion Hs. subst Γ' Δ'. clear Hs.
remember (Γ•((φ1 → φ2) → φ3)) as Γ0 eqn:Heq0.
assert(HeqΓ : Γ ≡ Γ0 ∖ {[((φ1 → φ2) → φ3)]}) by ms.
rwl HeqΓ.
assert(Hin : ((φ1 → φ2) → φ3) ∈ Γ0) by (subst Γ0; ms).
dependent destruction Hp.
- forwardl. auto with proof.
- forwardl. auto with proof.
- rwl (symmetry HeqΓ). apply AndR; ImpLImp_duptac H; now rewrite <- Heq0.
- forwardl. apply AndL. exchl 0.
do 2 (exchl 1; exchl 2; exchl 3; try exchl 0).
assert((φ ∧ ψ) ∈ Γ) by (rewrite HeqΓ, env_replace; ms).
replace (Γ0 ∖ {[(φ1 → φ2) → φ3]}) with (Γ ∖ {[φ ∧ ψ]}) by ms.
ImpLImp_duptac H.
rwl HeqΓ. exchl 0; exchl 1. lazy_apply Hp.
rewrite (env_replace (φ ∧ ψ) Hin0), env_add_remove.
rewrite difference_singleton. ms. ms.
- apply OrR. ImpLImp_duptac H. peapply Hp.
- forwardl.
assert((φ ∨ ψ) ∈ Γ) by (rewrite HeqΓ, env_replace; ms).
replace (Γ0 ∖ {[(φ1 → φ2) → φ3]}) with (Γ ∖ {[φ ∨ ψ]}) by ms.
apply OrL; backwardl.
+ ImpLImp_duptac H. backwardl. peapply Hp1.
+ ImpLImp_duptac H. backwardl. peapply Hp2.
- subst Γ0. rewrite env_add_remove. apply ImpR.
+ exchl 0; exchl 1; exchl 2. ImpLImp_duptac H. exchl 0. peapply Hp1.
+ repeat box_tac. exchl 0; exchl 1; exchl 2. exchl 1; exchl 0. apply open_box_L.
exchl 0; exchl 1. ImpLImp_duptac H. exchl 0. peapply Hp2.
- do 2 forwardl. exchl 0. apply ImpLVar. exchl 0.
assert((# p) ∈ Γ) by (rewrite HeqΓ; repeat rewrite env_replace; ms).
assert(((# p) → φ) ∈ Γ) by (rewrite HeqΓ; repeat rewrite env_replace; ms).
backwardl.
replace ((Γ0 • (# p)) ∖ {[(φ1 → φ2) → φ3]}) with (Γ ∖ {[(# p) → φ]}) by ms.
backwardl.
ImpLImp_duptac H. backwardl. peapply Hp.
- forwardl. apply ImpLAnd.
assert(((φ0 ∧ φ4) → φ5) ∈ Γ) by (rewrite HeqΓ, env_replace; ms).
replace (Γ0 ∖ {[(φ1 → φ2) → φ3]}) with (Γ ∖ {[(φ0 ∧ φ4) → φ5]}) by ms.
backwardl. ImpLImp_duptac H. backwardl. peapply Hp.
- forwardl. apply ImpLOr. exchl 0.
assert(((φ0 ∨ φ4) → φ5) ∈ Γ) by (rewrite HeqΓ, env_replace; ms).
replace (Γ0 ∖ {[(φ1 → φ2) → φ3]}) with (Γ ∖ {[(φ0 ∨ φ4) → φ5]}) by ms.
do 2 backwardl. ImpLImp_duptac H. backwardl. peapply Hp.
- case (decide (((φ0 → φ4) → φ5) = ((φ1 → φ2) → φ3))); intro Heq.
+ dependent destruction Heq; subst. rewrite env_add_remove.
replace Γ0 with Γ in * by ms. apply HImpL; trivial.
(* use the ImpL case we just proved *)
* exchl 0. exact Hp1.
* do 2 (exchl 0; apply weakeningl). peapply Hp3.
+ forwardl.
assert(((φ0 → φ4) → φ5) ∈ Γ) by (rewrite HeqΓ, env_replace; ms).
replace (Γ0 ∖ {[(φ1 → φ2) → φ3]}) with (Γ ∖ {[(φ0 → φ4) → φ5]}) by ms.
apply ImpLImp.
* exchl 0; do 2 backwardl.
ImpLImp_duptac H. backwardl. peapply Hp1.
* repeat box_tac. exchl 0; exchl 1; exchl 2; exchl 3.
exchl 2; exchl 1; exchl 0. apply open_box_L.
exchl 1; exchl 0; exchl 2; exchl 1.
assert(Ho := open_boxes_remove Γ ((φ0 → φ4) → φ5) H0).
replace ((⊗ Γ) ∖ ({[(φ0 → φ4) → φ5]})) with (⊗ (Γ ∖ ({[(φ0 → φ4) → φ5]})))
by ms.
ImpLImp_duptac H.
replace ((⊗ (Γ ∖ ({[(φ0 → φ4) → φ5]})))) with (⊗ (Γ0 ∖ ({[(φ1 → φ2) → φ3]})))
by(f_equal; ms).
box_tac. backwardl. rewrite env_add_remove. peapply Hp2.
* backwardl. ImpLImp_duptac H. backwardl. peapply Hp3.
- forwardl.
assert((□ φ0 → φ4) ∈ Γ) by (rewrite HeqΓ, env_replace; ms).
replace (Γ0 ∖ {[(φ1 → φ2) → φ3]}) with (Γ ∖ {[□ φ0 → φ4]}) by ms.
apply ImpLBox; repeat box_tac.
+ exchl 0.
assert(Ho := open_boxes_remove Γ ((□ φ0) → φ4) H0).
replace ((⊗ Γ) ∖ ({[(□ φ0) → φ4]})) with (⊗ (Γ ∖ ({[(□ φ0) → φ4]})))
by ms.
exchl 3; exchl 2; exchl 1; exchl 0. apply open_box_L; exchl 0; exchl 1.
exchl 2; exchl 1; exchl 0. exchl 3; exchl 2; exchl 1. exchl 3; exchl 2.
ImpLImp_duptac H.
replace ((⊗ (Γ ∖ ({[(□ φ0) → φ4]})))) with (⊗ (Γ0 ∖ ({[(φ1 → φ2) → φ3]})))
by(f_equal; ms).
box_tac. backwardl. rewrite env_add_remove. peapply Hp1.
+ backwardl. ImpLImp_duptac H. backwardl. peapply Hp2.
- apply BoxR. repeat box_tac. backwardl.
exchl 1; exchl 0; apply open_box_L; exchl 0; exchl 1.
ImpLImp_duptac H. backwardl. peapply Hp.
}
(* contractionr *)
{
destruct s as [Γ' Δ']. intros Γ Δ ψ Hs Hp.
inversion Hs. subst Γ' Δ'. clear HImpL Hs.
dependent destruction Hp generalizing Δ H.
- case(decide (ψ = Var p)); intro; subst.
+ apply Atom.
+ apply env_equiv_eq, env_add_inv in x; [|auto]. rwr x. apply Atom.
- auto with proof.
- case (decide (ψ = (φ ∧ ψ0))); intro Heq ; subst.
+ apply AndR.
* contrrtac H. apply (AndR_rev φ ψ0). rpeapply Hp1.
* contrrtac H. apply (AndR_rev φ ψ0). rpeapply Hp2.
+ assert(HeqΔ := x).
assert(Hin' : (φ ∧ ψ0) ∈ ((Δ • ψ) • ψ)) by (rewrite <- HeqΔ; ms).
apply env_equiv_eq, env_add_inv in x; [|auto]. rwr x.
assert(Heqψ : ((Δ0 ∖ ({[ψ]})) ≡ ((Δ ∖ {[φ ∧ ψ0]}) • ψ)))
by (apply env_add_inv in x; ms).
assert((φ ∧ ψ0) ∈ Δ) by ms.
apply AndR.
* rwr Heqψ. exchr 0. contrrtac H. exchr 1. rwr (symmetry Heqψ). rpeapply Hp1.
* rwr Heqψ. exchr 0. contrrtac H. exchr 1. rwr (symmetry Heqψ). rpeapply Hp2.
- apply AndL. contrrtac H.
- case (decide (ψ = (φ ∨ ψ0))); intro Heq ; subst.
+ apply OrR. contrrtac H. exchr 1; exchr 0. contrrtac H. exchr 1. exchr 0.
apply OrR_rev. rpeapply Hp.
+ assert(Hin : (φ ∨ ψ0) ∈ Δ) by intac x.
exhibit Hin 1.
exchr 0. apply OrR. exchr 1; exchr 0. contrrtac H. do 2 backwardr.
rwr (symmetry x). rewrite env_add_remove. exact Hp.
- apply OrL; contrrtac H.
- case (decide (ψ = (φ → ψ0))); intro Heq ; subst.
(* Here we need to do the contraction on the left at the same time *)
+ apply ImpR ; auto. contrltac H. contrrtac H.
apply ImpR_revl. rpeapply Hp1.
+ assert(Hin : (φ → ψ0) ∈ Δ) by intac x.
exhibit Hin 1. exchr 0. apply ImpR; auto.
exchr 0. contrrtac H. do 2 backwardr. rewrite <- x, env_add_remove. exact Hp1.
- apply ImpLVar. contrrtac H.
- apply ImpLAnd. contrrtac H.
- apply ImpLOr. contrrtac H.
- apply ImpLImp.
+ exchr 0. contrrtac H; [|rpeapply Hp1].
repeat setoid_rewrite (Permutation_swap ψ). order_tac.
+ assumption.
+ contrrtac H.
- apply ImpLBox; trivial. contrrtac H.
- case (decide (ψ = □ φ)).
+ intro Heq; subst; apply BoxR, Hp.
+ intro Hneq. assert(Hin : (□ φ) ∈ Δ) by intac x.
exhibit Hin 1. exchr 0. now apply BoxR.
}
{
(* contractionl *)
destruct s as [Γ' Δ']. intros Γ Δ ψ Hs Hp.
inversion Hs. subst Γ' Δ'. clear HImpL Hs.
dependent destruction Hp generalizing Γ H.
- case (decide(#p = ψ)); intro Heq; subst.
+ apply Atom.
+ assert(Hin : (#p) ∈ Γ) by intac x. exhibit Hin 1. exchl 0. apply Atom.
- case (decide(⊥ = ψ)); intro Heq; subst.
+ apply ExFalso.
+ assert(Hin : ⊥ ∈ Γ) by intac x. exhibit Hin 1. exchl 0. apply ExFalso.
- apply AndR; contrltac H.
- case (decide((φ ∧ ψ0) = ψ)); intro Heq; subst.
+ apply AndL. contrltac H. exchl 1; exchl 0. contrltac H. exchl 1.
exchl 0. apply AndL_rev. peapply Hp.
+ assert(Hin : (φ ∧ ψ0) ∈ Γ) by intac x.
exhibit Hin 1. exchl 0. apply AndL. exchl 1; exchl 0.
contrltac H. do 2 backwardl. peapply Hp.
- apply OrR. contrltac H.
- case (decide((φ ∨ ψ0) = ψ)); intro Heq; subst.
+ apply OrL.
* contrltac H. apply OrL_rev with (ψ := ψ0). peapply Hp1.
* contrltac H. apply OrL_rev with (φ := φ). peapply Hp2.
+ assert(Hin : (φ ∨ ψ0) ∈ Γ) by intac x.
exhibit Hin 1. exchl 0. apply OrL.
* exchl 0. contrltac H. do 2 backwardl. peapply Hp1.
* exchl 0. contrltac H. do 2 backwardl. peapply Hp2.
- apply ImpR.
+ exchl 0. contrltac H. peapply Hp1.
+ box_tac. exchl 0. assert(Hψ := weight_open_box ψ).
contrltac H. exchl 1; exchl 0. peapply Hp2.
- case (decide (ψ = (p → φ))); intro Heq.
+ subst. assert(Hin : (#p) ∈ Γ). {
apply env_equiv_eq, symmetry, env_add_inv', env_add_inv' in x; auto.
rewrite x, env_add_remove. apply in_difference; auto; ms. }
exhibit Hin 1. apply ImpLVar. contrltac H.
exchl 1. apply ImpLVar_rev. backwardl. peapply Hp.
+ case (decide (ψ = #p)).
* intro; subst. assert(Hin : ((# p) → φ) ∈ Γ) by intac x.
exhibit Hin 1. exchl 0. apply ImpLVar. exchl 0. contrltac H.
do 2 backwardl. peapply Hp.
* intro. assert(Hin : ((# p) → φ) ∈ Γ) by intac x.
assert(Hin' : (# p) ∈ (Γ ∖ ({[(# p) → φ]}))). {
apply env_equiv_eq, env_add_inv, env_add_inv' in x; auto; try setoid_rewrite x.
apply in_difference, in_difference, env_in_add, or_intror, in_difference; ms.
}
lazy_apply(ImpLVar (Γ ∖ {[(# p) → φ]} ∖ {[# p]} • ψ) Δ p φ).
-- exchl 1. exchl 0. contrltac H.
rwl difference_singleton. do 2 backwardl. peapply Hp.
-- do 2 rewrite (env_add_comm _ ψ).
now do 2 (rewrite difference_singleton by ms).
- case (decide (ψ = (φ1 ∧ φ2 → φ3))); intro Heq.
+ subst. apply ImpLAnd. contrltac H. apply ImpLAnd_rev. exchl 0. peapply Hp.
+ assert(Hin : ((φ1 ∧ φ2) → φ3) ∈ Γ) by intac x.
exhibit Hin 1. exchl 0. apply ImpLAnd. backwardl.
contrltac H. do 2 backwardl. peapply Hp.
- case (decide (ψ = (φ1 ∨ φ2 → φ3))); intro Heq.
+ subst. apply ImpLOr. contrltac H. exchl 1; exchl 0. contrltac H.
exchl 1. exchl 0. apply ImpLOr_rev. exchl 0; exchl 1; exchl 0. peapply Hp.
+ assert(Hin : ((φ1 ∨ φ2) → φ3) ∈ Γ) by intac x.
exhibit Hin 1. exchl 0. apply ImpLOr. exchl 1; exchl 0. contrltac H.
do 2 backwardl. peapply Hp.
- case (decide (ψ = ((φ1 → φ2) → φ3))); intro Heq.
+ subst. apply ImpLImp.
* contrltac H. exchl 1; exchl 0. contrltac H. contrltac H.
exchl 2. ImpLImp_duptac H. (* mutual induction hypothesis *)
(* This seems to be where the high constant in the order comes from *)
peapply Hp1.
* contrltac H. exchl 1; exchl 0. do 2 contrltac H. exchl 2. ImpLImp_duptac H.
exchl 0; exchl 1; exchl 0.
assert(Heq0 : Γ0 ≡ (Γ• ((φ1 → φ2) → φ3))) by ms.
replace ((⊗ Γ) • ((φ1 → φ2) → φ3)) with (⊗(Γ • ((φ1 → φ2) → φ3))) by ms.
lazy_apply Hp2. rewrite Heq0. ms.
* contrltac H. apply (ImpLImp_prev _ φ1 φ2 φ3). exchl 0. peapply Hp3.
+ assert(Hin : ((φ1 → φ2) → φ3) ∈ Γ) by intac x.
exhibit Hin 1. exchl 0. apply ImpLImp.
* exchl 1; exchl 0. contrltac H. do 2 backwardl. peapply Hp1.
* box_tac. exchl 1; exchl 0.
assert(Hw := weight_open_box ψ). contrltac H.
box_tac. do 2 backwardl. apply env_equiv_eq, env_add_inv' in x; auto.
lazy_apply Hp2. rewrite x. ms.
* backwardl. contrltac H. do 2 backwardl. peapply Hp3.
- case (decide (ψ = (□ φ1 → φ2))); intro Heq.
+ subst. apply ImpLBox.
* exchl 0. do 2 contrltac H. exchl 2; exchl 1; exchl 0. contrltac H.
exchl 1; exchl 2. apply ImpLBox_dup. exchl 0; exchl 1.
assert(Hin : ((□ φ1) → φ2) ∈ Γ0). {
apply env_equiv_eq, env_add_inv' in x.
rewrite x, env_add_remove. ms. }
lazy_apply Hp1.
apply env_equiv_eq, env_add_inv' in x; auto; try setoid_rewrite x. ms.
* contrltac H. apply (ImpLBox_prev _ φ1 φ2). exchl 0. peapply Hp2.
+ assert(Hin : ((□ φ1) → φ2) ∈ Γ) by intac x.
exhibit Hin 1. exchl 0. apply ImpLBox.
* box_tac. exchl 1; exchl 0.
assert(Hψ := weight_open_box ψ).
contrltac H. box_tac. do 2 backwardl.
apply (f_equal open_boxes), env_equiv_eq in x.
repeat rewrite open_boxes_add in x.
peapply Hp1.
* exchl 0. contrltac H. do 2 backwardl. peapply Hp2.
- apply BoxR. box_tac. exchl 0. assert(Hψ := weight_open_box ψ). contrltac H.
exchl 1; exchl 0. peapply Hp.
}
Qed.
Proposition ImpL Γ φ ψ Δ: Γ ⊢ Δ • φ -> Γ • ψ ⊢ Δ -> Γ • (φ → ψ) ⊢ Δ.
Proof. intros. now apply ((ImpL_dup_contr (Γ • (φ → ψ), Δ)).1.1.1). Qed.
Lemma MP (φ ψ : form) (Γ Δ : env) :
Γ • (φ → ψ) • φ ⊢ Δ • ψ.
Proof.
exchl 0 ; apply ImpL ; auto with proof.
Qed.
Lemma contractionl Γ ψ Δ : Γ • ψ • ψ ⊢ Δ -> Γ • ψ ⊢ Δ.
Proof. intros. now apply ((ImpL_dup_contr (Γ • ψ, Δ)).2). Qed.
Global Hint Resolve contractionl : proof.
Lemma contractionr Γ ψ Δ : Γ ⊢ Δ • ψ • ψ -> Γ ⊢ Δ • ψ.
Proof. intros. now apply ((ImpL_dup_contr (Γ, Δ • ψ)).1.2). Qed.
Global Hint Resolve contractionr : proof.
(* Another partial inversion lemma for ImpLImp.
This is actually stronger, as the right-hand-side does not contain φ2. *)
(* This is crucial to prove Cut. *)
Lemma ImpLImp_prev' Γ Δ φ1 φ2 φ3 :
Γ • ((φ1 → φ2) → φ3) ⊢ Δ ->
Γ • φ1 • (φ2 → φ3) ⊢ Δ.
Proof.
intro Hp. apply contractionl.
eapply ((ImpL_dup_contr _).1.1.2); eauto.
Qed.
Theorem generalised_contractionl (Γ Γ' : env) Δ:
Γ' ⊎ Γ' ⊎ Γ ⊢ Δ -> Γ' ⊎ Γ ⊢ Δ.
Proof.
revert Γ.
induction Γ' as [| x Γ' IHΓ'] using gmultiset_rec; intros Γ Hp.
- peapply Hp.
- peapply (contractionl (Γ' ⊎ Γ) x). peapply (IHΓ' (Γ•x•x)). peapply Hp.
Qed.
Theorem generalised_contractionr (Γ : env) Δ Δ':
Γ ⊢ Δ ⊎ Δ ⊎ Δ' -> Γ ⊢ Δ ⊎ Δ'.
Proof.
revert Δ'.
induction Δ as [| x Δ IHΔ] using gmultiset_rec; intros Δ' Hp.
- setoid_rewrite gmultiset_disj_union_right_id in Hp. exact Hp.
- lazy_apply (contractionr Γ x (Δ ⊎ Δ')); [|ms].
lazy_apply(IHΔ (Δ' • x • x)); [|ms].
lazy_apply Hp. ms.
Qed.
(* Adapted from Lemma 5.3 (Dyckhoff Negri 2000): an implication on the left may
be weakened. *)
Lemma imp_cut φ Γ ψ θ: Γ•(φ → ψ) ⊢ θ -> Γ•ψ ⊢ θ.
Proof.
intro Hp.
remember (Γ•(φ → ψ)) as Γ0 eqn:HH.
assert (Heq: Γ ≡ Γ0 ∖ {[(φ → ψ)]}) by ms.
assert(Hin : (φ → ψ) ∈ Γ0) by ms. clear HH.
rwl Heq. clear Heq Γ.
remember (weight φ) as w.
assert(Hle : weight φ ≤ w) by lia.
clear Heqw. revert Γ0 φ ψ θ Hle Hin Hp.
induction w; intros Γ φ ψ θ Hle Hin Hp;
[destruct φ; simpl in Hle; lia|].
induction Hp.
- forwardl. auto with proof.
- forwardl. auto with proof.
-apply AndR; intuition.
- forwardl; apply AndL. exchl 0. do 2 backwardl. apply IHHp; trivial. ms.
- apply OrR; intuition.
- forwardl. apply OrL; backwardl; [apply IHHp1 | apply IHHp2]; ms.
- apply ImpR.
+ backwardl. apply IHHp1; trivial. ms.
+ repeat box_tac. backwardl. apply open_box_L, IHHp2. ms.
- case (decide ((p → φ0) = (φ → ψ))); intro Heq0.
+ dependent destruction Heq0; subst. peapply Hp.
+ do 2 forwardl. exchl 0. apply ImpLVar. exchl 0. do 2 backwardl. apply IHHp; ms.
- case (decide ((φ1 ∧ φ2 → φ3) = (φ → ψ))); intro Heq0.
+ dependent destruction Heq0; subst.
assert(Heq1 : ((Γ•(φ1 ∧ φ2 → ψ)) ∖ {[φ1 ∧ φ2 → ψ]}) ≡ Γ) by ms;
rwl Heq1; clear Heq1. simpl in Hle.
peapply (IHw (Γ•(φ2 → ψ)) φ2 ψ Δ); [lia|ms|].
peapply (IHw (Γ•(φ1 → φ2 → ψ)) φ1 (φ2 → ψ) Δ); [lia|ms|trivial].
+ forwardl. apply ImpLAnd. backwardl. apply IHHp; trivial. ms.
- case (decide ((φ1 ∨ φ2 → φ3) = (φ → ψ))); intro Heq0.
+ dependent destruction Heq0.
apply contractionl. simpl in Hle.
peapply (IHw (Γ•ψ•(φ1 → ψ)) φ1 ψ); [lia|ms|].
exchl 0.
peapply (IHw (Γ•(φ1 → ψ)•(φ2 → ψ)) φ2 ψ); trivial; [lia|ms].
+ forwardl. apply ImpLOr; exchl 0; do 2 backwardl; apply IHHp; ms.
- case (decide (((φ1 → φ2) → φ3) = (φ → ψ))); intro Heq0.
+ dependent destruction Heq0. rewrite env_add_remove. exact Hp3.
+ forwardl. apply ImpLImp.
* exchl 0; do 2 backwardl; apply IHHp1. ms.
* repeat box_tac. exchl 0; do 2 backwardl; apply open_box_L, IHHp2. ms.
* backwardl. apply IHHp3. ms.
- case (decide((□φ1 → φ2) = (φ → ψ))).
+ intro Heq. dependent destruction Heq. peapply Hp2.
+ intro Hneq. forwardl. apply ImpLBox; repeat box_tac.
* exchl 0. do 2 backwardl. apply open_box_L. apply IHHp1; trivial. ms.
* backwardl. apply IHHp2; trivial. ms.
- apply BoxR. repeat box_tac. backwardl. apply open_box_L, IHHp; trivial.
apply env_in_add. right. auto with proof.
Qed.
Global Hint Resolve imp_cut : proof.
Lemma open_boxes_case Δ : {φ | (□ φ) ∈ Δ} + {Δ ≡ ⊗Δ}.
Proof.
unfold open_boxes.
induction Δ as [|ψ Δ IH] using gmultiset_rec.
- right. ms.
- case_eq(is_box ψ); intro Hbox.
+ left. exists (⊙ψ).
dependent destruction ψ; try discriminate Hbox. ms.
+ destruct IH as [[φ Hφ]| Heq].
* left. exists φ. ms.
* right. symmetry. etransitivity.
-- apply env_equiv_eq, list_to_set_disj_perm, Permutation_map.
apply gmultiset_elements_disj_union.
-- rewrite map_app, list_to_set_disj_app. rewrite <- Heq. apply env_equiv_eq.
f_equal.
unfold elements. apply is_not_box_open_box in Hbox. rewrite <- Hbox at 2.
transitivity (list_to_set_disj (map open_box (id [ψ])) : env).
++ apply list_to_set_disj_perm, Permutation_map.
apply Permutation_refl', gmultiset_elements_singleton.
++ simpl. ms.
Qed.
Lemma OrR_idemp Γ Δ ψ : Γ ⊢ Δ • (ψ ∨ ψ) -> Γ ⊢ Δ • ψ.
Proof. intro Hp. apply contractionr, OrR_rev, Hp. Qed.
Lemma strongness φ Γ Δ : Γ • φ ⊢ Δ • □ φ.
Proof. apply BoxR. box_tac. apply weakeningl, open_box_L, generalised_axiom. Qed.
Proof. intros. now apply ((ImpL_dup_contr (Γ • (φ → ψ), Δ)).1.1.1). Qed.
Lemma MP (φ ψ : form) (Γ Δ : env) :
Γ • (φ → ψ) • φ ⊢ Δ • ψ.
Proof.
exchl 0 ; apply ImpL ; auto with proof.
Qed.
Lemma contractionl Γ ψ Δ : Γ • ψ • ψ ⊢ Δ -> Γ • ψ ⊢ Δ.
Proof. intros. now apply ((ImpL_dup_contr (Γ • ψ, Δ)).2). Qed.
Global Hint Resolve contractionl : proof.
Lemma contractionr Γ ψ Δ : Γ ⊢ Δ • ψ • ψ -> Γ ⊢ Δ • ψ.
Proof. intros. now apply ((ImpL_dup_contr (Γ, Δ • ψ)).1.2). Qed.
Global Hint Resolve contractionr : proof.
(* Another partial inversion lemma for ImpLImp.
This is actually stronger, as the right-hand-side does not contain φ2. *)
(* This is crucial to prove Cut. *)
Lemma ImpLImp_prev' Γ Δ φ1 φ2 φ3 :
Γ • ((φ1 → φ2) → φ3) ⊢ Δ ->
Γ • φ1 • (φ2 → φ3) ⊢ Δ.
Proof.
intro Hp. apply contractionl.
eapply ((ImpL_dup_contr _).1.1.2); eauto.
Qed.
Theorem generalised_contractionl (Γ Γ' : env) Δ:
Γ' ⊎ Γ' ⊎ Γ ⊢ Δ -> Γ' ⊎ Γ ⊢ Δ.
Proof.
revert Γ.
induction Γ' as [| x Γ' IHΓ'] using gmultiset_rec; intros Γ Hp.
- peapply Hp.
- peapply (contractionl (Γ' ⊎ Γ) x). peapply (IHΓ' (Γ•x•x)). peapply Hp.
Qed.
Theorem generalised_contractionr (Γ : env) Δ Δ':
Γ ⊢ Δ ⊎ Δ ⊎ Δ' -> Γ ⊢ Δ ⊎ Δ'.
Proof.
revert Δ'.
induction Δ as [| x Δ IHΔ] using gmultiset_rec; intros Δ' Hp.
- setoid_rewrite gmultiset_disj_union_right_id in Hp. exact Hp.
- lazy_apply (contractionr Γ x (Δ ⊎ Δ')); [|ms].
lazy_apply(IHΔ (Δ' • x • x)); [|ms].
lazy_apply Hp. ms.
Qed.
(* Adapted from Lemma 5.3 (Dyckhoff Negri 2000): an implication on the left may
be weakened. *)
Lemma imp_cut φ Γ ψ θ: Γ•(φ → ψ) ⊢ θ -> Γ•ψ ⊢ θ.
Proof.
intro Hp.
remember (Γ•(φ → ψ)) as Γ0 eqn:HH.
assert (Heq: Γ ≡ Γ0 ∖ {[(φ → ψ)]}) by ms.
assert(Hin : (φ → ψ) ∈ Γ0) by ms. clear HH.
rwl Heq. clear Heq Γ.
remember (weight φ) as w.
assert(Hle : weight φ ≤ w) by lia.
clear Heqw. revert Γ0 φ ψ θ Hle Hin Hp.
induction w; intros Γ φ ψ θ Hle Hin Hp;
[destruct φ; simpl in Hle; lia|].
induction Hp.
- forwardl. auto with proof.
- forwardl. auto with proof.
-apply AndR; intuition.
- forwardl; apply AndL. exchl 0. do 2 backwardl. apply IHHp; trivial. ms.
- apply OrR; intuition.
- forwardl. apply OrL; backwardl; [apply IHHp1 | apply IHHp2]; ms.
- apply ImpR.
+ backwardl. apply IHHp1; trivial. ms.
+ repeat box_tac. backwardl. apply open_box_L, IHHp2. ms.
- case (decide ((p → φ0) = (φ → ψ))); intro Heq0.
+ dependent destruction Heq0; subst. peapply Hp.
+ do 2 forwardl. exchl 0. apply ImpLVar. exchl 0. do 2 backwardl. apply IHHp; ms.
- case (decide ((φ1 ∧ φ2 → φ3) = (φ → ψ))); intro Heq0.
+ dependent destruction Heq0; subst.
assert(Heq1 : ((Γ•(φ1 ∧ φ2 → ψ)) ∖ {[φ1 ∧ φ2 → ψ]}) ≡ Γ) by ms;
rwl Heq1; clear Heq1. simpl in Hle.
peapply (IHw (Γ•(φ2 → ψ)) φ2 ψ Δ); [lia|ms|].
peapply (IHw (Γ•(φ1 → φ2 → ψ)) φ1 (φ2 → ψ) Δ); [lia|ms|trivial].
+ forwardl. apply ImpLAnd. backwardl. apply IHHp; trivial. ms.
- case (decide ((φ1 ∨ φ2 → φ3) = (φ → ψ))); intro Heq0.
+ dependent destruction Heq0.
apply contractionl. simpl in Hle.
peapply (IHw (Γ•ψ•(φ1 → ψ)) φ1 ψ); [lia|ms|].
exchl 0.
peapply (IHw (Γ•(φ1 → ψ)•(φ2 → ψ)) φ2 ψ); trivial; [lia|ms].
+ forwardl. apply ImpLOr; exchl 0; do 2 backwardl; apply IHHp; ms.
- case (decide (((φ1 → φ2) → φ3) = (φ → ψ))); intro Heq0.
+ dependent destruction Heq0. rewrite env_add_remove. exact Hp3.
+ forwardl. apply ImpLImp.
* exchl 0; do 2 backwardl; apply IHHp1. ms.
* repeat box_tac. exchl 0; do 2 backwardl; apply open_box_L, IHHp2. ms.
* backwardl. apply IHHp3. ms.
- case (decide((□φ1 → φ2) = (φ → ψ))).
+ intro Heq. dependent destruction Heq. peapply Hp2.
+ intro Hneq. forwardl. apply ImpLBox; repeat box_tac.
* exchl 0. do 2 backwardl. apply open_box_L. apply IHHp1; trivial. ms.
* backwardl. apply IHHp2; trivial. ms.
- apply BoxR. repeat box_tac. backwardl. apply open_box_L, IHHp; trivial.
apply env_in_add. right. auto with proof.
Qed.
Global Hint Resolve imp_cut : proof.
Lemma open_boxes_case Δ : {φ | (□ φ) ∈ Δ} + {Δ ≡ ⊗Δ}.
Proof.
unfold open_boxes.
induction Δ as [|ψ Δ IH] using gmultiset_rec.
- right. ms.
- case_eq(is_box ψ); intro Hbox.
+ left. exists (⊙ψ).
dependent destruction ψ; try discriminate Hbox. ms.
+ destruct IH as [[φ Hφ]| Heq].
* left. exists φ. ms.
* right. symmetry. etransitivity.
-- apply env_equiv_eq, list_to_set_disj_perm, Permutation_map.
apply gmultiset_elements_disj_union.
-- rewrite map_app, list_to_set_disj_app. rewrite <- Heq. apply env_equiv_eq.
f_equal.
unfold elements. apply is_not_box_open_box in Hbox. rewrite <- Hbox at 2.
transitivity (list_to_set_disj (map open_box (id [ψ])) : env).
++ apply list_to_set_disj_perm, Permutation_map.
apply Permutation_refl', gmultiset_elements_singleton.
++ simpl. ms.
Qed.
Lemma OrR_idemp Γ Δ ψ : Γ ⊢ Δ • (ψ ∨ ψ) -> Γ ⊢ Δ • ψ.
Proof. intro Hp. apply contractionr, OrR_rev, Hp. Qed.
Lemma strongness φ Γ Δ : Γ • φ ⊢ Δ • □ φ.
Proof. apply BoxR. box_tac. apply weakeningl, open_box_L, generalised_axiom. Qed.
- var_not_tautology: A variable cannot be a tautology.
- bot_not_tautology: ∅ is not a tautology.
- bot_not_tautology: The empty conclusion is not a tautology.
- box_var_not_tautology: A boxed variable cannot be a tautology.
- box_bot_not_tautology: A boxed ⊥ cannot be a tautology.
Lemma env_add_non_empty (Γ : env) (φ : form) : ((Γ • φ) = ∅) -> False.
Proof.
intros H. assert(Hf : φ ∈ (∅ : env)) by (rewrite <- H; ms).
now apply gmultiset_elem_of_empty in Hf.
Qed.
Lemma bot_not_tautology : (∅ ⊢ ∅ • ⊥) -> False.
Proof.
intro Hf. dependent destruction Hf; simpl in *;
try match goal with x : _ ⊎ {[+?φ+]} = ?Δ |- _ =>
exfalso; eapply (gmultiset_elem_of_empty φ);
try (apply symmetry, env_equiv_eq, env_add_inv', symmetry in x);
setoid_rewrite <- x; try apply in_difference; ms end.
Qed.
Lemma empty_not_tautology : (∅ ⊢ ∅) -> False.
Proof.
intro Hf. dependent destruction Hf; simpl in *;
try match goal with x : _ ⊎ {[+?φ+]} = ?Δ |- _ =>
apply env_add_non_empty in x; exfalso; apply x end.
Qed.
Lemma var_not_tautology v: (∅ ⊢ ∅ • Var v) -> False.
Proof.
intro Hp.
remember ∅ as Γ.
dependent induction Hp;
try match goal with | Heq : (_ • ?f%stdpp) = _ |- _ => symmetry in Heq;
assert(Heq' := env_equiv_eq _ _ Heq);
apply (gmultiset_not_elem_of_empty f);
subst; try (apply env_add_inv' in Heq'); rewrite Heq';
try apply in_difference; ms
end.
Qed.
Lemma box_var_not_tautology v: (∅ ⊢ ∅ • □ (Var v)) -> False.
Proof.
intro Hp.
remember ∅ as Γ.
dependent destruction Hp.
1-12 : try match goal with | Heq : (_ • ?f%stdpp) = _ |- _ => symmetry in Heq;
assert(Heq' := env_equiv_eq _ _ Heq);
apply (gmultiset_not_elem_of_empty f);
subst; try (apply env_add_inv' in Heq'); rewrite Heq' end.
3, 5, 7 : (apply in_difference; ms).
1-9 : ms.
subst. apply env_equiv_eq, symmetry, singleton_eq_inv in x.
destruct x as [Heq Heq']. inversion Heq'. subst.
clear Heq' Δ Heq. rewrite open_boxes_empty in Hp.
dependent destruction Hp.
1-12 : try match goal with | Heq : (_ • ?f%stdpp) = _ |- _ => symmetry in Heq;
assert(Heq' := env_equiv_eq _ _ Heq);
apply (gmultiset_not_elem_of_empty f);
subst; try (apply env_add_inv' in Heq'); rewrite Heq' end.
2-12: (apply in_difference; ms).
- apply env_equiv_eq, symmetry, singleton_eq_inv in x0. intuition discriminate.
- apply env_equiv_eq, symmetry, singleton_eq_inv in x. intuition discriminate.
Qed.
Lemma box_bot_not_tautology: (∅ ⊢ ∅ • □⊥) -> False.
Proof.
intro Hp. dependent destruction Hp;
try match goal with | Heq : (_ • ?f%stdpp) = _ |- _ => symmetry in Heq;
pose(Heq' := env_equiv_eq _ _ Heq);
apply (gmultiset_not_elem_of_empty f); rewrite Heq'; ms
end.
all : (apply env_equiv_eq, symmetry, singleton_eq_inv in x;
destruct x as [Heq Heq']; try discriminate).
inversion Heq'. subst. clear Heq Heq'. rewrite open_boxes_empty in Hp.
dependent destruction Hp.
1-12 : try match goal with | Heq : (_ • ?f%stdpp) = _ |- _ => symmetry in Heq;
assert(Heq' := env_equiv_eq _ _ Heq);
apply (gmultiset_not_elem_of_empty f);
subst; try (apply env_add_inv' in Heq'); rewrite Heq' end.
2-12: (apply in_difference; ms).
- apply env_equiv_eq, symmetry, singleton_eq_inv in x0. intuition discriminate.
- apply env_equiv_eq, symmetry, singleton_eq_inv in x. intuition discriminate.
Qed.
(* A tautology is either equal to ⊤ or has a weight of at least 3. *)
Lemma weight_tautology φ : (∅ ⊢ ∅ • φ) -> 3 ≤ weight φ.
Proof.
intro Hp.
destruct φ.
- contradict Hp. apply var_not_tautology.
- contradict Hp. apply bot_not_tautology.
- simpl. pose(weight_pos φ1). pose(weight_pos φ2). lia.
- simpl. pose(weight_pos φ1). pose(weight_pos φ2). lia.
- simpl. pose(weight_pos φ1). pose(weight_pos φ2). lia.
- dependent destruction φ.
+ contradict Hp. apply box_var_not_tautology.
+ contradict Hp. apply box_bot_not_tautology.
+ simpl. pose(weight_pos φ1). pose(weight_pos φ2). lia.
+ simpl. pose(weight_pos φ1). pose(weight_pos φ2). lia.
+ simpl. pose(weight_pos φ1). pose(weight_pos φ2). lia.
+ simpl. pose(weight_pos φ). lia.
Qed.
Lemma top_Provable Γ Δ : Γ ⊢ Δ • ⊤.
Proof. apply ImpR; apply ExFalso. Qed.
Global Hint Resolve top_Provable : proof.