diff --git a/theories/iSL/Environments.v b/theories/iSL/Environments.v index 3b9a7b9..e0994af 100755 --- a/theories/iSL/Environments.v +++ b/theories/iSL/Environments.v @@ -158,22 +158,28 @@ match obviously_smaller φ ψ with Definition make_conj φ ψ := match ψ with - | ψ1 ∧ ψ2 => + | ψ1 ∧ ψ2 => match obviously_smaller φ ψ1 with | Lt => φ ∧ ψ2 | Gt => ψ1 ∧ ψ2 | Eq => φ ∧ (ψ1 ∧ ψ2) end - | ψ1 ∨ ψ2 => - if decide (obviously_smaller φ ψ1 = Lt ) - then φ - else φ ∧ (ψ1 ∨ ψ2) - | ψ1 → ψ2 => if decide (obviously_smaller φ ψ1 = Lt) then choose_conj φ ψ2 else choose_conj φ ψ - | ψ => choose_conj φ ψ + | ψ1 ∨ ψ2 => + if decide (obviously_smaller φ ψ1 = Lt ) then φ + else if decide (obviously_smaller φ ψ2 = Lt ) then φ + else choose_conj φ (ψ1 ∨ ψ2) + | ψ1 → ψ2 => + if decide (obviously_smaller φ ψ1 = Lt) then choose_conj φ ψ2 + else choose_conj φ ψ + | ψ => match φ with + | φ1 → φ2 => + if decide (obviously_smaller ψ φ1 = Lt) + then choose_conj φ2 ψ + else choose_conj φ ψ + | _ => choose_conj φ ψ + end end. - - Infix "⊼" := make_conj (at level 60). Lemma occurs_in_make_conj v φ ψ : occurs_in v (φ ⊼ ψ) -> occurs_in v φ \/ occurs_in v ψ. @@ -209,9 +215,9 @@ match ψ with | Eq => φ ∨ (ψ1 ∨ ψ2) end | ψ1 ∧ ψ2 => - if decide (obviously_smaller φ ψ1 = Gt ) - then φ - else φ ∨ (ψ1 ∧ ψ2) + if decide (obviously_smaller φ ψ1 = Gt ) then φ + else if decide (obviously_smaller φ ψ2 = Gt ) then φ + else choose_disj φ (ψ1 ∧ ψ2) |_ => choose_disj φ ψ end. @@ -649,3 +655,6 @@ 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 θ0; split; [eauto using difference_include|simpl; tauto]; eauto] end. + + +(* TODO: move in optimisations *) \ No newline at end of file diff --git a/theories/iSL/Optimizations.v b/theories/iSL/Optimizations.v index a22dff6..025cfaa 100644 --- a/theories/iSL/Optimizations.v +++ b/theories/iSL/Optimizations.v @@ -172,7 +172,7 @@ case_eq (obviously_smaller φ' ψ'); intro Heq. Qed. -Lemma choose_and_equiv_R φ ψ φ' ψ': +Lemma choose_conj_equiv_R φ ψ φ' ψ': (φ' ≼ φ) -> (ψ' ≼ ψ) -> choose_conj φ' ψ' ≼ φ ∧ ψ. Proof. intros Hφ Hψ. @@ -199,15 +199,25 @@ Proof. intros Hφ Hψ. unfold make_conj. destruct ψ'; try (apply choose_conj_equiv_L; assumption). +- destruct φ'; try (apply choose_conj_equiv_L; assumption). + case decide; intro; try (apply choose_conj_equiv_L; assumption). + apply obviously_smaller_compatible_LT in e. + apply weak_cut with ((φ ∧ φ'1) ∧ ψ). + + apply AndL; repeat apply AndR. auto with proof. + * exch 0. apply weakening; apply weak_cut with v; assumption. + * apply generalised_axiom. + + apply choose_conj_equiv_L; auto with proof. +- apply exfalso, AndL. exch 0. apply weakening, Hψ. - case_eq (obviously_smaller φ' ψ'1); intro Heq. + apply and_congruence; assumption. + apply and_congruence. * assumption. * apply AndR_rev in Hψ; apply Hψ. + apply AndL. exch 0. apply weakening. assumption. -- case (decide (obviously_smaller φ' ψ'1 = Lt)); intro. +- repeat case decide; intros. + apply AndL. now apply weakening. - + apply and_congruence; assumption. + + apply AndL. now apply weakening. + + apply choose_conj_equiv_L ; assumption. - case (decide (obviously_smaller φ' ψ'1 = Lt)); intro. + apply weak_cut with (φ ∧ (φ ∧ ψ)). * apply AndR; auto with proof. @@ -217,6 +227,15 @@ destruct ψ'; try (apply choose_conj_equiv_L; assumption). -- apply weak_cut with φ'; auto with proof. -- apply ImpR. exch 0. apply ImpR_rev, AndL. exch 0. apply weakening, Hψ. + apply choose_conj_equiv_L; assumption. +- destruct φ'; try (apply choose_conj_equiv_L; assumption). + case decide; intro; try (apply choose_conj_equiv_L; assumption). + apply weak_cut with (ψ ∧ (φ ∧ φ'1)). + + apply AndL, AndR. auto with proof. apply AndR. auto with proof. + exch 0. apply weakening. apply weak_cut with (□ ψ'). auto with proof. + now apply obviously_smaller_compatible_LT. + + apply weak_cut with ((φ ∧ φ'1) ∧ ψ). + * apply AndR; auto with proof. + * apply choose_conj_equiv_L; auto with proof. Qed. Lemma make_conj_equiv_R φ ψ φ' ψ' : @@ -225,8 +244,10 @@ Proof. intros Hφ Hψ. unfold make_conj. destruct ψ'. -- now apply choose_and_equiv_R. -- now apply choose_and_equiv_R. +- destruct φ'; try case decide; intros; apply choose_conj_equiv_R; try assumption. + eapply imp_cut; eassumption. +- destruct φ'; try case decide; intros; apply choose_conj_equiv_R; try assumption. + eapply imp_cut; eassumption. - case_eq (obviously_smaller φ' ψ'1); intro Heq. + now apply and_congruence. + apply AndR. @@ -240,17 +261,23 @@ destruct ψ'. -- apply obviously_smaller_compatible_GT; apply Heq. -- assumption. * assumption. -- case (decide (obviously_smaller φ' ψ'1 = Lt)); [intro HLt | intro Hneq]. +- repeat case decide; intros. + apply AndR. * assumption. * eapply weak_cut. - -- apply obviously_smaller_compatible_LT; apply HLt. + -- apply obviously_smaller_compatible_LT; eassumption. -- apply OrL_rev in Hψ; apply Hψ. - + apply and_congruence; assumption. + + apply AndR. + * assumption. + * eapply weak_cut. + -- apply obviously_smaller_compatible_LT; eassumption. + -- apply OrL_rev in Hψ; apply Hψ. + + apply choose_conj_equiv_R; assumption. - case decide; intro Heq. - + apply choose_and_equiv_R. assumption. eapply weak_cut; [|exact Hψ]. auto with proof. - + apply choose_and_equiv_R; assumption. -- apply choose_and_equiv_R; assumption. + + apply choose_conj_equiv_R. assumption. eapply weak_cut; [|exact Hψ]. auto with proof. + + apply choose_conj_equiv_R; assumption. +- destruct φ'; try case decide; intros; apply choose_conj_equiv_R; try assumption. + eapply imp_cut; eassumption. Qed. Lemma specialised_weakening Γ φ ψ : (φ ≼ ψ) -> Γ•φ ⊢ ψ. @@ -357,13 +384,19 @@ Lemma make_disj_equiv_L φ ψ φ' ψ' : Proof. intros Hφ Hψ. unfold make_disj. -destruct ψ'; try (apply choose_disj_equiv_L; assumption). - case (decide (obviously_smaller φ' ψ'1 = Gt)); [intro HGt | intro Hneq1]. +destruct ψ'; try (apply choose_disj_equiv_L; assumption). +- repeat case decide; intros. + apply OrL. * assumption. * eapply weak_cut. -- apply Hψ. -- apply AndL; apply weakening; now apply obviously_smaller_compatible_GT. - + now apply or_congruence. + + apply OrL. + * assumption. + * eapply weak_cut. + -- apply Hψ. + -- apply AndL; exch 0. apply weakening; now apply obviously_smaller_compatible_GT. + + now apply choose_disj_equiv_L. - case_eq (obviously_smaller φ' ψ'1); intro Heq. + now apply or_congruence. + apply OrL. @@ -387,9 +420,10 @@ unfold make_disj. destruct ψ'. - now apply choose_disj_equiv_R. - now apply choose_disj_equiv_R. -- case (decide (obviously_smaller φ' ψ'1 = Gt)); intro. +- repeat case decide; intros. + now apply OrR1. - + now apply or_congruence. + + now apply OrR1. + + now apply choose_disj_equiv_R. - case_eq (obviously_smaller φ' ψ'1); intro Heq. + now apply or_congruence. + now apply OrR2. @@ -401,8 +435,6 @@ destruct ψ'. - now apply choose_disj_equiv_R. Qed. - - Lemma make_disj_sound_L Γ φ ψ θ : Γ•φ ∨ψ ⊢ θ -> Γ•make_disj φ ψ ⊢ θ. Proof. intro H. @@ -469,7 +501,7 @@ assert(Hcut : - intro Hall. case in_dec; intro; apply (fst IHΔ); auto with *. - case in_dec in Hψ; apply IHΔ in Hψ; destruct Hψ as [Hψ Hind]. - + split; trivial; intros φ Hin; destruct (decide (φ = a)); auto with *. + + split; trivial; intros φ Hin; destruct (decide (φ = a)); auto 2 with *. subst. apply Hind. now apply elem_of_list_In. + apply make_disj_complete_L in Hψ. apply OrL_rev in Hψ as [Hψ Ha]. diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index a6b2092..9241024 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -4,22 +4,192 @@ Require Import ISL.Environments ISL.Sequents ISL.SequentProps ISL.Cut ISL.Optimi that there are no disjuctions on the left of any of the input formulas, i.e. φ and ψ cannot be of the form ((... ∨ ... ) ∨ ...). Since this function is called with the inputs previously simplified (see `simp`) this invariant is assured. *) +Fixpoint simp_ors φ ψ := +match (φ,ψ) with + |(φ1 ∨ φ2, ψ1 ∨ ψ2) => φ1 ⊻ (ψ1 ⊻ (simp_ors φ2 ψ2)) + |(φ1 ∨ φ2, ψ) => ψ ⊻ (φ1 ∨ φ2) + |(φ, ψ1 ∨ ψ2) => φ ⊻ (ψ1 ∨ ψ2) + |(φ, ψ) => φ ⊻ ψ +end. + +(* Same as `simp_ors` but for large conjunctions. *) +Fixpoint simp_ands φ ψ := +match (φ,ψ) with + |(φ1 ∧ φ2, ψ1 ∧ ψ2) => φ1 ⊼ (ψ1 ⊼ (simp_ands φ2 ψ2)) + |(φ1 ∧ φ2, ψ) => ψ ⊼ (φ1 ∧ φ2) + |(φ, ψ1 ∧ ψ2) => φ ⊼ (ψ1 ∧ ψ2) + |(φ, ψ) => φ ⊼ ψ +end. + + +Definition simp_imp φ ψ := + if decide (obviously_smaller φ ψ = Lt) then ⊤ + else if decide (obviously_smaller φ ⊥ = Lt) then ⊤ + else if decide (obviously_smaller ψ ⊤ = Gt) then ⊤ + else if decide (obviously_smaller φ ⊤ = Gt) then ψ + else if decide (obviously_smaller ψ ⊥ = Lt) then ¬φ + else φ → ψ. + +(* Same as `simp_ors` but for nested implications. *) +Fixpoint simp_imps φ ψ := +match (φ,ψ) with + |(φ1, ψ1 → ψ2) => simp_imps (simp_ands φ1 ψ1) ψ2 + |(φ, ψ) => simp_imp φ ψ +end. Fixpoint simp φ := match φ with - | φ ∨ ψ => make_disj (simp φ) (simp ψ) - | φ ∧ ψ => make_conj (simp φ) (simp ψ) - | φ → ψ => make_impl (simp φ) (simp ψ) + | φ ∨ ψ => simp_ors (simp φ) (simp ψ) + | φ ∧ ψ => simp_ands (simp φ) (simp ψ) + | φ → ψ => simp_imps (simp φ) (simp ψ) | □ φ => □ (simp φ) | _ => φ end. +Lemma or_comm φ ψ: φ ∨ ψ ≼ ψ ∨ φ. +Proof. +apply OrL; [apply OrR2 | apply OrR1]; apply generalised_axiom. +Qed. + + +Lemma or_comm_ctx_L φ ψ ϴ: (φ ∨ ψ ≼ ϴ) -> ψ ∨ φ ≼ ϴ. +Proof. +intro H. +eapply weak_cut; [apply or_comm | assumption]. +Qed. + +Lemma or_comm_ctx_R φ ψ ϴ: (ϴ ≼ φ ∨ ψ ) -> ϴ ≼ ψ ∨ φ. +Proof. +intro H. +eapply weak_cut; [apply H | apply or_comm]. +Qed. + +Lemma or_assoc_R φ ψ ϴ : ((φ ∨ ψ) ∨ ϴ ≼ φ ∨ (ψ ∨ ϴ)). +Proof. + apply OrL. + - apply OrL. + + apply OrR1; apply generalised_axiom. + + apply OrR2; apply OrR1; apply generalised_axiom. + - apply OrR2; apply OrR2; apply generalised_axiom. +Qed. + +Lemma or_assoc_L φ ψ ϴ : (φ ∨ (ψ ∨ ϴ) ≼ (φ ∨ ψ) ∨ ϴ). +Proof. + apply OrL. + - apply OrR1; apply OrR1; apply generalised_axiom. + - apply OrL. + + apply OrR1; apply OrR2; apply generalised_axiom. + + apply OrR2; apply generalised_axiom. +Qed. + + +Lemma or_assoc_ctx_L_R φ ψ ϴ a: + (φ ∨ (ψ ∨ ϴ) ≼ a) -> ((φ ∨ ψ) ∨ ϴ) ≼ a. +Proof. +intro H. +eapply weak_cut; [apply or_assoc_R | assumption]. +Qed. + +Lemma or_assoc_ctx_R_L φ ψ ϴ a: + (a ≼ (φ ∨ ψ) ∨ ϴ) ->a ≼ φ ∨ (ψ ∨ ϴ). +Proof. +intro H. +eapply weak_cut; [apply H | apply or_assoc_R]. +Qed. + +Lemma or_assoc_ctx_R_R φ ψ ϴ a: + (a ≼ φ ∨ (ψ ∨ ϴ)) ->a ≼ (φ ∨ ψ) ∨ ϴ. +Proof. +intro H. +eapply weak_cut; [apply H | apply or_assoc_L]. +Qed. + +Lemma make_disj_comm φ ψ : + (φ ⊻ ψ) ≼ (ψ ⊻ φ). +Proof. +apply (weak_cut _ (φ ∨ ψ) _). +- apply make_disj_equiv_R; apply generalised_axiom. +- apply (weak_cut _ (ψ ∨ φ) _). + + apply or_comm. + + apply make_disj_equiv_L; apply generalised_axiom. +Qed. + +Lemma make_disj_comm_ctx_R a φ ψ : + (a ≼ φ ⊻ ψ) -> a ≼ ψ ⊻ φ. +Proof. +intro H. +eapply weak_cut; [apply H | apply make_disj_comm]. +Qed. + +Lemma make_disj_comm_ctx_L a φ ψ : + (φ ⊻ ψ ≼ a) -> ψ ⊻ φ ≼ a. +Proof. +intro H. +eapply weak_cut; [apply make_disj_comm | apply H]. +Qed. + +Lemma simp_ors_self_equiv_L φ ψ: + (φ ∨ ψ) ≼ simp_ors φ ψ. +Proof. +generalize ψ. +induction φ; +intro ψ0; +destruct ψ0; unfold simp_ors; try (eapply make_disj_equiv_L; apply generalised_axiom); +try (apply make_disj_comm_ctx_R; apply make_disj_equiv_L; apply generalised_axiom). +assert (H: φ1 ∨ ψ0_1 ∨ φ2 ∨ ψ0_2 ≼ φ1 ⊻ (ψ0_1 ⊻ simp_ors φ2 ψ0_2)). +- apply make_disj_equiv_L. + + apply generalised_axiom. + + apply make_disj_equiv_L. + * apply generalised_axiom. + * apply IHφ2. +- eapply weak_cut. + + apply or_assoc_ctx_L_R. + apply OrL. + * apply OrR1. apply generalised_axiom. + * apply OrR2. apply or_comm_ctx_L. + apply OrL. + -- apply or_assoc_ctx_R_L. apply or_comm_ctx_L. + apply or_comm_ctx_L. + apply or_comm_ctx_R. + apply or_assoc_ctx_R_L. + apply OrR1. + apply or_comm. + -- apply OrR2; apply OrR1; apply generalised_axiom. + + assumption. +Qed. Lemma simp_equiv_or_L φ ψ : (φ ≼ simp φ) -> (ψ ≼ simp ψ) -> (φ ∨ ψ) ≼ simp (φ ∨ ψ). Proof. intros Hφ Hψ. -eapply weak_cut; [apply or_congruence; [apply Hφ | apply Hψ] | apply make_disj_equiv_L; apply generalised_axiom]. +eapply weak_cut; [apply or_congruence; [apply Hφ | apply Hψ] | apply simp_ors_self_equiv_L]. +Qed. + + +Lemma simp_ors_self_equiv_R φ ψ: + simp_ors φ ψ ≼ φ ∨ ψ. +Proof. +generalize ψ. +induction φ; +intro ψ0; +destruct ψ0; unfold simp_ors; +try (eapply make_disj_equiv_R; apply generalised_axiom); +try (apply make_disj_comm_ctx_L; apply make_disj_equiv_R; apply generalised_axiom). +assert (H: φ1 ⊻ (ψ0_1 ⊻ simp_ors φ2 ψ0_2) ≼ φ1 ∨ ψ0_1 ∨ φ2 ∨ ψ0_2). +- apply make_disj_equiv_R. + + apply generalised_axiom. + + apply make_disj_equiv_R. + * apply generalised_axiom. + * apply IHφ2. +- apply or_assoc_ctx_R_R. + eapply weak_cut. + + apply H. + + apply OrL. + * apply OrR1; apply generalised_axiom. + * apply OrR2. apply or_comm_ctx_R. apply or_assoc_ctx_R_R. + apply OrL. + -- apply OrR1; apply generalised_axiom. + -- apply OrR2; apply or_comm. Qed. Lemma simp_equiv_or_R φ ψ: @@ -27,7 +197,7 @@ Lemma simp_equiv_or_R φ ψ: simp (φ ∨ ψ) ≼ (φ ∨ ψ). Proof. intros Hφ Hψ. -eapply weak_cut; [ apply make_disj_equiv_R; apply generalised_axiom | apply or_congruence; [apply Hφ | apply Hψ]]. +eapply weak_cut; [ apply simp_ors_self_equiv_R | apply or_congruence; [apply Hφ | apply Hψ]]. Qed. Lemma simp_equiv_or φ ψ: @@ -40,35 +210,159 @@ split; [ apply simp_equiv_or_L | apply simp_equiv_or_R]; try apply IHφ ; try ap Qed. -Lemma box_congr φ ψ: - (φ ≼ ψ) -> □ φ ≼ □ ψ. -Proof. +Lemma and_comm φ ψ: + φ ∧ ψ ≼ ψ ∧ φ. +Proof. +apply AndL; apply AndR; [exch 0|]; apply weakening; apply generalised_axiom. +Qed. + + +Lemma and_comm_ctx_L φ ψ ϴ: + (φ ∧ ψ ≼ ϴ) -> ψ ∧ φ ≼ ϴ. +Proof. intro H. -apply BoxR. -box_tac. apply weakening. -ms. +eapply weak_cut; [apply and_comm | assumption]. Qed. -Lemma simp_equiv_box φ: - (φ ≼ simp φ) * (simp φ ≼ φ) -> - (□ φ ≼ □ (simp φ)) * (□ (simp φ) ≼ □ φ). + +Lemma and_assoc_R φ ψ ϴ : + ((φ ∧ ψ) ∧ ϴ ≼ φ ∧ (ψ ∧ ϴ)). Proof. -intro IHφ. -split; apply box_congr; apply IHφ. + apply AndL; exch 0; apply AndL. + apply AndR. + - exch 0. apply generalised_axiom. + - apply AndR. + + apply generalised_axiom. + + exch 1. exch 0. apply generalised_axiom. +Qed. + +Lemma and_assoc_L φ ψ ϴ : + (φ ∧ (ψ ∧ ϴ) ≼ (φ ∧ ψ) ∧ ϴ). +Proof. + apply AndL; apply AndL. + apply AndR. + - apply AndR. + + exch 1. exch 0. apply generalised_axiom. + + exch 0. apply generalised_axiom. + - apply generalised_axiom. +Qed. + + +Lemma and_assoc_ctx_L_R φ ψ ϴ a: + (φ ∧ (ψ ∧ ϴ) ≼ a) -> ((φ ∧ ψ) ∧ ϴ) ≼ a. +Proof. +intro H. +eapply weak_cut; [apply and_assoc_R | assumption]. +Qed. + +Lemma and_assoc_ctx_R_L φ ψ ϴ a: + (a ≼ (φ ∧ ψ) ∧ ϴ) -> a ≼ φ ∧ (ψ ∧ ϴ). +Proof. +intro H. +eapply weak_cut; [apply H | apply and_assoc_R]. +Qed. + +Lemma and_assoc_ctx_R_R φ ψ ϴ a: + (a ≼ φ ∧ (ψ ∧ ϴ)) -> a ≼ (φ ∧ ψ) ∧ ϴ. +Proof. +intro H. +eapply weak_cut; [apply H | apply and_assoc_L]. +Qed. + + +Lemma make_conj_comm φ ψ : + (φ ⊼ ψ) ≼ (ψ ⊼ φ). +Proof. +apply (weak_cut _ (φ ∧ ψ) _). +- apply make_conj_equiv_R; apply generalised_axiom. +- apply (weak_cut _ (ψ ∧ φ) _). + + apply and_comm. + + apply make_conj_equiv_L; apply generalised_axiom. +Qed. + +Lemma make_conj_comm_ctx_R a φ ψ : + (a ≼ φ ⊼ ψ) -> a ≼ ψ ⊼ φ. +Proof. +intro H. +eapply weak_cut; [apply H | apply make_conj_comm]. +Qed. + +Lemma make_conj_comm_ctx_L a φ ψ : + (φ ⊼ ψ ≼ a) -> ψ ⊼ φ ≼ a. +Proof. +intro H. +eapply weak_cut; [apply make_conj_comm | apply H]. +Qed. + + +Lemma simp_ands_self_equiv_L φ ψ: + (φ ∧ ψ) ≼ simp_ands φ ψ. +Proof. +generalize ψ. +induction φ; +intro ψ0; unfold simp_ands; +destruct ψ0; try (eapply make_conj_equiv_L; apply generalised_axiom); +try (apply make_conj_comm_ctx_R; apply make_conj_equiv_L; apply generalised_axiom). +assert (H: φ1 ∧ ψ0_1 ∧ φ2 ∧ ψ0_2 ≼ φ1 ⊼ (ψ0_1 ⊼ simp_ands φ2 ψ0_2)). +- apply make_conj_equiv_L. + + apply generalised_axiom. + + apply make_conj_equiv_L. + * apply generalised_axiom. + * apply IHφ2. +- eapply weak_cut. + + apply and_assoc_ctx_L_R. + do 3 (apply AndL). + apply AndR. + * exch 2. exch 1. exch 0. apply generalised_axiom. + * apply AndR. + -- exch 0. apply generalised_axiom. + -- apply AndR. + ++ exch 1. exch 0. apply generalised_axiom. + ++ apply generalised_axiom. + + assumption. +Qed. + + +Lemma simp_ands_self_equiv_R φ ψ: + simp_ands φ ψ ≼ φ ∧ ψ. +Proof. +generalize ψ. +induction φ; +intro ψ0; +destruct ψ0; +try (eapply make_conj_equiv_R; apply generalised_axiom); +try (apply make_conj_comm_ctx_L; apply make_conj_equiv_R; apply generalised_axiom). +assert (H: φ1 ⊼ (ψ0_1 ⊼ simp_ands φ2 ψ0_2) ≼ φ1 ∧ ψ0_1 ∧ φ2 ∧ ψ0_2). +- apply make_conj_equiv_R. + + apply generalised_axiom. + + apply make_conj_equiv_R. + * apply generalised_axiom. + * apply IHφ2. +- apply and_assoc_ctx_R_R. + eapply weak_cut. + + apply H. + + do 3 (apply AndL). + apply AndR. + * exch 2. exch 1. exch 0. apply generalised_axiom. + * apply AndR. + -- exch 0. apply generalised_axiom. + -- apply AndR. + ++ exch 1. exch 0. apply generalised_axiom. + ++ apply generalised_axiom. Qed. Lemma simp_equiv_and_L φ ψ : (φ ≼ simp φ) -> (ψ ≼ simp ψ) -> (φ ∧ ψ) ≼ simp (φ ∧ ψ). Proof. intros Hφ Hψ. -eapply weak_cut; [apply and_congruence; [apply Hφ | apply Hψ] | apply make_conj_equiv_L; apply generalised_axiom]. +eapply weak_cut; [apply and_congruence; [apply Hφ | apply Hψ] | apply simp_ands_self_equiv_L]. Qed. Lemma simp_equiv_and_R φ ψ : (simp φ ≼ φ) -> (simp ψ ≼ ψ) -> simp (φ ∧ ψ) ≼ φ ∧ ψ. Proof. intros Hφ Hψ. -eapply weak_cut; [apply make_conj_equiv_R; apply generalised_axiom | apply and_congruence; [apply Hφ | apply Hψ]]. +eapply weak_cut; [apply simp_ands_self_equiv_R | apply and_congruence; [apply Hφ | apply Hψ]]. Qed. Lemma simp_equiv_and φ ψ: @@ -80,15 +374,96 @@ intros IHφ IHψ. split; [ apply simp_equiv_and_L | apply simp_equiv_and_R]; try apply IHφ ; try apply IHψ. Qed. +Lemma simp_imp_self_equiv_L φ ψ: + (φ → ψ) ≼ simp_imp φ ψ. +Proof. +unfold simp_imp. +case decide as [Heq |]; [apply top_provable|]. +case decide as [HφBot |]; [apply top_provable|]. +case decide as [HψTop |]; [apply top_provable|]. +case decide as [HφTop |]. +- apply weak_ImpL. + + eapply additive_cut. + * apply top_provable. + * eapply additive_cut. + -- apply obviously_smaller_compatible_GT; apply HφTop. + -- apply generalised_axiom. + + apply generalised_axiom. +- case decide as [HψBot |]. + + apply ImpR. exch 0. apply ImpL. + * apply weakening. apply generalised_axiom. + * eapply additive_cut with ⊥. + -- exch 0. apply weakening, obviously_smaller_compatible_LT, HψBot. + -- do 2 (exch 0; apply weakening). now apply obviously_smaller_compatible_LT. + + apply ImpR. exch 0. apply ImpL. + * apply weakening, generalised_axiom. + * exch 0. apply weakening, generalised_axiom. +Qed. + +Lemma simp_imp_self_equiv_R φ ψ: + simp_imp φ ψ ≼ φ → ψ. +Proof. +unfold simp_imp. +case decide as [Heq |]. + - apply weakening, ImpR, obviously_smaller_compatible_LT, Heq. + - case decide as [HφBot |]. + + apply weakening. + apply ImpR. + eapply weak_cut with ⊥. + * apply obviously_smaller_compatible_LT, HφBot. + * apply ExFalso. + + case decide as [HψTop |]. + * apply weakening. + apply ImpR. + eapply weak_cut. + -- apply top_provable. + -- apply obviously_smaller_compatible_GT, HψTop. + * case decide as [HφTop |]. + -- apply ImpR. apply weakening, generalised_axiom. + -- case decide as [HψBot |]. + ++ apply ImpR. + eapply additive_cut with ψ. + ** exch 0. apply weak_ImpL. + --- apply generalised_axiom. + --- apply ExFalso. + ** apply generalised_axiom. + ++ apply ImpR. exch 0. apply ImpL. + ** apply weakening, generalised_axiom. + ** exch 0. apply weakening, generalised_axiom. +Qed. + +Lemma simp_imps_self_equiv_L φ ψ: + (φ → ψ) ≼ simp_imps φ ψ. +Proof. +revert φ; induction ψ; intro φ; unfold simp_imps; +auto using simp_imp_self_equiv_L. +fold simp_imps. apply ImpLAnd_rev. +eapply weak_cut; [| apply IHψ2]. +apply ImpR. exch 0. apply ImpL. +- apply weakening, simp_ands_self_equiv_R. +- apply generalised_axiom. +Qed. + +Lemma simp_imps_self_equiv_R φ ψ: + simp_imps φ ψ ≼ (φ → ψ). +Proof. +revert φ; induction ψ; intro φ; unfold simp_imps; +auto using simp_imp_self_equiv_R. +fold simp_imps. apply ImpR, ImpR, AndL_rev, ImpR_rev. +eapply weak_cut; [apply IHψ2|]. +apply ImpR. exch 0. apply ImpL. +- apply weakening, simp_ands_self_equiv_L. +- apply generalised_axiom. +Qed. + Lemma simp_equiv_imp_L φ ψ : (simp φ ≼ φ) -> (ψ ≼ simp ψ) -> (φ → ψ) ≼ simp (φ → ψ). Proof. intros HφR HψL. simpl. -eapply weak_cut. apply make_impl_sound_R, generalised_axiom. -apply make_impl_sound_R, make_impl_sound_L. -apply ImpR. exch 0. apply ImpL. +eapply weak_cut; [| apply simp_imps_self_equiv_L]. apply ImpR. exch 0. +apply ImpL. - apply weakening. apply HφR. - exch 0. apply weakening. apply HψL. Qed. @@ -100,7 +475,7 @@ Proof. intros HφR HψL. simpl. eapply weak_cut with (simp φ → simp ψ). -- apply make_impl_complete_R, generalised_axiom. +- apply simp_imps_self_equiv_R. - apply ImpR. exch 0. apply ImpL. + apply weakening, HφR. + exch 0. apply weakening, HψL. @@ -115,6 +490,22 @@ intros IHφ IHψ. split; [ apply simp_equiv_imp_L | apply simp_equiv_imp_R]; try apply IHφ ; try apply IHψ. Qed. +Lemma box_congr φ ψ: + (φ ≼ ψ) -> □ φ ≼ □ ψ. +Proof. +intro H. +apply BoxR. +box_tac. apply weakening. +ms. +Qed. + +Lemma simp_equiv_box φ: + (φ ≼ simp φ) * (simp φ ≼ φ) -> + (□ φ ≼ □ (simp φ)) * (□ (simp φ) ≼ □ φ). +Proof. +intro IHφ. +split; apply box_congr; apply IHφ. +Qed. Theorem simp_equiv φ : (φ ≼ (simp φ)) * ((simp φ) ≼ φ). @@ -195,20 +586,27 @@ Proof. intros H. unfold make_disj. destruct ψ; try (now apply vars_incl_choose_disj); -destruct (obviously_smaller φ ψ1); try assumption; vars_incl_tac. -apply or_vars_incl. -- now apply (or_vars_incl _ (Or ψ1 ψ2)). -- apply or_vars_incl in H. - apply (or_vars_incl ψ1 _). - apply H. +repeat case decide; intros; try assumption; vars_incl_tac. +- now apply vars_incl_choose_disj. +- apply or_vars_incl in H. case obviously_smaller; vars_tac; firstorder. Qed. -Lemma vars_incl_make_disj φ ψ V : - vars_incl φ V -> vars_incl ψ V -> vars_incl (make_disj φ ψ) V. +Lemma vars_incl_simp_ors φ ψ V : + vars_incl φ V -> vars_incl ψ V -> vars_incl (simp_ors φ ψ) V. Proof. generalize ψ. induction φ; intro ψ0; destruct ψ0; intros Hφ Hψ; try ( apply vars_incl_make_disj_equiv_disj; apply or_vars_incl; assumption). +simpl. +apply vars_incl_make_disj_equiv_disj. +apply or_vars_incl. +- now apply (or_vars_incl _ φ2 _). +- apply vars_incl_make_disj_equiv_disj. + apply or_vars_incl. + + now apply (or_vars_incl _ ψ0_2 _). + + apply IHφ2. + * now apply (or_vars_incl φ1 _ _). + * now apply (or_vars_incl ψ0_1 _ _). Qed. @@ -233,23 +631,53 @@ Proof. intros H. unfold make_conj. destruct ψ; try (now apply vars_incl_choose_conj); -destruct (obviously_smaller φ ψ1); repeat case decide; intros; try discriminate; try assumption; vars_incl_tac; +match goal with |- vars_incl match ?a with _ => _ end _ => destruct a end; +repeat case decide; intros; try discriminate; try assumption; vars_incl_tac; try apply vars_incl_choose_conj; apply and_vars_incl; vars_incl_tac; apply and_vars_incl in H; vars_tac; vars_incl_tac. Qed. -Lemma vars_incl_make_conj φ ψ V : - vars_incl φ V -> vars_incl ψ V -> vars_incl (make_conj φ ψ) V. +Lemma vars_incl_simp_ands φ ψ V : + vars_incl φ V -> vars_incl ψ V -> vars_incl (simp_ands φ ψ) V. Proof. generalize ψ. induction φ; intro ψ0; destruct ψ0; intros Hφ Hψ; try (apply vars_incl_make_conj_equiv_conj; apply and_vars_incl; assumption). +simpl. +apply vars_incl_make_conj_equiv_conj. +apply and_vars_incl. +- vars_incl_tac. +- apply vars_incl_make_conj_equiv_conj. + apply and_vars_incl. + + vars_incl_tac. + + apply IHφ2; vars_incl_tac. Qed. -Lemma vars_incl_make_impl φ ψ V : - vars_incl φ V -> vars_incl ψ V -> vars_incl (make_impl φ ψ) V. +Lemma vars_incl_simp_imp φ ψ V : + vars_incl φ V -> vars_incl ψ V -> vars_incl (simp_imp φ ψ) V. Proof. -intros Hφ Hψ x Hx. apply occurs_in_make_impl in Hx. intuition. +intros Hφ Hψ. +simpl. unfold simp_imp. +case decide as []. + + vars_incl_tac. + + case decide as []. + * vars_incl_tac. + * case decide as []. + -- vars_incl_tac. + -- case decide as []. + ++ assumption. + ++ case decide as []; vars_incl_tac. +Qed. + +Lemma vars_incl_simp_imps φ ψ V : + vars_incl φ V -> vars_incl ψ V -> vars_incl (simp_imps φ ψ) V. +Proof. +revert φ; induction ψ; intros φ Hφ Hψ; simpl; +try apply vars_incl_simp_imp; trivial. +apply IHψ2. +- apply vars_incl_simp_ands; trivial. + intros ? ?; apply Hψ; simpl; tauto. +- intros ? ?; apply Hψ; simpl; tauto. Qed. Lemma vars_incl_simp φ V : @@ -257,9 +685,9 @@ Lemma vars_incl_simp φ V : Proof. intro H. induction φ; auto; simpl; -[ apply vars_incl_make_conj; [apply IHφ1| apply IHφ2]| - apply vars_incl_make_disj; [apply IHφ1| apply IHφ2]| - apply vars_incl_make_impl; [apply IHφ1| apply IHφ2] +[ apply vars_incl_simp_ands; [apply IHφ1| apply IHφ2]| + apply vars_incl_simp_ors; [apply IHφ1| apply IHφ2]| + apply vars_incl_simp_imps; [apply IHφ1| apply IHφ2] ]; vars_incl_tac. Qed. @@ -343,3 +771,5 @@ Proof. reflexivity. Qed. Example ex5: simp (And (Implies (Var "a") (Var "a")) (Implies (Var "a") (Var "a"))) = Implies Bot Bot. Proof. reflexivity. Qed. +Example ex6: simp (Or ⊥ (And (Var "a") (Var "b")))= (And (Var "a") (Var "b")). +Proof. reflexivity. Qed.