diff --git a/bin/benchmark.ml b/bin/benchmark.ml index 871ea55..2b311c8 100644 --- a/bin/benchmark.ml +++ b/bin/benchmark.ml @@ -27,11 +27,12 @@ let time f x = { value = fx; time = Sys.time () -. t } let print_value_results { name; before; after } = - Printf.printf "| %s | %d | %d | %.2f | %.4f |\n" name before.value after.value + Printf.printf "| %s | %d | %d | %.2f | %.4f | %.4f |\n" name before.value + after.value (percentage_reduction (float_of_int before.value) (float_of_int after.value)) - before.time + before.time after.time let bench_one fs = let f = eval fs in @@ -55,8 +56,9 @@ let bench_one fs = let print_bench_value_info benches = Printf.printf "| Formula | Interpolant weight | Simplified interpolant weight | \ - Percentage reduction |Interpolant computation time (s)|\n\ - |--|--|--|--|--|\n"; + Percentage reduction | Interpolant computation time (s)| Simplification \ + computation time (s)|\n\ + |--|--|--|--|--|--|\n"; List.iter print_value_results benches; print_newline (); diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index 0d3b998..4fc57bd 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -1,13 +1,24 @@ Require Import ISL.Environments ISL.Sequents ISL.SequentProps ISL.Cut. -Definition obviously_smaller (φ : form) ψ := - if decide (φ = ⊥) then Lt - else if decide (ψ = ⊥) then Gt - else if decide (φ = ⊤) then Gt - else if decide (ψ = ⊤) then Lt - else if decide (φ = ψ) then Lt - else Eq. +Fixpoint obviously_smaller (φ : form) (ψ : form) := +match (φ, ψ) with + |(Bot, _) => Lt + |(_, Bot) => Gt + |(Bot → _, _) => Gt + |(_, Bot → _) => Lt + |(φ ∧ ψ, ϴ) => match (obviously_smaller φ ϴ, obviously_smaller ψ ϴ) with + | (Lt, _) | (_, Lt) => Lt + | (Gt, Gt) => Gt + | _ => Eq + end + |(φ ∨ ψ, ϴ) => match (obviously_smaller φ ϴ, obviously_smaller ψ ϴ) with + | (Gt, _) | (_, Gt) => Gt + | (Lt, Lt) => Lt + | _ => Eq + end + |(φ, ψ) => if decide (φ = ψ) then Lt else Eq +end. Definition choose_or φ ψ := @@ -26,10 +37,9 @@ match (φ, ψ) with | Eq => φ ∨ (ψ1 ∨ ψ2) end | (φ, ψ1 ∧ ψ2) => - match obviously_smaller φ ψ1 with - | Gt => φ - | _ => φ ∨ (ψ1 ∧ ψ2) - end + if decide (obviously_smaller φ ψ1 = Gt ) + then φ + else φ ∨ (ψ1 ∧ ψ2) |(φ,ψ) => choose_or φ ψ end. @@ -60,10 +70,9 @@ match (φ, ψ) with | Eq => φ ∧ (ψ1 ∧ ψ2) end | (φ, ψ1 ∨ ψ2) => - match obviously_smaller φ ψ1 with - | Lt => φ - | _ => φ ∧ (ψ1 ∨ ψ2) - end + if decide (obviously_smaller φ ψ1 = Lt ) + then φ + else φ ∧ (ψ1 ∨ ψ2) |(φ,ψ) => choose_and φ ψ end. @@ -79,10 +88,13 @@ match (φ,ψ) with |(φ, ψ) => φ ⊼ ψ end. + Definition simp_imp φ ψ := - if decide (φ = ⊤) then ψ - else if decide (φ = ⊥) then ⊤ - else if decide (φ = ψ) then ⊤ + 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 φ → ψ. Fixpoint simp φ := @@ -110,9 +122,8 @@ Lemma preorder_singleton φ ψ: {[φ]} ⊢ ψ -> (φ ≼ ψ). Proof. intro H. -assert (H3: (φ ≼ ψ) = ({[φ]} ⊢ ψ)) by (apply proper_Provable; ms). -rewrite H3. -apply H. +assert (H': ∅ • φ ⊢ ψ ) by peapply H. +apply H'. Qed. Corollary cut2 φ ψ θ: @@ -128,22 +139,65 @@ Proof. apply H. Qed. + +(* Some tactics for the obviously_smaller proofs. *) + +Ltac eq_clean H e := case decide in H; [rewrite e; apply generalised_axiom | discriminate]. + + +Ltac bot_clean := +match goal with +| [ |- Bot ≼ _] => apply ExFalso +| [ |- _ ≼ Bot → _ ] => apply ImpR; apply ExFalso +| _ => idtac +end. + + +Ltac induction_auto := +match goal with +| IH : obviously_smaller ?f ?f2 = Lt → ?f ≼ ?f2 , H : obviously_smaller ?f ?f2 = Lt |- (∅ • ?f) ⊢ ?f2 => + apply IH; assumption +| IH : obviously_smaller ?f ?f2 = Gt → ?f2 ≼ ?f , H : obviously_smaller ?f ?f2 = Gt |- (∅ • ?f2) ⊢ ?f => + apply IH; assumption + +| IH : obviously_smaller ?f _ = Lt → ?f ≼ _ , H : obviously_smaller ?f _ = Lt |- ?f ∧ _ ≼ _ => + apply AndL; apply weakening; apply IH; assumption +| IH : obviously_smaller ?f _ = Lt → ?f ≼ _ , H : obviously_smaller ?f _ = Lt |- _ ∧ ?f ≼ _ => + apply AndL; exch 0; apply weakening; apply IH; assumption + +| IH : obviously_smaller ?f _ = Gt → _ ≼ ?f , H : obviously_smaller ?f _ = Gt |- _ ≼ ?f ∨ _ => + apply OrR1; apply IH; assumption +| IH : obviously_smaller ?f _ = Gt → _ ≼ ?f , H : obviously_smaller ?f _ = Gt |- _ ≼ _ ∨ ?f => + apply OrR2; apply IH; assumption +| _ => idtac +end. + +Ltac imp_clean := +match goal with +| [ H : obviously_smaller _ (?f → _) = Lt |- _ ≼ ?f → _ ] => destruct f; simpl in H; try discriminate; bot_clean +| [ H : obviously_smaller (?f → _) _ = Lt |- (?f → _) ≼ _ ] => destruct f; simpl in H; discriminate +| [ H : obviously_smaller _ (?f → _) = Gt |- (?f → _) ≼ _ ] => destruct f; simpl in H; discriminate +| _ => idtac +end. + + Lemma obviously_smaller_compatible_LT φ ψ : obviously_smaller φ ψ = Lt -> φ ≼ ψ. Proof. intro H. -unfold obviously_smaller in H. -case decide in H. -- rewrite e. apply ExFalso. -- case decide in H. - + contradict H; auto. - + case decide in H. - * contradict H; auto. - * case decide in H. - -- rewrite e. apply top_provable. - -- case decide in H. - ++ rewrite e; apply generalised_axiom. - ++ contradict H; auto. + +induction φ; destruct ψ; try (unfold obviously_smaller in H; try discriminate; eq_clean H e); bot_clean; +imp_clean; +match goal with +| |- _ ∧ _ ≼ ?f => + case_eq (obviously_smaller φ1 f); case_eq (obviously_smaller φ2 f); intros H0 H1; + simpl in H; rewrite H0 in H; rewrite H1 in H; try discriminate; induction_auto +| |- _ ∨ _ ≼ ?f => + case_eq (obviously_smaller φ1 f); case_eq (obviously_smaller φ2 f); intros H0 H1; + simpl in H; rewrite H0 in H; rewrite H1 in H; try discriminate; + apply OrL; induction_auto +| _ => idtac +end; try (destruct φ1; try eq_clean H e; discriminate). Qed. @@ -151,21 +205,30 @@ Lemma obviously_smaller_compatible_GT φ ψ : obviously_smaller φ ψ = Gt -> ψ ≼ φ . Proof. intro H. -unfold obviously_smaller in H. -case decide in H. -- contradict H; auto. -- case decide in H. - + rewrite e. apply ExFalso. - + case decide in H. - * rewrite e. apply top_provable. - * case decide in H. - -- contradict H; auto. - -- case decide in H; contradict H; auto. +induction φ; destruct ψ; try (unfold obviously_smaller in H; try discriminate; eq_clean H e); bot_clean; +imp_clean; +match goal with +| |- ?f ≼ _ ∧ _ => + case_eq (obviously_smaller φ1 f); case_eq (obviously_smaller φ2 f); intros H0 H1; + simpl in H; rewrite H0 in H; rewrite H1 in H; try discriminate; apply AndR; induction_auto +| |- ?f ≼ _∨ _ => + case_eq (obviously_smaller φ1 f); case_eq (obviously_smaller φ2 f); intros H0 H1; + simpl in H; rewrite H0 in H; rewrite H1 in H; try discriminate; induction_auto +| _ => idtac +end; +match goal with +| |- (_ → _) ≼ _ → _ => idtac +| |- (?f → _) ≼ _ => destruct f; discriminate +| |- (∅ • (?f → _)) ⊢ _ => destruct f; discriminate +| |- _ ≼ (?f → _) => destruct φ1; try discriminate; bot_clean +| _ => idtac +end. +simpl in H; destruct ψ1; destruct φ1; try eq_clean H e; bot_clean; simpl in H; discriminate. Qed. + Lemma or_congruence φ ψ φ' ψ': - (φ ≼ φ') -> (ψ ≼ ψ') -> - (φ ∨ ψ) ≼ φ' ∨ ψ'. + (φ ≼ φ') -> (ψ ≼ ψ') -> (φ ∨ ψ) ≼ φ' ∨ ψ'. Proof. intros Hφ Hψ. apply OrL. @@ -174,15 +237,13 @@ apply OrL. Qed. -Lemma or_comm φ ψ: - φ ∨ ψ ≼ ψ ∨ φ. +Lemma or_comm φ ψ: φ ∨ ψ ≼ ψ ∨ φ. Proof. apply OrL; [apply OrR2 | apply OrR1]; apply generalised_axiom. Qed. -Lemma or_comm_ctx_L φ ψ ϴ: - (φ ∨ ψ ≼ ϴ) -> ψ ∨ φ ≼ ϴ. +Lemma or_comm_ctx_L φ ψ ϴ: (φ ∨ ψ ≼ ϴ) -> ψ ∨ φ ≼ ϴ. Proof. intro H. eapply cut2. @@ -190,8 +251,7 @@ apply or_comm. assumption. Qed. -Lemma or_comm_ctx_R φ ψ ϴ: - (ϴ ≼ φ ∨ ψ ) -> ϴ ≼ ψ ∨ φ. +Lemma or_comm_ctx_R φ ψ ϴ: (ϴ ≼ φ ∨ ψ ) -> ϴ ≼ ψ ∨ φ. Proof. intro H. eapply cut2. @@ -199,8 +259,7 @@ apply H. apply or_comm. Qed. -Lemma or_assoc_R φ ψ ϴ : - ((φ ∨ ψ) ∨ ϴ ≼ φ ∨ (ψ ∨ ϴ)). +Lemma or_assoc_R φ ψ ϴ : ((φ ∨ ψ) ∨ ϴ ≼ φ ∨ (ψ ∨ ϴ)). Proof. apply OrL. - apply OrL. @@ -209,8 +268,7 @@ Proof. - apply OrR2; apply OrR2; apply generalised_axiom. Qed. -Lemma or_assoc_L φ ψ ϴ : - (φ ∨ (ψ ∨ ϴ) ≼ (φ ∨ ψ) ∨ ϴ). +Lemma or_assoc_L φ ψ ϴ : (φ ∨ (ψ ∨ ϴ) ≼ (φ ∨ ψ) ∨ ϴ). Proof. apply OrL. - apply OrR1; apply OrR1; apply generalised_axiom. @@ -229,7 +287,6 @@ apply or_assoc_R. assumption. Qed. - Lemma or_assoc_ctx_R_L φ ψ ϴ a: (a ≼ (φ ∨ ψ) ∨ ϴ) ->a ≼ φ ∨ (ψ ∨ ϴ). Proof. @@ -239,8 +296,6 @@ apply H. apply or_assoc_R. Qed. - - Lemma or_assoc_ctx_R_R φ ψ ϴ a: (a ≼ φ ∨ (ψ ∨ ϴ)) ->a ≼ (φ ∨ ψ) ∨ ϴ. Proof. @@ -256,22 +311,31 @@ Lemma choose_or_equiv_L φ ψ φ' ψ': Proof. intros Hφ Hψ. unfold choose_or. -case (decide (obviously_smaller φ' ψ' = Lt)); [intro HLt | intro Hneq1]. --rewrite HLt. apply OrL. +case_eq (obviously_smaller φ' ψ'); intro Heq. +- apply or_congruence; assumption. +- apply OrL. + eapply cut2. * apply Hφ. * apply obviously_smaller_compatible_LT; assumption. - + assumption. - case (decide (obviously_smaller φ' ψ' = Gt)); [intro HGt| intro Hneq2]. - + rewrite HGt. apply OrL. - * assumption. + + assumption. +- apply OrL. + + assumption. + + eapply cut2. * eapply cut2. - -- eapply cut2. - ++ apply Hψ. - ++ apply obviously_smaller_compatible_GT. apply HGt. - -- apply generalised_axiom. - + case (decide (obviously_smaller φ' ψ' = Eq)); [intro HEq| intro Hneq3]. - * rewrite HEq. apply or_congruence; [apply Hφ | apply Hψ]. - * destruct (obviously_smaller φ' ψ'); [contradict Hneq3 | contradict Hneq1 |contradict Hneq2]; trivial. + -- apply Hψ. + -- apply obviously_smaller_compatible_GT. apply Heq. + * apply generalised_axiom. +Qed. + + +Lemma choose_or_equiv_R φ ψ φ' ψ' : + (φ' ≼ φ) -> (ψ' ≼ ψ) -> + choose_or φ' ψ' ≼ φ ∨ ψ. +Proof. +intros Hφ Hψ. +unfold choose_or. +case_eq (obviously_smaller φ' ψ'); intro Heq; +[apply or_congruence| apply OrR2| apply OrR1]; assumption. Qed. Lemma simp_or_equiv_L φ ψ φ' ψ' : @@ -282,44 +346,26 @@ intros Hφ Hψ. unfold simp_or. destruct ψ'; try (apply choose_or_equiv_L; assumption). - case (decide (obviously_smaller φ' ψ'1 = Gt)); [intro HGt | intro Hneq1]. - + rewrite HGt. apply OrL. + + apply OrL. * assumption. * eapply cut2. -- apply Hψ. -- apply AndL; apply weakening; now apply obviously_smaller_compatible_GT. - + destruct (obviously_smaller φ' ψ'1); - [idtac|idtac|contradict Hneq1; auto]; (apply or_congruence; [apply Hφ | apply Hψ]). -- (case (decide (obviously_smaller φ' ψ'1 = Lt)); [intro HLt | intro Hneq1]). - + rewrite HLt. apply OrL. + + apply or_congruence; assumption. +- case_eq (obviously_smaller φ' ψ'1); intro Heq. + + apply or_congruence; assumption. + + apply OrL. * eapply cut2. -- apply Hφ. -- apply OrR1. apply obviously_smaller_compatible_LT; assumption. * assumption. - + case (decide (obviously_smaller φ' ψ'1 = Gt)); [intro HGt| intro Hneq2]. - * rewrite HGt. apply OrL. - -- apply OrR1; assumption. - -- eapply cut2. - ++ apply Hψ. - ++ apply or_congruence; [apply obviously_smaller_compatible_GT; assumption| apply generalised_axiom]. - * case (decide (obviously_smaller φ' ψ'1 = Eq)); [intro HEq| intro Hneq3]. - -- rewrite HEq. apply or_congruence; [apply Hφ | apply Hψ]. - -- destruct (obviously_smaller φ' ψ'1); [contradict Hneq3 | contradict Hneq1 |contradict Hneq2]; trivial. + + apply OrL. + * apply OrR1; assumption. + * eapply cut2. + -- apply Hψ. + -- apply or_congruence; [apply obviously_smaller_compatible_GT; assumption| apply generalised_axiom]. Qed. -Lemma choose_or_equiv_R φ ψ φ' ψ' : - (φ' ≼ φ) -> (ψ' ≼ ψ) -> - choose_or φ' ψ' ≼ φ ∨ ψ. -Proof. -intros Hφ Hψ. -unfold choose_or. -case (decide (obviously_smaller φ' ψ' = Lt)); [intro HLt | intro Hneq1]. -- rewrite HLt. apply OrR2; assumption. -- case (decide (obviously_smaller φ' ψ' = Gt)); [intro HGt| intro Hneq2]. - + rewrite HGt. apply OrR1; assumption. - + case (decide (obviously_smaller φ' ψ' = Eq)); [intro HEq| intro Hneq3]. - * rewrite HEq. apply or_congruence; [apply Hφ | apply Hψ]. - * destruct (obviously_smaller φ' ψ'); [contradict Hneq3 | contradict Hneq1 |contradict Hneq2]; trivial. -Qed. Lemma simp_or_equiv_R φ ψ φ' ψ' : @@ -328,22 +374,21 @@ Lemma simp_or_equiv_R φ ψ φ' ψ' : Proof. intros Hφ Hψ. unfold simp_or. -destruct ψ'; try (apply choose_or_equiv_R; assumption). -- case (decide (obviously_smaller φ' ψ'1 = Gt)); [intro HGt | intro Hneq1]. - + rewrite HGt. now apply OrR1. - + destruct (obviously_smaller φ' ψ'1); - [idtac|idtac|contradict Hneq1; auto]; (apply or_congruence; [apply Hφ | apply Hψ]). -- case (decide (obviously_smaller φ' ψ'1 = Lt)); [intro HLt | intro Hneq1]. - + rewrite HLt. apply OrR2; assumption. - + case (decide (obviously_smaller φ' ψ'1 = Gt)); [intro HGt| intro Hneq2]. - * rewrite HGt. apply OrL. - -- apply OrR1; assumption. - -- apply OrL_rev in Hψ. - apply OrR2. - apply Hψ. - * case (decide (obviously_smaller φ' ψ'1 = Eq)); [intro HEq| intro Hneq3]. - -- rewrite HEq. apply or_congruence; [apply Hφ | apply Hψ]. - -- destruct (obviously_smaller φ' ψ'1); [contradict Hneq3 | contradict Hneq1 |contradict Hneq2]; trivial. +destruct ψ'. +- apply choose_or_equiv_R; assumption. +- apply choose_or_equiv_R; assumption. +- case (decide (obviously_smaller φ' ψ'1 = Gt)); intro. + + now apply OrR1. + + apply or_congruence; assumption. +- case_eq (obviously_smaller φ' ψ'1); intro Heq. + + apply or_congruence; assumption. + + apply OrR2; assumption. + + apply OrL. + * apply OrR1; assumption. + * apply OrL_rev in Hψ. + apply OrR2, Hψ. +- apply choose_or_equiv_R; assumption. +- apply choose_or_equiv_R; assumption. Qed. Lemma simp_or_comm φ ψ : @@ -551,13 +596,10 @@ Lemma choose_and_equiv_L φ ψ φ' ψ': Proof. intros Hφ Hψ. unfold choose_and. -case (decide (obviously_smaller φ' ψ' = Lt)); [intro HLt | intro Hneq1]. -- rewrite HLt. apply AndL. apply weakening. apply Hφ. -- case (decide (obviously_smaller φ' ψ' = Gt)); [intro HGt| intro Hneq2]. - + rewrite HGt. apply AndL. exch 0. apply weakening. apply Hψ. - + case (decide (obviously_smaller φ' ψ' = Eq)); [intro HEq| intro Hneq3]. - * rewrite HEq. apply and_congruence; [apply Hφ | apply Hψ]. - * destruct (obviously_smaller φ' ψ'); [contradict Hneq3 | contradict Hneq1 |contradict Hneq2]; trivial. +case_eq (obviously_smaller φ' ψ'); intro Heq. +- apply and_congruence; assumption. +- apply AndL, weakening, Hφ. +- apply AndL. exch 0. apply weakening, Hψ. Qed. @@ -567,21 +609,18 @@ Lemma choose_and_equiv_R φ ψ φ' ψ': Proof. intros Hφ Hψ. unfold choose_and. -case (decide (obviously_smaller φ' ψ' = Lt)); [intro HLt | intro Hneq1]. -- rewrite HLt. apply AndR. +case_eq (obviously_smaller φ' ψ'); intro Heq. +- apply and_congruence; assumption. +- apply AndR. + assumption. + eapply cut2. - * apply obviously_smaller_compatible_LT. apply HLt. + * apply obviously_smaller_compatible_LT, Heq. * assumption. -- case (decide (obviously_smaller φ' ψ' = Gt)); [intro HGt| intro Hneq2]. - + rewrite HGt. apply AndR. - * eapply cut2. - -- apply obviously_smaller_compatible_GT. apply HGt. - -- assumption. +- apply AndR. + + eapply cut2. + * apply obviously_smaller_compatible_GT, Heq. * assumption. - + case (decide (obviously_smaller φ' ψ' = Eq)); [intro HEq| intro Hneq3]. - * rewrite HEq. apply and_congruence; [apply Hφ | apply Hψ]. - * destruct (obviously_smaller φ' ψ'); [contradict Hneq3 | contradict Hneq1 |contradict Hneq2]; trivial. + + assumption. Qed. @@ -592,19 +631,15 @@ Proof. intros Hφ Hψ. unfold simp_and. destruct ψ'; try (apply choose_and_equiv_L; assumption). -- case (decide (obviously_smaller φ' ψ'1 = Lt)); [intro HLt | intro Hneq1]. - + rewrite HLt. apply and_congruence. +- case_eq (obviously_smaller φ' ψ'1); intro Heq. + + apply and_congruence; assumption. + + apply and_congruence. * assumption. * apply AndR_rev in Hψ; apply Hψ. - + case (decide (obviously_smaller φ' ψ'1 = Gt)); [intro HGt| intro Hneq2]. - * rewrite HGt. apply AndL. exch 0. apply weakening. assumption. - * case (decide (obviously_smaller φ' ψ'1 = Eq)); [intro HEq| intro Hneq3]. - -- rewrite HEq. apply and_congruence; [apply Hφ | apply Hψ]. - -- destruct (obviously_smaller φ' ψ'1); [contradict Hneq3 | contradict Hneq1 |contradict Hneq2]; trivial. -- case (decide (obviously_smaller φ' ψ'1 = Lt)); [intro HLt | intro Hneq1]. - + rewrite HLt. apply AndL. now apply weakening. - + destruct (obviously_smaller φ' ψ'1); - [idtac | contradict Hneq1; auto | idtac]; (apply and_congruence; [apply Hφ | apply Hψ]). + + apply AndL. exch 0. apply weakening. assumption. +- case (decide (obviously_smaller φ' ψ'1 = Lt)); intro. + + apply AndL. now apply weakening. + + apply and_congruence; assumption. Qed. Lemma simp_and_equiv_R φ ψ φ' ψ' : @@ -613,32 +648,31 @@ Lemma simp_and_equiv_R φ ψ φ' ψ' : Proof. intros Hφ Hψ. unfold simp_and. -destruct ψ'; try (apply choose_and_equiv_R; assumption). -- case (decide (obviously_smaller φ' ψ'1 = Lt)); [intro HLt | intro Hneq1]. - + rewrite HLt. apply AndR. +destruct ψ'. +- apply choose_and_equiv_R; assumption. +- apply choose_and_equiv_R; assumption. +- case_eq (obviously_smaller φ' ψ'1); intro Heq. + + apply and_congruence; assumption. + + apply AndR. * apply AndL. apply weakening; assumption. * apply (cut2 _ ( ψ'1 ∧ ψ'2) _). -- apply and_congruence; [now apply obviously_smaller_compatible_LT | apply generalised_axiom]. -- assumption. - + case (decide (obviously_smaller φ' ψ'1 = Gt)); [intro HGt| intro Hneq2]. - * rewrite HGt. apply AndR. - -- apply AndL. apply weakening. eapply cut2. - ++ apply obviously_smaller_compatible_GT; apply HGt. - ++ assumption. + + apply AndR. + * apply AndL. apply weakening. eapply cut2. + -- apply obviously_smaller_compatible_GT; apply Heq. -- assumption. - * case (decide (obviously_smaller φ' ψ'1 = Eq)); [intro HEq| intro Hneq3]. - -- rewrite HEq. apply and_congruence; [apply Hφ | apply Hψ]. - -- destruct (obviously_smaller φ' ψ'1); - [contradict Hneq3 | contradict Hneq1 |contradict Hneq2]; trivial. -- case (decide (obviously_smaller φ' ψ'1 = Lt)); [intro HLt | intro Hneq1]. - + rewrite HLt. apply AndR. + * assumption. +- case (decide (obviously_smaller φ' ψ'1 = Lt)); [intro HLt | intro Hneq]. + + apply AndR. * assumption. * eapply cut2. -- apply obviously_smaller_compatible_LT; apply HLt. -- apply OrL_rev in Hψ; apply Hψ. - + destruct (obviously_smaller φ' ψ'1); - [idtac | contradict Hneq1; auto | idtac]; (apply and_congruence; [apply Hφ | apply Hψ]). + + apply and_congruence; assumption. +- apply choose_and_equiv_R; assumption. +- apply choose_and_equiv_R; assumption. Qed. Lemma simp_and_comm φ ψ : @@ -698,7 +732,6 @@ assert (H: φ1 ∧ ψ0_1 ∧ φ2 ∧ ψ0_2 ≼ φ1 ⊼ (ψ0_1 ⊼ simp_ands φ2 Qed. - Lemma simp_ands_self_equiv_R φ ψ: simp_ands φ ψ ≼ φ ∧ ψ. Proof. @@ -765,33 +798,56 @@ Lemma simp_equiv_imp_L φ ψ : Proof. intros HφR HψL. simpl. unfold simp_imp. -case decide as [Htop |]. -- rewrite Htop in HφR. - apply weak_ImpL. - + eapply TopL_rev. - apply HφR. - + apply HψL. -- case decide as []. - + apply weakening. - apply top_provable. - + case decide as []. - * apply ImpR. - apply ExFalso. - * apply ImpR. - exch 0. - apply ImpL. - -- apply weakening. apply HφR. - -- exch 0. apply weakening. - apply HψL. -Qed. +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. + --- exch 0. apply weakening. assumption. + ++ assumption. + -- case decide as [HψBot |]. + ++ apply ImpR. exch 0. apply ImpL. + ** apply weakening. assumption. + ** eapply additive_cut. + --- exch 0. apply weakening, HψL. + --- do 2 (exch 0; apply weakening). now apply obviously_smaller_compatible_LT. + ++ apply ImpR. exch 0. apply ImpL. + ** apply weakening. apply HφR. + ** exch 0. apply weakening. apply HψL. +Qed. + + +Definition tmp φ ψ := + if decide (φ = ⊤) then ψ + else if decide (φ = ⊥) then ⊤ + else if decide (φ = ψ) then ⊤ + else φ → ψ. -Lemma simp_equiv_imp_R φ ψ : - (φ ≼ simp φ) -> - (simp ψ ≼ ψ) -> - simp (φ → ψ) ≼ (φ → ψ). + +Fixpoint simp2 φ := +match φ with + | φ ∨ ψ => simp_ors (simp φ) (simp ψ) + | φ ∧ ψ => simp_ands (simp φ) (simp ψ) + | φ → ψ => tmp (simp2 φ) (simp2 ψ) + | □ φ => □ (simp φ) + | _ => φ +end. + + +Lemma tmp_equiv_imp_R φ ψ : + (φ ≼ simp2 φ) -> + (simp2 ψ ≼ ψ) -> + simp2 (φ → ψ) ≼ (φ → ψ). Proof. intros HφL HψR. -simpl. unfold simp_imp. +simpl. unfold tmp. case decide as [Htop |]. - apply ImpR. apply weakening. @@ -812,12 +868,57 @@ case decide as [Htop |]. * apply ImpR. exch 0. apply ImpL. - -- apply weakening. apply HφL. -- exch 0. apply weakening. apply HψR. Qed. + +Lemma simp_equiv_imp_R φ ψ : + (φ ≼ simp φ) -> + (simp ψ ≼ ψ) -> + simp (φ → ψ) ≼ (φ → ψ). +Proof. +intros HφR HψL. +simpl. unfold simp_imp. +case decide as [Heq |]. + - apply weakening. + apply ImpR. + eapply cut2. + + apply HφR. + + eapply cut2. + * apply obviously_smaller_compatible_LT. apply Heq. + * assumption. + - case decide as [HφBot |]. + + apply weakening. + apply ImpR. + eapply cut2. + * apply HφR. + * eapply cut2. + -- apply obviously_smaller_compatible_LT. apply HφBot. + -- apply ExFalso. + + case decide as [HψTop |]. + * apply weakening. + apply ImpR. + eapply cut2. + -- apply top_provable. + -- eapply cut2. + ++ apply obviously_smaller_compatible_GT. apply HψTop. + ++ assumption. + * case decide as [HφTop |]. + -- apply ImpR. apply weakening. assumption. + -- case decide as [HψBot |]. + ++ apply ImpR. + eapply additive_cut. + ** exch 0. apply weak_ImpL. + --- assumption. + --- apply ExFalso. + ** apply generalised_axiom. + ++ apply ImpR. exch 0. apply ImpL. + ** apply weakening. apply HφR. + ** exch 0. apply weakening. apply HψL. +Qed. + Lemma simp_equiv_imp φ ψ: (φ ≼ simp φ) * (simp φ ≼ φ) -> (ψ ≼ simp ψ) * (simp ψ ≼ ψ) -> @@ -1002,7 +1103,7 @@ Lemma vars_incl_simp_ands φ ψ V : Proof. generalize ψ. induction φ; intro ψ0; destruct ψ0; intros Hφ Hψ; -try ( apply vars_incl_simp_and_equiv_and; apply and_vars_incl; assumption). +try (apply vars_incl_simp_and_equiv_and; apply and_vars_incl; assumption). simpl. apply vars_incl_simp_and_equiv_and. apply and_vars_incl. @@ -1015,6 +1116,40 @@ apply and_vars_incl. * now apply (and_vars_incl ψ0_1 _ _). Qed. + + +Lemma imp_vars_incl φ ψ V: + (vars_incl (Implies φ ψ) V -> + vars_incl φ V * vars_incl ψ V)* + ( vars_incl φ V -> + vars_incl ψ V -> + vars_incl (Implies φ ψ) V). +Proof. +split. +- intros H. + split; intros x H1; apply H; simpl; auto. +- unfold vars_incl. simpl. intuition. +Qed. + +Lemma vars_incl_simp_imp φ ψ V : + vars_incl φ V -> vars_incl ψ V -> + vars_incl (simp_imp φ ψ) V. +Proof. +intros Hφ Hψ. +simpl. unfold simp_imp. +case decide as []. + + apply top_vars_incl. + + case decide as []. + * apply top_vars_incl. + * case decide as []. + -- apply top_vars_incl. + -- case decide as []. + ++ assumption. + ++ case decide as []. + ** apply and_vars_incl; [assumption | apply bot_vars_incl ]. + ** apply and_vars_incl; assumption. +Qed. + Lemma vars_incl_simp φ V : vars_incl φ V -> vars_incl (simp φ) V. Proof. @@ -1030,19 +1165,10 @@ induction φ; auto. [ apply IHφ1; apply (or_vars_incl _ φ2)| apply IHφ2; apply (or_vars_incl φ1 _) ]; assumption. -- simpl. unfold simp_imp. - case decide as []. - + apply IHφ2. - eapply and_vars_incl. - apply H. - + case decide as []. - * apply top_vars_incl. - * case decide as []. - -- apply top_vars_incl. - -- apply and_vars_incl; - [ apply IHφ1; apply (and_vars_incl _ φ2)| - apply IHφ2; eapply and_vars_incl]; - apply H. +- simpl. apply vars_incl_simp_imp; + [ apply IHφ1; apply (imp_vars_incl _ φ2)| + apply IHφ2; apply (imp_vars_incl φ1 _) ]; + assumption. Qed. Theorem iSL_uniform_interpolation_simp p V: p ∉ V ->