KM.Sequent.PropQuantifiers
Propositional Quantifiers
Require Import Sequents syntax syntax_facts.
Require Import SequentProps Order Simplifications Optimizations.
From Stdlib Require Import Program.Equality.
From Equations Require Import Equations.
(* We define propositional quantifiers given a simplification method
for formulas and contexts. *)
Module PropQuant (Import S : SimpT).
Throughout the construction and proof, we fix a variable p, with respect to
which the propositional quantifier will be computed.
We define the formulas Eφ and Aφ associated to any formula φ. This
mimics Pitts' Table 5 for IPC, together with a (mostly automatic)
proof that the definition terminates
(* Solves the obligations of the following programs *)
Obligation Tactic :=
intros; order_tac.
Open Scope list_scope.
First, the implementation of the rules for calculating E. The names of the rules
refer to the table in Pitts' paper. note the use of "lazy" conjunctions, disjunctions and implications
Equations e_rule {Γ: list form}
{E : ∀ Γ0 (Hpe : (Γ0, []) ≺· (Γ, [])), form}
{A : ∀ pe (Hpe : pe ≺· (Γ, [])), form}
(θ: form) {Hin : θ ∈ Γ} : form :=
| Bot := ⊥;
| Var q :=
if decide (p = q) then ⊤ (* default *)
else q (* E1 modified *);
(* E2 *)
| δ₁ ∧ δ₂ := let Γ' := rm (δ₁ ∧ δ₂) Γ in
E (Γ' • δ₁ • δ₂) _;
(* E3 *)
| δ₁ ∨ δ₂ := let Γ' := rm (δ₁ ∨ δ₂) Γ in
E (Γ' • δ₁) _ ⊻ E (Γ' • δ₂) _;
| Var q → δ := let Γ' := rm (Var q → δ) Γ in
if decide (Var q ∈ Γ) then E (Γ'•δ) _ (* E5 modified *)
else if decide (p = q) then ⊤
else q ⇢ (E (Γ'•δ) _) ; (* E4 *)
(* E6 *)
| (δ₁ ∧ δ₂)→ δ₃ := let Γ' := rm ((δ₁ ∧ δ₂)→ δ₃) Γ in
E (Γ'•(δ₁ → (δ₂ → δ₃))) _;
(* E7 *)
| (δ₁ ∨ δ₂)→ δ₃ := let Γ' := rm ((δ₁ ∨ δ₂)→ δ₃) Γ in
E (Γ' • (δ₁ → δ₃)•(δ₂ → δ₃)) _;
(* E8 modified *)
| (δ₁→ δ₂)→ δ₃ := let Γ' := rm ((δ₁→ δ₂)→ δ₃) Γ in
(□ (E (□⁻¹ Γ' • (δ₂ → δ₃) • δ₁) _ ⇢ A (□⁻¹ Γ' • (δ₂ → δ₃) • δ₁, [δ₂]) _)) ⇢
(E (Γ'•δ₃) _ ⊻ E (Γ'• (δ₂ → δ₃) • δ₁) _);
(* Added disjunct to E8 *)
| ⊥ → _ := ⊤;
(* E9 *)
| □ φ := □E (□⁻¹ Γ) _;
(* E10 *)
| □δ1 → δ2 := let Γ' := rm (□δ1 → δ2) Γ in
(□(E((□⁻¹ Γ') • □δ1 • δ2) _
⇢ A((□⁻¹ Γ') • □δ1 • δ2, [δ1]) _))
⇢ E(Γ' • δ2) _
.
Next Obligation.
rewrite <- Permutation_cons_append, <- Permutation_rm, app_nil_r by trivial.
eapply env_order_open_box; eauto.
Qed.
Hint Extern 2 (_ <= _) => lia : order.
The implementation of the rules for defining A is separated into two pieces.
Referring to Table 5 in Pitts, the definition a_rule_l handles left rules,
while definition a_rule_r handles right rules.
Equations a_rule_l {Γ Δ : list form}
{E : ∀ Γ0 (Hpe : (Γ0, []) ≺· (Γ, Δ)), form}
{A : ∀ pe (Hpe : pe ≺· (Γ, Δ)), form}
(θ: form) {Hin : θ ∈ Γ} : form :=
| Var q :=
if decide (p = q) then
if decide (Var p ∈ Δ) then ⊤ (* A10 *)
else ⊥
else ⊥; (* A1 modified : A (Γ', Δ) can be removed *)
(* A2 *)
| δ₁ ∧ δ₂ := let Γ' := rm (δ₁ ∧ δ₂) Γ in A ((Γ'•δ₁)•δ₂, Δ) _;
(* A3 *)
| δ₁ ∨ δ₂ := let Γ' := rm (δ₁ ∨ δ₂) Γ in
(E (Γ'•δ₁) _ ⇢ A (Γ'•δ₁, Δ) _)
⊼ (E (Γ'•δ₂) _ ⇢ A (Γ'•δ₂, Δ) _);
| Var q → δ := let Γ' := rm (Var q → δ) Γ in
if decide (Var q ∈ Γ) then A (Γ'•δ, Δ) _ (* A5 modified *)
else if decide (p = q) then ⊥
else q ⊼ A (Γ'•δ, Δ) _; (* A4 *)
(* A6 *)
| (δ₁ ∧ δ₂)→ δ₃ := let Γ' := rm ((δ₁ ∧ δ₂)→ δ₃) Γ in
A (Γ'•(δ₁ → (δ₂ → δ₃)), Δ) _;
(* A7 *)
| (δ₁ ∨ δ₂)→ δ₃ := let Γ' := rm ((δ₁ ∨ δ₂)→ δ₃) Γ in
A ((Γ'•(δ₁ → δ₃))•(δ₂ → δ₃), Δ) _;
(* A8 modified*)
| (δ₁→ δ₂)→ δ₃ := let Γ' := rm ((δ₁→ δ₂)→ δ₃) Γ in
(E (Γ'•(δ₂ → δ₃) • δ₁) _ ⇢ A (Γ'•(δ₂ → δ₃) • δ₁, Δ) _) ⊼
(□ (E ((□⁻¹ Γ') • (δ₂ → δ₃) • δ₁) _ ⇢ A ((□⁻¹ Γ') •(δ₂ → δ₃) • δ₁, [δ₂]) _)) ⊼
(E (Γ'• δ₃) _ ⇢ A (Γ'• δ₃, Δ) _);
| Bot := ⊥;
| Bot → _ := ⊥;
| □δ := ⊥;
(* A15 *)
| (□δ1) → δ2 :=
let Γ' := rm ((□δ1) → δ2) Γ in
let Γ'' := □⁻¹ Γ' • □δ1 • δ2 in
(□(E(Γ'') _ ⇢ A(Γ'', [δ1]) _)) ∧ A(Γ' • δ2, Δ) _
(* using ⊼ here breaks congruence *)
.
Equations a_rule_r {Γ Δ : list form}
{E : ∀ Γ0 (Hpe : (Γ0, []) ≺· (Γ, Δ)), form}
{A : ∀ pe (Hpe : pe ≺· (Γ, Δ)), form}
(θ: form) {Hin : θ ∈ Δ} : form :=
| Var q :=
if decide (p = q) (* This could be changed to p∈Vars(Δ) *)
then ⊥
else Var q; (* A9 *)
(* A11 *)
| ϕ₁ ∧ ϕ₂ := let Δ' := rm (ϕ₁ ∧ ϕ₂) Δ in A (Γ, Δ' • ϕ₁) _ ⊼ A (Γ, Δ' • ϕ₂) _;
(* A12 *)
| ϕ₁ ∨ ϕ₂ := let Δ' := rm (ϕ₁ ∨ ϕ₂) Δ in A (Γ, Δ' • ϕ₁ • ϕ₂) _ ;
(* A13 *)
| ϕ₁→ ϕ₂ := let Δ' := rm (ϕ₁→ ϕ₂) Δ in
(□ (E ((□⁻¹ Γ) • ϕ₁) _ ⇢ A ((□⁻¹ Γ) • ϕ₁, [ϕ₂]) _)) ⊼
(E (Γ • ϕ₁) _ ⇢ A (Γ • ϕ₁, Δ' • ϕ₂) _) ;
| Bot := ⊥;
(* A14 *)
| □δ := □((E ((□⁻¹ Γ) • □δ) _) ⇢ A((□⁻¹ Γ) • □δ, [δ]) _)
.
Instance WF_pointed_env_order : WellFounded env_pair_order := wf_pointed_order.
Obligation Tactic := (eapply env_order_lt_le_trans; [eassumption|]; order_tac).
Equations EA (b : bool) (pe : env_pair) : form by wf pe env_pair_order :=
(* E *)
EA true pe :=
let Γ := simp_envL pe.1 in
let E Γ0 H := EA true (Γ0, []) in
let A pe H := EA false pe in
⋀ (in_map Γ (@e_rule Γ E A));
(* A *)
EA false pe :=
let Γ := simp_envL pe.1 in
let Δ := simp_envR pe.2 in
let E Γ0 H := EA true (Γ0, []) in
let A pe H := EA false pe in
⋁ ((in_map Γ (@a_rule_l Γ Δ E A)) ++ (in_map Δ (@a_rule_r Γ Δ E A))).
Definition E Γ := EA true (Γ, []).
Definition A := EA false.
Definition Ef (ψ : form) := simp_form (E ([simp_form ψ])).
Definition Af (ψ : form) := simp_form (A ([], [simp_form ψ])).
End PropQuantDefinition.
Lemma e_rule_cong_strong p Γ θ (Hin1 Hin2: θ ∈ Γ) E1 A1 E2 A2:
(forall pe Hpe1 Hpe2, E1 pe Hpe1 = E2 pe Hpe2) ->
(forall pe Hpe1 Hpe2, A1 pe Hpe1 = A2 pe Hpe2) ->
@e_rule p Γ E1 A1 θ Hin1 = @e_rule p Γ E2 A2 θ Hin2.
Proof.
intros HeqE HeqA.
destruct θ; simp a_rule_l; simp e_rule; simpl; trivial; repeat (destruct decide).
- f_equal; repeat erewrite ?HeqE, ?HeqA; trivial;
destruct θ1; try (destruct decide); trivial; simp e_rule; simpl;
repeat erewrite ?HeqE, ?HeqA; trivial.
- destruct θ1; try (destruct decide); trivial; simp e_rule; simpl;
repeat erewrite ?HeqE, ?HeqA; trivial.
repeat (destruct decide; trivial). f_equal ; f_equal ; apply HeqE.
- f_equal. apply HeqE.
Qed.
Lemma a_rule_l_cong_strong p Γ Δ θ Hin1 Hin2 E1 A1 E2 A2:
(forall pe Hpe1 Hpe2, E1 pe Hpe1 = E2 pe Hpe2) ->
(forall pe Hpe1 Hpe2, A1 pe Hpe1 = A2 pe Hpe2) ->
@a_rule_l p Γ Δ E1 A1 θ Hin1 = @a_rule_l p Γ Δ E2 A2 θ Hin2.
Proof.
intros HeqE HeqA.
destruct θ; simp a_rule_l; simpl; trivial; repeat (destruct decide).
- f_equal; repeat erewrite ?HeqE, ?HeqA; trivial;
destruct θ1; try (destruct decide); trivial; simp a_rule_l; simpl;
repeat erewrite ?HeqE, ?HeqA; trivial.
- destruct θ1; try (destruct decide); trivial; simp a_rule_l; simpl;
repeat erewrite ?HeqE, ?HeqA; trivial.
repeat (destruct decide; trivial). f_equal. apply HeqA.
Qed.
Lemma a_rule_r_cong_strong p Γ Δ θ Hin1 Hin2 E1 A1 E2 A2:
(forall pe Hpe1 Hpe2, E1 pe Hpe1 = E2 pe Hpe2) ->
(forall pe Hpe1 Hpe2, A1 pe Hpe1 = A2 pe Hpe2) ->
@a_rule_r p Γ Δ E1 A1 θ Hin1 = @a_rule_r p Γ Δ E2 A2 θ Hin2.
Proof.
intros HeqE HeqA.
destruct θ; simp a_rule_r; simpl; trivial; repeat (destruct decide).
- f_equal; repeat erewrite ?HeqE, ?HeqA; trivial;
destruct θ1; try (destruct decide); trivial; simp a_rule_l; simpl;
repeat erewrite ?HeqE, ?HeqA; trivial.
- destruct θ1; try (destruct decide); trivial; simp a_rule_l; simpl;
repeat erewrite ?HeqE, ?HeqA; trivial.
- destruct θ; try (destruct decide); trivial; simp a_rule_l; simpl;
repeat erewrite ?HeqE, ?HeqA; trivial.
Qed.
End PropQuant.
Module PropQuantProp (Import S : SimpT) (Import SoundS : SoundSimpT S).
Module Import SP := MakeSimpProps S.
Module Import PropQuandDef := PropQuant S.
{E : ∀ Γ0 (Hpe : (Γ0, []) ≺· (Γ, Δ)), form}
{A : ∀ pe (Hpe : pe ≺· (Γ, Δ)), form}
(θ: form) {Hin : θ ∈ Γ} : form :=
| Var q :=
if decide (p = q) then
if decide (Var p ∈ Δ) then ⊤ (* A10 *)
else ⊥
else ⊥; (* A1 modified : A (Γ', Δ) can be removed *)
(* A2 *)
| δ₁ ∧ δ₂ := let Γ' := rm (δ₁ ∧ δ₂) Γ in A ((Γ'•δ₁)•δ₂, Δ) _;
(* A3 *)
| δ₁ ∨ δ₂ := let Γ' := rm (δ₁ ∨ δ₂) Γ in
(E (Γ'•δ₁) _ ⇢ A (Γ'•δ₁, Δ) _)
⊼ (E (Γ'•δ₂) _ ⇢ A (Γ'•δ₂, Δ) _);
| Var q → δ := let Γ' := rm (Var q → δ) Γ in
if decide (Var q ∈ Γ) then A (Γ'•δ, Δ) _ (* A5 modified *)
else if decide (p = q) then ⊥
else q ⊼ A (Γ'•δ, Δ) _; (* A4 *)
(* A6 *)
| (δ₁ ∧ δ₂)→ δ₃ := let Γ' := rm ((δ₁ ∧ δ₂)→ δ₃) Γ in
A (Γ'•(δ₁ → (δ₂ → δ₃)), Δ) _;
(* A7 *)
| (δ₁ ∨ δ₂)→ δ₃ := let Γ' := rm ((δ₁ ∨ δ₂)→ δ₃) Γ in
A ((Γ'•(δ₁ → δ₃))•(δ₂ → δ₃), Δ) _;
(* A8 modified*)
| (δ₁→ δ₂)→ δ₃ := let Γ' := rm ((δ₁→ δ₂)→ δ₃) Γ in
(E (Γ'•(δ₂ → δ₃) • δ₁) _ ⇢ A (Γ'•(δ₂ → δ₃) • δ₁, Δ) _) ⊼
(□ (E ((□⁻¹ Γ') • (δ₂ → δ₃) • δ₁) _ ⇢ A ((□⁻¹ Γ') •(δ₂ → δ₃) • δ₁, [δ₂]) _)) ⊼
(E (Γ'• δ₃) _ ⇢ A (Γ'• δ₃, Δ) _);
| Bot := ⊥;
| Bot → _ := ⊥;
| □δ := ⊥;
(* A15 *)
| (□δ1) → δ2 :=
let Γ' := rm ((□δ1) → δ2) Γ in
let Γ'' := □⁻¹ Γ' • □δ1 • δ2 in
(□(E(Γ'') _ ⇢ A(Γ'', [δ1]) _)) ∧ A(Γ' • δ2, Δ) _
(* using ⊼ here breaks congruence *)
.
Equations a_rule_r {Γ Δ : list form}
{E : ∀ Γ0 (Hpe : (Γ0, []) ≺· (Γ, Δ)), form}
{A : ∀ pe (Hpe : pe ≺· (Γ, Δ)), form}
(θ: form) {Hin : θ ∈ Δ} : form :=
| Var q :=
if decide (p = q) (* This could be changed to p∈Vars(Δ) *)
then ⊥
else Var q; (* A9 *)
(* A11 *)
| ϕ₁ ∧ ϕ₂ := let Δ' := rm (ϕ₁ ∧ ϕ₂) Δ in A (Γ, Δ' • ϕ₁) _ ⊼ A (Γ, Δ' • ϕ₂) _;
(* A12 *)
| ϕ₁ ∨ ϕ₂ := let Δ' := rm (ϕ₁ ∨ ϕ₂) Δ in A (Γ, Δ' • ϕ₁ • ϕ₂) _ ;
(* A13 *)
| ϕ₁→ ϕ₂ := let Δ' := rm (ϕ₁→ ϕ₂) Δ in
(□ (E ((□⁻¹ Γ) • ϕ₁) _ ⇢ A ((□⁻¹ Γ) • ϕ₁, [ϕ₂]) _)) ⊼
(E (Γ • ϕ₁) _ ⇢ A (Γ • ϕ₁, Δ' • ϕ₂) _) ;
| Bot := ⊥;
(* A14 *)
| □δ := □((E ((□⁻¹ Γ) • □δ) _) ⇢ A((□⁻¹ Γ) • □δ, [δ]) _)
.
Instance WF_pointed_env_order : WellFounded env_pair_order := wf_pointed_order.
Obligation Tactic := (eapply env_order_lt_le_trans; [eassumption|]; order_tac).
Equations EA (b : bool) (pe : env_pair) : form by wf pe env_pair_order :=
(* E *)
EA true pe :=
let Γ := simp_envL pe.1 in
let E Γ0 H := EA true (Γ0, []) in
let A pe H := EA false pe in
⋀ (in_map Γ (@e_rule Γ E A));
(* A *)
EA false pe :=
let Γ := simp_envL pe.1 in
let Δ := simp_envR pe.2 in
let E Γ0 H := EA true (Γ0, []) in
let A pe H := EA false pe in
⋁ ((in_map Γ (@a_rule_l Γ Δ E A)) ++ (in_map Δ (@a_rule_r Γ Δ E A))).
Definition E Γ := EA true (Γ, []).
Definition A := EA false.
Definition Ef (ψ : form) := simp_form (E ([simp_form ψ])).
Definition Af (ψ : form) := simp_form (A ([], [simp_form ψ])).
End PropQuantDefinition.
Lemma e_rule_cong_strong p Γ θ (Hin1 Hin2: θ ∈ Γ) E1 A1 E2 A2:
(forall pe Hpe1 Hpe2, E1 pe Hpe1 = E2 pe Hpe2) ->
(forall pe Hpe1 Hpe2, A1 pe Hpe1 = A2 pe Hpe2) ->
@e_rule p Γ E1 A1 θ Hin1 = @e_rule p Γ E2 A2 θ Hin2.
Proof.
intros HeqE HeqA.
destruct θ; simp a_rule_l; simp e_rule; simpl; trivial; repeat (destruct decide).
- f_equal; repeat erewrite ?HeqE, ?HeqA; trivial;
destruct θ1; try (destruct decide); trivial; simp e_rule; simpl;
repeat erewrite ?HeqE, ?HeqA; trivial.
- destruct θ1; try (destruct decide); trivial; simp e_rule; simpl;
repeat erewrite ?HeqE, ?HeqA; trivial.
repeat (destruct decide; trivial). f_equal ; f_equal ; apply HeqE.
- f_equal. apply HeqE.
Qed.
Lemma a_rule_l_cong_strong p Γ Δ θ Hin1 Hin2 E1 A1 E2 A2:
(forall pe Hpe1 Hpe2, E1 pe Hpe1 = E2 pe Hpe2) ->
(forall pe Hpe1 Hpe2, A1 pe Hpe1 = A2 pe Hpe2) ->
@a_rule_l p Γ Δ E1 A1 θ Hin1 = @a_rule_l p Γ Δ E2 A2 θ Hin2.
Proof.
intros HeqE HeqA.
destruct θ; simp a_rule_l; simpl; trivial; repeat (destruct decide).
- f_equal; repeat erewrite ?HeqE, ?HeqA; trivial;
destruct θ1; try (destruct decide); trivial; simp a_rule_l; simpl;
repeat erewrite ?HeqE, ?HeqA; trivial.
- destruct θ1; try (destruct decide); trivial; simp a_rule_l; simpl;
repeat erewrite ?HeqE, ?HeqA; trivial.
repeat (destruct decide; trivial). f_equal. apply HeqA.
Qed.
Lemma a_rule_r_cong_strong p Γ Δ θ Hin1 Hin2 E1 A1 E2 A2:
(forall pe Hpe1 Hpe2, E1 pe Hpe1 = E2 pe Hpe2) ->
(forall pe Hpe1 Hpe2, A1 pe Hpe1 = A2 pe Hpe2) ->
@a_rule_r p Γ Δ E1 A1 θ Hin1 = @a_rule_r p Γ Δ E2 A2 θ Hin2.
Proof.
intros HeqE HeqA.
destruct θ; simp a_rule_r; simpl; trivial; repeat (destruct decide).
- f_equal; repeat erewrite ?HeqE, ?HeqA; trivial;
destruct θ1; try (destruct decide); trivial; simp a_rule_l; simpl;
repeat erewrite ?HeqE, ?HeqA; trivial.
- destruct θ1; try (destruct decide); trivial; simp a_rule_l; simpl;
repeat erewrite ?HeqE, ?HeqA; trivial.
- destruct θ; try (destruct decide); trivial; simp a_rule_l; simpl;
repeat erewrite ?HeqE, ?HeqA; trivial.
Qed.
End PropQuant.
Module PropQuantProp (Import S : SimpT) (Import SoundS : SoundSimpT S).
Module Import SP := MakeSimpProps S.
Module Import PropQuandDef := PropQuant S.
This section contains the proof of Proposition 5, the main correctness result,
stating that the E- and A-formulas defined above are indeed existential and
universal propositional quantified versions of the original formula, respectively.
(i) Variables
In this subsection we prove (i), which states that the variable p no longer
occurs in the E- and A-formulas, and that the E- and A-formulas contain no
more variables than the original formula.
(* A general tactic for variable occurrences *)
Ltac vars_tac :=
intros; subst;
repeat match goal with
| HE : context [occurs_in ?x (?E _ _)], H : occurs_in ?x (?E _ _) |- _ =>
apply HE in H
end;
intuition;
repeat match goal with | H : exists x, _ |- _ => destruct H end;
intuition;
simpl in *; in_tac; try (split; [tauto || auto with *|]); simpl in *;
try match goal with
| H : ?a ∈ [] |- _ => inversion H
| H : occurs_in _ (?a ⇢ (?b ⇢ ?c)) |- _ => apply occurs_in_make_impl2 in H
| H : occurs_in _ (?a ⇢ ?b) |- _ => apply occurs_in_make_impl in H
| H : occurs_in _ (?a ⊻ ?b) |- _ => apply occurs_in_make_disj in H
| H : occurs_in _ (?a ⊼ ?b) |- _ => apply occurs_in_make_conj in H
| H : _ ∈ @in_map _ _ _ |- _ => apply in_in_map in H; decompose record H
| H : occurs_in _ (conjunction _) |- _ => apply variables_conjunction in H
|H1 : ?x0 ∈ (⊗ ?Γ), H2 : occurs_in ?x ?x0 |- _ =>
apply (occurs_in_open_boxes _ _ _ H2) in H1
|H1 : ?x0 ∈ (map open_box ?Γ), H2 : occurs_in ?x ?x0 |- _ =>
apply (occurs_in_map_open_box _ _ _ H2) in H1
end; repeat rewrite elem_of_cons in * ; intuition; subst;
repeat match goal with | H : exists x, _ |- _ => destruct H end; intuition;
try multimatch goal with
| H : ?θ0 ∈ ?Γ0 |- context [exists θ, θ ∈ ?Γ /\ occurs_in ?x θ] =>
solve[try right; exists θ; split; [eauto using remove_include|]; simpl; eauto] end;
try solve[eexists; split; simpl; eauto using remove_include ; simpl; eauto];
try solve[eexists; split; simpl; [|eauto]; simpl; eauto using remove_include].
Ltac occ :=
repeat setoid_rewrite env_in_add; intuition; subst; intuition; simpl in *;
repeat multimatch goal with
| Hocc : ∀ φ0, φ0 ∈ (?Δ • ?a) → occurs_in _ φ0 -> False |- _ =>
destruct (Hocc a); [ms|]; simpl; intuition
| Hin : ?φ ∈ ?Γ ∖ _ |- _ => let Hin' := fresh "Hin'" in
try assert(Hin' : φ ∈ Γ) by ms; clear Hin
| Hin : ?φ ∈ ?Γ, Hocc: ∀ φ0, φ0 ∈ ?Γ → occurs_in _ φ0 → False |- _ =>
apply Hocc in Hin; intuition; simpl; intuition; clear Hin
| Hin : ?φ ∈ (⊗ ?Γ), Hocc: ∀ φ0, φ0 ∈ ?Γ → occurs_in _ φ0 → False |- _ =>
edestruct occurs_in_open_boxes in Hin; eauto; intuition
| Hin : ?φ ∈ ?Γ, Hocc: ∀ φ0, φ0 ∈ (?Γ • ?a) → occurs_in _ φ0 → False |- _ =>
let Hin' := fresh "Hin" in assert(Hin' : φ ∈ (Γ • a)) by ms;
apply Hocc in Hin'; intuition; simpl; intuition; clear Hin
| Hin : ?φ ∈ (⊗ (?Γ∖ _)), Hocc: ∀ φ0, φ0 ∈ ?Γ → occurs_in _ φ0 → False |- _ =>
edestruct occurs_in_open_boxes in Hin; eauto; intuition
end;
intuition;
try match goal with | Hin : (?a ∈ ∅) |- _ => inversion Hin end.
Lemma e_rule_vars Γ (θ : form) (Hin : θ ∈ Γ)
(E0 : ∀ Γ0 (Hpe : (Γ0, []) ≺· (Γ, [])), form)
(A0 : ∀ pe (Hpe : pe ≺· (Γ, [])), form)
x
(HE0 : ∀ Γ0 HΓ0,
(occurs_in x (E0 Γ0 HΓ0) -> x ≠ p ∧ ∃ θ, (θ ∈ Γ0) /\ occurs_in x θ))
(HA0 : ∀ pe Hpe,
(occurs_in x (A0 pe Hpe) -> x ≠ p ∧ (∃ θ, (θ ∈ pe.1 \/ θ ∈ pe.2) /\ occurs_in x θ))) :
occurs_in x (@e_rule p _ E0 A0 θ Hin) -> x ≠ p ∧ ∃ θ', θ' ∈ Γ/\ occurs_in x θ'.
Proof.
destruct θ; simp e_rule; simpl in *; try tauto; try solve [repeat case decide; repeat vars_tac].
destruct θ1; simp e_rule; repeat case decide; repeat vars_tac.
exists (# n → θ2); split; simpl; eauto.
Qed.
Lemma a_rule_l_vars Γ θ Hin Δ
(E0 : ∀ Γ0 (Hpe : (Γ0, []) ≺· (Γ, Δ)), form)
(A0 : ∀ pe (Hpe : pe ≺· (Γ, Δ)), form)
x
(HE0 : ∀ Γ0 HΓ0,
(occurs_in x (E0 Γ0 HΓ0) -> x ≠ p ∧ ∃ θ, (θ ∈ Γ0) /\ occurs_in x θ))
(HA0 : ∀ pe Hpe,
(occurs_in x (A0 pe Hpe) -> x ≠ p ∧ (∃ θ, (θ ∈ pe.1 \/ θ ∈ pe.2) /\ occurs_in x θ))) :
occurs_in x (@a_rule_l p _ _ E0 A0 θ Hin) -> x ≠ p ∧ (∃ θ, (θ ∈ Γ \/ θ ∈ Δ) /\ occurs_in x θ).
Proof.
destruct θ; simp a_rule_l; try tauto; try solve [repeat case decide; repeat vars_tac].
destruct θ1; simp a_rule_l; repeat case decide; try solve[repeat vars_tac].
- simpl. intro Hin'. vars_tac. exists (# n → θ2); split; simpl; eauto.
- intro Hf. repeat (apply occurs_in_make_conj in Hf as [Hf | Hf]); repeat vars_tac.
Qed.
Lemma a_rule_r_vars Γ Δ (θ : form) (Hin : θ ∈ Δ)
(E0 : ∀ Γ0 (Hpe : (Γ0, []) ≺· (Γ, Δ)), form)
(A0 : ∀ pe (Hpe : pe ≺· (Γ, Δ)), form)
x
(HE0 : ∀ Γ0 HΓ0,
(occurs_in x (E0 Γ0 HΓ0) -> x ≠ p ∧ ∃ θ, (θ ∈ Γ0) /\ occurs_in x θ))
(HA0 : ∀ pe Hpe,
(occurs_in x (A0 pe Hpe) -> x ≠ p ∧ (∃ θ, (θ ∈ pe.1 \/ θ ∈ pe.2) /\ occurs_in x θ))) :
occurs_in x (@a_rule_r p _ _ E0 A0 θ Hin) -> x ≠ p ∧ ∃ θ, (θ ∈ Γ \/ θ ∈ Δ) /\ occurs_in x θ.
Proof.
destruct θ; simp a_rule_r; simpl; try tauto; try solve [repeat case decide; repeat vars_tac].
Qed.
Proposition EA_vars Γ Δ x:
(occurs_in x (E p Γ) -> x <> p /\ ∃ θ, θ ∈ Γ /\ occurs_in x θ) /\
(occurs_in x (A p (Γ, Δ)) -> x <> p /\ (∃ θ, (θ ∈ Γ \/ θ ∈ Δ) /\ occurs_in x θ)).
Proof.
remember (Γ, Δ) as pe.
replace Γ with pe.1 by now subst.
replace Δ with pe.2 by now subst. clear Heqpe Γ Δ. revert pe.
refine (@well_founded_induction _ _ wf_pointed_order _ _).
intros [Γ Δ] Hind. simpl. split.
(* E *)
- intros Hocc.
unfold E, A in Hocc. simp EA in Hocc; simpl in Hocc.
apply variables_conjunction in Hocc as (φ&Hin&Hφ).
apply in_in_map in Hin as (ψ&Hin&Heq). subst φ.
apply e_rule_vars in Hφ as [Hneq [θ [Hθ Hocc]]].
+ split; trivial. destruct (equiv_envL_vars Γ x) as [θ'' [Hθ'' Hocc']];
eexists; split; eauto.
+ intros Γ0 Ho Hocc. fold (E p Γ0) in Hocc. eapply (Hind (Γ0, [])) in Hocc.
* exact Hocc.
* auto with order.
+ intros pe Hpe. simp EA. simpl. intro Hocc.
apply variables_disjunction in Hocc as (φ&Hin'&Hφ').
apply elem_of_app in Hin' as [Hinl | Hinr].
* apply in_in_map in Hinl as (ψ'&Hin'&Heq). subst φ.
apply a_rule_l_vars in Hφ' as [Hneq [θ [[Hθ|Hθ] Hocc]]].
-- split; trivial.
destruct (equiv_envL_vars pe.1 x) as [θ' Hθ']; [eexists; split; eauto|].
eexists; intuition eauto.
-- split; trivial.
destruct (equiv_envR_vars pe.2 x) as [θ' Hθ']; [eexists; split; eauto|].
eexists; intuition eauto.
-- intros Γ0 Ho Hocc. fold (E p Γ0) in Hocc.
apply (Hind (Γ0, [])); trivial.
unfold env_pair_order. simpl. transitivity (pe.1 ++ pe.2 ++ pe.2).
++ eapply env_order_lt_le_trans; [exact Ho|]. simpl. auto with order.
++ eapply env_order_lt_le_trans; [exact Hpe|]. simpl. auto with order.
-- intros pe' Ho Hocc. fold (A p pe') in Hocc.
apply (Hind pe') in Hocc as [Hneq [θ [[Hθ|Hθ] Hocc]]].
++ intuition eauto.
++ intuition eauto.
++ unfold env_pair_order. simpl. transitivity (pe.1 ++ pe.2 ++ pe.2).
** eapply env_order_lt_le_trans; [exact Ho|]. simpl. auto with order.
** eapply env_order_lt_le_trans; [exact Hpe|]. simpl. auto with order.
* apply in_in_map in Hinr as (ψ'&Hin'&Heq). subst φ.
apply a_rule_r_vars in Hφ' as [Hneq [θ [[Hθ|Hθ] Hocc]]].
-- split; trivial.
destruct (equiv_envL_vars pe.1 x) as [θ' Hθ']; [eexists; split; eauto|].
eexists; intuition eauto.
-- split; trivial.
destruct (equiv_envR_vars pe.2 x) as [θ' Hθ']; [eexists; split; eauto|].
eexists; intuition eauto.
-- intros Γ0 Ho Hocc. fold (E p Γ0) in Hocc.
apply (Hind (Γ0, [])); trivial.
unfold env_pair_order. simpl. transitivity (pe.1 ++ pe.2 ++ pe.2).
++ eapply env_order_lt_le_trans; [exact Ho|]. simpl. auto with order.
++ eapply env_order_lt_le_trans; [exact Hpe|]. simpl. auto with order.
-- intros pe' Ho Hocc. fold (A p pe') in Hocc.
apply (Hind pe') in Hocc as [Hneq [θ [[Hθ|Hθ] Hocc]]].
++ intuition eauto.
++ intuition eauto.
++ unfold env_pair_order. simpl. transitivity (pe.1 ++ pe.2 ++ pe.2).
** eapply env_order_lt_le_trans; [exact Ho|]. simpl. auto with order.
** eapply env_order_lt_le_trans; [exact Hpe|]. simpl. auto with order.
(* A *)
- intro Hocc.
unfold E, A in Hocc. simp EA in Hocc; simpl in Hocc.
apply variables_disjunction in Hocc as (φ&Hin&Hφ).
apply elem_of_app in Hin as [Hin|Hin].
{
apply in_in_map in Hin as (ψ&Hin&Heq). subst φ.
apply a_rule_l_vars in Hφ.
+ intuition. destruct H0 as [θ [H0 H1]]. occ.
* destruct (equiv_envL_vars Γ x) as [χ [H0 H3]] ; [ exists θ ; auto | ].
exists χ ; auto.
* destruct (equiv_envR_vars Δ x) as [χ [H0 H3]] ; [ exists θ ; auto | ].
exists χ ; auto.
+ intros pe Hpe. simp EA. simpl. intro Hocc.
destruct (variables_conjunction _ _ Hocc) as [θ [H H0]].
pose (Hind (pe, [])) ; cbn in a ; unfold E in a ; simp EA in a ;
apply a ; auto with order.
+ intros pe Hpe Hocc. simp EA in Hocc ; simpl in Hocc.
destruct (variables_disjunction _ _ Hocc) as [θ [H H0]].
pose (Hind pe) ; cbn in a ; unfold A in a ; simp EA in a ;
apply a; auto with order.
}
(* The proof below is the same as the one above in the curly brackets. *)
apply in_in_map in Hin as (ψ&Hin&Heq). subst φ.
apply a_rule_r_vars in Hφ.
+ intuition. destruct H0 as [θ [H0 H1]]. occ.
* destruct (equiv_envL_vars Γ x) as [χ [H0 H3]] ; [ exists θ ; auto | ].
exists χ ; auto.
* destruct (equiv_envR_vars Δ x) as [χ [H0 H3]] ; [ exists θ ; auto | ].
exists χ ; auto.
+ intros pe Hpe. simp EA. simpl. intro Hocc.
destruct (variables_conjunction _ _ Hocc) as [θ [H H0]].
pose (Hind (pe, [])) ; cbn in a ; unfold E in a ; simp EA in a ;
apply a; auto with order.
+ intros pe Hpe Hocc. simp EA in Hocc ; simpl in Hocc.
destruct (variables_disjunction _ _ Hocc) as [θ [H H0]].
pose (Hind pe) ; cbn in a ; unfold A in a ; simp EA in a ;
apply a; auto with order.
Qed.
End VariablesCorrect.
In this section we prove (ii), which states that the E- and A-formula are
entailed by the original formula and entail the original formula,
respectively.
Opaque make_disj.
Opaque make_conj.
Ltac l_tac := repeat rewrite list_to_set_disj_open_boxes; rwl list_to_set_disj_env_add'.
Ltac r_tac := repeat rewrite list_to_set_disj_open_boxes;
rwr list_to_set_disj_env_add'.
Lemma a_rule_l_spec (Γ : list form) θ Δ Hin
(E0 : ∀ Γ0 (Hpe : (Γ0, []) ≺· (Γ, Δ)), form)
(A0 : ∀ pe (Hpe : pe ≺· (Γ, Δ)), form)
(HE : forall Γ Hpe, (list_to_set_disj Γ ⊢ {[+ E0 Γ Hpe +]}))
(HA : forall Γ Δ Hpe, (list_to_set_disj Γ • A0 (Γ, Δ) Hpe ⊢ list_to_set_disj Δ)) :
(list_to_set_disj Γ • @a_rule_l p _ _ E0 A0 θ Hin ⊢ list_to_set_disj Δ).
Proof with (auto with proof).
assert(Hi : θ ∈ list_to_set_disj Γ) by now apply elem_of_list_to_set_disj.
destruct θ; simp a_rule_l; simpl; exhibit Hi 1 ;
match goal with |- ?d ∖ {[?f]} • _ • _ ⊢ _ => rwl (symmetry (list_to_set_disj_rm Γ f)) end.
- simpl; case decide; intro Hp.
+ subst. case_decide as Hin'.
* apply elem_of_list_to_set_disj in Hin'. exhibit Hin' 0...
* apply ExFalso.
+ exchl 0...
- constructor 2.
- simpl; exchl 0. apply AndL. exchl 1 ; exchl 0. do 2 l_tac...
- apply make_conj_sound_L.
exchl 0. apply OrL; exchl 0.
+ apply AndL. apply make_impl_sound_L. exchl 0. apply make_impl_sound_L.
l_tac. apply ImpL.
* apply weakeningl, generalised_weakeningrL...
* exchl 0. apply weakeningl...
+ apply AndL. l_tac. apply make_impl_sound_L. exchl 0. apply make_impl_sound_L...
apply weakeningl. apply ImpL... apply generalised_weakeningrL...
- destruct θ1; simp a_rule_l; simpl.
+ case decide; intro Hp.
* assert (Hin'' : Var n ∈ (list_to_set_disj (rm (n → θ2) Γ) : env)).
by (rewrite list_to_set_disj_rm; apply in_difference; try easy;
now apply elem_of_list_to_set_disj).
exhibit Hin'' 2. exchl 0; exchl 1. apply ImpLVar. exchl 0. backwardl.
rewrite env_add_remove. exchl 0. l_tac...
* case decide; intro; subst.
-- apply ExFalso.
-- apply make_conj_sound_L. constructor 4. exchl 0. exchl 1. exchl 0. apply ImpLVar.
exchl 0. exchl 1. l_tac. apply weakeningl...
+ constructor 2.
+ exchl 0. apply ImpLAnd. exchl 0. l_tac...
+ exchl 0. apply ImpLOr. exchl 1. l_tac. exchl 0. l_tac...
+ apply make_conj_sound_L, AndL. exchl 0. apply make_conj_sound_L, AndL.
exchl 0; apply make_impl_sound_L. exchl 2; exchl 1. exchl 0.
apply ImpLImp.
* exchl 2; exchl 1 ; exchl 0. apply weakeningl.
exchl 2; exchl 1 ; exchl 0. apply weakeningl.
exchl 1; exchl 0. apply ImpL.
-- repeat l_tac. apply generalised_weakeningrL...
-- apply weakeningr. do 2 l_tac...
* repeat box_tac. exchl 1 ; exchl 0. apply weakeningl.
exchl 2. exchl 1. exchl 0. apply weakeningl.
exchl 1. exchl 0. apply make_impl_sound_L, ImpL.
-- repeat l_tac. apply generalised_weakeningrL...
-- do 2 l_tac...
* do 2 (exchl 0; apply weakeningl). exchl 0.
apply make_impl_sound_L, ImpL.
-- apply generalised_weakeningrL. peapply HE.
-- l_tac...
+ apply AndL. exchl 1; exchl 0. apply ImpLBox.
* box_tac. box_tac. exchl 1; exchl 0. apply weakeningl. exchl 1; exchl 0.
apply make_impl_sound_L. do 2 l_tac. apply ImpL.
-- apply generalised_weakeningrL...
-- apply HA.
* exchl 1; exchl 0. apply weakeningl. exchl 0. l_tac. auto with proof.
- auto with proof.
Qed.
Proposition entail_correct Γ Δ:
(list_to_set_disj Γ ⊢ ∅ • E p Γ) *
(list_to_set_disj Γ • A p (Γ, Δ) ⊢ list_to_set_disj Δ).
Proof with (auto with proof).
remember (Γ, Δ) as pe.
replace Γ with pe.1 by now subst.
replace Δ with pe.2 by now subst. clear Heqpe Γ Δ. revert pe.
refine (@well_founded_induction _ _ wf_pointed_order _ _).
unfold env_pair_order.
intros (Γ, Δ) Hind. simpl.
unfold E, A. simp EA. simpl.
remember (simp_envL Γ) as Γ'.
remember (simp_envR Δ) as Δ'.
assert (Hind' := λ y H, Hind y (simp_env_pointed_env_order y Γ Δ H)).
clear Hind.
(* uncurry the induction hypothesis for convenience *)
assert (HE := fun d x => fst (Hind' (d, []) x)).
assert (HA := fun d Δ' x=> snd (Hind' (d, Δ') x)).
unfold E, A in *; simpl in HE, HA.
simpl in *. clear Hind'.
split.
{
(* E *)
apply conjunction_R1. intros φ Hin. apply in_in_map in Hin.
destruct Hin as (ψ&Hin&Heq). subst φ.
apply equiv_envL_simp_env.
rewrite <- HeqΓ' in *. clear HeqΓ' Γ. rename Γ' into Γ.
assert(Hi : ψ ∈ list_to_set_disj Γ) by now apply elem_of_list_to_set_disj.
dependent destruction ψ; simp e_rule ; exhibit Hi 0;
match goal with |- ?d ∖ {[?f]} • _ ⊢ _ => rwl (list_to_set_disj_rm_rev Γ f) end.
- case decide...
- auto with proof.
- simpl. apply AndL. do 2 l_tac...
- apply make_disj_sound_R, OrL.
+ l_tac. apply OrR, weakeningr. apply HE. order_tac.
+ l_tac. apply OrR. exchr 0. apply weakeningr, HE. order_tac.
- dependent destruction ψ1; simp e_rule; simpl; auto 3 using HE with proof.
+ case decide; intro Hp.
* assert(Hin'' : Var n ∈ (list_to_set_disj (rm (n → ψ2) Γ) : env))
by (rewrite list_to_set_disj_rm; apply in_difference;
try easy; now apply elem_of_list_to_set_disj).
exhibit Hin'' 1. apply ImpLVar. exchl 0. backwardl. rewrite env_add_remove.
l_tac. apply HE...
* case decide; intro; subst.
-- apply top_Provable.
-- apply make_impl_sound_R, ImpR.
++ exchl 0. apply ImpLVar. exchl 0. l_tac...
++ apply open_boxes_R. exchl 0. apply ImpLVar. exchl 0.
apply weakeningl. l_tac...
+ apply ImpLAnd. l_tac...
+ apply ImpLOr. do 2 l_tac...
+ apply make_impl_sound_R, ImpR; apply make_disj_sound_R, OrR.
* exchl 0; apply ImpLImp.
-- exchl 1 ; exchl 0 ; apply weakeningl.
apply weakeningr. exchr 0. apply weakeningr. do 2 l_tac...
-- do 2 box_tac. exchl 1 ; exchl 0 ; apply make_impl_sound_L, ImpL.
++ exchr 0. apply weakeningr. do 2 l_tac...
++ do 2 l_tac...
-- exchl 0 ; apply weakeningl, weakeningr. l_tac...
(* Similar subproof *)
* apply open_boxes_R. exchl 0; apply ImpLImp.
-- exchl 1 ; exchl 0 ; apply weakeningl.
apply weakeningr. exchr 0. apply weakeningr. do 2 l_tac...
-- do 2 box_tac. exchl 1 ; exchl 0 ; apply make_impl_sound_L, ImpL.
++ exchr 0. apply weakeningr. do 2 l_tac...
++ do 2 l_tac...
-- exchl 0 ; apply weakeningl, weakeningr. l_tac...
+ apply make_impl_sound_R, ImpR.
* exchl 0. apply ImpLBox.
-- box_tac. exchl 1; exchl 0. apply make_impl_sound_L, ImpL.
++ do 2 l_tac. exchr 0. apply weakeningr...
++ do 2 l_tac...
-- exchl 0. l_tac. apply weakeningl...
(* Similar subproof *)
* apply open_boxes_R. exchl 0. apply ImpLBox.
-- box_tac. exchl 1; exchl 0. apply make_impl_sound_L, ImpL.
++ do 2 l_tac. exchr 0. apply weakeningr...
++ do 2 l_tac...
-- exchl 0. l_tac. apply weakeningl...
- apply BoxR. apply weakeningl. rwl list_to_set_disj_env_add'.
rewrite list_to_set_disj_open_boxes. peapply HE.
+ eapply env_pair_order_nil_l, env_order_open_box; eauto.
+ now rewrite <- Permutation_rm.
}
(* A *)
apply disjunction_L ; intros φ Hin ; apply elem_of_list_In,in_app_or in Hin.
replace (list_to_set_disj Γ • φ) with ({[+φ+]} ⊎ list_to_set_disj Γ : env) by ms.
eapply equiv_envL_spec; [apply equiv_envL_simp_env|].
replace ({[+φ+]} ⊎ list_to_set_disj (simp_envL Γ) : env)
with (list_to_set_disj (simp_envL Γ) • φ : env) by ms.
apply equiv_envR_simp_env.
rewrite <- HeqΓ', <- HeqΔ' in *. clear HeqΓ' HeqΔ' Γ Δ.
rename Γ' into Γ. rename Δ' into Δ.
remember (in_map Γ (a_rule_l p)) as l. destruct (In_form_dec l φ) ; subst l.
- apply elem_of_list_In in i. apply in_in_map in i as (ψ & Hin' & H) ; subst φ.
clear Hin. apply a_rule_l_spec.
+ intros. rewrite env_singleton. apply HE. subst. trivial.
+ intros. apply HA; subst; trivial.
- remember (in_map Δ (a_rule_r p)) as l.
assert (Hin' : In φ l) by (destruct Hin ; [ exfalso ; auto | auto]) ; subst l. clear Hin n.
apply elem_of_list_In in Hin'. apply in_in_map in Hin' as (ψ & Hin' & H) ; subst φ.
assert(Hin'' := Hin').
rewrite <- elem_of_list_to_set_disj in Hin''.
dependent destruction ψ; simp a_rule_r; exhibit Hin'' 0; cbn ;
match goal with |- _ ⊢ ?d ∖ {[?f]} • _ => rwr (list_to_set_disj_rm_rev Δ f) end.
+ case decide; intro; subst ; [constructor 2|constructor 1].
+ apply ExFalso.
+ simpl. apply make_conj_sound_L, AndL, AndR; r_tac.
* apply weakeningl, HA...
* exchl 0. apply weakeningl, HA...
+ apply OrR. do 2 r_tac. apply HA...
+ apply make_conj_sound_L,AndL,make_impl_sound_L. exchl 0.
apply ImpR.
* exchl 0 ; exchl 1. l_tac. apply weakeningl. apply ImpL.
-- apply generalised_weakeningrL. rewrite env_singleton. apply HE...
-- r_tac. apply HA...
* do 2 box_tac. exchl 1 ; exchl 0 ; apply weakeningl ; exchl 0.
l_tac. apply make_impl_sound_L, ImpL.
-- exchr 0. apply weakeningr, HE...
-- apply HA...
+ apply BoxR. box_tac. exchl 0. l_tac. apply make_impl_sound_L, ImpL.
* exchr 0. apply weakeningr, HE...
* apply HA...
Qed.
End EntailmentCorrect.
The proof in this section, which is the most complex part of the argument,
shows that the E- and A-formulas constructed above are indeed their
propositionally quantified versions, that is, *any* formula entailed by the
original formula and using only variables from that formula except p is
already a consequence of the E-quantified version, and similarly on the other
side for the A-quantifier.
(* This holds by idempotence of simp_env *)
Lemma A_simp_env Γ Δ: A p (simp_envL Γ, simp_envR Δ) = A p (Γ, Δ).
Proof.
unfold A. simp EA. simpl.
repeat rewrite simp_envL_idempotent, simp_envR_idempotent ; auto.
Qed.
Lemma E_simp_env Γ : E p (simp_envL Γ) = E p Γ.
Proof. unfold E; simp EA. simpl. repeat rewrite simp_envL_idempotent ; auto. Qed.
Notation e_rule :=
(λ p Γ φ Hin, (@e_rule p _ (λ Γ0 _, E p Γ0)
(λ pe (_ : pe ≺· (Γ, [])), A p pe) φ Hin)).
Notation a_rule_l :=
(λ p Γ Δ φ Hin, @a_rule_l p _ _ (λ Γ0 _, E p Γ0)
(λ pe (_ : pe ≺· (Γ, Δ)), A p pe) φ Hin).
Notation a_rule_r :=
(λ p Γ Δ φ Hin, @a_rule_r p _ _ (λ Γ0 _, E p Γ0)
(λ pe (_ : pe ≺· (Γ, Δ)), A p pe) φ Hin).
Lemma E_left {Γ0 Γ Δ} {Γ' : list form} {φ : form}:
(Γ' = simp_envL Γ) -> ∀ (Hin : φ ∈ Γ'),
(Γ0 • e_rule p Γ' φ Hin) ⊢ Δ ->
Γ0 • E p Γ' ⊢ Δ.
Proof.
intros Heq Hin Hp. subst Γ'.
rewrite E_simp_env. unfold E; simp EA; simpl.
assert(Hin' := Hin).
eapply in_map_in in Hin'. destruct Hin' as [Hin' Hrule].
eapply conjunction_L.
- exact Hrule.
- erewrite e_rule_cong_strong ; auto. exact Hp.
Unshelve. exact form_eq_dec.
Qed.
Local Lemma A_right {Γ0 Γ Γ' Δ Δ' φ} :
(Γ' = simp_envL Γ) -> (Δ' = simp_envR Δ) -> ∀ (Hin : φ ∈ Δ'),
Γ0 ⊢ ∅ • a_rule_r p Γ' Δ' φ Hin ->
Γ0 ⊢ ∅ • A p (Γ', Δ').
Proof.
intros Heq Heq' Hin Hp. subst Γ' Δ'. rewrite A_simp_env. unfold A; simp EA; simpl.
assert(Hin' := Hin).
eapply in_map_in in Hin'. destruct Hin' as [Hin' Hrule].
apply op_disjunction_R with (a_rule_r p (simp_envL Γ) (simp_envR Δ) φ Hin').
- apply elem_of_app ; right. exact Hrule.
- erewrite a_rule_r_cong_strong.
+ exact Hp.
+ trivial.
+ trivial.
Unshelve. exact form_eq_dec.
Qed.
Local Lemma A_left {Γ0 Γ Γ' φ Δ0 Δ Δ'} :
(Δ' = simp_envR Δ) -> (Γ' = simp_envL Γ) -> ∀ (Hin : φ ∈ Γ'),
Γ0 ⊢ Δ0 •
a_rule_l p Γ' Δ' φ Hin ->
Γ0 ⊢ Δ0 • A p (Γ', Δ').
Proof.
intros Heq Heq' Hin Hp. subst Γ' Δ'.
rewrite A_simp_env. unfold A; simp EA; simpl.
assert(Hin' := Hin).
eapply in_map_in in Hin'. destruct Hin' as [Hin' Hrule].
eapply op_disjunction_R.
- apply elem_of_app. left. exact Hrule.
- erewrite a_rule_l_cong_strong ; auto. exact Hp.
Unshelve. exact form_eq_dec.
Qed.
Local Ltac Etac := match goal with
| HeqΓ0': ?Γ0' = simp_envL ?Γ0, Hin : ?a ∈ list_to_set_disj ?Γ0' |- _ • E _ ?Γ0' ⊢ _=>
apply (E_left HeqΓ0' (proj1 (elem_of_list_to_set_disj _ _) Hin)); simp e_rule end.
Proposition pq_correct Γ Γ0 Δ Δ0:
(∀ φ0, (φ0 ∈ Γ) -> ¬ occurs_in p φ0) ->
(* a *)
((∀ φ0, (φ0 ∈ Δ) -> ¬ occurs_in p φ0) -> (Γ ⊎ list_to_set_disj Γ0) ⊢ Δ
-> Γ • E p Γ0 ⊢ Δ) *
(* b *)
((Γ ⊎ list_to_set_disj Γ0) ⊢ list_to_set_disj Δ0
-> Γ • E p Γ0 ⊢ ∅ • A p (Γ0, Δ0)).
Proof.
(* This proof goes by induction on the ordering w.r.t (Γ ⊎ Γ0, Δ ⊎ Δ0)
instead of on the structure of Γ ⊎ Γ0 ⊢ Δ, to allow better rules *)
(* we want to use an E rule *)
(* we want to use an A rule defined in a_rule_l *)
Local Ltac Al := match goal with
| HeqΔ0': ?Δ0' = simp_envR ?Δ0, HeqΓ0': ?Γ0' = simp_envL ?Γ0, HinΓ : ?a ∈ list_to_set_disj ?Γ0'
|- _ ⊢ (_ • A _ (?Γ0', ?Δ0')) =>
apply (A_left HeqΔ0' HeqΓ0' (proj1 (elem_of_list_to_set_disj _ _) HinΓ)); simp a_rule_l end.
(* we want to use an A rule defined in a_rule_r *)
Local Ltac Ar := match goal with
| HeqΔ0': ?Δ0' = simp_envR ?Δ0, HeqΓ0': ?Γ0' = simp_envL ?Γ0, HinΔ : ?a ∈ list_to_set_disj ?Δ0'
|- _ ⊢ (_ • A _ (?Γ0', ?Δ0')) =>
apply (A_right HeqΓ0' HeqΔ0' (proj1 (elem_of_list_to_set_disj _ _) HinΔ)); simp a_rule_r end.
Ltac occ :=
repeat setoid_rewrite env_in_add; intuition; subst; intuition; simpl in *;
repeat multimatch goal with
| Hocc : ∀ φ0, φ0 ∈ (?Δ • ?a) → occurs_in _ φ0 -> False |- _ =>
destruct (Hocc a); [ms|]; simpl; intuition
| Hin : ?φ ∈ ?Γ ∖ _ |- _ => let Hin' := fresh "Hin'" in
try assert(Hin' : φ ∈ Γ) by ms; clear Hin
| Hin : ?φ ∈ ?Γ, Hocc: ∀ φ0, φ0 ∈ ?Γ → occurs_in _ φ0 → False |- _ =>
apply Hocc in Hin; intuition; simpl; intuition; clear Hin
| Hin : ?φ ∈ (⊗ ?Γ), Hocc: ∀ φ0, φ0 ∈ ?Γ → occurs_in _ φ0 → False |- _ =>
edestruct occurs_in_open_boxes in Hin; eauto; intuition
| Hin : ?φ ∈ ?Γ, Hocc: ∀ φ0, φ0 ∈ (?Γ • ?a) → occurs_in _ φ0 → False |- _ =>
let Hin' := fresh "Hin" in assert(Hin' : φ ∈ (Γ • a)) by ms;
apply Hocc in Hin'; intuition; simpl; intuition; clear Hin
| Hin : ?φ ∈ (⊗ (?Γ∖ _)), Hocc: ∀ φ0, φ0 ∈ ?Γ → occurs_in _ φ0 → False |- _ =>
edestruct occurs_in_open_boxes in Hin; eauto; intuition
end;
intuition;
try match goal with | Hin : (?a ∈ ∅) |- _ => inversion Hin end.
Ltac applyE Hind :=
apply (fun a b c => Hind a b c []);
[|try solve[occ]|try solve[occ]|].
Ltac applyA Hind :=
apply (fun a b d e f => (Hind a b ∅ d e f));
[apply env_pair_order_cancel_left|try solve[occ]|].
Local Ltac equiv_tac :=
try match goal with H : ?a ∈ ?Γ |- context g [(⊗?Γ) ∖ {[?a]}] =>
assert(a ∈ ⊗ Γ) by auto with proof end;
try (rewrite difference_singleton; trivial); try rw_env;
try (rewrite open_boxes_remove by auto with proof; simpl);
repeat rewrite ?open_boxes_disj_union, ?list_to_set_disj_open_boxes;
try (rewrite union_difference_L by trivial);
try (rewrite union_difference_R by trivial);
repeat rewrite ?list_to_set_disj_env_add, ?list_to_set_disj_rm_rev, ?open_boxes_disj_union;
try (rewrite open_boxes_remove by trivial);
try timeout 1 ms.
Local Ltac peapply' th :=
(erewrite proper_Provable; [| |reflexivity]); [eapply th|equiv_tac].
Local Ltac rpeapply' th :=
(erewrite proper_Provable; [|reflexivity|]); [eapply th|equiv_tac].
remember (elements Γ ++ Γ0, elements Δ ++ Δ0) as pe.
revert pe Γ Γ0 Δ Δ0 Heqpe.
refine (@well_founded_induction _ _ wf_pointed_order _ _).
intros (Γ', Δ') Hind Γ Γ0 Δ Δ0 Heq Hnin.
inversion Heq; subst; clear Heq.
assert(Ho' : env_pair_order_refl (elements Γ ++ simp_envL Γ0, elements Δ ++ simp_envR Δ0)
(elements Γ ++ Γ0, elements Δ ++ Δ0))
by (unfold env_pair_order_refl; simpl; order_tac).
assert(Hind' := λ Γ1 Γ2 Δ1 Δ2 Ho,
Hind (elements Γ1 ++ Γ2, elements Δ1 ++ Δ2)
(env_order_lt_le_trans _ _ _ Ho Ho') _ _ _ _ eq_refl).
clear Ho'.
clear Hind. rename Hind' into Hind.
rewrite <- E_simp_env, <- A_simp_env.
Ltac order_tacl := try apply env_pair_order_cancel_right;
repeat rewrite app_nil_r; repeat order_tac.
Ltac order_tacr :=
try replace (elements ∅) with ([] : list form) by ms;
try apply env_pair_order_cancel_left;
repeat rewrite app_nil_l; repeat rewrite <- app_assoc; repeat order_tac.
Ltac setup Γ Γ0' Δ Δ0' Heq Hin0 HeqΔ :=
(* try and solve the easy case where the main formula is on the left *)
try match goal with
| H : (?Γ0•?a•?b) = Γ ⊎ list_to_set_disj Γ0' |- _ => rename H into Heq;
pose(Heq' := env_equiv_eq _ _ Heq); apply env_add_inv' in Heq'
| H : ((?Γ0 • ?a) = Γ ⊎ list_to_set_disj Γ0') |- _ => rename H into Heq;
assert(Hin : a ∈ (Γ ⊎ list_to_set_disj Γ0')) by (rewrite <- Heq; ms);
pose(Heq' := env_equiv_eq _ _ Heq); apply env_add_inv' in Heq';
try (case (decide (a ∈ Γ)); intro Hin0;
[exhibit Hin0 1; rewrite union_difference_L in Heq' by trivial|
case (decide (a ∈ (list_to_set_disj Γ0' : env))); intro Hin0';
[rewrite union_difference_R in Heq' by trivial|
apply gmultiset_elem_of_disj_union in Hin; exfalso; tauto]])
end; simpl;
try match goal with
| Heq : ((?Δ1 • ?a) = list_to_set_disj Δ0') |- _ => rename Heq into HeqΔ;
assert(Hin' : a ∈ (list_to_set_disj Δ0')) by (rewrite <- HeqΔ; ms);
assert(HinΔ0 : a ∈ Δ0') by (now apply elem_of_list_to_set_disj);
pose(HeqΔ' := env_equiv_eq _ _ HeqΔ); apply env_add_inv' in HeqΔ';
rewrite list_to_set_disj_rm_rev in HeqΔ';
try exhibit HinΔ0 0 end.
split.
(* a) *)
{
intros Hocc Hp.
eapply equiv_envL_spec in Hp; [|apply symmetric_equiv_envL, equiv_envL_simp_env].
remember (simp_envL Γ0) as Γ0'.
remember (simp_envR Δ0) as Δ0'.
dependent destruction Hp; setup Γ Γ0' Δ Δ0 Heq Hin0 HeqΔ.
(* Atom *)
- auto with proof.
- Etac. rewrite decide_False. auto with proof. occ.
(* ExFalso *)
- auto 2 with proof.
- Etac. auto with proof.
(* AndR *)
- apply AndR; applyE Hind; auto with proof.
(* AndL *)
- exchl 0. apply AndL. exchl 1; exchl 0. applyE Hind; auto with proof.
peapply' Hp.
- Etac. simpl. applyE Hind; auto; auto with proof.
+ order_tacl.
+ peapply' Hp.
(* OrR *)
- apply OrR. applyE Hind; auto with proof.
(* OrL *)
- exchl 0. apply OrL; exchl 0.
+ applyE Hind; auto with proof. peapply' Hp1.
+ applyE Hind; auto with proof. peapply' Hp2.
- Etac. apply make_disj_sound_L, OrL; applyE Hind; auto with proof; simpl.
+ order_tacr.
+ peapply' Hp1.
+ order_tacr.
+ peapply' Hp2.
(* ImpR *)
- (* nontrivial ; similar to ImpBox *)
destruct (open_boxes_case (list_to_set_disj Γ0')) as [[θ Hθ] | Hequiv].
+ (* either Γ0' has a box ; then E p Γ0' contains E p (⊗Γ0') ... *)
apply contractionl. Etac. apply ImpR.
* exchl 0. apply weakeningl. exchl 0. applyE Hind; auto with proof.
peapply Hp1.
* do 2 box_tac. exchl 1. exchl 0. apply weakeningl. exchl 0.
clear Hθ. applyE Hind; [order_tacl|]. peapply' Hp2.
+ (* ... or Γ0' = ⊗ Γ0' *)
apply ImpR.
* exchl 0. applyE Hind; auto with proof. peapply Hp1.
* box_tac. exchl 0. apply open_box_L. applyE Hind; [order_tacl|].
rwl Hequiv. peapply' Hp2.
- (* ImpLVar *)
case (decide ((Var p0 → φ) ∈ Γ)).
+ intro Hin0.
assert (Hocc' := Hnin _ Hin0). simpl in Hocc'.
case (decide (Var p0 ∈ Γ)); intro Hin1.
* (* subcase 1: p0, (p0 → φ) ∈ Γ *)
assert (Hin2 : Var p0 ∈ Γ ∖ {[Var p0 → φ]})
by (apply in_difference; trivial; discriminate).
exhibit Hin0 1; exhibit Hin2 2; exchl 0; exchl 1.
apply ImpLVar ; exchl 1; exchl 0.
applyE Hind; auto with proof. peapply' Hp.
* assert(Hin0' : Var p0 ∈ (Γ1•Var p0•(p0 → φ) : env)) by ms.
rewrite Heq in Hin0'.
case (decide (Var p0 ∈ (list_to_set_disj Γ0': env))); intro Hp0;
[|apply gmultiset_elem_of_disj_union in Hin0'; exfalso; tauto].
(* subcase 3: p0 ∈ Γ0 ; (p0 → φ) ∈ Γ *)
apply contractionl. Etac. rewrite decide_False by tauto.
exhibit Hin0 2. exchl 1. exchl 0. apply ImpLVar. exchl 0.
apply weakeningl. exchl 0.
applyE Hind; [auto with proof|]. peapply' Hp.
+ intro.
assert(Hin : (Var p0 → φ) ∈ (Γ1•Var p0•(p0 → φ))) by ms.
rewrite Heq in Hin.
case (decide ((Var p0 → φ) ∈ (list_to_set_disj Γ0' : env))); intro Hin0;
[|apply gmultiset_elem_of_disj_union in Hin; exfalso; tauto].
case (decide (Var p0 ∈ Γ)); intro Hin1.
* (* subcase 2: p0 ∈ Γ ; (p0 → φ) ∈ Γ0 *)
exhibit Hin1 1. Etac.
case decide; intro Hp0;[|case decide; intro; subst; [auto with *|]].
-- simpl. applyE Hind.
++ clear Hp0. order_tacl.
++ peapply' Hp.
-- apply make_impl_sound_L, ImpLVar. exchl 0. backwardl.
rewrite env_add_remove. applyE Hind.
++ clear Hin2 Hin1. order_tacl.
++ peapply' Hp.
* assert(Hin': Var p0 ∈ Γ ⊎ list_to_set_disj Γ0') by (rewrite <- Heq; ms).
apply gmultiset_elem_of_disj_union in Hin'.
case (decide (Var p0 ∈ (list_to_set_disj Γ0': env))); intro Hin1'; [|exfalso; tauto].
(* subcase 4: p0,(p0 → φ) ∈ Γ0 *)
case (decide (p = p0)); intro.
-- (* subsubcase p = p0 *)
apply elem_of_list_to_set_disj in Hin1'.
Etac; repeat rewrite decide_True by trivial.
clear Heq. applyE Hind.
++ clear Hin1'. order_tacl.
++ peapply' Hp.
-- (* subsubcase p ≠ p0 *)
apply contractionl. Etac. rewrite decide_False by trivial. exchl 0.
assert((p0 → φ) ∈ list_to_set_disj Γ0') by ms. Etac.
rewrite decide_True by now apply elem_of_list_to_set_disj.
exchl 0. apply weakeningl. applyE Hind.
++ order_tacl.
++ peapply' Hp.
(* ImpLAnd *)
- exchl 0. apply ImpLAnd. exchl 0. applyE Hind; auto with proof. peapply' Hp.
- Etac. simpl. applyE Hind.
+ order_tacl.
+ peapply' Hp.
(* ImpLOr *)
- exchl 0; apply ImpLOr. exchl 1; exchl 0.
applyE Hind; [auto with proof|]. peapply' Hp.
- Etac. applyE Hind.
+ order_tacl.
+ peapply' Hp.
(* ImpLImp *)
- destruct (open_boxes_case (list_to_set_disj Γ0')) as [[θ HΓ0'] | Hequiv].
(* Either Γ0' has a box ...*)
+ apply contractionl. Etac. exchl 1; exchl 0. apply ImpLImp.
* exchl 1; exchl 0. apply weakeningl. exchl 1; exchl 0.
applyE Hind; [auto with proof|]. peapply' Hp1.
* do 2 box_tac. exchl 2; exchl 1. exchl 0. apply weakeningl.
exchl 1; exchl 0. applyE Hind.
-- clear HΓ0'. order_tacl.
-- peapply' Hp2.
* exchl 0. apply weakeningl. exchl 0.
applyE Hind; [auto with proof|]. peapply' Hp3.
+ (* ... or Γ0' = ⊗ Γ0' *)
exchl 0. apply ImpLImp.
* exchl 1; exchl 0. applyE Hind; [auto with proof|]. clear Hequiv.
peapply' Hp1.
* box_tac. exchl 1. exchl 0. apply open_box_L. applyE Hind.
-- order_tacl.
-- rwl Hequiv. clear Hequiv. peapply' Hp2.
* clear Hequiv. exchl 0. applyE Hind; [auto with proof|]. peapply' Hp3.
- (* subcase 2: ((φ1 → φ2) → φ3) ∈ Γ0 *)
Etac. simpl. apply make_impl_sound_L. apply ImpLBox.
+ do 2 apply weakeningl. apply make_impl_sound_R, Int_ImpR. applyA Hind.
* order_tac. rewrite Permutation_app_comm. order_tac.
* peapply' Hp2.
+ apply make_disj_sound_L, OrL.
* applyE Hind.
-- order_tacl.
-- peapply' Hp3.
* applyE Hind.
-- order_tacl.
-- (* This is where the stronger ImpLImp rule comes into play. *)
assert(Hp1' : Γ1 • (φ2 → φ3) • φ1 ⊢KM Δ).
{ exchl 0. apply ImpLImp_prev', ImpLImp; trivial. }
peapply' Hp1'.
- (* ImpBox, external *)
destruct (open_boxes_case (list_to_set_disj Γ0')) as [[θ Hθ] | Hequiv].
+ apply contractionl. Etac. exchl 1; exchl 0; apply ImpLBox.
* box_tac. box_tac. exchl 2; exchl 1; exchl 0. apply weakeningl.
exchl 1; exchl 0. applyE Hind.
-- clear Hθ. order_tacl.
-- peapply' Hp1.
* exchl 0. apply weakeningl. exchl 0. applyE Hind.
-- order_tacl.
-- peapply' Hp2.
+ exchl 0. apply ImpLBox.
* box_tac. exchl 1; exchl 0. apply open_box_L. applyE Hind.
-- order_tacl.
-- rwl Hequiv. clear Hequiv. peapply' Hp1.
* exchl 0. applyE Hind.
-- order_tacl.
-- clear Hequiv. peapply' Hp2.
- Etac. simpl. apply make_impl_sound_L, ImpLBox.
+ do 2 apply weakeningl. apply make_impl_sound_R, Int_ImpR. applyA Hind.
* order_tacl. rewrite Permutation_app_comm. order_tac.
* peapply' Hp1.
+ applyE Hind.
* order_tacl.
* peapply' Hp2.
- destruct (open_boxes_case (list_to_set_disj Γ0')) as [[θ Hθ] | Hequiv].
+ Etac. apply BoxR. box_tac. exchl 0. applyE Hind.
* clear Hθ. order_tacl.
* peapply' Hp.
+ apply BoxR. box_tac. exchl 0. apply open_box_L. applyE Hind.
* order_tacl.
* rwl Hequiv. clear Hequiv. peapply' Hp.
}
(* b) *)
(* Atom *)
intros Hp.
eapply equiv_envL_spec in Hp; [|apply symmetric_equiv_envL, equiv_envL_simp_env].
apply equiv_envR_simp_env in Hp.
remember (simp_envL Γ0) as Γ0'.
remember (simp_envR Δ0) as Δ0'.
dependent destruction Hp; setup Γ Γ0' Δ Δ0' Heq Hin0 HeqΔ.
- case (decide (p = p0)).
+ intro Heqp0. subst p0. exfalso. now apply (Hnin (#p)).
+ intro Hneq. Ar. rewrite decide_False by trivial. apply weakeningl, Atom.
- Etac. case decide.
+ intro Heqp0. Al. do 2 rewrite decide_True by ms. auto with proof.
+ intro Hneq. Ar. rewrite decide_False by trivial. apply Atom.
(* ExFalso *)
- auto 2 with proof.
- Etac; auto with proof.
(* AndR *)
- Ar. simpl. apply make_conj_sound_R, AndR.
+ applyA Hind; [order_tacr| rpeapply Hp1].
+ applyA Hind; [order_tacr| rpeapply Hp2].
(* AndL *)
- exchl 0. apply AndL. exchl 1; exchl 0. applyA Hind; [order_tacr|peapply' Hp].
- Al. Etac. simpl. applyA Hind; [order_tacr|]. peapply' Hp.
(* OrR *)
- Ar. simpl. applyA Hind; [order_tacr|rpeapply' Hp].
(* OrL *)
- exchl 0. apply OrL; exchl 0.
+ applyA Hind; [order_tacr|]. peapply' Hp1.
+ applyA Hind; [order_tacr|]. peapply' Hp2.
- Al. apply weakeningl. apply make_conj_sound_R,AndR, make_impl_sound_R.
+ apply make_impl_sound_R, Int_ImpR. applyA Hind.
* auto with proof.
* peapply' Hp1.
+ apply Int_ImpR. applyA Hind.
* order_tac.
* peapply' Hp2.
(* ImpR *)
- Ar. simpl. apply weakeningl, make_conj_sound_R, AndR.
+ apply BoxR, weakeningl, make_impl_sound_R, Int_ImpR. applyA Hind.
* order_tac. repeat rewrite <- Permutation_middle. order_tac.
* simpl. peapply' Hp2.
+ apply make_impl_sound_R, Int_ImpR. applyA Hind.
* order_tacr. rewrite <- Permutation_middle. order_tac.
* simpl. rwr (symmetry HeqΔ').
replace (Γ ⊎ ({[+ φ +]} ⊎ list_to_set_disj Γ0'))
with (Γ ⊎ list_to_set_disj Γ0' • φ) by ms. rpeapply Hp1.
(* ImpLVar *)
- pose(Heq'' := Heq'); apply env_add_inv' in Heq''.
case (decide ((Var p0 → φ) ∈ Γ)).
+ intro Hin0.
assert (Hocc := Hnin _ Hin0). simpl in Hocc.
case (decide (Var p0 ∈ Γ)); intro Hin1.
* (* subcase 1: p0, (p0 → φ) ∈ Γ *)
assert (Hin2 : Var p0 ∈ Γ ∖ {[Var p0 → φ]}) by (apply in_difference; trivial; discriminate).
clear Hin1. exhibit Hin0 1; exhibit Hin2 2; exchl 0; exchl 1.
apply ImpLVar; exchl 1; exchl 0. applyA Hind; [order_tacr | peapply' Hp].
* assert(Hin0' : Var p0 ∈ (Γ1•Var p0•(p0 → φ))) by ms. rewrite Heq in Hin0'.
case (decide (Var p0 ∈ (list_to_set_disj Γ0': env))); intro Hp0;
[|apply gmultiset_elem_of_disj_union in Hin0'; exfalso; tauto].
(* subcase 3: p0 ∈ Γ0 ; (p0 → φ) ∈ Γ *)
clear Heq''. apply contractionl. Etac. rewrite decide_False by tauto.
exhibit Hin0 2. exchl 1; exchl 0. apply ImpLVar. exchl 0. apply weakeningl.
exchl 0. applyA Hind; [order_tacr|]. peapply' Hp.
+ intro.
assert(Hin : (Var p0 → φ) ∈ (Γ1•Var p0•(p0 → φ))) by ms.
rewrite Heq in Hin.
case (decide ((Var p0 → φ) ∈ (list_to_set_disj Γ0' : env))); intro Hin0;
[|apply gmultiset_elem_of_disj_union in Hin; exfalso; tauto].
case (decide (Var p0 ∈ Γ)); intro Hin1.
* (* subcase 2: p0 ∈ Γ ; (p0 → φ) ∈ Γ0 *)
exhibit Hin1 1. Etac. Al.
case decide; intro Hp0;[|case decide; intro; subst; [auto with *|]].
-- simpl. clear Hp0. applyA Hind; [order_tacr|]. peapply' Hp.
-- apply make_impl_sound_L, ImpLVar.
apply make_conj_sound_R, AndR; auto 2 with proof.
exchl 0. backwardl. rewrite env_add_remove. clear Hin2.
applyA Hind; [auto with proof|]. peapply' Hp.
* assert(Hin': Var p0 ∈ Γ ⊎ list_to_set_disj Γ0') by (rewrite <- Heq; ms).
apply gmultiset_elem_of_disj_union in Hin'.
case (decide (Var p0 ∈ (list_to_set_disj Γ0': env))); intro Hin1'; [|exfalso; tauto].
(* subcase 4: p0,(p0 → φ) ∈ Γ0 *)
case (decide (p = p0)); intro.
-- (* subsubcase p = p0 *)
apply elem_of_list_to_set_disj in Hin1'.
Etac; Al. repeat rewrite decide_True by trivial.
applyA Hind; [auto with proof|]. peapply' Hp.
-- (* subsubcase p ≠ p0 *)
assert((p0 → φ) ∈ list_to_set_disj Γ0') by ms. Etac. Al.
do 2 rewrite decide_True by (now apply elem_of_list_to_set_disj).
applyA Hind; [auto with proof|]. peapply' Hp.
(* ImpLAnd *)
- exchl 0. apply ImpLAnd. exchl 0. applyA Hind; [order_tacr|peapply' Hp].
- Etac. Al. simpl. applyA Hind; [auto with proof|]. peapply' Hp.
(* ImpLOr *)
- exchl 0; apply ImpLOr. exchl 1; exchl 0. applyA Hind; [order_tacr| peapply' Hp].
- Etac. Al. applyA Hind; [auto with proof|]. peapply' Hp.
(* ImpLImp *)
- (* subcase 1: ((φ1 → φ2) → φ3) ∈ Γ *)
destruct (open_boxes_case (list_to_set_disj Γ0')) as [[θ HΓ0'] | Hequiv].
(* Either Γ0' has a box *)
+ apply contractionl. Etac. exchl 1. exchl 0; apply ImpLImp; exchl 0.
* exchl 1; exchl 0; apply weakeningl. exchl 1; exchl 0. apply weakeningr.
applyA Hind; [order_tacr|].
(* Crucial use of the double implication left inversion lemma. *)
peapply ImpLImp_prev'; [apply ImpLImp; eauto|]. ms.
* do 2 box_tac. exchl 2. exchl 1; exchl 0. exchl 1. apply weakeningl.
exchl 1; exchl 0. applyE Hind.
-- clear HΓ0'. order_tacl.
-- peapply' Hp2.
* apply weakeningl. exchl 0. applyA Hind; [order_tacr|]. peapply' Hp3.
(* ... or Γ0' = ⊗ Γ0' *)
+ exchl 0. apply ImpLImp.
* exchl 1; exchl 0. apply weakeningr. applyA Hind; [order_tacr|].
peapply ImpLImp_prev'; [apply ImpLImp; eauto|]. ms.
* box_tac. exchl 1. exchl 0. apply open_box_L. applyE Hind.
-- order_tacl.
-- rwl Hequiv. clear Hequiv. peapply' Hp2.
* exchl 0. applyA Hind; [order_tacr|]. clear Hequiv. peapply' Hp3.
- (* subcase 2: ((φ1 → φ2) → φ3) ∈ Γ0 *)
apply weakeningl. Al. apply make_conj_sound_R, AndR; [apply make_conj_sound_R, AndR|].
+ apply make_impl_sound_R, Int_ImpR. applyA Hind.
-- order_tacr.
-- assert(Hp1' : Γ1 • (φ2 → φ3) • φ1 ⊢KM list_to_set_disj Δ0').
{ exchl 0. apply ImpLImp_prev', ImpLImp; trivial. }
peapply' Hp1'.
+ apply BoxR, make_impl_sound_R, weakeningl, Int_ImpR. applyA Hind.
* order_tacr. rewrite Permutation_app_comm. order_tac.
* peapply' Hp2.
+ apply make_impl_sound_R, Int_ImpR. applyA Hind; [order_tac|]. peapply' Hp3.
- (* ImpBox, external *)
destruct (open_boxes_case (list_to_set_disj Γ0')) as [[θ Hθ] | Hequiv].
+ apply contractionl. Etac. exchl 1; exchl 0; apply ImpLBox.
* box_tac. box_tac. exchl 2; exchl 1; exchl 0. apply weakeningl.
exchl 1; exchl 0. clear Hθ. applyE Hind; [order_tacl|]. peapply' Hp1.
* exchl 0. apply weakeningl. exchl 0.
applyA Hind; [order_tacr|]. peapply' Hp2.
+ exchl 0. apply ImpLBox.
* box_tac. exchl 1; exchl 0. apply open_box_L. applyE Hind; [order_tacl|].
rwl Hequiv. clear Hequiv. peapply' Hp1.
* exchl 0. applyA Hind; [order_tacr|]. clear Hequiv. peapply' Hp2.
- Al. apply AndR.
+ apply weakeningl, BoxR, weakeningl. apply make_impl_sound_R, Int_ImpR.
applyA Hind.
* order_tac. apply env_order_cancel_right.
rewrite Permutation_app_comm. order_tac.
* peapply' Hp1.
+ Etac. simpl.
apply make_impl_sound_L, ImpLBox.
* apply weakeningl,weakeningl, make_impl_sound_R, Int_ImpR. applyA Hind.
-- order_tac. apply env_order_cancel_right.
rewrite Permutation_app_comm. order_tac.
-- peapply' Hp1.
* applyA Hind; [order_tac|]. peapply' Hp2.
- Ar. apply BoxR. box_tac. apply weakeningl, weakeningl, make_impl_sound_R, Int_ImpR.
applyA Hind; [|peapply' Hp].
order_tac.
rewrite Permutation_app_comm. simpl.
repeat rewrite <- Permutation_middle. auto with order.
Qed.
End PropQuantCorrect.
End Correctness.
Open Scope type_scope.
Lemma E_of_empty p : E p [] = ⊤.
Proof.
unfold E; simp EA; simpl. rewrite simp_envL_nil, in_map_empty.
now unfold conjunction, nodup, foldl.
Qed.
Definition vars_incl φ l := forall x, occurs_in x φ -> In x l.
The overall correctness result is summarized here.
Theorem KM_uniform_interpolation p V: p ∉ V ->
∀ φ, vars_incl φ (p :: V) ->
(vars_incl (Ef p φ) V)
* ({[φ]} ⊢ {[Ef p φ]})
* (∀ ψ, vars_incl ψ V -> {[φ]} ⊢ {[ψ]} -> {[Ef p φ]} ⊢ {[ψ]})
* (vars_incl (Af p φ) V)
* ({[Af p φ]} ⊢ {[φ]})
* (∀ θ, vars_incl θ V -> {[θ]} ⊢ {[φ]} -> {[θ]} ⊢ {[Af p φ]}).
Proof.
unfold Ef, Af.
intros Hp φ Hvarsφ; repeat split.
+ intros x Hx.
apply occurs_in_simp_form, (@EA_vars p _ [] x) in Hx.
destruct Hx as [Hneq [θ [Hθ Hocc]]]. apply elem_of_list_singleton in Hθ. subst.
apply occurs_in_simp_form, Hvarsφ in Hocc. destruct Hocc; subst; tauto.
+ replace {[φ]} with (list_to_set_disj [φ] : env) by ms.
peapply (equiv_form_equiv_env _ _ (symmetric_equiv_form (equiv_form_simp_form φ))).
rpeapply (equiv_form_equiv_envF _ _ ((equiv_form_simp_form (E p [simp_form φ])))).
peapply (@entail_correct p [simp_form φ] []).
+ intros ψ Hψ Hyp. rewrite elem_of_list_In in Hp.
peapply (equiv_form_equiv_env _ _ ((equiv_form_simp_form (E p [simp_form φ])))).
peapply (@pq_correct p ∅ [simp_form φ] {[ψ]}).
* exact [].
* intros θ Hin. inversion Hin.
* intros φ' Hφ' HF. apply gmultiset_elem_of_singleton in Hφ'. subst.
apply Hψ in HF. tauto.
* peapply (equiv_form_equiv_env _ _ (equiv_form_simp_form φ)).
peapply Hyp.
+ intros x Hx.
apply occurs_in_simp_form, EA_vars in Hx.
destruct Hx as [Hneq [θ [[HF|Hx] Hocc]]].
* inversion HF.
* inversion Hx; subst; [|auto with *]. clear Hx.
apply occurs_in_simp_form, Hvarsφ in Hocc.
firstorder. subst; tauto.
+ peapply (equiv_form_equiv_env _ _ (equiv_form_simp_form (A p ([],[simp_form φ])))).
rpeapply (equiv_form_equiv_envF _ _ (symmetric_equiv_form (equiv_form_simp_form φ))).
peapply (@entail_correct p []).
+ intros ψ Hψ Hyp. rewrite elem_of_list_In in Hp.
rpeapply (equiv_form_equiv_envF _ _ (equiv_form_simp_form (A p ([], [simp_form φ])))).
peapply (equiv_form_equiv_env _ _ (symmetric_equiv_form(equiv_form_simp_form ψ))).
apply (TopL_rev _ ⊥). peapply (@pq_correct p {[simp_form ψ]}).
* exact ∅.
* intros φ0 Hφ0. apply gmultiset_elem_of_singleton in Hφ0. subst.
intro Ho; apply occurs_in_simp_form in Ho. auto with *.
* simpl.
apply (equiv_form_equiv_envF _ _ (equiv_form_simp_form _)).
peapply (equiv_form_equiv_env _ _ (equiv_form_simp_form ψ)).
simpl. erewrite proper_Provable; [exact Hyp| |]; ms.
* rewrite E_of_empty. ms.
Qed.
End PropQuantProp.