KM.Sequent.DecisionProcedure
This file implements a decision procedure for KM. There are two versions,
with the same proof. `Proof_tree_dec` computes a proof tree for the sequent,
while `Provable_dec` only decides the provability of the sequent.
Global Instance proper_rm : Proper ((=) ==> (≡ₚ) ==> (≡ₚ)) rm.
Proof.
intros x y Heq. subst y.
induction 1; simpl; trivial.
- case form_eq_dec; auto with *.
- case form_eq_dec; auto with * ;
case form_eq_dec; auto with *. intros. apply Permutation_swap.
- now rewrite IHPermutation1.
Qed.
Definition exists_dec {A : Type} (P : A -> bool) (l : list A):
{x & (In x l) /\ P x} + {forall x, In x l -> ¬ P x}.
Proof.
induction l as [|x l].
- right. tauto.
- case_eq (P x); intro Heq.
+ left. exists x. split; auto with *.
+ destruct IHl as [(y & Hin & Hy)|Hf].
* left. exists y. split; auto with *.
* right. simpl. intros z [Hz|Hz]; subst; try rewrite Heq; auto with *.
Defined.
The function Proof_tree_dec computes a proof tree of a sequent, if there
is one, or produces a proof that there is none. The proof is performed by
induction on the well-ordering or pointed environments and tries to apply
all the sequent rules to reduce the weight of the environment.
Local Definition is_var φ : bool := match φ with
| Var p => true | _ => false end.
Local Definition is_imp φ : bool := match φ with
| (_ → _) => true | _ => false end.
Local Definition is_conj φ : bool := match φ with
| (_ ∧ _) => true | _ => false end.
Local Definition is_disj φ : bool := match φ with
| (_ ∨ _) => true | _ => false end.
Local Definition is_box φ : bool := match φ with
| □ _ => true | _ => false end.
Notation "□⁻¹ Γ" := (map open_box Γ) (at level 75).
Proposition Proof_tree_dec Γ Δ :
{_ : list_to_set_disj Γ ⊢ list_to_set_disj Δ & True} +
{forall H : list_to_set_disj Γ ⊢ list_to_set_disj Δ, False}.
Proof.
(* duplicate *)
Ltac l_tac := repeat rewrite list_to_set_disj_open_boxes;
rewrite (proper_Provable _ _ (list_to_set_disj_env_add _ _) _ _ (env_refl _))
|| rewrite (proper_Provable _ _
(equiv_disj_union_compat_r (list_to_set_disj_env_add _ _)) _ _ (env_refl _))
|| rewrite (proper_Provable _ _
(equiv_disj_union_compat_r
(equiv_disj_union_compat_r (list_to_set_disj_env_add _ _))) _ _ (env_refl _))
|| rewrite (proper_Provable _ _
(equiv_disj_union_compat_r
(equiv_disj_union_compat_r
(equiv_disj_union_compat_r (list_to_set_disj_env_add _ _)))) _ _ (env_refl _)).
remember (Γ, Δ) as pe.
replace Γ with pe.1 by now inversion Heqpe.
replace Δ with pe.2 by now inversion Heqpe. clear Heqpe Γ Δ.
revert pe.
(* Induction on the well-ordering of pointed environments *)
refine (@well_founded_induction _ _ wf_pointed_order _ _).
(* Cleaning up the induction hypothesis *)
intros (Γ& Δ) Hind; simpl.
assert(Hind' := λ Γ' Δ', Hind(Γ', Δ')). simpl in Hind'. clear Hind. rename Hind' into Hind.
(* ExFalso *)
case (decide (⊥ ∈ Γ)); intro Hbot.
{ left. eexists; trivial. apply elem_of_list_to_set_disj in Hbot. exhibit Hbot 0. apply ExFalso. }
(* Atom *)
assert(Hvar : {p | (Var p ∈ Δ /\ Var p ∈ Γ)} + {∀ p, Var p ∈ Δ -> Var p ∈ Γ -> False}). {
pose (VΔ := filter is_var Δ). pose (VΓ := filter is_var Γ).
case_eq (list_find (fun x => is_var x /\ x ∈ VΓ) VΔ).
- intros [p φ] HSome. rewrite list_find_Some in HSome.
destruct HSome as (Heq & (Hvar & Hin) & _). apply elem_of_list_lookup_2 in Heq.
clear p. left. destruct φ as [p | | | | | ]. 2-6 : inversion Hvar.
exists p. subst VΔ VΓ. rewrite elem_of_list_filter in Heq, Hin. tauto.
- intro HN. right. intros p HpΔ HpΓ. apply list_find_None in HN.
rewrite Forall_forall in HN. subst VΔ VΓ. apply (HN (# p)).
+ rewrite <- elem_of_list_In, elem_of_list_filter. simpl. tauto.
+ rewrite elem_of_list_filter. simpl; tauto.
}
destruct Hvar as [[p [Hp' Hp]]|Hvar].
{ subst. left. eexists; trivial. apply elem_of_list_to_set_disj in Hp, Hp'.
exhibit Hp 0. exhibit Hp' 0. apply Atom. }
(* AndL *)
assert(HAndL : {ψ1 & {ψ2 & (And ψ1 ψ2) ∈ Γ}} + {∀ ψ1 ψ2, (And ψ1 ψ2) ∈ Γ -> False}). {
destruct (exists_dec is_conj Γ) as [(θ & Hin & Hθ) | Hf].
- left. destruct θ. 3: { eexists. eexists. apply elem_of_list_In. eauto. }
all: auto with *.
- right. intros ψ1 ψ2 Hψ. rewrite elem_of_list_In in Hψ. apply Hf in Hψ. simpl in Hψ. tauto.
}
destruct HAndL as [(ψ1 & ψ2 & Hin)|HAndL].
{ destruct (Hind (ψ2 :: ψ1 :: rm (And ψ1 ψ2) Γ) Δ) as [[Hp' _] | Hf].
- order_tac.
- left. eexists; trivial. apply elem_of_list_to_set_disj in Hin.
exhibit Hin 0. apply AndL. peapply Hp'.
- right. intro Hf'. apply Hf. peapply AndL_rev.
rwl list_to_set_disj_rm_rev. apply elem_of_list_to_set_disj in Hin.
rwl list_to_set_disj_rm. rwl difference_singleton. apply Hf'.
}
(* OrL *)
assert(HOrL : {ψ1 & {ψ2 & (Or ψ1 ψ2) ∈ Γ}} + {∀ ψ1 ψ2, (Or ψ1 ψ2) ∈ Γ -> False}). {
destruct (exists_dec is_disj Γ) as [(θ & Hin & Hθ) | Hf].
- left. destruct θ. 4: { eexists. eexists. apply elem_of_list_In. eauto. }
all: inversion Hθ.
- right. intros ψ1 ψ2 Hψ. rewrite elem_of_list_In in Hψ. apply Hf in Hψ. simpl in Hψ. tauto.
}
destruct HOrL as [(ψ1 & ψ2 & Hin)|HOrL].
{ apply elem_of_list_to_set_disj in Hin.
destruct (Hind (ψ1 :: rm (Or ψ1 ψ2) Γ) Δ) as [[Hp1 _] | Hf].
- order_tac.
- destruct (Hind (ψ2 :: rm (Or ψ1 ψ2) Γ) Δ) as [[Hp2 _] | Hf].
+ order_tac.
+ left. eexists; trivial. exhibit Hin 0. apply OrL.
* peapply Hp1.
* peapply Hp2.
+ right; intro Hf'.
apply Hf. rwl list_to_set_disj_env_add.
apply OrL_rev with (φ := ψ1). lazy_apply Hf'.
now rewrite list_to_set_disj_rm, difference_singleton.
- right; intro Hf'. apply Hf. rwl list_to_set_disj_env_add.
apply OrL_rev with (ψ := ψ2). lazy_apply Hf'.
now rewrite list_to_set_disj_rm, difference_singleton.
}
(* AndR *)
assert(HAndR : {φ1 & {φ2 & (And φ1 φ2) ∈ Δ}} + {∀ φ1 φ2, ¬ (And φ1 φ2) ∈ Δ}). {
destruct (exists_dec is_conj Δ) as [(θ & Hin & Hθ) | Hf].
- left. destruct θ. 3: { eexists. eexists. apply elem_of_list_In. eauto. }
all: auto with *.
- right. intros ψ1 ψ2 Hψ. rewrite elem_of_list_In in Hψ. apply Hf in Hψ. simpl in Hψ. tauto.
}
destruct HAndR as [(φ1 & φ2 & Hin) | HAndR].
{ subst.
destruct (Hind Γ (φ1 :: rm (φ1 ∧ φ2) Δ)) as [(Hp1&_) | H1].
- order_tac.
- destruct (Hind Γ (φ2 :: rm (φ1 ∧ φ2) Δ)) as [(Hp2&_) | H2].
+ order_tac.
+ left. eexists; trivial. apply elem_of_list_to_set_disj in Hin.
exhibit Hin 0. apply AndR.
* rpeapply Hp1.
* rpeapply Hp2.
+ right. intro Hp. apply H2. rwr list_to_set_disj_env_add.
apply AndR_rev with (φ1 := φ1). lazy_apply Hp.
apply elem_of_list_to_set_disj in Hin.
now rewrite list_to_set_disj_rm, difference_singleton.
- right. intro Hp. apply H1.
apply elem_of_list_to_set_disj in Hin. rwr list_to_set_disj_env_add.
apply AndR_rev with (φ2 := φ2). lazy_apply Hp.
now rewrite list_to_set_disj_rm, difference_singleton.
}
(* OrR is invertible in KM, but isn't in iSL *)
(* This case is symmetrical to AndL *)
assert(HOrR :
{φ1 & {φ2 & (φ1 ∨ φ2) ∈ Δ}} +
{∀ φ1 φ2, ¬ (φ1 ∨ φ2) ∈ Δ}).
{
destruct (exists_dec is_disj Δ) as [(θ & Hin & Hθ) | Hf].
- left. destruct θ. 4: { eexists. eexists. apply elem_of_list_In. exact Hin. }
all: auto with *.
- right. intros ψ1 ψ2 Hψ. rewrite elem_of_list_In in Hψ. apply Hf in Hψ. simpl in Hψ. tauto.
}
destruct HOrR as [(φ1 & φ2 & Hin)| HOrR].
{ destruct (Hind Γ (φ2 :: φ1 :: rm (Or φ1 φ2) Δ)) as [[Hp' _] | Hf].
- order_tac.
- left. eexists; trivial. apply elem_of_list_to_set_disj in Hin.
exhibit Hin 0. apply OrR. rpeapply Hp'.
- right. intro Hf'. apply Hf. rpeapply OrR_rev.
apply elem_of_list_to_set_disj in Hin.
rwr difference_singleton. exact Hf'.
}
(* ImpLVar *)
assert(HImpLVar : {p & {ψ & Var p ∈ Γ /\ (#p → ψ) ∈ Γ}} +
{∀ p ψ, Var p ∈ Γ -> (#p → ψ) ∈ Γ -> False}). {
pose (fIp :=λ p θ, match θ with | (#q → _) =>
if decide (p = q) then true else false | _ => false end).
pose (fp:= (fun θ => match θ with |Var p =>
if (exists_dec (fIp p) Γ) then true else false | _ => false end)).
destruct (exists_dec fp Γ) as [(θ & Hin & Hθ) | Hf].
- left. subst fp. destruct θ. 2-6: auto with *.
case exists_dec as [(ψ &Hinψ & Hψ)|] in Hθ; [|auto with *].
unfold fIp in Hψ. destruct ψ. 1-4, 6: auto with *.
destruct ψ1. 2-6: auto with *. case decide in Hψ; [|auto with *].
subst. apply elem_of_list_In in Hinψ, Hin.
do 2 eexists. split; eauto.
- right. intros p ψ Hp Hψ. rewrite elem_of_list_In in Hp, Hψ. apply Hf in Hp. subst fp fIp.
simpl in Hp. case exists_dec as [|Hf'] in Hp. auto with *.
apply (Hf' _ Hψ). rewrite decide_True; trivial. auto with *.
}
destruct HImpLVar as [[p [ψ [Hinp Hinψ]]]|HImpLVar].
{ apply elem_of_list_to_set_disj in Hinp.
apply elem_of_list_to_set_disj in Hinψ.
assert(Hinp' : Var p ∈ (list_to_set_disj Γ ∖ {[#p → ψ]} : env))
by (apply in_difference; [discriminate| assumption]).
destruct (Hind (ψ :: rm (#p → ψ) Γ) Δ) as [[Hp _]|Hf].
- order_tac.
- left. eexists; trivial. exhibit Hinψ 0.
exhibit Hinp' 1. apply ImpLVar.
rwl difference_singleton. peapply Hp.
- right. intro Hf'. apply Hf. rwl list_to_set_disj_env_add.
rwl list_to_set_disj_rm.
exhibit Hinp' 1. apply ImpLVar_rev.
do 2 rwl difference_singleton. exact Hf'.
}
(* ImpLAnd *)
assert(HImpLAnd : {φ1 & {φ2 & {φ3 & ((And φ1 φ2) → φ3) ∈ Γ}}} +
{∀ φ1 φ2 φ3, ((φ1 ∧ φ2) → φ3) ∈ Γ -> False}). {
pose (fII := (fun θ => match θ with |(And _ _) → _ => true | _ => false end)).
destruct (exists_dec fII Γ) as [(θ & Hin & Hθ) | Hf].
- left. subst fII. destruct θ. 1-4, 6: auto with *.
destruct θ1. 1-2,4-6: auto with *. do 3 eexists; apply elem_of_list_In; eauto.
- right. intros ψ1 ψ2 ψ3 Hψ. rewrite elem_of_list_In in Hψ. apply Hf in Hψ. subst fII. simpl in Hψ. tauto.
}
destruct HImpLAnd as [(φ1&φ2&φ3&Hin)|HImpLAnd].
{ apply elem_of_list_to_set_disj in Hin.
destruct (Hind ((φ1 → (φ2 → φ3)) :: rm ((φ1 ∧ φ2) → φ3) Γ) Δ) as [[Hp _]|Hf].
- order_tac.
- left. eexists; trivial. exhibit Hin 0. apply ImpLAnd.
peapply Hp.
- right. intro Hf'. apply Hf.
rwl list_to_set_disj_env_add. apply ImpLAnd_rev.
rwl list_to_set_disj_rm. rwl difference_singleton. exact Hf'.
}
(* ImpLOr *)
assert(HImpLOr : {φ1 & {φ2 & {φ3 & ((φ1 ∨ φ2) → φ3) ∈ Γ}}} +
{∀ φ1 φ2 φ3, ((φ1 ∨ φ2) → φ3) ∈ Γ -> False}). {
pose (fII := (fun θ => match θ with | (Or _ _) → _ => true | _ => false end)).
destruct (exists_dec fII Γ) as [(θ & Hin & Hθ) | Hf].
- left. subst fII. destruct θ. 1-4, 6: auto with *.
destruct θ1. 1-3, 5-6: auto with *. do 3 eexists; apply elem_of_list_In; eauto.
- right. intros ψ1 ψ2 ψ3 Hψ. rewrite elem_of_list_In in Hψ. apply Hf in Hψ. subst fII. simpl in Hψ. tauto.
}
destruct HImpLOr as [(φ1&φ2&φ3&Hin)|HImpLOr].
{ apply elem_of_list_to_set_disj in Hin.
destruct (Hind ((φ2 → φ3) :: (φ1 → φ3) :: rm ((φ1 ∨ φ2) → φ3) Γ) Δ) as [[Hp _]|Hf].
- order_tac.
- left. eexists; trivial. exhibit Hin 0. apply ImpLOr. peapply Hp.
- right. intro Hf'. apply Hf.
do 2 rwl list_to_set_disj_env_add. apply ImpLOr_rev.
rwl list_to_set_disj_rm. rwl difference_singleton. exact Hf'.
}
(* non invertible right rules *)
(* ImpR is non-invertible in KM, but is in iSL *)
assert(HImpR : ∀ Δ2 Δ1, Δ1 ++ Δ2 = Δ -> {φ1 & {φ2 &
{ Hp1 : (list_to_set_disj Γ • φ1 ⊢KM list_to_set_disj (rm (φ1 → φ2) Δ) • φ2) &
{ Hp2 : (⊗ (list_to_set_disj Γ) • φ1 ⊢KM ∅ • φ2) & (φ1 → φ2) ∈ Δ2 }}}} +
{∀ φ1 φ2, (list_to_set_disj Γ • φ1 ⊢KM list_to_set_disj (rm (φ1 → φ2) Δ) • φ2) ->
(⊗ (list_to_set_disj Γ) • φ1 ⊢KM ∅ • φ2) ->
¬ (φ1 → φ2) ∈ Δ2 }).
{
clear Hbot Hvar HAndL HOrL HAndR HOrR HImpLOr HImpLVar HImpLOr.
induction Δ2 as [|θ Δ2]; intros Δ1 Heq.
- right. intros φ1 φ2 Hp1 Hp2 Hin. inversion Hin.
- destruct (IHΔ2 (Δ1 ++ [θ])) as [(φ1 & φ2 & Hp1 & Hp2 & Hin) | Hf].
+ auto with *.
+ left. exists φ1; exists φ2. repeat split; trivial. auto with *.
+ destruct θ. 5 : {
destruct (Hind (θ1 :: Γ) (θ2 :: rm (θ1 → θ2) Δ)) as [[Hp1 _] | Hf'].
- order_tac. repeat rewrite <- Permutation_middle. order_tac.
destruct sumbool_rec; [|tauto]. order_tac.
- destruct (Hind (θ1 :: □⁻¹ Γ) [θ2]) as [[Hp2 _] | Hf'].
+ order_tac.
+ left. exists θ1; exists θ2. repeat split; try l_tac.
* rwl (symmetry (list_to_set_disj_env_add Γ θ1)). rpeapply Hp1.
* rwl list_to_set_disj_open_boxes.
rwl (symmetry (list_to_set_disj_env_add (□⁻¹ Γ) θ1)). rpeapply Hp2.
* ms.
+ right; intros φ1 φ2 Hp1' Hp2 He; apply elem_of_list_In in He;
destruct He as [Heq''| Hin]; [|apply elem_of_list_In in Hin; eapply Hf; eauto].
dependent destruction Heq''. apply Hf'.
rwl list_to_set_disj_env_add.
rwl (symmetry (list_to_set_disj_open_boxes Γ)). rpeapply Hp2.
- right; intros φ1 φ2 Hp1 Hp2 He; apply elem_of_list_In in He;
destruct He as [Heq''| Hin]; [|apply elem_of_list_In in Hin; eapply Hf; eauto].
dependent destruction Heq''. apply Hf'.
rwl list_to_set_disj_env_add. rpeapply Hp1.
}
all: (right; intros φ1 φ2 Hp1 Hp2 He;
apply elem_of_list_In in He; destruct He as [Heq''| Hin];
[discriminate|apply elem_of_list_In in Hin; eapply Hf; eauto]).
}
destruct (HImpR Δ [] (app_nil_l _)) as [(φ1 & φ2 & Hp1 & Hp2 & Hin) | HfImpR].
{ apply elem_of_list_to_set_disj in Hin.
left. eexists; trivial. exhibit Hin 0.
rwr (symmetry (list_to_set_disj_rm Δ (φ1→ φ2))). apply ImpR; assumption.
}
clear HImpR.
(* BoxR *)
assert(HBoxR :
{φ & {Hp : (⊗ (list_to_set_disj Γ) • □ φ ⊢ ∅ • φ) & (□ φ) ∈ Δ}}
+ { ∀ φ, ⊗ (list_to_set_disj Γ) • □ φ ⊢ ∅ • φ -> ¬ (□ φ) ∈ Δ}).
{
clear Hbot Hvar HAndL HOrL HAndR HOrR HImpLOr HImpLVar HImpLOr HfImpR.
induction Δ as [|θ Δ].
- right. intros φ Hp Hin. inversion Hin.
- destruct IHΔ as [(φ & Hp & Hin) | Hf].
+ intros. apply Hind. unfold env_pair_order in *. etransitivity; eauto.
order_tac.
+ left. exists φ. split; trivial. ms.
+ destruct θ. 6: {
destruct (Hind ((□ θ) :: map open_box Γ) [θ])as [[Hp _]|Hf'].
- order_tac.
- left. exists θ. simpl in Hp. eexists; eauto.
+ lazy_apply Hp. rewrite list_to_set_disj_open_boxes. ms.
+ ms.
- right. intros φ' Hp Hin. apply elem_of_list_In in Hin.
destruct Hin as [Heq |Hin].
+ inversion Heq; subst. apply Hf'. lazy_apply Hp.
rewrite list_to_set_disj_open_boxes. ms.
+ apply (Hf φ'); trivial. now apply elem_of_list_In.
}
all : auto with *.
}
destruct HBoxR as [(φ' & Hp & Hin)| HBoxR ].
{ left. subst. eexists; trivial. apply elem_of_list_to_set_disj in Hin.
exhibit Hin 0. apply BoxR, Hp. }
simpl in HBoxR.
(* non invertible left rules *)
(* ImpLImp *)
assert(HImpLImp : ∀Γ2 Γ1, Γ1 ++ Γ2 = Γ ->
{φ1 & {φ2 & {φ3 &{H2312 :
((list_to_set_disj (rm ((φ1 → φ2) → φ3) Γ) • (φ2 → φ3) • φ1) ⊢ (list_to_set_disj Δ • φ2))
&{H2312' :
((⊗ (list_to_set_disj (rm ((φ1 → φ2) → φ3) Γ)) • (φ2 → φ3) • φ1) ⊢ (∅ • φ2))
& {H3: (list_to_set_disj (rm ((φ1 → φ2) → φ3) Γ) • φ3) ⊢ list_to_set_disj Δ & ((φ1 → φ2) → φ3) ∈ Γ2}}}}}}
+ {∀ φ1 φ2 φ3, (list_to_set_disj (rm ((φ1 → φ2) → φ3) Γ) • (φ2 → φ3) • φ1) ⊢ (list_to_set_disj Δ • φ2)
-> ((⊗ (list_to_set_disj (rm ((φ1 → φ2) → φ3) Γ)) • (φ2 → φ3) • φ1) ⊢ (∅ • φ2))
-> (list_to_set_disj (rm ((φ1 → φ2) → φ3) Γ) • φ3) ⊢ list_to_set_disj Δ ->
((φ1 → φ2) → φ3) ∈ Γ2 → False}).
{
induction Γ2 as [|θ Γ2]; intros Γ1 Heq.
- right. intros φ1 φ2 φ3 _ _ _ Hin. inversion Hin.
- assert(Heq' : (Γ1 ++ [θ]) ++ Γ2 = Γ) by (subst; auto with *).
destruct (IHΓ2 (Γ1 ++ [θ]) Heq') as [(φ1 & φ2 & φ3 & Hp1 & Hp2 & Hp3 & Hin)|Hf].
+ left. repeat eexists; eauto. now right.
+ destruct θ.
5: destruct θ1.
9 : {
destruct (Hind (θ1_1 :: (θ1_2 → θ2) :: rm ((θ1_1 → θ1_2) → θ2) Γ)
(θ1_2 :: Δ)) as [[Hp1 _] | Hf'].
- order_tac. rewrite <- Permutation_middle. unfold rm.
destruct form_eq_dec; [|tauto]. order_tac.
- destruct (Hind (θ2 :: rm ((θ1_1 → θ1_2) → θ2) Γ) Δ) as [[Hp2 _] | Hf''].
+ order_tac. rewrite <- Permutation_middle. unfold rm.
destruct form_eq_dec; [|tauto]. order_tac.
+ destruct (Hind (θ1_1 :: (θ1_2 → θ2) :: □⁻¹ (rm ((θ1_1 → θ1_2) → θ2) Γ))
[θ1_2]) as [[Hp3 _] | Hf''].
* order_tac. repeat rewrite <- Permutation_middle.
simpl app.
destruct sumbool_rec; [|tauto]. order_tac.
* left. exists θ1_1; exists θ1_2; exists θ2; repeat split; try l_tac.
-- rwr list_to_set_disj_env_add'. peapply Hp1.
-- peapply Hp3.
-- peapply Hp2.
-- ms.
* right; intros φ1 φ2 φ3 Hp1' Hp2' Hp3' He; apply elem_of_list_In in He;
destruct He as [Heq''| Hin]; [|apply elem_of_list_In in Hin; eapply Hf; eauto].
dependent destruction Heq''. apply Hf''.
lazy_apply Hp2'.
rewrite list_to_set_disj_open_boxes. ms.
+ right; intros φ1 φ2 φ3 Hp1' Hp2 Hp3 He; apply elem_of_list_In in He;
destruct He as [Heq''| Hin]; [|apply elem_of_list_In in Hin; eapply Hf; eauto].
dependent destruction Heq''. apply Hf''. peapply Hp3.
- right; intros φ1 φ2 φ3 Hp1 Hp2 Hp3 He; apply elem_of_list_In in He;
destruct He as [Heq''| Hin]; [|apply elem_of_list_In in Hin; eapply Hf; eauto].
dependent destruction Heq''. apply Hf'.
rwr list_to_set_disj_env_add.
peapply Hp1.
}
all: (right; intros φ1 φ2 φ3 Hp1 Hp2 Hp3 He;
apply elem_of_list_In in He; destruct He as [Heq''| Hin];
[discriminate|apply elem_of_list_In in Hin; eapply Hf; eauto]).
}
destruct (HImpLImp Γ [] (app_nil_l _)) as [(φ1 & φ2 & φ3 & Hp1 & Hp2 & Hp3 & Hin)|HfImpl].
{ apply elem_of_list_to_set_disj in Hin.
left. eexists; trivial. exhibit Hin 0.
rwl (symmetry (list_to_set_disj_rm Γ((φ1 → φ2) → φ3))).
apply ImpLImp; assumption.
}
(* ImpLBox *)
assert(HImpLBox : ∀Γ2 Γ1, Γ1 ++ Γ2 = Γ ->
{φ1 & {φ2
& {H2312 : ((⊗(list_to_set_disj (rm ((□ φ1) → φ2) Γ)) • □ φ1 • φ2) ⊢ ∅ • φ1)
& {H3: (list_to_set_disj (rm ((□ φ1) → φ2) Γ) • φ2 ⊢ list_to_set_disj Δ)
& ((□ φ1) → φ2) ∈ Γ2}}}}
+ {∀ φ1 φ2, ((⊗ (list_to_set_disj (rm ((□ φ1) → φ2) Γ)) • □ φ1 • φ2) ⊢ ∅ • φ1)
-> list_to_set_disj (rm ((□ φ1) → φ2) Γ) • φ2 ⊢ list_to_set_disj Δ ->
((□ φ1) → φ2) ∈ Γ2 → False}).
{
induction Γ2 as [|θ Γ2]; intros Γ1 Heq.
- right. intros φ1 φ2 _ _ Hin. inversion Hin.
- assert(Heq' : (Γ1 ++ [θ]) ++ Γ2 = Γ) by (subst; auto with *).
destruct (IHΓ2 (Γ1 ++ [θ]) Heq') as [(φ1 & φ2 & Hp1 & Hp2 & Hin)|Hf].
+ left. repeat eexists; eauto. subst. now right.
+ destruct θ. 5: destruct θ1.
10 : {
destruct (Hind (θ2 :: (□θ1) :: map open_box (rm ((□ θ1) → θ2) Γ)) [θ1])
as [[Hp1 _] | Hf'].
- order_tac. repeat rewrite <- Permutation_middle. unfold rm.
destruct form_eq_dec; [|tauto]. fold rm. order_tac.
- destruct (Hind (θ2 :: rm ((□ θ1) → θ2) Γ) Δ) as [[Hp2 _] | Hf''].
+ order_tac. rewrite <- Permutation_middle. unfold rm.
destruct form_eq_dec; [|tauto]. order_tac.
+ left. exists θ1, θ2. repeat eexists; [peapply Hp1| peapply Hp2 | ms].
+ right; intros φ1 φ2 Hp1' Hp2 He; apply elem_of_list_In in He;
destruct He as [Heq''| Hin]; [|apply elem_of_list_In in Hin; eapply Hf; eauto].
dependent destruction Heq''. apply Hf''. peapply Hp2.
- right; intros φ1 φ2 Hp1 Hp2 He; apply elem_of_list_In in He;
destruct He as [Heq''| Hin]; [|apply elem_of_list_In in Hin; eapply Hf; eauto].
dependent destruction Heq''. subst. apply Hf'.
(erewrite proper_Provable; [| |reflexivity]); [eapply Hp1|].
repeat rewrite <- ?list_to_set_disj_env_add, list_to_set_disj_open_boxes.
ms.
}
all: (right ; try destruct K; trivial; intros φ1 φ2 Hp1 Hp2 He;
apply elem_of_list_In in He; destruct He as [Heq''| Hin];
[discriminate|apply elem_of_list_In in Hin; eapply Hf; eauto]).
}
destruct (HImpLBox Γ [] (app_nil_l _)) as [(φ1 & φ2 & Hp1 & Hp2 & Hin)|HfImpLBox].
{ apply elem_of_list_to_set_disj in Hin. left. eexists; trivial.
exhibit Hin 0. rwl list_to_set_disj_rm_rev. apply ImpLBox; assumption.
}
(* All the sequent rules have been applied *)
clear Hind HImpLImp HImpLBox.
right.
Ltac eqt Γ := match goal with | H : (_ • ?φ) = list_to_set_disj Γ |- _ =>
let Heq := fresh "Heq" in assert(Heq := H); let Hinφ := fresh "Hin" in
assert(Hinφ : φ ∈ Γ) by (apply elem_of_list_to_set_disj; setoid_rewrite <- H; ms);
apply env_equiv_eq, env_add_inv', symmetry in Heq; rewrite <- list_to_set_disj_rm in Heq end.
intro Hp. dependent destruction Hp; subst; try eqt Γ; try eqt Δ; eauto 2.
- eapply HAndR; eauto.
- eapply HOrR; eauto.
- eapply HfImpR; eauto. rwr Heq. exact Hp1.
- eapply HImpLVar; eauto. apply elem_of_list_to_set_disj.
match goal with H : _ = list_to_set_disj Γ |- _ => setoid_rewrite <- H end; ms.
- eapply HfImpl; eauto; now rwl Heq.
- eapply HfImpLBox; eauto.
+ now rwl (proper_open_boxes _ _ Heq).
+ now rwl Heq.
- eapply HBoxR; eauto.
Defined.
The function Provable_dec decides whether a sequent is provable.
The proof is essentially the same as the definition of Proof_tree_dec.
Proposition Provable_dec Γ Δ :
(exists _ : list_to_set_disj Γ ⊢ list_to_set_disj Δ, True) +
(forall H : list_to_set_disj Γ ⊢ list_to_set_disj Δ, False).
Proof.
remember (Γ, Δ) as pe.
replace Γ with pe.1 by now inversion Heqpe.
replace Δ with pe.2 by now inversion Heqpe. clear Heqpe Γ Δ.
revert pe.
(* Induction on the well-ordering of pointed environments *)
refine (@well_founded_induction _ _ wf_pointed_order _ _).
(* Cleaning up the induction hypothesis *)
intros (Γ& Δ) Hind; simpl.
assert(Hind' := λ Γ' Δ', Hind(Γ', Δ')). simpl in Hind'. clear Hind. rename Hind' into Hind.
(* ExFalso *)
case (decide (⊥ ∈ Γ)); intro Hbot.
{ left. eexists; trivial. apply elem_of_list_to_set_disj in Hbot. exhibit Hbot 0. apply ExFalso. }
(* Atom *)
assert(Hvar : {p | (Var p ∈ Δ /\ Var p ∈ Γ)} + {∀ p, Var p ∈ Δ -> Var p ∈ Γ -> False}). {
pose (VΔ := filter is_var Δ). pose (VΓ := filter is_var Γ).
case_eq (list_find (fun x => is_var x /\ x ∈ VΓ) VΔ).
- intros [p φ] HSome. rewrite list_find_Some in HSome.
destruct HSome as (Heq & (Hvar & Hin) & _). apply elem_of_list_lookup_2 in Heq.
clear p. left. destruct φ as [p | | | | | ]. 2-6 : inversion Hvar.
exists p. subst VΔ VΓ. rewrite elem_of_list_filter in Heq, Hin. tauto.
- intro HN. right. intros p HpΔ HpΓ. apply list_find_None in HN.
rewrite Forall_forall in HN. subst VΔ VΓ. apply (HN (# p)).
+ rewrite <- elem_of_list_In, elem_of_list_filter. simpl. tauto.
+ rewrite elem_of_list_filter. simpl; tauto.
}
destruct Hvar as [[p [Hp' Hp]]|Hvar].
{ subst. left. eexists; trivial. apply elem_of_list_to_set_disj in Hp, Hp'.
exhibit Hp 0. exhibit Hp' 0. apply Atom. }
(* AndL *)
assert(HAndL : {ψ1 & {ψ2 & (And ψ1 ψ2) ∈ Γ}} + {∀ ψ1 ψ2, (And ψ1 ψ2) ∈ Γ -> False}). {
destruct (exists_dec is_conj Γ) as [(θ & Hin & Hθ) | Hf].
- left. destruct θ. 3: { eexists. eexists. apply elem_of_list_In. eauto. }
all: auto with *.
- right. intros ψ1 ψ2 Hψ. rewrite elem_of_list_In in Hψ. apply Hf in Hψ. simpl in Hψ. tauto.
}
destruct HAndL as [(ψ1 & ψ2 & Hin)|HAndL].
{ destruct (Hind (ψ2 :: ψ1 :: rm (And ψ1 ψ2) Γ) Δ) as [Hp' | Hf].
- order_tac.
- left. destruct Hp' as [Hp' _].
eexists; trivial. apply elem_of_list_to_set_disj in Hin.
exhibit Hin 0. apply AndL. peapply Hp'.
- right. intro Hf'. apply Hf. peapply AndL_rev.
apply elem_of_list_to_set_disj in Hin. rwl difference_singleton. exact Hf'.
}
(* OrL *)
assert(HOrL : {ψ1 & {ψ2 & (Or ψ1 ψ2) ∈ Γ}} + {∀ ψ1 ψ2, (Or ψ1 ψ2) ∈ Γ -> False}). {
destruct (exists_dec is_disj Γ) as [(θ & Hin & Hθ) | Hf].
- left. destruct θ. 4: { eexists. eexists. apply elem_of_list_In. eauto. }
all: inversion Hθ.
- right. intros ψ1 ψ2 Hψ. rewrite elem_of_list_In in Hψ. apply Hf in Hψ. simpl in Hψ. tauto.
}
destruct HOrL as [(ψ1 & ψ2 & Hin)|HOrL].
{ apply elem_of_list_to_set_disj in Hin.
destruct (Hind (ψ1 :: rm (Or ψ1 ψ2) Γ) Δ) as [Hp1 | Hf].
- order_tac.
- destruct (Hind (ψ2 :: rm (Or ψ1 ψ2) Γ) Δ) as [Hp2 | Hf].
+ order_tac.
+ left. destruct Hp1 as [Hp1 _]. destruct Hp2 as [Hp2 _].
eexists; trivial. exhibit Hin 0.
rwl list_to_set_disj_rm_rev. apply OrL.
* peapply Hp1.
* peapply Hp2.
+ right; intro Hf'.
apply Hf. rwl list_to_set_disj_env_add.
apply OrL_rev with (φ := ψ1). lazy_apply Hf'.
now rewrite list_to_set_disj_rm, difference_singleton.
- right; intro Hf'. apply Hf.
rwl list_to_set_disj_env_add.
apply OrL_rev with (ψ := ψ2). lazy_apply Hf'.
now rewrite list_to_set_disj_rm, difference_singleton.
}
(* AndR *)
assert(HAndR : {φ1 & {φ2 & (And φ1 φ2) ∈ Δ}} + {∀ φ1 φ2, ¬ (And φ1 φ2) ∈ Δ}). {
destruct (exists_dec is_conj Δ) as [(θ & Hin & Hθ) | Hf].
- left. destruct θ. 3: { eexists. eexists. apply elem_of_list_In. eauto. }
all: auto with *.
- right. intros ψ1 ψ2 Hψ. rewrite elem_of_list_In in Hψ. apply Hf in Hψ. simpl in Hψ. tauto.
}
destruct HAndR as [(φ1 & φ2 & Hin) | HAndR].
{ subst.
destruct (Hind Γ (φ1 :: rm (φ1 ∧ φ2) Δ)) as [Hp1 | H1].
- order_tac.
- destruct (Hind Γ (φ2 :: rm (φ1 ∧ φ2) Δ)) as [Hp2 | H2].
+ order_tac.
+ left. destruct Hp1 as [Hp1 _]. destruct Hp2 as [Hp2 _].
eexists; trivial. apply elem_of_list_to_set_disj in Hin.
exhibit Hin 0. apply AndR.
* rpeapply Hp1.
* rpeapply Hp2.
+ right. intro Hp. apply H2.
rwr list_to_set_disj_env_add. apply AndR_rev with (φ1 := φ1). lazy_apply Hp.
apply elem_of_list_to_set_disj in Hin.
now rewrite list_to_set_disj_rm, difference_singleton.
- right. intro Hp. apply H1.
apply elem_of_list_to_set_disj in Hin.
rwr list_to_set_disj_env_add.
apply AndR_rev with (φ2 := φ2). lazy_apply Hp.
now rewrite list_to_set_disj_rm, difference_singleton.
}
(* OrR is invertible in KM, but isn't in iSL *)
(* This case is symmetrical to AndL *)
assert(HOrR :
{φ1 & {φ2 & (φ1 ∨ φ2) ∈ Δ}} +
{∀ φ1 φ2, ¬ (φ1 ∨ φ2) ∈ Δ}).
{
destruct (exists_dec is_disj Δ) as [(θ & Hin & Hθ) | Hf].
- left. destruct θ. 4: { eexists. eexists. apply elem_of_list_In. exact Hin. }
all: auto with *.
- right. intros ψ1 ψ2 Hψ. rewrite elem_of_list_In in Hψ. apply Hf in Hψ. simpl in Hψ. tauto.
}
destruct HOrR as [(φ1 & φ2 & Hin)| HOrR].
{ destruct (Hind Γ (φ2 :: φ1 :: rm (Or φ1 φ2) Δ)) as [Hp' | Hf].
- order_tac.
- left. destruct Hp' as [Hp' _].
eexists; trivial. apply elem_of_list_to_set_disj in Hin.
exhibit Hin 0. apply OrR. rpeapply Hp'.
- right. intro Hf'. apply Hf. rpeapply OrR_rev.
apply elem_of_list_to_set_disj in Hin. rwr difference_singleton. exact Hf'.
}
(* ImpLVar *)
assert(HImpLVar : {p & {ψ & Var p ∈ Γ /\ (#p → ψ) ∈ Γ}} +
{∀ p ψ, Var p ∈ Γ -> (#p → ψ) ∈ Γ -> False}). {
pose (fIp :=λ p θ, match θ with | (#q → _) =>
if decide (p = q) then true else false | _ => false end).
pose (fp:= (fun θ => match θ with |Var p =>
if (exists_dec (fIp p) Γ) then true else false | _ => false end)).
destruct (exists_dec fp Γ) as [(θ & Hin & Hθ) | Hf].
- left. subst fp. destruct θ. 2-6: auto with *.
case exists_dec as [(ψ &Hinψ & Hψ)|] in Hθ; [|auto with *].
unfold fIp in Hψ. destruct ψ. 1-4, 6: auto with *.
destruct ψ1. 2-6: auto with *. case decide in Hψ; [|auto with *].
subst. apply elem_of_list_In in Hinψ, Hin.
do 2 eexists. split; eauto.
- right. intros p ψ Hp Hψ. rewrite elem_of_list_In in Hp, Hψ. apply Hf in Hp. subst fp fIp.
simpl in Hp. case exists_dec as [|Hf'] in Hp. auto with *.
apply (Hf' _ Hψ). rewrite decide_True; trivial. auto with *.
}
destruct HImpLVar as [[p [ψ [Hinp Hinψ]]]|HImpLVar].
{ apply elem_of_list_to_set_disj in Hinp.
apply elem_of_list_to_set_disj in Hinψ.
assert(Hinp' : Var p ∈ (list_to_set_disj Γ ∖ {[#p → ψ]} : env))
by (apply in_difference; [discriminate| assumption]).
destruct (Hind (ψ :: rm (#p → ψ) Γ) Δ) as [Hp|Hf].
- order_tac.
- left. destruct Hp as [Hp _]. eexists; trivial. exhibit Hinψ 0.
exhibit Hinp' 1. apply ImpLVar. rwl difference_singleton.
rwl list_to_set_disj_rm_rev. peapply Hp.
- right. intro Hf'. apply Hf.
rwl list_to_set_disj_env_add.
rwl list_to_set_disj_rm.
exhibit Hinp' 1. apply ImpLVar_rev.
do 2 rwl difference_singleton. exact Hf'.
}
(* ImpLAnd *)
assert(HImpLAnd : {φ1 & {φ2 & {φ3 & ((And φ1 φ2) → φ3) ∈ Γ}}} +
{∀ φ1 φ2 φ3, ((φ1 ∧ φ2) → φ3) ∈ Γ -> False}). {
pose (fII := (fun θ => match θ with |(And _ _) → _ => true | _ => false end)).
destruct (exists_dec fII Γ) as [(θ & Hin & Hθ) | Hf].
- left. subst fII. destruct θ. 1-4, 6: auto with *.
destruct θ1. 1-2,4-6: auto with *. do 3 eexists; apply elem_of_list_In; eauto.
- right. intros ψ1 ψ2 ψ3 Hψ. rewrite elem_of_list_In in Hψ.
apply Hf in Hψ. subst fII. simpl in Hψ. tauto.
}
destruct HImpLAnd as [(φ1&φ2&φ3&Hin)|HImpLAnd].
{ apply elem_of_list_to_set_disj in Hin.
destruct (Hind ((φ1 → (φ2 → φ3)) :: rm ((φ1 ∧ φ2) → φ3) Γ) Δ) as [Hp|Hf].
- order_tac.
- left. destruct Hp as [Hp _]. eexists; trivial. exhibit Hin 0. apply ImpLAnd.
rwl list_to_set_disj_rm_rev. peapply Hp.
- right. intro Hf'. apply Hf. rwl list_to_set_disj_env_add.
rwl list_to_set_disj_rm. apply ImpLAnd_rev.
rwl difference_singleton. exact Hf'.
}
(* ImpLOr *)
assert(HImpLOr : {φ1 & {φ2 & {φ3 & ((φ1 ∨ φ2) → φ3) ∈ Γ}}} +
{∀ φ1 φ2 φ3, ((φ1 ∨ φ2) → φ3) ∈ Γ -> False}). {
pose (fII := (fun θ => match θ with | (Or _ _) → _ => true | _ => false end)).
destruct (exists_dec fII Γ) as [(θ & Hin & Hθ) | Hf].
- left. subst fII. destruct θ. 1-4, 6: auto with *.
destruct θ1. 1-3, 5-6: auto with *. do 3 eexists; apply elem_of_list_In; eauto.
- right. intros ψ1 ψ2 ψ3 Hψ. rewrite elem_of_list_In in Hψ.
apply Hf in Hψ. subst fII. simpl in Hψ. tauto.
}
destruct HImpLOr as [(φ1&φ2&φ3&Hin)|HImpLOr].
{ apply elem_of_list_to_set_disj in Hin.
destruct (Hind ((φ2 → φ3) :: (φ1 → φ3) :: rm ((φ1 ∨ φ2) → φ3) Γ) Δ) as [Hp|Hf].
- order_tac.
- left. destruct Hp as [Hp _].
eexists; trivial. exhibit Hin 0. apply ImpLOr.
rwl list_to_set_disj_rm_rev. peapply Hp.
- right. intro Hf'. apply Hf.
do 2 rwl list_to_set_disj_env_add. rwl list_to_set_disj_rm. apply ImpLOr_rev.
rwl difference_singleton. exact Hf'.
}
(* non invertible right rules *)
(* ImpR is non-invertible in KM, but is in iSL *)
assert(HImpR : ∀ Δ2 Δ1, Δ1 ++ Δ2 = Δ -> {φ1 & {φ2 &
exists (_ : (list_to_set_disj Γ • φ1 ⊢KM list_to_set_disj (rm (φ1 → φ2) Δ) • φ2)),
exists (_ :(⊗ (list_to_set_disj Γ) • φ1 ⊢KM ∅ • φ2)), (φ1 → φ2) ∈ Δ2 }} +
{∀ φ1 φ2, (list_to_set_disj Γ • φ1 ⊢KM list_to_set_disj (rm (φ1 → φ2) Δ) • φ2) ->
(⊗ (list_to_set_disj Γ) • φ1 ⊢KM ∅ • φ2) ->
¬ (φ1 → φ2) ∈ Δ2 }).
{
clear Hbot Hvar HAndL HOrL HAndR HOrR HImpLOr HImpLVar HImpLOr.
induction Δ2 as [|θ Δ2]; intros Δ1 Heq.
- right. intros φ1 φ2 Hp1 Hp2 Hin. inversion Hin.
- destruct (IHΔ2 (Δ1 ++ [θ])) as [(φ1 & φ2 & Hp) | Hf].
+ auto with *.
+ left. do 2 eexists. destruct Hp as (Hp1 & Hp2 & Hin).
do 2 (eexists; eauto). auto with *.
+ destruct θ. 5 : {
destruct (Hind (θ1 :: Γ) (θ2 :: rm (θ1 → θ2) Δ)) as [Hp1 | Hf'].
- order_tac. repeat rewrite <- Permutation_middle. order_tac.
destruct sumbool_rec; [|tauto]. order_tac.
- destruct (Hind (θ1 :: □⁻¹ Γ) [θ2]) as [Hp2 | Hf'].
+ order_tac.
+ left. exists θ1; exists θ2. destruct Hp1 as [Hp1 _]. destruct Hp2 as [Hp2 _].
repeat split; try l_tac.
* rwl list_to_set_disj_env_add'. rpeapply Hp1.
* rwl list_to_set_disj_open_boxes.
rwl list_to_set_disj_env_add'. rpeapply Hp2.
* ms.
+ right; intros φ1 φ2 Hp1' Hp2 He; apply elem_of_list_In in He;
destruct He as [Heq''| Hin]; [|apply elem_of_list_In in Hin; eapply Hf; eauto].
dependent destruction Heq''. apply Hf'.
rwl list_to_set_disj_env_add.
rwl (symmetry (list_to_set_disj_open_boxes Γ)). rpeapply Hp2.
- right; intros φ1 φ2 Hp1 Hp2 He; apply elem_of_list_In in He;
destruct He as [Heq''| Hin]; [|apply elem_of_list_In in Hin; eapply Hf; eauto].
dependent destruction Heq''. apply Hf'.
rwl list_to_set_disj_env_add. rpeapply Hp1.
}
all: (right; intros φ1 φ2 Hp1 Hp2 He;
apply elem_of_list_In in He; destruct He as [Heq''| Hin];
[discriminate|apply elem_of_list_In in Hin; eapply Hf; eauto]).
}
destruct (HImpR Δ [] (app_nil_l _)) as [(φ1 & φ2 & Hp) | HfImpR].
{ left. destruct Hp as (Hp1 & Hp2 & Hin).
apply elem_of_list_to_set_disj in Hin.
eexists; trivial. exhibit Hin 0.
rwr list_to_set_disj_rm_rev. apply ImpR; assumption.
}
clear HImpR.
(* BoxR *)
assert(HBoxR :
{φ & exists (Hp : (⊗ (list_to_set_disj Γ) • □ φ ⊢ ∅ • φ)), (□ φ) ∈ Δ}
+ { ∀ φ, ⊗ (list_to_set_disj Γ) • □ φ ⊢ ∅ • φ -> ¬ (□ φ) ∈ Δ}).
{
clear Hbot Hvar HAndL HOrL HAndR HOrR HImpLOr HImpLVar HImpLOr HfImpR.
induction Δ as [|θ Δ].
- right. intros φ Hp Hin. inversion Hin.
- destruct IHΔ as [(φ & Hp) | Hf].
+ intros. apply Hind. unfold env_pair_order in *. etransitivity; eauto.
order_tac.
+ left. exists φ. destruct Hp as [Hp Hin]. split; trivial. ms.
+ destruct θ. 6: {
destruct (Hind ((□ θ) :: map open_box Γ) [θ])as [Hp|Hf'].
- order_tac.
- left. exists θ. destruct Hp as [Hp Hin]. simpl in Hp. eexists; eauto.
+ lazy_apply Hp. rewrite list_to_set_disj_open_boxes. ms.
+ ms.
- right. intros φ' Hp Hin. apply elem_of_list_In in Hin.
destruct Hin as [Heq |Hin].
+ inversion Heq; subst. apply Hf'. lazy_apply Hp.
rewrite list_to_set_disj_open_boxes. ms.
+ apply (Hf φ'); trivial. now apply elem_of_list_In.
}
all : auto with *.
}
destruct HBoxR as [(φ' & Hp)| HBoxR ].
{ left. destruct Hp as [Hp Hin]. subst. eexists; trivial.
apply elem_of_list_to_set_disj in Hin.
exhibit Hin 0. apply BoxR, Hp. }
(* non invertible left rules *)
(* ImpLImp *)
assert(HImpLImp : ∀Γ2 Γ1, Γ1 ++ Γ2 = Γ ->
{φ1 & {φ2 & {φ3 & exists _ :
(list_to_set_disj (rm ((φ1 → φ2) → φ3) Γ) • (φ2 → φ3) • φ1) ⊢ (list_to_set_disj Δ • φ2),
exists _ :
(⊗ (list_to_set_disj (rm ((φ1 → φ2) → φ3) Γ)) • (φ2 → φ3) • φ1) ⊢ (∅ • φ2),
exists _ : (list_to_set_disj (rm ((φ1 → φ2) → φ3) Γ) • φ3) ⊢ list_to_set_disj Δ,
((φ1 → φ2) → φ3) ∈ Γ2}}}
+ {∀ φ1 φ2 φ3, (list_to_set_disj (rm ((φ1 → φ2) → φ3) Γ) • (φ2 → φ3) • φ1) ⊢ (list_to_set_disj Δ • φ2)
-> ((⊗ (list_to_set_disj (rm ((φ1 → φ2) → φ3) Γ)) • (φ2 → φ3) • φ1) ⊢ (∅ • φ2))
-> (list_to_set_disj (rm ((φ1 → φ2) → φ3) Γ) • φ3) ⊢ list_to_set_disj Δ ->
((φ1 → φ2) → φ3) ∈ Γ2 → False}).
{
induction Γ2 as [|θ Γ2]; intros Γ1 Heq.
- right. intros φ1 φ2 φ3 _ _ _ Hin. inversion Hin.
- assert(Heq' : (Γ1 ++ [θ]) ++ Γ2 = Γ) by (subst; auto with * ).
destruct (IHΓ2 (Γ1 ++ [θ]) Heq') as [(φ1 & φ2 & φ3 & Hp)|Hf].
+ left. do 3 eexists. destruct Hp as (Hp1 & Hp2 & Hp3 & Hin).
do 3 (eexists; eauto). now right.
+ destruct θ.
5: destruct θ1.
9 : {
destruct (Hind (θ1_1 :: (θ1_2 → θ2) :: rm ((θ1_1 → θ1_2) → θ2) Γ)
(θ1_2 :: Δ)) as [Hp1 | Hf'].
- order_tac. rewrite <- Permutation_middle. unfold rm.
destruct form_eq_dec; [|tauto]. order_tac.
- destruct (Hind (θ2 :: rm ((θ1_1 → θ1_2) → θ2) Γ) Δ) as [Hp2 | Hf''].
+ order_tac. rewrite <- Permutation_middle. unfold rm.
destruct form_eq_dec; [|tauto]. order_tac.
+ destruct (Hind (θ1_1 :: (θ1_2 → θ2) :: □⁻¹ (rm ((θ1_1 → θ1_2) → θ2) Γ))
[θ1_2]) as [Hp3 | Hf''].
* order_tac. repeat rewrite <- Permutation_middle. simpl app.
destruct sumbool_rec; [|tauto]. order_tac.
* left. exists θ1_1; exists θ1_2; exists θ2.
destruct Hp1 as [Hp1 _]. destruct Hp2 as [Hp2 _]. destruct Hp3 as [Hp3 _].
repeat split; try l_tac.
-- rwr list_to_set_disj_env_add'. peapply Hp1.
-- peapply Hp3.
-- peapply Hp2.
-- ms.
* right; intros φ1 φ2 φ3 Hp1' Hp2' Hp3' He; apply elem_of_list_In in He;
destruct He as [Heq''| Hin]; [|apply elem_of_list_In in Hin; eapply Hf; eauto].
dependent destruction Heq''. apply Hf''.
lazy_apply Hp2'.
rewrite list_to_set_disj_open_boxes. ms.
+ right; intros φ1 φ2 φ3 Hp1' Hp2 Hp3 He; apply elem_of_list_In in He;
destruct He as [Heq''| Hin]; [|apply elem_of_list_In in Hin; eapply Hf; eauto].
dependent destruction Heq''. apply Hf''. peapply Hp3.
- right; intros φ1 φ2 φ3 Hp1 Hp2 Hp3 He; apply elem_of_list_In in He;
destruct He as [Heq''| Hin]; [|apply elem_of_list_In in Hin; eapply Hf; eauto].
dependent destruction Heq''. apply Hf'.
rwr list_to_set_disj_env_add. peapply Hp1.
}
all: (right; intros φ1 φ2 φ3 Hp1 Hp2 Hp3 He;
apply elem_of_list_In in He; destruct He as [Heq''| Hin];
[discriminate|apply elem_of_list_In in Hin; eapply Hf; eauto]).
}
destruct (HImpLImp Γ [] (app_nil_l _)) as [(φ1 & φ2 & φ3 & Hp)|HfImpl].
{ left. destruct Hp as (Hp1 & Hp2 & Hp3 & Hin).
apply elem_of_list_to_set_disj in Hin.
eexists; trivial. exhibit Hin 0.
rwl list_to_set_disj_rm_rev.
apply ImpLImp; assumption.
}
(* ImpLBox *)
assert(HImpLBox : ∀Γ2 Γ1, Γ1 ++ Γ2 = Γ ->
{φ1 & {φ2
& exists _ : (⊗(list_to_set_disj (rm ((□ φ1) → φ2) Γ)) • □ φ1 • φ2) ⊢ ∅ • φ1,
exists _ : list_to_set_disj (rm ((□ φ1) → φ2) Γ) • φ2 ⊢ list_to_set_disj Δ,
((□ φ1) → φ2) ∈ Γ2}}
+ {∀ φ1 φ2, ((⊗ (list_to_set_disj (rm ((□ φ1) → φ2) Γ)) • □ φ1 • φ2) ⊢ ∅ • φ1)
-> list_to_set_disj (rm ((□ φ1) → φ2) Γ) • φ2 ⊢ list_to_set_disj Δ ->
((□ φ1) → φ2) ∈ Γ2 → False}).
{
induction Γ2 as [|θ Γ2]; intros Γ1 Heq.
- right. intros φ1 φ2 _ _ Hin. inversion Hin.
- assert(Heq' : (Γ1 ++ [θ]) ++ Γ2 = Γ) by (subst; auto with * ).
destruct (IHΓ2 (Γ1 ++ [θ]) Heq') as [(φ1 & φ2 & Hp)|Hf].
+ left. do 2 (eexists; eauto).
destruct Hp as (Hp1 & Hp2 & Hin). repeat eexists; eauto. subst. now right.
+ destruct θ. 5: destruct θ1.
10 : {
destruct (Hind (θ2 :: (□θ1) :: map open_box (rm ((□ θ1) → θ2) Γ)) [θ1])
as [Hp1 | Hf'].
- order_tac. repeat rewrite <- Permutation_middle. unfold rm.
destruct form_eq_dec; [|tauto]. fold rm. order_tac.
- destruct (Hind (θ2 :: rm ((□ θ1) → θ2) Γ) Δ) as [Hp2 | Hf''].
+ order_tac. rewrite <- Permutation_middle. unfold rm.
destruct form_eq_dec; [|tauto]. order_tac.
+ left. exists θ1, θ2. destruct Hp1 as (Hp1 & _). destruct Hp2 as (Hp2 & _).
repeat eexists; [peapply Hp1| peapply Hp2 | ms].
+ right; intros φ1 φ2 Hp1' Hp2 He; apply elem_of_list_In in He;
destruct He as [Heq''| Hin]; [|apply elem_of_list_In in Hin; eapply Hf; eauto].
dependent destruction Heq''. apply Hf''. peapply Hp2.
- right; intros φ1 φ2 Hp1 Hp2 He; apply elem_of_list_In in He;
destruct He as [Heq''| Hin]; [|apply elem_of_list_In in Hin; eapply Hf; eauto].
dependent destruction Heq''. subst. apply Hf'.
(erewrite proper_Provable; [| |reflexivity]); [eapply Hp1|].
repeat rewrite <- ?list_to_set_disj_env_add, list_to_set_disj_open_boxes.
ms.
}
all: (right ; try destruct K; trivial; intros φ1 φ2 Hp1 Hp2 He;
apply elem_of_list_In in He; destruct He as [Heq''| Hin];
[discriminate|apply elem_of_list_In in Hin; eapply Hf; eauto]).
}
destruct (HImpLBox Γ [] (app_nil_l _)) as [(φ1 & φ2 & Hp)|HfImpLBox].
{ left. destruct Hp as (Hp1 & Hp2 & Hin). eexists; trivial.
apply elem_of_list_to_set_disj in Hin.
exhibit Hin 0. rwl list_to_set_disj_rm_rev. apply ImpLBox; assumption.
}
(* All the sequent rules have been applied *)
clear Hind HImpLImp HImpLBox.
right.
intro Hp. dependent destruction Hp; subst; try eqt Γ; try eqt Δ; eauto 2.
- eapply HAndR; eauto.
- eapply HOrR; eauto.
- eapply HfImpR; eauto. rwr Heq. exact Hp1.
- eapply HImpLVar; eauto. apply elem_of_list_to_set_disj.
match goal with H : _ = list_to_set_disj Γ |- _ => setoid_rewrite <- H end; ms.
- eapply HfImpl; eauto; now rwl Heq.
- eapply HfImpLBox; eauto.
+ now rwl (proper_open_boxes _ _ Heq).
+ now rwl Heq.
- eapply HBoxR; eauto.
Defined.
Global Infix "⊢?" := Provable_dec (at level 80).
Lemma Provable_dec_of_Prop Γ Δ:
(∃ _ : list_to_set_disj Γ ⊢ list_to_set_disj Δ, True) ->
(list_to_set_disj Γ ⊢ list_to_set_disj Δ).
Proof.
destruct (Proof_tree_dec Γ Δ) as [[Hφ1' _] | Hf']. tauto.
intros Hf. exfalso. destruct Hf as [Hf _]. tauto.
Qed.
(exists _ : list_to_set_disj Γ ⊢ list_to_set_disj Δ, True) +
(forall H : list_to_set_disj Γ ⊢ list_to_set_disj Δ, False).
Proof.
remember (Γ, Δ) as pe.
replace Γ with pe.1 by now inversion Heqpe.
replace Δ with pe.2 by now inversion Heqpe. clear Heqpe Γ Δ.
revert pe.
(* Induction on the well-ordering of pointed environments *)
refine (@well_founded_induction _ _ wf_pointed_order _ _).
(* Cleaning up the induction hypothesis *)
intros (Γ& Δ) Hind; simpl.
assert(Hind' := λ Γ' Δ', Hind(Γ', Δ')). simpl in Hind'. clear Hind. rename Hind' into Hind.
(* ExFalso *)
case (decide (⊥ ∈ Γ)); intro Hbot.
{ left. eexists; trivial. apply elem_of_list_to_set_disj in Hbot. exhibit Hbot 0. apply ExFalso. }
(* Atom *)
assert(Hvar : {p | (Var p ∈ Δ /\ Var p ∈ Γ)} + {∀ p, Var p ∈ Δ -> Var p ∈ Γ -> False}). {
pose (VΔ := filter is_var Δ). pose (VΓ := filter is_var Γ).
case_eq (list_find (fun x => is_var x /\ x ∈ VΓ) VΔ).
- intros [p φ] HSome. rewrite list_find_Some in HSome.
destruct HSome as (Heq & (Hvar & Hin) & _). apply elem_of_list_lookup_2 in Heq.
clear p. left. destruct φ as [p | | | | | ]. 2-6 : inversion Hvar.
exists p. subst VΔ VΓ. rewrite elem_of_list_filter in Heq, Hin. tauto.
- intro HN. right. intros p HpΔ HpΓ. apply list_find_None in HN.
rewrite Forall_forall in HN. subst VΔ VΓ. apply (HN (# p)).
+ rewrite <- elem_of_list_In, elem_of_list_filter. simpl. tauto.
+ rewrite elem_of_list_filter. simpl; tauto.
}
destruct Hvar as [[p [Hp' Hp]]|Hvar].
{ subst. left. eexists; trivial. apply elem_of_list_to_set_disj in Hp, Hp'.
exhibit Hp 0. exhibit Hp' 0. apply Atom. }
(* AndL *)
assert(HAndL : {ψ1 & {ψ2 & (And ψ1 ψ2) ∈ Γ}} + {∀ ψ1 ψ2, (And ψ1 ψ2) ∈ Γ -> False}). {
destruct (exists_dec is_conj Γ) as [(θ & Hin & Hθ) | Hf].
- left. destruct θ. 3: { eexists. eexists. apply elem_of_list_In. eauto. }
all: auto with *.
- right. intros ψ1 ψ2 Hψ. rewrite elem_of_list_In in Hψ. apply Hf in Hψ. simpl in Hψ. tauto.
}
destruct HAndL as [(ψ1 & ψ2 & Hin)|HAndL].
{ destruct (Hind (ψ2 :: ψ1 :: rm (And ψ1 ψ2) Γ) Δ) as [Hp' | Hf].
- order_tac.
- left. destruct Hp' as [Hp' _].
eexists; trivial. apply elem_of_list_to_set_disj in Hin.
exhibit Hin 0. apply AndL. peapply Hp'.
- right. intro Hf'. apply Hf. peapply AndL_rev.
apply elem_of_list_to_set_disj in Hin. rwl difference_singleton. exact Hf'.
}
(* OrL *)
assert(HOrL : {ψ1 & {ψ2 & (Or ψ1 ψ2) ∈ Γ}} + {∀ ψ1 ψ2, (Or ψ1 ψ2) ∈ Γ -> False}). {
destruct (exists_dec is_disj Γ) as [(θ & Hin & Hθ) | Hf].
- left. destruct θ. 4: { eexists. eexists. apply elem_of_list_In. eauto. }
all: inversion Hθ.
- right. intros ψ1 ψ2 Hψ. rewrite elem_of_list_In in Hψ. apply Hf in Hψ. simpl in Hψ. tauto.
}
destruct HOrL as [(ψ1 & ψ2 & Hin)|HOrL].
{ apply elem_of_list_to_set_disj in Hin.
destruct (Hind (ψ1 :: rm (Or ψ1 ψ2) Γ) Δ) as [Hp1 | Hf].
- order_tac.
- destruct (Hind (ψ2 :: rm (Or ψ1 ψ2) Γ) Δ) as [Hp2 | Hf].
+ order_tac.
+ left. destruct Hp1 as [Hp1 _]. destruct Hp2 as [Hp2 _].
eexists; trivial. exhibit Hin 0.
rwl list_to_set_disj_rm_rev. apply OrL.
* peapply Hp1.
* peapply Hp2.
+ right; intro Hf'.
apply Hf. rwl list_to_set_disj_env_add.
apply OrL_rev with (φ := ψ1). lazy_apply Hf'.
now rewrite list_to_set_disj_rm, difference_singleton.
- right; intro Hf'. apply Hf.
rwl list_to_set_disj_env_add.
apply OrL_rev with (ψ := ψ2). lazy_apply Hf'.
now rewrite list_to_set_disj_rm, difference_singleton.
}
(* AndR *)
assert(HAndR : {φ1 & {φ2 & (And φ1 φ2) ∈ Δ}} + {∀ φ1 φ2, ¬ (And φ1 φ2) ∈ Δ}). {
destruct (exists_dec is_conj Δ) as [(θ & Hin & Hθ) | Hf].
- left. destruct θ. 3: { eexists. eexists. apply elem_of_list_In. eauto. }
all: auto with *.
- right. intros ψ1 ψ2 Hψ. rewrite elem_of_list_In in Hψ. apply Hf in Hψ. simpl in Hψ. tauto.
}
destruct HAndR as [(φ1 & φ2 & Hin) | HAndR].
{ subst.
destruct (Hind Γ (φ1 :: rm (φ1 ∧ φ2) Δ)) as [Hp1 | H1].
- order_tac.
- destruct (Hind Γ (φ2 :: rm (φ1 ∧ φ2) Δ)) as [Hp2 | H2].
+ order_tac.
+ left. destruct Hp1 as [Hp1 _]. destruct Hp2 as [Hp2 _].
eexists; trivial. apply elem_of_list_to_set_disj in Hin.
exhibit Hin 0. apply AndR.
* rpeapply Hp1.
* rpeapply Hp2.
+ right. intro Hp. apply H2.
rwr list_to_set_disj_env_add. apply AndR_rev with (φ1 := φ1). lazy_apply Hp.
apply elem_of_list_to_set_disj in Hin.
now rewrite list_to_set_disj_rm, difference_singleton.
- right. intro Hp. apply H1.
apply elem_of_list_to_set_disj in Hin.
rwr list_to_set_disj_env_add.
apply AndR_rev with (φ2 := φ2). lazy_apply Hp.
now rewrite list_to_set_disj_rm, difference_singleton.
}
(* OrR is invertible in KM, but isn't in iSL *)
(* This case is symmetrical to AndL *)
assert(HOrR :
{φ1 & {φ2 & (φ1 ∨ φ2) ∈ Δ}} +
{∀ φ1 φ2, ¬ (φ1 ∨ φ2) ∈ Δ}).
{
destruct (exists_dec is_disj Δ) as [(θ & Hin & Hθ) | Hf].
- left. destruct θ. 4: { eexists. eexists. apply elem_of_list_In. exact Hin. }
all: auto with *.
- right. intros ψ1 ψ2 Hψ. rewrite elem_of_list_In in Hψ. apply Hf in Hψ. simpl in Hψ. tauto.
}
destruct HOrR as [(φ1 & φ2 & Hin)| HOrR].
{ destruct (Hind Γ (φ2 :: φ1 :: rm (Or φ1 φ2) Δ)) as [Hp' | Hf].
- order_tac.
- left. destruct Hp' as [Hp' _].
eexists; trivial. apply elem_of_list_to_set_disj in Hin.
exhibit Hin 0. apply OrR. rpeapply Hp'.
- right. intro Hf'. apply Hf. rpeapply OrR_rev.
apply elem_of_list_to_set_disj in Hin. rwr difference_singleton. exact Hf'.
}
(* ImpLVar *)
assert(HImpLVar : {p & {ψ & Var p ∈ Γ /\ (#p → ψ) ∈ Γ}} +
{∀ p ψ, Var p ∈ Γ -> (#p → ψ) ∈ Γ -> False}). {
pose (fIp :=λ p θ, match θ with | (#q → _) =>
if decide (p = q) then true else false | _ => false end).
pose (fp:= (fun θ => match θ with |Var p =>
if (exists_dec (fIp p) Γ) then true else false | _ => false end)).
destruct (exists_dec fp Γ) as [(θ & Hin & Hθ) | Hf].
- left. subst fp. destruct θ. 2-6: auto with *.
case exists_dec as [(ψ &Hinψ & Hψ)|] in Hθ; [|auto with *].
unfold fIp in Hψ. destruct ψ. 1-4, 6: auto with *.
destruct ψ1. 2-6: auto with *. case decide in Hψ; [|auto with *].
subst. apply elem_of_list_In in Hinψ, Hin.
do 2 eexists. split; eauto.
- right. intros p ψ Hp Hψ. rewrite elem_of_list_In in Hp, Hψ. apply Hf in Hp. subst fp fIp.
simpl in Hp. case exists_dec as [|Hf'] in Hp. auto with *.
apply (Hf' _ Hψ). rewrite decide_True; trivial. auto with *.
}
destruct HImpLVar as [[p [ψ [Hinp Hinψ]]]|HImpLVar].
{ apply elem_of_list_to_set_disj in Hinp.
apply elem_of_list_to_set_disj in Hinψ.
assert(Hinp' : Var p ∈ (list_to_set_disj Γ ∖ {[#p → ψ]} : env))
by (apply in_difference; [discriminate| assumption]).
destruct (Hind (ψ :: rm (#p → ψ) Γ) Δ) as [Hp|Hf].
- order_tac.
- left. destruct Hp as [Hp _]. eexists; trivial. exhibit Hinψ 0.
exhibit Hinp' 1. apply ImpLVar. rwl difference_singleton.
rwl list_to_set_disj_rm_rev. peapply Hp.
- right. intro Hf'. apply Hf.
rwl list_to_set_disj_env_add.
rwl list_to_set_disj_rm.
exhibit Hinp' 1. apply ImpLVar_rev.
do 2 rwl difference_singleton. exact Hf'.
}
(* ImpLAnd *)
assert(HImpLAnd : {φ1 & {φ2 & {φ3 & ((And φ1 φ2) → φ3) ∈ Γ}}} +
{∀ φ1 φ2 φ3, ((φ1 ∧ φ2) → φ3) ∈ Γ -> False}). {
pose (fII := (fun θ => match θ with |(And _ _) → _ => true | _ => false end)).
destruct (exists_dec fII Γ) as [(θ & Hin & Hθ) | Hf].
- left. subst fII. destruct θ. 1-4, 6: auto with *.
destruct θ1. 1-2,4-6: auto with *. do 3 eexists; apply elem_of_list_In; eauto.
- right. intros ψ1 ψ2 ψ3 Hψ. rewrite elem_of_list_In in Hψ.
apply Hf in Hψ. subst fII. simpl in Hψ. tauto.
}
destruct HImpLAnd as [(φ1&φ2&φ3&Hin)|HImpLAnd].
{ apply elem_of_list_to_set_disj in Hin.
destruct (Hind ((φ1 → (φ2 → φ3)) :: rm ((φ1 ∧ φ2) → φ3) Γ) Δ) as [Hp|Hf].
- order_tac.
- left. destruct Hp as [Hp _]. eexists; trivial. exhibit Hin 0. apply ImpLAnd.
rwl list_to_set_disj_rm_rev. peapply Hp.
- right. intro Hf'. apply Hf. rwl list_to_set_disj_env_add.
rwl list_to_set_disj_rm. apply ImpLAnd_rev.
rwl difference_singleton. exact Hf'.
}
(* ImpLOr *)
assert(HImpLOr : {φ1 & {φ2 & {φ3 & ((φ1 ∨ φ2) → φ3) ∈ Γ}}} +
{∀ φ1 φ2 φ3, ((φ1 ∨ φ2) → φ3) ∈ Γ -> False}). {
pose (fII := (fun θ => match θ with | (Or _ _) → _ => true | _ => false end)).
destruct (exists_dec fII Γ) as [(θ & Hin & Hθ) | Hf].
- left. subst fII. destruct θ. 1-4, 6: auto with *.
destruct θ1. 1-3, 5-6: auto with *. do 3 eexists; apply elem_of_list_In; eauto.
- right. intros ψ1 ψ2 ψ3 Hψ. rewrite elem_of_list_In in Hψ.
apply Hf in Hψ. subst fII. simpl in Hψ. tauto.
}
destruct HImpLOr as [(φ1&φ2&φ3&Hin)|HImpLOr].
{ apply elem_of_list_to_set_disj in Hin.
destruct (Hind ((φ2 → φ3) :: (φ1 → φ3) :: rm ((φ1 ∨ φ2) → φ3) Γ) Δ) as [Hp|Hf].
- order_tac.
- left. destruct Hp as [Hp _].
eexists; trivial. exhibit Hin 0. apply ImpLOr.
rwl list_to_set_disj_rm_rev. peapply Hp.
- right. intro Hf'. apply Hf.
do 2 rwl list_to_set_disj_env_add. rwl list_to_set_disj_rm. apply ImpLOr_rev.
rwl difference_singleton. exact Hf'.
}
(* non invertible right rules *)
(* ImpR is non-invertible in KM, but is in iSL *)
assert(HImpR : ∀ Δ2 Δ1, Δ1 ++ Δ2 = Δ -> {φ1 & {φ2 &
exists (_ : (list_to_set_disj Γ • φ1 ⊢KM list_to_set_disj (rm (φ1 → φ2) Δ) • φ2)),
exists (_ :(⊗ (list_to_set_disj Γ) • φ1 ⊢KM ∅ • φ2)), (φ1 → φ2) ∈ Δ2 }} +
{∀ φ1 φ2, (list_to_set_disj Γ • φ1 ⊢KM list_to_set_disj (rm (φ1 → φ2) Δ) • φ2) ->
(⊗ (list_to_set_disj Γ) • φ1 ⊢KM ∅ • φ2) ->
¬ (φ1 → φ2) ∈ Δ2 }).
{
clear Hbot Hvar HAndL HOrL HAndR HOrR HImpLOr HImpLVar HImpLOr.
induction Δ2 as [|θ Δ2]; intros Δ1 Heq.
- right. intros φ1 φ2 Hp1 Hp2 Hin. inversion Hin.
- destruct (IHΔ2 (Δ1 ++ [θ])) as [(φ1 & φ2 & Hp) | Hf].
+ auto with *.
+ left. do 2 eexists. destruct Hp as (Hp1 & Hp2 & Hin).
do 2 (eexists; eauto). auto with *.
+ destruct θ. 5 : {
destruct (Hind (θ1 :: Γ) (θ2 :: rm (θ1 → θ2) Δ)) as [Hp1 | Hf'].
- order_tac. repeat rewrite <- Permutation_middle. order_tac.
destruct sumbool_rec; [|tauto]. order_tac.
- destruct (Hind (θ1 :: □⁻¹ Γ) [θ2]) as [Hp2 | Hf'].
+ order_tac.
+ left. exists θ1; exists θ2. destruct Hp1 as [Hp1 _]. destruct Hp2 as [Hp2 _].
repeat split; try l_tac.
* rwl list_to_set_disj_env_add'. rpeapply Hp1.
* rwl list_to_set_disj_open_boxes.
rwl list_to_set_disj_env_add'. rpeapply Hp2.
* ms.
+ right; intros φ1 φ2 Hp1' Hp2 He; apply elem_of_list_In in He;
destruct He as [Heq''| Hin]; [|apply elem_of_list_In in Hin; eapply Hf; eauto].
dependent destruction Heq''. apply Hf'.
rwl list_to_set_disj_env_add.
rwl (symmetry (list_to_set_disj_open_boxes Γ)). rpeapply Hp2.
- right; intros φ1 φ2 Hp1 Hp2 He; apply elem_of_list_In in He;
destruct He as [Heq''| Hin]; [|apply elem_of_list_In in Hin; eapply Hf; eauto].
dependent destruction Heq''. apply Hf'.
rwl list_to_set_disj_env_add. rpeapply Hp1.
}
all: (right; intros φ1 φ2 Hp1 Hp2 He;
apply elem_of_list_In in He; destruct He as [Heq''| Hin];
[discriminate|apply elem_of_list_In in Hin; eapply Hf; eauto]).
}
destruct (HImpR Δ [] (app_nil_l _)) as [(φ1 & φ2 & Hp) | HfImpR].
{ left. destruct Hp as (Hp1 & Hp2 & Hin).
apply elem_of_list_to_set_disj in Hin.
eexists; trivial. exhibit Hin 0.
rwr list_to_set_disj_rm_rev. apply ImpR; assumption.
}
clear HImpR.
(* BoxR *)
assert(HBoxR :
{φ & exists (Hp : (⊗ (list_to_set_disj Γ) • □ φ ⊢ ∅ • φ)), (□ φ) ∈ Δ}
+ { ∀ φ, ⊗ (list_to_set_disj Γ) • □ φ ⊢ ∅ • φ -> ¬ (□ φ) ∈ Δ}).
{
clear Hbot Hvar HAndL HOrL HAndR HOrR HImpLOr HImpLVar HImpLOr HfImpR.
induction Δ as [|θ Δ].
- right. intros φ Hp Hin. inversion Hin.
- destruct IHΔ as [(φ & Hp) | Hf].
+ intros. apply Hind. unfold env_pair_order in *. etransitivity; eauto.
order_tac.
+ left. exists φ. destruct Hp as [Hp Hin]. split; trivial. ms.
+ destruct θ. 6: {
destruct (Hind ((□ θ) :: map open_box Γ) [θ])as [Hp|Hf'].
- order_tac.
- left. exists θ. destruct Hp as [Hp Hin]. simpl in Hp. eexists; eauto.
+ lazy_apply Hp. rewrite list_to_set_disj_open_boxes. ms.
+ ms.
- right. intros φ' Hp Hin. apply elem_of_list_In in Hin.
destruct Hin as [Heq |Hin].
+ inversion Heq; subst. apply Hf'. lazy_apply Hp.
rewrite list_to_set_disj_open_boxes. ms.
+ apply (Hf φ'); trivial. now apply elem_of_list_In.
}
all : auto with *.
}
destruct HBoxR as [(φ' & Hp)| HBoxR ].
{ left. destruct Hp as [Hp Hin]. subst. eexists; trivial.
apply elem_of_list_to_set_disj in Hin.
exhibit Hin 0. apply BoxR, Hp. }
(* non invertible left rules *)
(* ImpLImp *)
assert(HImpLImp : ∀Γ2 Γ1, Γ1 ++ Γ2 = Γ ->
{φ1 & {φ2 & {φ3 & exists _ :
(list_to_set_disj (rm ((φ1 → φ2) → φ3) Γ) • (φ2 → φ3) • φ1) ⊢ (list_to_set_disj Δ • φ2),
exists _ :
(⊗ (list_to_set_disj (rm ((φ1 → φ2) → φ3) Γ)) • (φ2 → φ3) • φ1) ⊢ (∅ • φ2),
exists _ : (list_to_set_disj (rm ((φ1 → φ2) → φ3) Γ) • φ3) ⊢ list_to_set_disj Δ,
((φ1 → φ2) → φ3) ∈ Γ2}}}
+ {∀ φ1 φ2 φ3, (list_to_set_disj (rm ((φ1 → φ2) → φ3) Γ) • (φ2 → φ3) • φ1) ⊢ (list_to_set_disj Δ • φ2)
-> ((⊗ (list_to_set_disj (rm ((φ1 → φ2) → φ3) Γ)) • (φ2 → φ3) • φ1) ⊢ (∅ • φ2))
-> (list_to_set_disj (rm ((φ1 → φ2) → φ3) Γ) • φ3) ⊢ list_to_set_disj Δ ->
((φ1 → φ2) → φ3) ∈ Γ2 → False}).
{
induction Γ2 as [|θ Γ2]; intros Γ1 Heq.
- right. intros φ1 φ2 φ3 _ _ _ Hin. inversion Hin.
- assert(Heq' : (Γ1 ++ [θ]) ++ Γ2 = Γ) by (subst; auto with * ).
destruct (IHΓ2 (Γ1 ++ [θ]) Heq') as [(φ1 & φ2 & φ3 & Hp)|Hf].
+ left. do 3 eexists. destruct Hp as (Hp1 & Hp2 & Hp3 & Hin).
do 3 (eexists; eauto). now right.
+ destruct θ.
5: destruct θ1.
9 : {
destruct (Hind (θ1_1 :: (θ1_2 → θ2) :: rm ((θ1_1 → θ1_2) → θ2) Γ)
(θ1_2 :: Δ)) as [Hp1 | Hf'].
- order_tac. rewrite <- Permutation_middle. unfold rm.
destruct form_eq_dec; [|tauto]. order_tac.
- destruct (Hind (θ2 :: rm ((θ1_1 → θ1_2) → θ2) Γ) Δ) as [Hp2 | Hf''].
+ order_tac. rewrite <- Permutation_middle. unfold rm.
destruct form_eq_dec; [|tauto]. order_tac.
+ destruct (Hind (θ1_1 :: (θ1_2 → θ2) :: □⁻¹ (rm ((θ1_1 → θ1_2) → θ2) Γ))
[θ1_2]) as [Hp3 | Hf''].
* order_tac. repeat rewrite <- Permutation_middle. simpl app.
destruct sumbool_rec; [|tauto]. order_tac.
* left. exists θ1_1; exists θ1_2; exists θ2.
destruct Hp1 as [Hp1 _]. destruct Hp2 as [Hp2 _]. destruct Hp3 as [Hp3 _].
repeat split; try l_tac.
-- rwr list_to_set_disj_env_add'. peapply Hp1.
-- peapply Hp3.
-- peapply Hp2.
-- ms.
* right; intros φ1 φ2 φ3 Hp1' Hp2' Hp3' He; apply elem_of_list_In in He;
destruct He as [Heq''| Hin]; [|apply elem_of_list_In in Hin; eapply Hf; eauto].
dependent destruction Heq''. apply Hf''.
lazy_apply Hp2'.
rewrite list_to_set_disj_open_boxes. ms.
+ right; intros φ1 φ2 φ3 Hp1' Hp2 Hp3 He; apply elem_of_list_In in He;
destruct He as [Heq''| Hin]; [|apply elem_of_list_In in Hin; eapply Hf; eauto].
dependent destruction Heq''. apply Hf''. peapply Hp3.
- right; intros φ1 φ2 φ3 Hp1 Hp2 Hp3 He; apply elem_of_list_In in He;
destruct He as [Heq''| Hin]; [|apply elem_of_list_In in Hin; eapply Hf; eauto].
dependent destruction Heq''. apply Hf'.
rwr list_to_set_disj_env_add. peapply Hp1.
}
all: (right; intros φ1 φ2 φ3 Hp1 Hp2 Hp3 He;
apply elem_of_list_In in He; destruct He as [Heq''| Hin];
[discriminate|apply elem_of_list_In in Hin; eapply Hf; eauto]).
}
destruct (HImpLImp Γ [] (app_nil_l _)) as [(φ1 & φ2 & φ3 & Hp)|HfImpl].
{ left. destruct Hp as (Hp1 & Hp2 & Hp3 & Hin).
apply elem_of_list_to_set_disj in Hin.
eexists; trivial. exhibit Hin 0.
rwl list_to_set_disj_rm_rev.
apply ImpLImp; assumption.
}
(* ImpLBox *)
assert(HImpLBox : ∀Γ2 Γ1, Γ1 ++ Γ2 = Γ ->
{φ1 & {φ2
& exists _ : (⊗(list_to_set_disj (rm ((□ φ1) → φ2) Γ)) • □ φ1 • φ2) ⊢ ∅ • φ1,
exists _ : list_to_set_disj (rm ((□ φ1) → φ2) Γ) • φ2 ⊢ list_to_set_disj Δ,
((□ φ1) → φ2) ∈ Γ2}}
+ {∀ φ1 φ2, ((⊗ (list_to_set_disj (rm ((□ φ1) → φ2) Γ)) • □ φ1 • φ2) ⊢ ∅ • φ1)
-> list_to_set_disj (rm ((□ φ1) → φ2) Γ) • φ2 ⊢ list_to_set_disj Δ ->
((□ φ1) → φ2) ∈ Γ2 → False}).
{
induction Γ2 as [|θ Γ2]; intros Γ1 Heq.
- right. intros φ1 φ2 _ _ Hin. inversion Hin.
- assert(Heq' : (Γ1 ++ [θ]) ++ Γ2 = Γ) by (subst; auto with * ).
destruct (IHΓ2 (Γ1 ++ [θ]) Heq') as [(φ1 & φ2 & Hp)|Hf].
+ left. do 2 (eexists; eauto).
destruct Hp as (Hp1 & Hp2 & Hin). repeat eexists; eauto. subst. now right.
+ destruct θ. 5: destruct θ1.
10 : {
destruct (Hind (θ2 :: (□θ1) :: map open_box (rm ((□ θ1) → θ2) Γ)) [θ1])
as [Hp1 | Hf'].
- order_tac. repeat rewrite <- Permutation_middle. unfold rm.
destruct form_eq_dec; [|tauto]. fold rm. order_tac.
- destruct (Hind (θ2 :: rm ((□ θ1) → θ2) Γ) Δ) as [Hp2 | Hf''].
+ order_tac. rewrite <- Permutation_middle. unfold rm.
destruct form_eq_dec; [|tauto]. order_tac.
+ left. exists θ1, θ2. destruct Hp1 as (Hp1 & _). destruct Hp2 as (Hp2 & _).
repeat eexists; [peapply Hp1| peapply Hp2 | ms].
+ right; intros φ1 φ2 Hp1' Hp2 He; apply elem_of_list_In in He;
destruct He as [Heq''| Hin]; [|apply elem_of_list_In in Hin; eapply Hf; eauto].
dependent destruction Heq''. apply Hf''. peapply Hp2.
- right; intros φ1 φ2 Hp1 Hp2 He; apply elem_of_list_In in He;
destruct He as [Heq''| Hin]; [|apply elem_of_list_In in Hin; eapply Hf; eauto].
dependent destruction Heq''. subst. apply Hf'.
(erewrite proper_Provable; [| |reflexivity]); [eapply Hp1|].
repeat rewrite <- ?list_to_set_disj_env_add, list_to_set_disj_open_boxes.
ms.
}
all: (right ; try destruct K; trivial; intros φ1 φ2 Hp1 Hp2 He;
apply elem_of_list_In in He; destruct He as [Heq''| Hin];
[discriminate|apply elem_of_list_In in Hin; eapply Hf; eauto]).
}
destruct (HImpLBox Γ [] (app_nil_l _)) as [(φ1 & φ2 & Hp)|HfImpLBox].
{ left. destruct Hp as (Hp1 & Hp2 & Hin). eexists; trivial.
apply elem_of_list_to_set_disj in Hin.
exhibit Hin 0. rwl list_to_set_disj_rm_rev. apply ImpLBox; assumption.
}
(* All the sequent rules have been applied *)
clear Hind HImpLImp HImpLBox.
right.
intro Hp. dependent destruction Hp; subst; try eqt Γ; try eqt Δ; eauto 2.
- eapply HAndR; eauto.
- eapply HOrR; eauto.
- eapply HfImpR; eauto. rwr Heq. exact Hp1.
- eapply HImpLVar; eauto. apply elem_of_list_to_set_disj.
match goal with H : _ = list_to_set_disj Γ |- _ => setoid_rewrite <- H end; ms.
- eapply HfImpl; eauto; now rwl Heq.
- eapply HfImpLBox; eauto.
+ now rwl (proper_open_boxes _ _ Heq).
+ now rwl Heq.
- eapply HBoxR; eauto.
Defined.
Global Infix "⊢?" := Provable_dec (at level 80).
Lemma Provable_dec_of_Prop Γ Δ:
(∃ _ : list_to_set_disj Γ ⊢ list_to_set_disj Δ, True) ->
(list_to_set_disj Γ ⊢ list_to_set_disj Δ).
Proof.
destruct (Proof_tree_dec Γ Δ) as [[Hφ1' _] | Hf']. tauto.
intros Hf. exfalso. destruct Hf as [Hf _]. tauto.
Qed.