diff --git a/theories/extraction/UIML_extraction.v b/theories/extraction/UIML_extraction.v index 1c6ec99..7f7f098 100644 --- a/theories/extraction/UIML_extraction.v +++ b/theories/extraction/UIML_extraction.v @@ -5,9 +5,9 @@ Require Import ExtrOcamlBasic ExtrOcamlString. Require Import K.Interpolation.UIK_braga. Require Import KS_export. -Require Import ISL.PropQuantifiers ISL.DecisionProcedure. +Require Import ISL.PropQuantifiers ISL.DecisionProcedure ISL.Simp. + -Require Import ISL.Simp. Fixpoint MPropF_of_form (f : Formulas.form) : MPropF := match f with diff --git a/theories/iSL/Order.v b/theories/iSL/Order.v index 1070bcf..c52accc 100644 --- a/theories/iSL/Order.v +++ b/theories/iSL/Order.v @@ -32,9 +32,17 @@ intro Hw. unfold env_order, ltof. do 2 rewrite env_weight_singleton. apply Nat.pow_lt_mono_r. lia. trivial. Qed. -Definition env_order_refl Δ Δ' := (Δ ≺ Δ') \/ Δ ≡ₚ Δ'. +Definition env_order_refl Δ Δ' := (env_weight Δ) ≤(env_weight Δ'). -Local Notation "Δ ≼ Δ'" := (env_order_refl Δ Δ') (at level 150). +Global Notation "Δ ≼ Δ'" := (env_order_refl Δ Δ') (at level 150). + +Lemma env_order_env_order_refl Δ Δ' : env_order Δ Δ' -> env_order_refl Δ Δ'. +Proof. unfold env_order, env_order_refl, ltof. lia. Qed. + +Global Hint Resolve env_order_env_order_refl: order. + +Lemma env_order_self Δ : Δ ≼ Δ. +Proof. unfold env_order_refl. trivial. Qed. Global Instance Proper_env_weight: Proper ((≡ₚ) ==> (=)) env_weight. Proof. @@ -44,12 +52,7 @@ Qed. Global Instance Proper_env_order_refl_env_weight: Proper ((env_order_refl) ==> le) env_weight. -Proof. -intros Γ Δ. -unfold env_order. intros [Hle | Heq]. -- auto with *. -- now rewrite Heq. -Qed. +Proof. intros Γ Δ Hle. auto with *. Qed. Global Hint Resolve Proper_env_order_refl_env_weight : order. @@ -164,8 +167,7 @@ Lemma env_order_refl_disj_union_compat Δ Δ' Δ'' Δ''': (env_order_refl Δ Δ'') -> (env_order_refl Δ' Δ''') -> env_order_refl (Δ ++ Δ') (Δ'' ++ Δ'''). Proof. unfold env_order_refl, env_order, ltof. repeat rewrite env_weight_disj_union. -intros [Hlt1 | Heq1] [Hlt2 | Heq2]; try rewrite Heq1; try rewrite Heq2; try lia. -right. trivial. +intros Hle1 Hle2; try rewrite Heq1; try rewrite Heq2; try lia. Qed. Global Hint Resolve env_order_refl_disj_union_compat : order. @@ -174,20 +176,13 @@ Hint Unfold env_order_refl : order. Lemma env_order_disj_union_compat_strong_right Δ Δ' Δ'' Δ''': (Δ ≺ Δ'') -> (Δ' ≼ Δ''') -> Δ ++ Δ' ≺ Δ'' ++ Δ'''. Proof. -intros H1 H2. -destruct H2 as [Hlt|Heq]. -- unfold env_order, ltof in *. do 2 rewrite env_weight_disj_union. lia. -- rewrite Heq. now apply env_order_disj_union_compat_left. +intros Hlt Hle. unfold env_order_refl, env_order, ltof in *. do 2 rewrite env_weight_disj_union. lia. Qed. Lemma env_order_disj_union_compat_strong_left Δ Δ' Δ'' Δ''': (Δ ≼ Δ'') -> (Δ' ≺ Δ''') -> Δ ++ Δ' ≺ Δ'' ++ Δ'''. Proof. -intros H1 H2. -destruct H1 as [Hlt|Heq]. -- unfold env_order, ltof in *. do 2 rewrite env_weight_disj_union. lia. -- rewrite Heq. now apply env_order_disj_union_compat_right. -Qed. +intros Hlt Hle. unfold env_order_refl, env_order, ltof in *. do 2 rewrite env_weight_disj_union. lia. Qed. Global Hint Resolve env_order_disj_union_compat_strong_left : order. Global Hint Rewrite elements_open_boxes : order. @@ -197,12 +192,9 @@ Proof. destruct φ; simpl; lia. Qed. Lemma open_boxes_env_order Δ : (map open_box Δ) ≼ Δ. Proof. -induction Δ as [|φ Δ]. -- right. trivial. -- destruct IHΔ as [Hlt | Heq]; simpl. - + left. apply env_order_compat'; trivial. apply weight_open_box. - + rewrite Heq. auto with order. destruct φ; simpl; try auto with order. - left. auto with order. +unfold env_order_refl. +induction Δ as [|φ Δ]; trivial. +simpl. do 2 rewrite env_weight_add. destruct φ; simpl; lia. Qed. Global Hint Resolve open_boxes_env_order : order. @@ -281,7 +273,7 @@ Proof. etransitivity; [|apply env_order_0]. assumption. Qed. Lemma env_order_eq_add Δ Δ' φ: (Δ ≼ Δ') -> (Δ • φ) ≼ (Δ' • φ). -Proof. intros[Heq|Hlt]. left. now apply env_order_add_compat. right. ms. Qed. +Proof. unfold env_order_refl. do 2 rewrite env_weight_add. lia. Qed. Global Hint Resolve env_order_0 : order. @@ -298,6 +290,8 @@ Ltac get_diff_form g := match g with | ?Γ ∖{[?φ]} => φ | _ (?Γ ∖{[?φ]}) => φ | _ (rm ?φ _) => φ +| (rm ?φ _) => φ +| ?Γ ++ _ => get_diff_form Γ | ?Γ • _ => get_diff_form Γ end. @@ -310,9 +304,9 @@ Global Hint Rewrite open_boxes_remove : order. Lemma remove_env_order Δ φ: rm φ Δ ≼ Δ. Proof. -induction Δ as [|ψ Δ]. -- simpl. right. auto. -- simpl. destruct form_eq_dec; auto with order. +unfold env_order_refl. +induction Δ as [|ψ Δ]. trivial. +simpl. destruct form_eq_dec; repeat rewrite env_weight_add; lia. Qed. Global Hint Resolve remove_env_order : order. @@ -331,10 +325,10 @@ Qed. Global Hint Resolve remove_In_env_order_refl : order. Lemma env_order_lt_le_trans Γ Γ' Γ'' : (Γ ≺ Γ') -> (Γ' ≼ Γ'') -> Γ ≺ Γ''. -Proof. intros Hlt [Hlt' | Heq]. transitivity Γ'; auto with order. now rewrite <- Heq. Qed. +Proof. unfold env_order, env_order_refl, ltof. lia. Qed. Lemma env_order_le_lt_trans Γ Γ' Γ'' : (Γ ≼ Γ') -> (Γ' ≺ Γ'') -> Γ ≺ Γ''. -Proof. intros [Hlt' | Heq] Hlt. transitivity Γ'; auto with order. now rewrite Heq. Qed. +Proof. unfold env_order, env_order_refl, ltof. lia. Qed. Lemma remove_In_env_order Δ φ: In φ Δ -> rm φ Δ ≺ Δ. Proof. @@ -367,6 +361,7 @@ unfold pointed_env_order; subst; simpl; repeat rewrite open_boxes_add; try match apply (env_order_equiv_right_compat (equiv_disj_union_compat_r(equiv_disj_union_compat_r(difference_singleton Γ ψ' H)))) || (eapply env_order_le_lt_trans; [| apply env_order_add_compat; eapply env_order_lt_le_trans; [| (apply env_order_eq_add; apply (remove_In_env_order_refl _ ψ'); try apply elem_of_list_In; trivial) ] ] ) +|H : ?a = _ |- context[?a] => rewrite H; try prepare_order end. @@ -389,8 +384,42 @@ Qed. Global Hint Resolve openboxes_env_order : order. +Lemma weight_Arrow_1 φ ψ : 1 < weight (φ → ψ). +Proof. simpl. pose (weight_pos φ). lia. Qed. + +Lemma weight_Box_1 φ: 1 < weight (□ φ). +Proof. simpl. pose (weight_pos φ). lia. Qed. + +Global Hint Resolve weight_Arrow_1 : order. +Global Hint Resolve weight_Box_1 : order. + Ltac order_tac := try unfold pointed_env_ms_order; prepare_order; repeat rewrite elements_env_add; simpl; auto 10 with order; try (apply env_order_disj_union_compat_right; order_tac). + +Global Hint Extern 5 (?a ≺ ?b) => order_tac : proof. +Hint Extern 5 (?a ≺· ?b) => order_tac : proof. + +Lemma pointed_env_order_bot_R pe Δ φ: (pe ≺· (Δ, ⊥)) -> pe ≺· (Δ, φ). +Proof. +intro Hlt. destruct pe as (Γ, ψ). unfold pointed_env_order. simpl. +eapply env_order_lt_le_trans. exact Hlt. simpl. +unfold env_order_refl. repeat rewrite env_weight_add. +assert(Hle: weight ⊥ ≤ weight φ) by (destruct φ; simpl; lia). +apply Nat.pow_le_mono_r with (a := 5) in Hle; lia. +Qed. + +Hint Resolve pointed_env_order_bot_R : order. + +Lemma pointed_env_order_bot_L pe Δ φ: ((Δ, φ) ≺· pe) -> (Δ, ⊥) ≺· pe. +Proof. +intro Hlt. destruct pe as (Γ, ψ). unfold pointed_env_order. simpl. +eapply env_order_le_lt_trans; [|exact Hlt]. simpl. +unfold env_order_refl. repeat rewrite env_weight_add. +assert(Hle: weight ⊥ ≤ weight φ) by (destruct φ; simpl; lia). +apply Nat.pow_le_mono_r with (a := 5) in Hle; lia. +Qed. + +Hint Resolve pointed_env_order_bot_L : order. diff --git a/theories/iSL/PropQuantifiers.v b/theories/iSL/PropQuantifiers.v index 65de444..037e12e 100644 --- a/theories/iSL/PropQuantifiers.v +++ b/theories/iSL/PropQuantifiers.v @@ -1,6 +1,8 @@ -Require Import ISL.Sequents. +Require Import ISL.Sequents ISL.Formulas. Require Import ISL.SequentProps ISL.Order ISL.Optimizations. Require Import Coq.Program.Equality. (* for dependent induction *) +Require Import ISL.Simp_env. + (** * Overview: Propositional Quantifiers @@ -37,14 +39,15 @@ Obligation Tactic := intros; order_tac. Notation "□⁻¹ Γ" := (map open_box Γ) (at level 75). + (** 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 *) Program Definition e_rule {Δ : list form } {ϕ : form} - (EA0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form * form) + (E : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form) + (A : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form) (θ: form) (Hin : θ ∈ Δ) : form := -let E Δ H := fst (EA0 (Δ, ϕ) H) in -let A pe0 H := snd (EA0 pe0 H) in +let E Δ H := E (Δ, ⊥) H in let Δ' := rm θ Δ in match θ with | Bot => ⊥ (* E0 *) @@ -76,10 +79,10 @@ end. Referring to Table 5 in Pitts, the definition a_rule_env handles A1-8 and A10, and the definition a_rule_form handles A9 and A11-13. *) Program Definition a_rule_env {Δ : list form} {ϕ : form} - (EA0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form * form) + (E : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form) + (A : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form) (θ: form) (Hin : θ ∈ Δ) : form := -let E Δ H := fst (EA0 (Δ, ϕ) H) in -let A pe0 H := snd (EA0 pe0 H) in +let E Δ H := E (Δ, ⊥) H in let Δ' := rm θ Δ in match θ with | Var q => @@ -115,13 +118,10 @@ match θ with (* using ⊼ here breaks congruence *) end. - -(* make sure that the proof obligations do not depend on EA0 *) -Obligation Tactic := intros Δ ϕ _ _ _; intros; order_tac. +Obligation Tactic := intros Δ ϕ _ _; intros; order_tac. Program Definition a_rule_form {Δ : list form} {ϕ : form} - (EA0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form * form) : form := -let E pe0 H := fst (EA0 pe0 H) in -let A pe0 H := snd (EA0 pe0 H) in + (E : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form) + (A : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form) := match ϕ with | Var q => if decide (p = q) (* TODO : change this to p∈Vars(ϕ) *) @@ -132,103 +132,111 @@ match ϕ with (* A12 *) | ϕ₁ ∨ ϕ₂ => A (Δ, ϕ₁) _ ⊻ A (Δ, ϕ₂) _ (* A13 *) -| ϕ₁→ ϕ₂ => E (Δ•ϕ₁, ϕ₂) _ ⇢ A (Δ•ϕ₁, ϕ₂) _ +| ϕ₁→ ϕ₂ => E (Δ•ϕ₁, ⊥) _ ⇢ A (Δ•ϕ₁, ϕ₂) _ (* TODO would a general right-implication rule be useful efficient? *) | Bot => ⊥ -| □δ => □((E ((□⁻¹ Δ) • □δ, δ) _) ⇢ A((□⁻¹ Δ) • □δ, δ) _) +| □δ => □((E ((□⁻¹ Δ) • □δ, ⊥) _) ⇢ A((□⁻¹ Δ) • □δ, δ) _) end. -Obligation Tactic := intros; order_tac. -Program Fixpoint EA (pe : list form * form) {wf pointed_env_order pe} := - let Δ := fst pe in - (⋀ (in_map Δ (e_rule EA)), - ⋁ (in_map Δ (a_rule_env EA)) ⊻ a_rule_form EA). -Next Obligation. apply wf_pointed_order. Defined. -Definition E pe := (EA pe).1. -Definition A pe := (EA pe).2. +Obligation Tactic := (try (apply Wf.measure_wf, wf_pointed_order)). +Program Fixpoint EA (b : bool) (pe : pointed_env) {wf pointed_env_order pe} : form := + let Δ := simp_env pe.1 in (* new: weight-decreasing simplification *) + let ϕ := pe.2 in + let E pe H := EA true pe in + let A pe H := EA false pe in + (* E *) + if b then ⋀ (in_map Δ (@e_rule Δ ϕ E A)) + (* A *) + else ⋁ (in_map Δ (@a_rule_env Δ ϕ E A)) ⊻ @a_rule_form Δ ϕ E A. +Next Obligation. intros. subst Δ ϕ. eapply env_order_lt_le_trans; [exact H|]. order_tac. Qed. +Next Obligation. intros. subst Δ ϕ. eapply env_order_lt_le_trans; [exact H|]. order_tac. Qed. -Definition Ef (ψ : form) := E ([ψ], ⊥). +Definition E Δ:= EA true (Δ, ⊥). +Definition A := EA false. + +Definition Ef (ψ : form) := E ([ψ]). Definition Af (ψ : form) := A ([], ψ). (** Congruence lemmas: if we apply any of e_rule, a_rule_env, or a_rule_form to two equal environments, then they give the same results. *) -Lemma e_rule_cong Δ ϕ θ (Hin: θ ∈ Δ) EA1 EA2: - (forall pe Hpe, EA1 pe Hpe = EA2 pe Hpe) -> - @e_rule Δ ϕ EA1 θ Hin = @e_rule Δ ϕ EA2 θ Hin. +Lemma e_rule_cong Δ ϕ θ (Hin: θ ∈ Δ) E1 A1 E2 A2: + (forall pe Hpe, E1 pe Hpe = E2 pe Hpe) -> + (forall pe Hpe, A1 pe Hpe = A2 pe Hpe) -> + @e_rule Δ ϕ E1 A1 θ Hin = @e_rule Δ ϕ E2 A2 θ Hin. Proof. - intro Heq. + intros HeqE HeqA. destruct θ; simpl; try (destruct θ1); repeat (destruct decide); - f_equal; repeat erewrite Heq; trivial. + f_equal; repeat erewrite ?HeqE, ?HeqA; trivial. Qed. -Lemma e_rule_cong_strong Δ ϕ θ (Hin1 Hin2: θ ∈ Δ) EA1 EA2: - (forall pe Hpe1 Hpe2, EA1 pe Hpe1 = EA2 pe Hpe2) -> - @e_rule Δ ϕ EA1 θ Hin1 = @e_rule Δ ϕ EA2 θ Hin2. +Lemma e_rule_cong_strong Δ ϕ θ (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 Δ ϕ E1 A1 θ Hin1 = @e_rule Δ ϕ E2 A2 θ Hin2. Proof. - intro Heq. + intros HeqE HeqA. destruct θ; simpl; try (destruct θ1); repeat (destruct decide); - f_equal; repeat erewrite Heq; trivial. + f_equal; repeat erewrite ?HeqE, ?HeqA; trivial. Qed. -Lemma a_rule_env_cong Δ ϕ θ Hin EA1 EA2: - (forall pe Hpe, EA1 pe Hpe = EA2 pe Hpe) -> - @a_rule_env Δ ϕ EA1 θ Hin = @a_rule_env Δ ϕ EA2 θ Hin. +Lemma a_rule_env_cong Δ ϕ θ Hin E1 A1 E2 A2: + (forall pe Hpe, E1 pe Hpe = E2 pe Hpe) -> + (forall pe Hpe, A1 pe Hpe = A2 pe Hpe) -> + @a_rule_env Δ ϕ E1 A1 θ Hin = @a_rule_env Δ ϕ E2 A2 θ Hin. Proof. - intro Heq. + intros HeqE HeqA. destruct θ; simpl; trivial; repeat (destruct decide); - f_equal; repeat erewrite Heq; trivial; + f_equal; repeat erewrite ?HeqE, ?HeqA; trivial; destruct θ1; try (destruct decide); trivial; simpl; - repeat erewrite Heq; trivial; (destruct decide); trivial. + repeat erewrite ?HeqE, ?HeqA; trivial; (destruct decide); trivial. Qed. -Lemma a_rule_env_cong_strong Δ ϕ θ Hin1 Hin2 EA1 EA2: - (forall pe Hpe1 Hpe2, EA1 pe Hpe1 = EA2 pe Hpe2) -> - @a_rule_env Δ ϕ EA1 θ Hin1 = @a_rule_env Δ ϕ EA2 θ Hin2. +Lemma a_rule_env_cong_strong Δ ϕ θ 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_env Δ ϕ E1 A1 θ Hin1 = @a_rule_env Δ ϕ E2 A2 θ Hin2. Proof. - intro Heq. + intros HeqE HeqA. destruct θ; simpl; trivial; repeat (destruct decide); - f_equal; repeat erewrite Heq; trivial; + f_equal; repeat erewrite ?HeqE, ?HeqA; trivial; destruct θ1; try (destruct decide); trivial; simpl; - repeat erewrite Heq; trivial; (destruct decide); trivial. + repeat erewrite ?HeqE, ?HeqA; trivial; (destruct decide); trivial. Qed. -Lemma a_rule_form_cong Δ ϕ EA1 EA2: - (forall pe Hpe, EA1 pe Hpe = EA2 pe Hpe) -> - @a_rule_form Δ ϕ EA1 = @a_rule_form Δ ϕ EA2. + +Lemma a_rule_form_cong Δ ϕ E1 A1 E2 A2: + (forall pe Hpe, E1 pe Hpe = E2 pe Hpe) -> + (forall pe Hpe, A1 pe Hpe = A2 pe Hpe) -> + @a_rule_form Δ ϕ E1 A1 = @a_rule_form Δ ϕ E2 A2. Proof. - intro Heq. + intros HeqE HeqA. destruct ϕ; simpl; repeat (destruct decide); trivial; - repeat (erewrite Heq; eauto); trivial. + repeat (erewrite ?HeqE, ?HeqA; eauto); trivial. Qed. -Lemma a_rule_form_cong_strong Δ ϕ EA1 EA2: - (forall pe Hpe1 Hpe2, EA1 pe Hpe1 = EA2 pe Hpe2) -> - @a_rule_form Δ ϕ EA1 = @a_rule_form Δ ϕ EA2. + +Lemma a_rule_form_cong_strong Δ ϕ 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_form Δ ϕ E1 A1 = @a_rule_form Δ ϕ E2 A2. Proof. - intro Heq. + intros HeqE HeqA. destruct ϕ; simpl; repeat (destruct decide); trivial; - repeat (erewrite Heq; eauto); trivial. + repeat (erewrite ?HeqE, ?HeqA; eauto); trivial. Qed. -Lemma EA_eq Δ ϕ: - (E (Δ, ϕ) = ⋀ (in_map Δ (@e_rule Δ ϕ (λ pe _, EA pe)))) /\ - (A (Δ, ϕ) = (⋁ (in_map Δ (@a_rule_env Δ ϕ (λ pe _, EA pe)))) ⊻ - @a_rule_form Δ ϕ (λ pe _, EA pe)). +Lemma EA_eq Δ ϕ: let Δ' := simp_env Δ in + (E Δ = ⋀ (in_map Δ' (@e_rule Δ' ϕ (λ pe _, E pe.1) (λ pe _, A pe)))) /\ + (A (Δ, ϕ) = (⋁ (in_map Δ' (@a_rule_env Δ' ϕ (λ pe _, E pe.1) (λ pe _, A pe)))) ⊻ + @a_rule_form Δ' ϕ (λ pe _, E pe.1) (λ pe _, A pe)). Proof. -simpl. unfold E, A, EA. simpl. -rewrite -> Wf.Fix_eq. -- simpl. split; trivial. -- intros Δ' f g Heq. f_equal; f_equal. - + apply in_map_ext. intros. apply e_rule_cong; intros. - now rewrite Heq. - + f_equal. apply in_map_ext. intros. apply a_rule_env_cong; intros. - now rewrite Heq. - + apply a_rule_form_cong; intros. now rewrite Heq. +simpl. unfold E, A, EA, EA_func. +repeat rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl. split; trivial. Qed. -Definition E_eq Δ ϕ := proj1 (EA_eq Δ ϕ). +Definition E_eq Δ := proj1 (EA_eq Δ ⊥). Definition A_eq Δ ϕ := proj2 (EA_eq Δ ϕ). End PropQuantDefinition. @@ -276,11 +284,13 @@ try multimatch goal with (** *** (a) *) Lemma e_rule_vars Δ (θ : form) (Hin : θ ∈ Δ) (ϕ : form) - (EA0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form * form) x - (HEA0 : ∀ pe Hpe, - (occurs_in x (fst (EA0 pe Hpe)) -> x ≠ p ∧ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ) /\ - (occurs_in x (snd (EA0 pe Hpe)) -> x ≠ p ∧ (occurs_in x pe.2 \/ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ))) : -occurs_in x (e_rule EA0 θ Hin) -> x ≠ p ∧ ∃ θ, θ ∈ Δ /\ occurs_in x θ. + (E0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form) + (A0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form) + x + (HE0 : ∀ pe Hpe, + (occurs_in x (E0 pe Hpe) -> x ≠ p ∧ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ) /\ + (occurs_in x (A0 pe Hpe) -> x ≠ p ∧ (occurs_in x pe.2 \/ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ))) : +occurs_in x (e_rule E0 A0 θ Hin) -> x ≠ p ∧ ∃ θ, θ ∈ Δ /\ occurs_in x θ. Proof. destruct θ; unfold e_rule; simpl; try tauto; try solve [repeat case decide; repeat vars_tac]. destruct θ1; repeat case decide; repeat vars_tac. @@ -290,11 +300,13 @@ Qed. (** *** (b) *) Lemma a_rule_env_vars Δ θ Hin ϕ - (EA0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form * form) x + (E0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form) + (A0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form) + x (HEA0 : ∀ pe Hpe, - (occurs_in x (fst (EA0 pe Hpe)) -> x ≠ p ∧ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ) /\ - (occurs_in x (snd (EA0 pe Hpe)) -> x ≠ p ∧ (occurs_in x pe.2 \/ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ))): -occurs_in x (a_rule_env EA0 θ Hin) -> x ≠ p ∧ (occurs_in x ϕ \/ ∃ θ, θ ∈ Δ /\ occurs_in x θ). + (occurs_in x (E0 pe Hpe) -> x ≠ p ∧ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ) /\ + (occurs_in x (A0 pe Hpe) -> x ≠ p ∧ (occurs_in x pe.2 \/ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ))): +occurs_in x (a_rule_env E0 A0 θ Hin) -> x ≠ p ∧ (occurs_in x ϕ \/ ∃ θ, θ ∈ Δ /\ occurs_in x θ). Proof. destruct θ; unfold a_rule_env; simpl; try tauto; try solve [repeat case decide; repeat vars_tac]. destruct θ1; repeat case decide; repeat vars_tac. @@ -302,17 +314,19 @@ Qed. Lemma a_rule_form_vars Δ ϕ - (EA0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form * form) x + (E0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form) + (A0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form) + x (HEA0 : ∀ pe Hpe, - (occurs_in x (fst (EA0 pe Hpe)) -> x ≠ p ∧ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ) /\ - (occurs_in x (snd (EA0 pe Hpe)) -> x ≠ p ∧ (occurs_in x pe.2 \/ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ))): - occurs_in x (a_rule_form EA0) -> x ≠ p ∧ (occurs_in x ϕ \/ ∃ θ, θ ∈ Δ /\ occurs_in x θ). + (occurs_in x (E0 pe Hpe) -> x ≠ p ∧ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ) /\ + (occurs_in x (A0 pe Hpe) -> x ≠ p ∧ (occurs_in x pe.2 \/ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ))): + occurs_in x (a_rule_form E0 A0) -> x ≠ p ∧ (occurs_in x ϕ \/ ∃ θ, θ ∈ Δ /\ occurs_in x θ). Proof. destruct ϕ; unfold a_rule_form; simpl; try tauto; try solve [repeat case decide; repeat vars_tac]. Qed. Proposition EA_vars Δ ϕ x: - (occurs_in x (E (Δ, ϕ)) -> x <> p /\ ∃ θ, θ ∈ Δ /\ occurs_in x θ) /\ + (occurs_in x (E Δ) -> x <> p /\ ∃ θ, θ ∈ Δ /\ occurs_in x θ) /\ (occurs_in x (A (Δ, ϕ)) -> x <> p /\ (occurs_in x ϕ \/ (∃ θ, θ ∈ Δ /\ occurs_in x θ))). Proof. remember (Δ, ϕ) as pe. @@ -326,25 +340,28 @@ split. - intros 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φ. - + trivial. - + intros; now apply Hind. + + intuition. now apply equiv_env_vars. + + intros; apply Hind. auto with order. (* A *) - intro Hocc. apply occurs_in_make_disj in Hocc as [Hocc|Hocc]. (* disjunction *) + apply variables_disjunction in Hocc as (φ&Hin&Hφ). apply in_in_map in Hin as (ψ&Hin&Heq). subst φ. - apply a_rule_env_vars in Hφ; trivial. + apply a_rule_env_vars in Hφ. + * intuition. right. now apply equiv_env_vars. + * intros pe Hpe. apply simp_env_pointed_env_order_L in Hpe. apply Hind in Hpe. tauto. (* pointer rule *) + apply a_rule_form_vars in Hocc. * destruct Hocc as [Hneq [Hocc | Hocc]]; vars_tac. - * vars_tac; apply Hind in H; trivial; tauto. + right. apply equiv_env_vars. vars_tac. + * vars_tac; apply Hind in H; trivial; intuition; auto with order. Qed. End VariablesCorrect. Ltac foldEA := repeat match goal with -| |- context C [(EA ?pe).1] => fold (E pe) -| |- context C [(EA ?pe).2] => fold (A pe) +| |- context C [EA true ?pe] => fold (E pe) +| |- context C [EA false ?pe] => fold (A pe) end. (** ** (ii) Entailment *) @@ -354,7 +371,6 @@ Section EntailmentCorrect. entailed by the original formula and entail the original formula, respectively. *) -Hint Extern 5 (?a ≺ ?b) => order_tac : proof. Opaque make_disj. Opaque make_conj. @@ -364,9 +380,11 @@ Local Ltac l_tac := repeat rewrite list_to_set_disj_open_boxes; || rewrite (proper_Provable _ _ (equiv_disj_union_compat_r (equiv_disj_union_compat_r (list_to_set_disj_env_add _ _))) _ _ eq_refl) || rewrite (proper_Provable _ _ (equiv_disj_union_compat_r(equiv_disj_union_compat_r (equiv_disj_union_compat_r (list_to_set_disj_env_add _ _)))) _ _ eq_refl). -Lemma a_rule_env_spec (Δ : list form) θ ϕ Hin (EA0 : ∀ pe, (pe ≺· (Δ, ϕ)) → form * form) - (HEA : forall Δ ϕ Hpe, (list_to_set_disj Δ ⊢ fst (EA0 (Δ, ϕ) Hpe)) * (list_to_set_disj Δ• snd(EA0 (Δ, ϕ) Hpe) ⊢ ϕ)) : - (list_to_set_disj Δ • a_rule_env EA0 θ Hin ⊢ ϕ). +Lemma a_rule_env_spec (Δ : list form) θ ϕ Hin + (E0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form) + (A0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form) + (HEA : forall Δ ϕ Hpe, (list_to_set_disj Δ ⊢ E0 (Δ, ϕ) Hpe) * (list_to_set_disj Δ• A0 (Δ, ϕ) Hpe ⊢ ϕ)) : + (list_to_set_disj Δ • a_rule_env E0 A0 θ Hin ⊢ ϕ). Proof with (auto with proof). assert (HE := λ Δ0 ϕ0 Hpe, fst (HEA Δ0 ϕ0 Hpe)). assert (HA := λ Δ0 ϕ0 Hpe, snd (HEA Δ0 ϕ0 Hpe)). @@ -410,7 +428,7 @@ rewrite (proper_Provable _ _ (equiv_disj_union_compat_r (equiv_disj_union_compat - auto with proof. Qed. -Proposition entail_correct Δ ϕ : (list_to_set_disj Δ ⊢ E (Δ, ϕ)) * (list_to_set_disj Δ•A (Δ, ϕ) ⊢ ϕ). +Proposition entail_correct Δ ϕ : (list_to_set_disj Δ ⊢ E Δ) * (list_to_set_disj Δ•A (Δ, ϕ) ⊢ ϕ). Proof with (auto with proof). remember (Δ, ϕ) as pe. replace Δ with pe.1 by now subst. @@ -419,15 +437,20 @@ refine (@well_founded_induction _ _ wf_pointed_order _ _). unfold pointed_env_order. intros (Δ, ϕ) Hind. simpl. rewrite E_eq, A_eq. +remember (simp_env Δ) as Δ'. +assert (Hind' := λ y H, Hind y (simp_env_pointed_env_order_L y Δ ϕ H)). +clear Hind. (* uncurry the induction hypothesis for convenience *) -assert (HE := fun d f x=> fst (Hind (d, f) x)). -assert (HA := fun d f x=> snd (Hind (d, f) x)). +assert (HE := fun d x=> fst (Hind' (d, ⊥) x)). +assert (HA := fun d f x=> snd (Hind' (d, f) x)). unfold E, A in *; simpl in HE, HA. -simpl in *. clear Hind. +simpl in *. clear Hind'. split. { (* E *) apply conjunction_R1. intros φ Hin. apply in_in_map in Hin. -destruct Hin as (ψ&Hin&Heq). subst. +destruct Hin as (ψ&Hin&Heq). subst φ. +apply simp_env_equiv_env. +rewrite <- HeqΔ' in *. clear HeqΔ' Δ. rename Δ' into Δ. assert(Hi : ψ ∈ list_to_set_disj Δ) by now apply elem_of_list_to_set_disj. destruct ψ; unfold e_rule; exhibit Hi 0; rewrite (proper_Provable _ _ (equiv_disj_union_compat_r (list_to_set_disj_rm _ _)) _ _ eq_refl). - case decide; intro; subst; simpl; auto using HE with proof. @@ -459,14 +482,17 @@ destruct ψ; unfold e_rule; exhibit Hi 0; rewrite (proper_Provable _ _ (equiv_di - apply BoxR. apply weakening. box_tac. l_tac. apply HE. order_tac. } (* A *) +apply ImpR_rev, simp_env_equiv_env, ImpR. +rewrite <- HeqΔ' in *. clear HeqΔ' Δ. rename Δ' into Δ. apply make_disj_sound_L, OrL. - apply disjunction_L. intros φ Hin. apply in_in_map in Hin as (φ' & Heq & Hφ'). subst φ. apply a_rule_env_spec; intros; split ; apply HE || apply HA; order_tac. + eapply pointed_env_order_bot_L in Hpe. exact Hpe. - destruct ϕ; simpl; auto using HE with proof. + case decide; intro; subst; [constructor 2|constructor 1]. + apply make_conj_sound_L, AndR; apply AndL; auto using HE with proof. - + apply ImpR. exch 0. l_tac. apply make_impl_sound_L, ImpL; auto using HE, HA with proof. + + apply ImpR. exch 0. l_tac. foldEA. apply make_impl_sound_L, ImpL; auto using HE, HA with proof. + foldEA. apply BoxR. box_tac. exch 0. l_tac. apply make_impl_sound_L, ImpL. * apply weakening, HE. order_tac. * apply HA. order_tac. @@ -477,46 +503,35 @@ End EntailmentCorrect. (** ** Uniformity *) Section PropQuantCorrect. -Hint Extern 5 (?a ≺· ?b) => order_tac : proof. - (** 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. *) -(** E's second argument is mostly irrelevant and is only there for uniform treatment with A *) -Lemma E_irr ϕ' Δ ϕ : E (Δ, ϕ) = E (Δ, ϕ'). -Proof. -remember ((Δ, ϕ) : pointed_env) as pe. -replace Δ with pe.1 by now subst. -replace ϕ with pe.2 by now subst. clear Heqpe Δ ϕ. - induction pe as [[Γ φ] Hind0] using (well_founded_induction_type wf_pointed_order). -assert(Hind : ∀ Γ0 φ0, ((Γ0, φ0) ≺· (Γ, φ)) → E (Γ0, φ0) = E (Γ0, ϕ')) - by exact (fun Γ0 φ0 => (Hind0 (Γ0, φ0))). -unfold E in Hind. simpl in Hind. -do 2 rewrite E_eq. f_equal. apply in_map_ext. -intros φ' Hin. unfold e_rule. -destruct φ'; repeat rewrite (Hind _ φ) by (trivial; order_tac); trivial. -destruct φ'1; repeat rewrite (Hind _ φ) by (trivial; order_tac); trivial. -Qed. +(* This holds by idempotence of simp_env *) +Lemma A_simp_env Δ φ: A(simp_env Δ, φ) = A (Δ, φ). +Proof. do 2 rewrite A_eq. now rewrite simp_env_idempotent. Qed. -Lemma E_left {Γ} {θ} {Δ} {φ φ'} (Hin : φ ∈ Δ) : -(Γ•e_rule (λ pe (_ : pe ≺· (Δ, φ')), EA pe) φ Hin) ⊢ θ -> -Γ•E (Δ, φ') ⊢ θ. -Proof. -intro Hp. rewrite E_eq. -destruct (@in_map_in _ _ _ (e_rule (λ pe (_ : pe ≺· (Δ, φ')), EA pe)) _ Hin) as [Hin' Hrule]. +Lemma E_simp_env Δ: E(simp_env Δ) = E (Δ). +Proof. do 2 rewrite E_eq. now rewrite simp_env_idempotent. Qed. + +Lemma E_left {Γ} {θ} {Δ' Δ : list form} {φ : form}: (Δ' = simp_env Δ) -> ∀ (Hin : φ ∈ Δ'), +(Γ • e_rule (λ pe (_ : pe ≺· (Δ', ⊥)), E pe.1) (λ pe (_ : pe ≺· (Δ', ⊥)), A pe) φ Hin) ⊢ θ -> +Γ • E Δ' ⊢ θ. +Proof. +intros Heq Hin Hp. subst Δ'. rewrite E_simp_env, E_eq. +destruct (@in_map_in _ _ _ (e_rule (λ pe (_ : pe ≺· (simp_env Δ, ⊥)), E pe.1) (λ pe (_ : pe ≺· (simp_env Δ, ⊥)), A pe) ) _ Hin) as [Hin' Hrule]. eapply conjunction_L. - apply Hrule. - exact Hp. Qed. -Lemma A_right {Γ} {Δ} {φ φ'} (Hin : φ ∈ Δ) : -Γ ⊢ a_rule_env (λ pe (_ : pe ≺· (Δ, φ')), EA pe) φ Hin -> -Γ ⊢ A (Δ, φ'). -Proof. intro Hp. rewrite A_eq. -destruct (@in_map_in _ _ _ (a_rule_env (λ pe (_ : pe ≺· (Δ, φ')), EA pe)) _ Hin) as [Hin' Hrule]. +Lemma A_right {Γ} {Δ Δ'} {φ φ'} : (Δ' = simp_env Δ) -> ∀ (Hin : φ ∈ Δ'), +Γ ⊢ a_rule_env (λ pe (_ : pe ≺· (Δ', φ')), E pe.1) (λ pe (_ : pe ≺· (Δ', φ')), A pe) φ Hin -> +Γ ⊢ A (Δ', φ'). +Proof. intros Heq Hin Hp. subst Δ'. rewrite A_simp_env, A_eq. +destruct (@in_map_in _ _ _ (a_rule_env (λ pe (_ : pe ≺· (simp_env Δ, φ')), E pe.1) (λ pe (_ : pe ≺· (simp_env Δ, φ')), A pe)) _ Hin) as [Hin' Hrule]. eapply make_disj_sound_R, OrR1, disjunction_R. - exact Hrule. - exact Hp. @@ -525,18 +540,19 @@ Qed. Proposition pq_correct Γ Δ ϕ: (∀ φ0, φ0 ∈ Γ -> ¬ occurs_in p φ0) -> (Γ ⊎ list_to_set_disj Δ ⊢ ϕ) -> - (¬ occurs_in p ϕ -> Γ•E (Δ, ϕ) ⊢ ϕ) * (Γ•E (Δ, ϕ) ⊢ A (Δ, ϕ)). + (¬ occurs_in p ϕ -> Γ•E Δ ⊢ ϕ) * (Γ•E Δ ⊢ A (Δ, ϕ)). Proof. (* This proof goes by induction on the ordering w.r.t (Γ ⊎Δ, ϕ) instead of on the structure of Γ ⊎Δ ⊢ ϕ, to allow better rules *) (* we want to use an E rule *) Local Ltac Etac := foldEA; intros; match goal with -| Hin : ?a ∈ list_to_set_disj ?Δ |- _•E (?Δ, _) ⊢ _=> - apply (E_left (proj1 (elem_of_list_to_set_disj _ _) Hin)); unfold e_rule end. +| HeqΔ': ?Δ' = simp_env ?Δ, Hin : ?a ∈ list_to_set_disj ?Δ' |- _•E ?Δ' ⊢ _=> + apply (E_left HeqΔ'(proj1 (elem_of_list_to_set_disj _ _) Hin)); unfold e_rule end. (* we want to use an A rule defined in a_rule_env *) -Local Ltac Atac := foldEA; match goal with | Hin : ?a ∈ list_to_set_disj ?Δ |- _ ⊢ A (?Δ, _) => - apply (A_right (proj1 (elem_of_list_to_set_disj _ _) Hin)); unfold a_rule_env end. +Local Ltac Atac := foldEA; match goal with +| HeqΔ': ?Δ' = simp_env ?Δ, Hin : ?a ∈ list_to_set_disj ?Δ' |- _ ⊢ A (?Δ', _) => + apply (A_right HeqΔ' (proj1 (elem_of_list_to_set_disj _ _) Hin)); unfold a_rule_env end. (* we want to use an A rule defined in a_rule_form *) Local Ltac Atac' := foldEA; rewrite A_eq; apply make_disj_sound_R, OrR2; simpl. @@ -577,19 +593,25 @@ revert pe Γ Δ ϕ Heqpe. refine (@well_founded_induction _ _ wf_pointed_order _ _). intros (ΓΔ, ϕ0) Hind Γ Δ ϕ Heq Hnin Hp. inversion Heq; subst; clear Heq. -assert(Hind' := λ Γ0 Δ0 ψ Ho, Hind (elements Γ0 ++ Δ0, ψ) Ho _ _ _ eq_refl). +assert(Ho' : pointed_env_order_refl (elements Γ ++ simp_env Δ, ϕ) (elements Γ ++ Δ, ϕ)) + by (unfold pointed_env_order_refl; simpl; order_tac). +assert(Hind' := λ Γ0 Δ0 ψ Ho, Hind (elements Γ0 ++ Δ0, ψ) (env_order_lt_le_trans _ _ _ Ho Ho') _ _ _ eq_refl). simpl in Hind'. clear Ho'. clear Hind. rename Hind' into Hind. +rewrite <- E_simp_env, <- A_simp_env. +assert(Hp' := equiv_env_L1 Γ _ _ _ (symmetric_equiv_env _ _ (simp_env_equiv_env Δ)) Hp). +remember (simp_env Δ) as Δ'. clear Hp. +rename Hp' into Hp. dependent destruction Hp; (* 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 Δ |- _ => rename H into Heq; +| H : (?Γ0•?a•?b) = Γ ⊎ list_to_set_disj Δ' |- _ => rename H into Heq; pose(Heq' := env_equiv_eq _ _ Heq); apply env_add_inv' in Heq' -| H : ((?Γ0 • ?a) = Γ ⊎ list_to_set_disj Δ) |- _ => rename H into Heq; - assert(Hin : a ∈ (Γ ⊎ list_to_set_disj Δ)) by (rewrite <- Heq; ms); +| H : ((?Γ0 • ?a) = Γ ⊎ list_to_set_disj Δ') |- _ => rename H into Heq; + assert(Hin : a ∈ (Γ ⊎ list_to_set_disj Δ')) by (rewrite <- Heq; ms); pose(Heq' := env_equiv_eq _ _ Heq); apply env_add_inv' in Heq'; try (case (decide (a ∈ Γ)); intro Hin0; [split; intros; exhibit Hin0 1| - case (decide (a ∈ (list_to_set_disj Δ : env))); intro Hin0'; + case (decide (a ∈ (list_to_set_disj Δ' : env))); intro Hin0'; [|apply gmultiset_elem_of_disj_union in Hin; exfalso; tauto]]) end; simpl. @@ -607,26 +629,26 @@ end; simpl. - split; Etac; auto with proof. (* AndR *) - split. - + intro Hocc. apply AndR; erewrite E_irr; apply Hind; auto with proof. - + Atac'. foldEA. apply make_conj_sound_R, AndR; erewrite E_irr; + + intro Hocc. apply AndR; apply Hind; auto with proof. + + Atac'. foldEA. do 2 rewrite A_simp_env. apply make_conj_sound_R, AndR; (eapply Hind; [order_tac | occ | trivial]). (* AndL *) - exch 0. apply AndL. exch 1; exch 0. peapply Hind; auto with proof. occ. peapply' Hp. - exch 0. apply AndL. exch 1; exch 0. peapply Hind; auto with proof. occ. peapply' Hp. - split. - + Etac. foldEA. apply Hind; auto with proof. peapply' Hp. + + Etac. foldEA. apply Hind; auto with proof. simpl. peapply' Hp. + Atac. Etac. apply Hind; auto; auto with proof. peapply' Hp. (* OrR1 & OrR2 *) - split. - + intro Hocc. apply OrR1. erewrite E_irr; apply Hind; auto with proof. + + intro Hocc. apply OrR1. apply Hind; auto with proof. + rewrite A_eq. apply make_disj_sound_R, OrR2. - apply make_disj_sound_R, OrR1; erewrite E_irr. + apply make_disj_sound_R, OrR1. rewrite A_simp_env. apply Hind; auto with proof. - simpl. split. - + intro Hocc. apply OrR2. erewrite E_irr; apply Hind; auto with proof. + + intro Hocc. apply OrR2. apply Hind; auto with proof. + rewrite A_eq. apply make_disj_sound_R, OrR2. - apply make_disj_sound_R, OrR2; erewrite E_irr. - apply Hind; auto with proof. + apply make_disj_sound_R, OrR2. rewrite A_simp_env. + apply Hind; auto with proof. (* OrL *) - exch 0. apply OrL; exch 0. + apply Hind; auto with proof. occ. peapply' Hp1. @@ -635,7 +657,7 @@ end; simpl. + apply Hind; auto with proof. occ. peapply' Hp1. + apply Hind; auto with proof. occ. peapply' Hp2. - split. - + Etac. apply make_disj_sound_L, OrL; apply Hind; auto with proof. + + Etac. apply make_disj_sound_L, OrL; apply Hind; auto with proof; simpl. * peapply' Hp1. * peapply' Hp2. + Atac. apply weakening. apply make_conj_sound_R,AndR, make_impl_sound_R. @@ -644,10 +666,10 @@ end; simpl. (* ImpR *) - split. + intro Hocc. apply ImpR. exch 0. - erewrite E_irr. apply Hind; auto with proof. occ. peapply Hp. + apply Hind; auto with proof. occ. peapply Hp. + Atac'. apply weakening, make_impl_sound_R, ImpR, Hind; auto with proof. order_tac. * rewrite <- Permutation_middle. order_tac. - * peapply Hp. + * simpl. subst Δ'. rewrite simp_env_idempotent. peapply Hp. (* ImpLVar *) - pose(Heq'' := Heq'); apply env_add_inv' in Heq''. case (decide ((Var p0 → φ) ∈ Γ)). @@ -660,11 +682,11 @@ end; simpl. split; [intro Hocc|]; exhibit Hin0 1; exhibit Hin2 2; exch 0; exch 1; apply ImpLVar; exch 1; exch 0; (apply Hind; auto with proof; [occ | peapply' Hp]). * assert(Hin0' : Var p0 ∈ (Γ0•Var p0•(p0 → φ))) by ms. rewrite Heq in Hin0'. - case (decide (Var p0 ∈ (list_to_set_disj Δ: env))); intro Hp0; + case (decide (Var p0 ∈ (list_to_set_disj Δ': env))); intro Hp0; [|apply gmultiset_elem_of_disj_union in Hin0'; exfalso; tauto]. (* subcase 3: p0 ∈ Δ ; (p0 → φ) ∈ Γ *) clear Heq''. - split; try case decide; intros; subst. + split; try case decide; intros. -- apply contraction. Etac. rewrite decide_False by tauto. exhibit Hin0 2. exch 1. exch 0. apply ImpLVar. exch 0. apply weakening. exch 0. apply Hind; auto with proof. occ. peapply' Hp. @@ -674,40 +696,40 @@ end; simpl. + intro. assert(Hin : (Var p0 → φ) ∈ (Γ0•Var p0•(p0 → φ))) by ms. rewrite Heq in Hin. - case (decide ((Var p0 → φ) ∈ (list_to_set_disj Δ : env))); intro Hin0; + case (decide ((Var p0 → φ) ∈ (list_to_set_disj Δ' : env))); intro Hin0; [|apply gmultiset_elem_of_disj_union in Hin; exfalso; tauto]. case (decide (Var p0 ∈ Γ)); intro Hin1. * (* subcase 2: p0 ∈ Γ ; (p0 → φ) ∈ Δ *) do 2 exhibit Hin1 1. split; [intro Hocc|]. -- Etac. case decide; intro Hp0;[|case decide; intro; subst; [auto with *|]]. - ++ foldEA. apply Hind; auto with proof; [order_tac; order_tac|occ | peapply' Hp]. + ++ foldEA. simpl. apply Hind; auto with proof. occ. peapply' Hp. ++ apply make_impl_sound_L, ImpLVar. exch 0. backward. rewrite env_add_remove. - apply Hind; auto with proof. peapply' Hp. + apply Hind; auto with proof. simpl. peapply' Hp. -- Etac. Atac. case decide; intro Hp0;[|case decide; intro; subst; [auto with *|]]. - ++ foldEA. apply Hind; auto with proof; [order_tac; order_tac|occ | peapply' Hp]. + ++ foldEA. apply Hind; auto with proof; [occ | peapply' Hp]. ++ apply make_impl_sound_L, ImpLVar. apply make_conj_sound_R, AndR; auto 2 with proof. exch 0. backward. rewrite env_add_remove. apply Hind; auto with proof. peapply' Hp. - * assert(Hin': Var p0 ∈ Γ ⊎ list_to_set_disj Δ) by (rewrite <- Heq; ms). + * assert(Hin': Var p0 ∈ Γ ⊎ list_to_set_disj Δ') by (rewrite <- Heq; ms). apply gmultiset_elem_of_disj_union in Hin'. - case (decide (Var p0 ∈ (list_to_set_disj Δ: env))); intro Hin1'; [|exfalso; tauto]. + case (decide (Var p0 ∈ (list_to_set_disj Δ': env))); intro Hin1'; [|exfalso; tauto]. (* subcase 4: p0,(p0 → φ) ∈ Δ *) case (decide (p = p0)); intro. -- (* subsubcase p = p0 *) apply elem_of_list_to_set_disj in Hin1'. - subst. split; Etac; repeat rewrite decide_True by trivial. - ++ clear Heq. apply Hind; auto with proof. peapply' Hp. + split; Etac; repeat rewrite decide_True by trivial. + ++ clear Heq. apply Hind; auto with proof. simpl. peapply' Hp. ++ Atac. repeat rewrite decide_True by trivial. clear Heq. apply Hind; auto with proof. peapply' Hp. -- (* subsubcase p ≠ p0 *) split; [intro Hocc|]. ++ apply contraction. Etac. rewrite decide_False by trivial. exch 0. - assert((p0 → φ) ∈ list_to_set_disj Δ) by ms. Etac. + assert((p0 → φ) ∈ list_to_set_disj Δ') by ms. Etac. rewrite decide_True by now apply elem_of_list_to_set_disj. - exch 0. apply weakening. apply Hind; auto with proof. peapply' Hp. - ++ apply contraction. Etac. exch 0. assert((p0 → φ) ∈ list_to_set_disj Δ) by ms. + exch 0. apply weakening. apply Hind; auto with proof. simpl. peapply' Hp. + ++ apply contraction. Etac. exch 0. assert((p0 → φ) ∈ list_to_set_disj Δ') by ms. Etac; Atac. rewrite decide_False by trivial. do 2 rewrite decide_True by now apply elem_of_list_to_set_disj. exch 0. apply weakening. @@ -716,40 +738,39 @@ end; simpl. - exch 0. apply ImpLAnd. exch 0. apply Hind; auto with proof; [occ|peapply' Hp]. - exch 0. apply ImpLAnd. exch 0. apply Hind; auto with proof; [occ|peapply' Hp]. - split; Etac. - + apply Hind; auto with proof. peapply' Hp. + + apply Hind; auto with proof. simpl. peapply' Hp. + Atac. simpl. apply Hind; auto with proof. peapply' Hp. (* ImpLOr *) - exch 0; apply ImpLOr. exch 1; exch 0. apply Hind; auto with proof. occ. peapply' Hp. - exch 0; apply ImpLOr. exch 1; exch 0. apply Hind; [order_tac | occ|peapply' Hp]. - split; Etac. - + apply Hind; auto with proof. peapply' Hp. + + apply Hind; auto with proof. simpl. peapply' Hp. + Atac. apply Hind; auto with proof. peapply' Hp. (* ImpLImp *) - (* subcase 1: ((φ1 → φ2) → φ3) ∈ Γ *) assert(ψ ≠ Var p) by (intro; subst; simpl in *; tauto). exch 0; apply ImpLImp; exch 0. - + erewrite E_irr. apply Hind; auto with proof. occ. peapply' Hp1. + + apply Hind; auto with proof. occ. peapply' Hp1. simpl. apply Hnin in Hin0. simpl in *. tauto. - + erewrite E_irr. apply Hind; auto with proof. occ. peapply' Hp2. + + apply Hind; auto with proof. occ. peapply' Hp2. - exch 0; apply ImpLImp; exch 0. - + erewrite E_irr. apply Hind; auto with proof. occ. peapply' Hp1. + + apply Hind; auto with proof. occ. peapply' Hp1. simpl. apply Hnin in Hin0. simpl in Hin0. tauto. + apply Hind; auto with proof. occ. peapply' Hp2. - (* subcase 2: ((φ1 → φ2) → φ3) ∈ Δ *) split. + Etac. apply make_impl_sound_L2'. apply ImpLImp. * apply weakening. apply ImpR. foldEA. - rewrite (E_irr φ2). apply Hind; auto with proof. -- order_tac. repeat rewrite Permutation_middle. order_tac. -- repeat setoid_rewrite gmultiset_disj_union_assoc. setoid_rewrite gmultiset_disj_union_comm. repeat setoid_rewrite gmultiset_disj_union_assoc. exch 0. apply ImpR_rev. peapply' Hp1. - * apply Hind; auto with proof. peapply' Hp2. + * apply Hind; auto with proof. simpl. peapply' Hp2. + Atac. apply make_conj_sound_R, AndR. * apply weakening. apply make_impl_sound_R, ImpR. foldEA. - rewrite (E_irr φ2). apply Hind; auto with proof. + apply Hind; auto with proof. -- order_tac. repeat rewrite Permutation_middle. order_tac. -- repeat setoid_rewrite gmultiset_disj_union_assoc. setoid_rewrite gmultiset_disj_union_comm. @@ -757,7 +778,7 @@ end; simpl. peapply' Hp1. * Etac. simpl. apply make_impl_sound_L2', ImpLImp. -- apply weakening. apply ImpR. foldEA. - rewrite (E_irr φ2). apply Hind; auto with proof. + apply Hind; auto with proof. ++ order_tac. repeat rewrite Permutation_middle. order_tac. ++ repeat setoid_rewrite gmultiset_disj_union_assoc. setoid_rewrite gmultiset_disj_union_comm. @@ -765,19 +786,19 @@ end; simpl. peapply' Hp1. -- apply Hind; auto with proof. peapply' Hp2. - (* ImpBox, external *) - destruct (open_boxes_case (list_to_set_disj Δ)) as [[θ Hθ] | Hequiv]. + destruct (open_boxes_case (list_to_set_disj Δ')) as [[θ Hθ] | Hequiv]. + apply contraction. Etac. exch 1; exch 0; apply ImpBox. * box_tac. box_tac. exch 2; exch 1; exch 0. apply weakening. foldEA. - erewrite E_irr with (ϕ' := φ1). exch 1; exch 0. apply Hind. -- order_tac. (* cannot handle it. manual proof *) rewrite elements_open_boxes. - do 2 apply env_order_cancel_right. apply env_order_4; simpl; try lia. left. + do 2 apply env_order_cancel_right. apply env_order_4; simpl; try lia. + apply env_order_env_order_refl. apply env_order_disj_union_compat_strong_left; order_tac. -- occ. intro HF. destruct (occurs_in_open_boxes _ _ _ HF Hin1) as (θ0 & Hθ0 & Hinθ). apply (Hnin θ0); ms. -- assert(Hθ' := In_open_boxes _ _ Hθ). - assert(Heq'' : Γ0 ≡ (Γ ∖ {[□ φ1 → φ2]} ⊎ list_to_set_disj ((□θ) :: rm (□ θ) Δ))). { + assert(Heq'' : Γ0 ≡ (Γ ∖ {[□ φ1 → φ2]} ⊎ list_to_set_disj ((□θ) :: rm (□ θ) Δ'))). { rewrite Heq'. simpl. rewrite union_difference_L by trivial. rewrite (difference_singleton _ _ Hθ). rewrite list_to_set_disj_rm. ms. @@ -789,14 +810,12 @@ end; simpl. rewrite open_boxes_add. simpl. ms. -- intro HF. apply (Hnin _ Hin0). simpl. tauto. * exch 0. apply weakening. exch 0. apply Hind; [order_tac | occ|peapply' Hp2| trivial]. - + assert(Heq'' : (⊗ Γ0) ≡ ((⊗Γ ∖ {[□ φ1 → φ2]}) ⊎ ⊗ (list_to_set_disj Δ))). { + + assert(Heq'' : (⊗ Γ0) ≡ ((⊗Γ ∖ {[□ φ1 → φ2]}) ⊎ ⊗ (list_to_set_disj Δ'))). { rewrite Heq'. rewrite union_difference_L by trivial. rewrite <- Hequiv, open_boxes_disj_union. rewrite open_boxes_remove by trivial. ms. } exch 0. apply ImpBox. - * box_tac. exch 1; exch 0. apply open_box_L. - erewrite E_irr with (ϕ' := φ1). - apply Hind. + * box_tac. exch 1; exch 0. apply open_box_L, Hind. -- order_tac. rewrite elements_open_boxes. repeat rewrite Permutation_middle. order_tac. -- occ. intro HF. destruct (occurs_in_open_boxes _ _ _ HF Hin1) as (θ0 & Hθ0 & Hinθ). apply (Hnin θ0); ms. @@ -805,19 +824,19 @@ end; simpl. * exch 0. apply Hind; [order_tac|occ | | trivial]. (erewrite proper_Provable; [| |reflexivity]); [eapply Hp2|]. rewrite Heq'. rewrite union_difference_L by trivial. ms. -- destruct (open_boxes_case (list_to_set_disj Δ)) as [[θ Hθ] | Hequiv]. +- destruct (open_boxes_case (list_to_set_disj Δ')) as [[θ Hθ] | Hequiv]. + apply contraction. Etac. exch 1; exch 0; apply ImpBox. * box_tac. box_tac. exch 2; exch 1; exch 0. apply weakening. foldEA. - erewrite E_irr with (ϕ' := φ1). exch 1; exch 0. apply Hind. -- order_tac. rewrite elements_open_boxes. - do 2 apply env_order_cancel_right. apply env_order_4; simpl; try lia. left. + do 2 apply env_order_cancel_right. apply env_order_4; simpl; try lia. + apply env_order_env_order_refl. apply env_order_disj_union_compat_strong_left; order_tac. -- occ. intro HF. destruct (occurs_in_open_boxes _ _ _ HF Hin1) as (θ0 & Hθ0 & Hinθ). apply (Hnin θ0); ms. -- assert(Hθ' := In_open_boxes _ _ Hθ). - assert(Heq'' : Γ0 ≡ (Γ ∖ {[□ φ1 → φ2]} ⊎ list_to_set_disj ((□θ) :: rm (□ θ) Δ))). { + assert(Heq'' : Γ0 ≡ (Γ ∖ {[□ φ1 → φ2]} ⊎ list_to_set_disj ((□θ) :: rm (□ θ) Δ'))). { rewrite Heq'. simpl. rewrite union_difference_L by trivial. rewrite (difference_singleton _ _ Hθ). rewrite list_to_set_disj_rm. ms. @@ -829,40 +848,36 @@ end; simpl. rewrite open_boxes_add. simpl. ms. -- intro HF. apply (Hnin _ Hin0). simpl. tauto. * exch 0. apply weakening. exch 0. apply Hind ; [order_tac|occ|peapply' Hp2]. - + erewrite E_irr with (ϕ' := φ1). - exch 0. apply ImpBox. + + exch 0. apply ImpBox. * box_tac. exch 1; exch 0. apply open_box_L. apply Hind. -- order_tac. rewrite elements_open_boxes. order_tac. -- occ. intro HF. destruct (occurs_in_open_boxes _ _ _ HF Hin1) as (θ0 & Hθ0 & Hinθ). apply (Hnin θ0); ms. - -- assert(Heq'' : (⊗ Γ0) ≡ ((⊗Γ ∖ {[□ φ1 → φ2]}) ⊎ ⊗ (list_to_set_disj Δ))). { + -- assert(Heq'' : (⊗ Γ0) ≡ ((⊗Γ ∖ {[□ φ1 → φ2]}) ⊎ ⊗ (list_to_set_disj Δ'))). { rewrite Heq'. rewrite union_difference_L by trivial. rewrite <- Hequiv, open_boxes_disj_union. rewrite open_boxes_remove by trivial. ms. } peapply Hp1. -- intro HF. apply (Hnin _ Hin0). simpl. tauto. - * erewrite E_irr with (ϕ' := ψ). - exch 0. apply Hind. order_tac. occ. clear Hequiv. peapply' Hp2. + * exch 0. apply Hind. order_tac. occ. clear Hequiv. peapply' Hp2. - split; Etac. + foldEA. apply make_impl_sound_L, ImpBox. - -- do 2 apply weakening. apply make_impl_sound_R, ImpR. - erewrite E_irr with (ϕ' := φ1) by ms. - apply Hind. + -- do 2 apply weakening. apply make_impl_sound_R, ImpR, Hind. ++ order_tac. rewrite elements_open_boxes. do 2 apply env_order_cancel_right. repeat rewrite Permutation_middle. apply env_order_disj_union_compat_strong_left; order_tac. ++ intros φ0 Hin1 HF. destruct (occurs_in_open_boxes _ _ _ HF Hin1) as (θ0 & Hθ0 & Hinθ). apply (Hnin θ0); ms. - ++ assert(Heq'' : (⊗ Γ0) ≡ ((⊗Γ) ⊎ list_to_set_disj (map open_box (rm (□ φ1 → φ2) Δ)))). { + ++ assert(Heq'' : (⊗ Γ0) ≡ ((⊗Γ) ⊎ list_to_set_disj (map open_box (rm (□ φ1 → φ2) Δ')))). { rewrite Heq'. repeat rewrite open_boxes_remove by ms. simpl. rewrite <- list_to_set_disj_open_boxes, <- list_to_set_disj_rm, open_boxes_disj_union. trivial. simpl. rewrite union_difference_R by auto with proof. rewrite open_boxes_remove by ms. ms. } peapply Hp1. - -- apply Hind. order_tac. occ. peapply' Hp2. trivial. - + assert(Heq'' : (⊗ Γ0) ≡ ((⊗Γ) ⊎ list_to_set_disj (map open_box (rm (□ φ1 → φ2) Δ)))). { + -- apply Hind. order_tac. occ. simpl. peapply' Hp2. trivial. + + assert(Heq'' : (⊗ Γ0) ≡ ((⊗Γ) ⊎ list_to_set_disj (map open_box (rm (□ φ1 → φ2) Δ')))). { rewrite Heq'. repeat rewrite open_boxes_remove by ms. simpl. rewrite <- list_to_set_disj_open_boxes, <- list_to_set_disj_rm, open_boxes_disj_union. trivial. @@ -870,10 +885,8 @@ end; simpl. } foldEA. Atac. apply AndR. * apply make_impl_sound_L, ImpBox. - -- do 2 apply weakening. apply make_impl_sound_R, ImpR. - erewrite E_irr with (ϕ' := φ1). - apply Hind. - ++ order_tac. rewrite elements_open_boxes. + -- do 2 apply weakening. apply make_impl_sound_R, ImpR, Hind. + ++ order_tac. rewrite elements_open_boxes. do 2 apply env_order_cancel_right. repeat rewrite Permutation_middle. apply env_order_disj_union_compat_strong_left; order_tac. @@ -881,7 +894,6 @@ end; simpl. apply (Hnin θ0); ms. ++ peapply Hp1. -- apply BoxR. box_tac. do 2 apply weakening. apply make_impl_sound_R, ImpR. foldEA. - erewrite E_irr with (ϕ' := φ1) by ms. apply Hind. ++ order_tac. rewrite elements_open_boxes. do 2 apply env_order_cancel_right. @@ -891,9 +903,7 @@ end; simpl. apply (Hnin θ0); ms. ++ peapply Hp1. * foldEA. apply make_impl_sound_L, ImpBox. - -- do 2 apply weakening. apply make_impl_sound_R, ImpR. - erewrite E_irr with (ϕ' := φ1). - apply Hind. + -- do 2 apply weakening. apply make_impl_sound_R, ImpR, Hind. ++ order_tac. rewrite elements_open_boxes. do 2 apply env_order_cancel_right. repeat rewrite Permutation_middle. @@ -903,15 +913,14 @@ end; simpl. ++ peapply Hp1. -- clear Heq''. apply Hind; [order_tac|occ|peapply' Hp2]. - split. - + intro Hocc. destruct (open_boxes_case (list_to_set_disj Δ)) as [[θ Hθ] | Hequiv]. - * Etac. foldEA. apply BoxR. box_tac. exch 0. - erewrite E_irr with (ϕ' := φ); apply Hind. - -- order_tac. + + intro Hocc. destruct (open_boxes_case (list_to_set_disj Δ')) as [[θ Hθ] | Hequiv]. + * Etac. foldEA. apply BoxR. box_tac. exch 0. apply Hind. + -- order_tac. rewrite elements_open_boxes. repeat rewrite Permutation_middle. apply env_order_disj_union_compat_strong_left. order_tac. apply env_order_2. simpl; lia. simpl; lia. - apply env_order_eq_add. left. order_tac. + apply env_order_eq_add. apply env_order_env_order_refl. order_tac. -- intros φ0 Hφ0 HF. apply gmultiset_elem_of_disj_union in Hφ0. destruct Hφ0 as [Hφ0|]; [|ms]. destruct (occurs_in_open_boxes _ _ _ HF Hφ0) as (θ0 & Hθ0 & Hinθ). apply (Hnin θ0); ms. @@ -922,35 +931,33 @@ end; simpl. rewrite open_boxes_remove by ms. rewrite <- difference_singleton by auto with proof. ms. -- trivial. - * apply BoxR. box_tac. exch 0. apply open_box_L. - erewrite E_irr with (ϕ' := φ). - apply Hind. + * apply BoxR. box_tac. exch 0. apply open_box_L, Hind. -- order_tac. rewrite elements_open_boxes. repeat rewrite Permutation_middle. apply env_order_disj_union_compat_strong_left. order_tac. - apply env_order_2. simpl; lia. simpl; lia. now right. + apply env_order_2. simpl; lia. simpl; lia. unfold env_order_refl. trivial. -- intros φ0 Hφ0 HF. apply gmultiset_elem_of_disj_union in Hφ0. destruct Hφ0 as [Hφ0|]; [|ms]. destruct (occurs_in_open_boxes _ _ _ HF Hφ0) as (θ0 & Hθ0 & Hinθ). apply (Hnin θ0); ms. -- (erewrite proper_Provable; [| |reflexivity]); [eapply Hp|]. rewrite open_boxes_disj_union, <- Hequiv. ms. -- trivial. - + Atac'. foldEA. apply BoxR. box_tac. apply weakening. erewrite E_irr with (ϕ' := φ). - apply weakening. apply make_impl_sound_R, ImpR. + + Atac'. foldEA. apply BoxR. box_tac. apply weakening, weakening, make_impl_sound_R, ImpR. apply Hind. - * order_tac. - rewrite elements_open_boxes. + * order_tac. rewrite elements_open_boxes, simp_env_idempotent. repeat rewrite Permutation_middle. order_tac. * intros φ0 Hφ0 HF. destruct (occurs_in_open_boxes _ _ _ HF Hφ0) as (θ0 & Hθ0 & Hinθ). apply (Hnin θ0); ms. * (erewrite proper_Provable; [| |reflexivity]); [eapply Hp|]. - rewrite open_boxes_disj_union. - rewrite <- list_to_set_disj_env_add. - rewrite <- list_to_set_disj_open_boxes. ms. + subst Δ'. rewrite simp_env_idempotent. + rewrite open_boxes_disj_union. + rewrite <- list_to_set_disj_env_add. + rewrite <- list_to_set_disj_open_boxes. ms. Qed. + End PropQuantCorrect. End Correctness. @@ -962,10 +969,9 @@ End UniformInterpolation. Open Scope type_scope. - -Lemma E_of_empty p φ : E p ([], φ) = (Implies Bot Bot). +Lemma E_of_empty p : E p [] = (Implies Bot Bot). Proof. - rewrite E_eq. rewrite in_map_empty. now unfold conjunction, nodup, foldl. + rewrite E_eq, simp_env_nil. simpl. rewrite in_map_empty. now unfold conjunction, nodup, foldl. Qed. Definition vars_incl φ l := forall x, occurs_in x φ -> In x l. @@ -985,8 +991,8 @@ intros Hp φ Hvarsφ; repeat split. + intros x Hx. apply (EA_vars p _ ⊥ x) in Hx. destruct Hx as [Hneq [θ [Hθ Hocc]]]. apply elem_of_list_singleton in Hθ. subst. apply Hvarsφ in Hocc. destruct Hocc; subst; tauto. - + replace {[φ]} with (list_to_set_disj [φ] : env). apply entail_correct. simpl. ms. - + intros ψ Hψ Hyp. rewrite elem_of_list_In in Hp. unfold Ef. rewrite E_irr with (ϕ' := ψ). + + replace {[φ]} with (list_to_set_disj [φ] : env). apply (entail_correct _ _ ⊥). ms. + + intros ψ Hψ Hyp. rewrite elem_of_list_In in Hp. unfold Ef. * peapply (pq_correct p ∅ [φ] ψ). -- intros θ Hin. inversion Hin. -- peapply Hyp. @@ -1001,4 +1007,4 @@ intros Hp φ Hvarsφ; repeat split. * intros φ0 Hφ0. apply gmultiset_elem_of_singleton in Hφ0. subst. auto with *. * peapply Hyp. * now rewrite E_of_empty. -Qed. +Qed. \ No newline at end of file diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index 3126de4..0ad4293 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -527,10 +527,10 @@ match goal with end. Qed. -Require Import ISL.PropQuantifiers. +Require Import ISL.PropQuantifiers ISL.Simp_env. -Definition E_simplified (p: variable) (ψ: form) := simp (E p ([ψ], ⊥)). -Definition A_simplified (p: variable) (ψ: form) := simp (Af p (ψ)). +Definition E_simplified (p: variable) (ψ: form) := simp_form (E p [ψ]). +Definition A_simplified (p: variable) (ψ: form) := simp_form (Af p (ψ)). (* Lemma bot_vars_incl V: vars_incl ⊥ V. diff --git a/theories/iSL/Simp_env.v b/theories/iSL/Simp_env.v new file mode 100644 index 0000000..beb196e --- /dev/null +++ b/theories/iSL/Simp_env.v @@ -0,0 +1,413 @@ +Require Import Coq.Program.Equality. +Require Import ISL.Sequents ISL.SequentProps. +Require Import ISL.Order ISL.DecisionProcedure. +Require Import Coq.Classes.RelationClasses. +Require Import ISL.Cut ISL.Optimizations. + +Definition applicable_AndL (Γ : list form): {ψ1 & {ψ2 | (And ψ1 ψ2) ∈ Γ}} + (∀ ψ1 ψ2, (And ψ1 ψ2) ∈ Γ -> False). +Proof. + pose (fA := (fun θ => match θ with |And _ _ => true | _ => false end)). + destruct (exists_dec fA Γ) as [(θ & Hin & Hθ) | Hf]. + - left. subst fA. destruct θ. 3: { eexists. eexists. apply elem_of_list_In. eauto. } + all: auto with *. + - right. intros ψ1 ψ2 Hψ. rewrite elem_of_list_In in Hψ. apply Hf in Hψ. subst fA. simpl in Hψ. tauto. +Defined. + +Definition applicable_ImpLVar (Γ : list form): + {q & {ψ | Var q ∈ Γ /\ (Implies (Var q) ψ) ∈ Γ}} + + (∀ q ψ, Var q ∈ Γ -> (Implies (Var q) ψ) ∈ Γ -> False). +Proof. + pose (fIp :=λ p θ, match θ with | Implies (Var q) _ => if decide (p = q) then true else false | _ => false end). + pose (fp:= (fun θ => match θ with |Var p => if (exists_dec (fIp p) Γ) then true else false | _ => false end)). + destruct (exists_dec fp Γ) as [(θ & Hin & Hθ) | Hf]. + - left. subst fp. destruct θ. 2-6: auto with *. + case exists_dec as [(ψ &Hinψ & Hψ)|] in Hθ; [|auto with *]. + unfold fIp in Hψ. destruct ψ. 1-4, 6: auto with *. + destruct ψ1. 2-6: auto with *. case decide in Hψ; [|auto with *]. + subst. apply elem_of_list_In in Hinψ, Hin. + do 2 eexists. split; eauto. + - right. intros q ψ Hp Hψ. rewrite elem_of_list_In in Hp, Hψ. apply Hf in Hp. subst fp fIp. + simpl in Hp. case exists_dec as [|Hf'] in Hp. auto with *. + apply (Hf' _ Hψ). rewrite decide_True; trivial. auto with *. +Defined. + +Definition applicable_ImpLAnd (Γ : list form): + {φ1 & {φ2 & {φ3 | (Implies (And φ1 φ2) φ3) ∈ Γ}}} + + (∀ φ1 φ2 φ3, (Implies (And φ1 φ2) φ3) ∈ Γ -> False). +Proof. + pose (fII := (fun θ => match θ with |Implies (And _ _) _ => true | _ => false end)). + destruct (exists_dec fII Γ) as [(θ & Hin & Hθ) | Hf]. + - left. subst fII. destruct θ. 1-4, 6: auto with *. + destruct θ1. 1-2,4-6: auto with *. do 3 eexists; apply elem_of_list_In; eauto. + - right. intros ψ1 ψ2 ψ3 Hψ. rewrite elem_of_list_In in Hψ. apply Hf in Hψ. subst fII. simpl in Hψ. tauto. +Defined. + +Definition applicable_ImpLOr (Γ : list form): + {φ1 & {φ2 & {φ3 | (Implies (Or φ1 φ2) φ3) ∈ Γ}}} + + (∀ φ1 φ2 φ3, (Implies (Or φ1 φ2) φ3) ∈ Γ -> False). +Proof. + pose (fII := (fun θ => match θ with |Implies (Or _ _) _ => true | _ => false end)). + destruct (exists_dec fII Γ) as [(θ & Hin & Hθ) | Hf]. + - left. subst fII. destruct θ. 1-4, 6: auto with *. + destruct θ1. 1-3, 5-6: auto with *. do 3 eexists; apply elem_of_list_In; eauto. + - right. intros ψ1 ψ2 ψ3 Hψ. rewrite elem_of_list_In in Hψ. apply Hf in Hψ. subst fII. simpl in Hψ. tauto. +Defined. + +Definition sumor_bind0 {A} {B : Prop} {C}: A + B -> (A -> C) -> C -> C := +λ qH f c, +match qH with +| inl a => f a +| inr _ => c +end. + +Definition sumor_bind1 {A A'} {B : Prop} {C}: {q : A | A' q} + B -> (forall x (_ : A' x), C) -> C -> C := +λ qH f c, +match qH with +| inl (exist _ q Hq) => f q Hq +| inr _ => c +end. + +Definition sumor_bind2 {A A' A''} {B : Prop} {C}: {q : A & {r : A' | A'' q r}} + B -> (forall x y (_ : A'' x y), C) -> C -> C := +λ qH f c, +match qH with +| inl (existT q (exist _ r Hq)) => f q r Hq +| inr _ => c +end. + +Definition sumor_bind3 {A A' A'' A'''} {B : Prop} {C}: + {q : A & {r : A' & { s : A'' | A''' q r s}}} + B -> (forall x y z (_ : A''' x y z), C) -> C -> C := +λ qH f c, +match qH with +| inl (existT q (existT r (exist _ s Hq))) => f q r s Hq +| inr _ => c +end. + +Notation "cond '?' A ':0' B" := (sumor_bind0 cond A B) (at level 150, right associativity). +Notation "cond '?' A ':1' B" := (sumor_bind1 cond A B) (at level 150, right associativity). +Notation "cond '?' A ':2' B" := (sumor_bind2 cond A B) (at level 150, right associativity). +Notation "cond '?' A ':3' B" := (sumor_bind3 cond A B) (at level 150, right associativity). + +Local Notation "Δ '•' φ" := (cons φ Δ). + +Infix "⊢?" := Provable_dec (at level 80). + +(* Probably very costly *) +Definition applicable_strong_weakening (Γ : list form): + {φ : form | φ ∈ Γ /\ exists (_ : list_to_set_disj (rm φ Γ) ⊢ φ), True} + + (∀ φ, φ ∈ Γ -> forall (_ : list_to_set_disj (rm φ Γ) ⊢ φ), False). +Proof. +destruct (exists_dec (λ φ, if Provable_dec (rm φ Γ) φ then true else false) Γ) as [[φ [Hin Hφ]]| Hf]. +- left. exists φ; split. + + now apply elem_of_list_In. + + destruct ((rm φ Γ) ⊢? φ). trivial. contradict Hφ. +- right. intros φ Hin Hφ. apply (Hf φ). now apply elem_of_list_In. + destruct ((rm φ Γ) ⊢? φ). auto with *. tauto. +Defined. + +Local Obligation Tactic := (simpl; intuition order_tac). +Program Fixpoint simp_env (Δ : list form) {wf env_order Δ} : list form := + (* invertible left rules *) + if Δ ⊢? ⊥ then [⊥] else + applicable_AndL Δ ? λ δ₁ δ₂ _, simp_env ((rm (δ₁ ∧ δ₂) Δ•δ₁)•δ₂) :2 + applicable_ImpLVar Δ ? λ q ψ _, simp_env ((rm (Var q → ψ) Δ • ψ)) :2 + applicable_ImpLAnd Δ ? λ δ₁ δ₂ δ₃ _, simp_env ((rm ((δ₁ ∧ δ₂)→ δ₃) Δ • (δ₁ → (δ₂ → δ₃)))) :3 + applicable_ImpLOr Δ ? λ δ₁ δ₂ δ₃ _, simp_env (rm ((δ₁ ∨ δ₂)→ δ₃) Δ • (δ₁ → δ₃) • (δ₂ → δ₃)) :3 + (* remove redundant assumptions *) + applicable_strong_weakening Δ ? λ φ _, simp_env (rm φ Δ) :1 + Δ +. +Next Obligation. apply Wf.measure_wf, wf_env_order. Qed. + +Lemma simp_env_eq (Δ : list form): simp_env Δ = + (* invertible left rules *) + if Δ ⊢? ⊥ then [⊥] else + applicable_AndL Δ ? λ δ₁ δ₂ _, simp_env ((rm (δ₁ ∧ δ₂) Δ•δ₁)•δ₂) :2 + applicable_ImpLVar Δ ? λ q ψ _, simp_env ((rm (Var q → ψ) Δ • ψ)) :2 + applicable_ImpLAnd Δ ? λ δ₁ δ₂ δ₃ _, simp_env ((rm ((δ₁ ∧ δ₂)→ δ₃) Δ • (δ₁ → (δ₂ → δ₃)))) :3 + applicable_ImpLOr Δ ? λ δ₁ δ₂ δ₃ _, simp_env (rm ((δ₁ ∨ δ₂)→ δ₃) Δ • (δ₁ → δ₃) • (δ₂ → δ₃)) :3 + (* remove redundant assumptions *) + (applicable_strong_weakening Δ ? λ φ _, simp_env (rm φ Δ) :1 + Δ). +Proof. +simpl. unfold simp_env. simpl. +repeat rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl. split; trivial. +Qed. + +Definition simp_form φ:= ⋀ (simp_env [φ]). + + +Definition pointed_env_order_refl pe1 pe2 := env_order_refl (pe1.2 :: pe1.2 :: pe1.1) (pe2.2 :: pe2.2 :: pe2.1). + +(* TODO: move *) + +Lemma empty_entails_not_bot : (∅ ⊢ ⊥) -> False. +Proof. +intro Hf. dependent destruction Hf; simpl in *; +match goal with x : _ ⊎ {[+?φ+]} = _ |- _ => +exfalso; eapply (gmultiset_elem_of_empty φ); setoid_rewrite <- x; ms end. +Qed. + +Ltac simp_env_tac := +let Hf := fresh "Hf" in +match goal with +| |- context[sumor_bind2 ?cond ?A ?B] => + let φ1 := fresh "φ1" in let φ2 := fresh "φ2" in let Hc := fresh "Hc" in + destruct cond as [(φ1 & φ2 & Hc) | Hf] +| |- context[sumor_bind3 ?cond ?A ?B] => + let φ1 := fresh "φ1" in let φ2 := fresh "φ2" in let φ3 := fresh "φ3" in let Hc := fresh "Hc" in + destruct cond as [(φ1 & φ2 & φ3 & Hc) | Hf] +| |- context[sumor_bind1 ?cond ?A ?B] => + let φ1 := fresh "φ1" in let Hc := fresh "Hc" in + destruct cond as [(φ1 & Hc) | Hf] +end; simpl. + +Lemma simp_env_order Δ : env_order_refl (simp_env Δ) Δ. +Proof. +revert Δ. apply (well_founded_induction_type wf_env_order). intros Δ Hind. +rewrite simp_env_eq. +case (Δ ⊢? ⊥). +{ intros [Hf _]. destruct Δ as [|φ Δ]. + + now apply empty_entails_not_bot in Hf. + + unfold env_order_refl. do 2 rewrite env_weight_add. simpl. pose (weight_pos φ). + replace 5 with (0 + 5^1) at 1 by trivial. apply Nat.add_le_mono. lia. + apply Nat.pow_le_mono_r; lia. +} +intro Hbot. +repeat simp_env_tac. +all: try (apply env_order_env_order_refl; eapply env_order_le_lt_trans; [apply Hind|]; intuition; order_tac). +apply env_order_self. +Qed. + +Global Hint Resolve simp_env_order : order. + +Lemma simp_env_nil: simp_env [] = []. +Proof. +assert(Ho := simp_env_order []). destruct (simp_env []) as [|φ Δ]. +trivial. +contradict Ho. unfold env_order_refl. rewrite env_weight_add. +apply Nat.lt_nge. +unfold env_weight. simpl. pose(Order.pow5_gt_0 (weight φ)). lia. +Qed. + +Lemma simp_env_pointed_env_order_L pe Δ φ: (pe ≺· (simp_env Δ, φ)) -> pe ≺· (Δ, φ). +Proof. +intro Hl. eapply env_order_lt_le_trans; eauto. simpl. auto with order. +Qed. + +Lemma simp_env_env_order_L Δ Δ0: (Δ0 ≺ simp_env Δ) -> Δ0 ≺ Δ. +Proof. +intro Hl. eapply env_order_lt_le_trans; eauto. auto with order. +Qed. + +Global Hint Resolve simp_env_pointed_env_order_L : order. +Global Hint Resolve simp_env_env_order_L : order. + +Section Equivalence. + +Definition equiv_form φ ψ : Type := (φ ≼ ψ) * (ψ ≼ φ). + + + +Definition equiv_env Δ Δ': Set := + (∀ φ, list_to_set_disj Δ ⊢ φ -> list_to_set_disj Δ' ⊢ φ) * + (∀ φ, list_to_set_disj Δ' ⊢ φ -> list_to_set_disj Δ ⊢ φ). +(* slightly too general + (∀ Γ φ, Γ ⊎ list_to_set_disj Δ ⊢ φ -> Γ ⊎ list_to_set_disj Δ' ⊢ φ) * + (∀ Γ φ, Γ ⊎ list_to_set_disj Δ' ⊢ φ -> Γ ⊎ list_to_set_disj Δ ⊢ φ). +*) +Lemma symmetric_equiv_env Δ Γ: equiv_env Δ Γ -> equiv_env Γ Δ . +Proof. intros [H1 H2]. split; trivial. Qed. + +(* TODO: move *) +Lemma conjunction_L' Γ Δ ϕ: (Γ ⊎ {[⋀ Δ]} ⊢ ϕ) -> Γ ⊎ list_to_set_disj Δ ⊢ ϕ. +Proof. +revert ϕ. unfold conjunction. +assert( Hstrong: ∀ θ ϕ : form, Γ ⊎ {[foldl make_conj θ (nodup form_eq_dec Δ)]} ⊢ ϕ + → (Γ ⊎ list_to_set_disj Δ) ⊎ {[θ]} ⊢ ϕ). +{ + induction Δ as [|δ Δ]; intros θ ϕ; simpl. + - intro Hp. peapply Hp. + - case in_dec; intros Hin Hp. + + peapply (weakening δ). apply IHΔ, Hp. ms. + + simpl in Hp. apply IHΔ in Hp. + peapply (AndL_rev (Γ ⊎ list_to_set_disj Δ) θ δ). apply make_conj_complete_L, Hp. +} + intros; apply additive_cut with (φ := ⊤); eauto with proof. +Qed. + +Lemma conjunction_R Δ: list_to_set_disj Δ ⊢ ⋀ Δ. +Proof. +apply conjunction_R1. intros φ Hφ. apply elem_of_list_to_set_disj in Hφ. +exhibit Hφ 0. apply generalised_axiom. +Qed. + +Lemma conjunction_L'' Γ Δ ϕ: Γ ⊎ list_to_set_disj Δ ⊢ ϕ -> (Γ ⊎ {[⋀ Δ]} ⊢ ϕ). +Proof. +revert ϕ. unfold conjunction. +assert( Hstrong: ∀ θ ϕ : form,(Γ ⊎ list_to_set_disj Δ) ⊎ {[θ]} ⊢ ϕ -> Γ ⊎ {[foldl make_conj θ (nodup form_eq_dec Δ)]} ⊢ ϕ). +{ + induction Δ as [|δ Δ]; intros θ ϕ; simpl. + - intro Hp. peapply Hp. + - case in_dec; intros Hin Hp. + + apply IHΔ. + assert(Hin' : δ ∈ (Γ ⊎ list_to_set_disj Δ)). + { apply gmultiset_elem_of_disj_union; right; apply elem_of_list_to_set_disj, elem_of_list_In, Hin. } + exhibit Hin' 1. exch 0. apply contraction. exch 1. exch 0. + rw (symmetry (difference_singleton _ _ Hin')) 2. peapply Hp. + + simpl. apply IHΔ. apply make_conj_sound_L, AndL. peapply Hp. +} +intros. apply Hstrong, weakening. assumption. +Qed. + +(* +Lemma equiv_env_L0 Δ Δ' φ: (equiv_env Δ Δ') -> + list_to_set_disj Δ ⊢ φ -> list_to_set_disj Δ' ⊢ φ. +Proof. +intros [Hp _] H. peapply (Hp ∅). peapply H. +Qed. +*) + +Lemma equiv_env_refl Δ : equiv_env Δ Δ. +Proof. split; trivial. Qed. + +Lemma equiv_env_trans Δ Δ' Δ'' : equiv_env Δ Δ' -> equiv_env Δ' Δ'' -> equiv_env Δ Δ''. +Proof. +intros [H11 H12] [H21 H22]. split; intros; auto. +Qed. + +(* TODO: move *) +Hint Resolve elem_of_list_to_set_disj : proof. + + +Ltac l_tac' := repeat rewrite list_to_set_disj_open_boxes; + rewrite (proper_Provable _ _ (symmetry (list_to_set_disj_env_add _ _)) _ _ eq_refl) +|| rewrite (proper_Provable _ _ (equiv_disj_union_compat_r (symmetry (list_to_set_disj_env_add _ _))) _ _ eq_refl) +|| rewrite (proper_Provable _ _ (equiv_disj_union_compat_r (equiv_disj_union_compat_r (symmetry (list_to_set_disj_env_add _ _)))) _ _ eq_refl) +|| rewrite (proper_Provable _ _ (equiv_disj_union_compat_r(equiv_disj_union_compat_r (equiv_disj_union_compat_r (symmetry (list_to_set_disj_env_add _ _))))) _ _ eq_refl). + +Lemma Provable_dec_of_Prop Γ φ: (∃ _ : list_to_set_disj Γ ⊢ φ, True) -> (list_to_set_disj Γ ⊢ φ). +Proof. +destruct (Proof_tree_dec Γ φ) as [[Hφ1' _] | Hf']. tauto. +intros Hf. exfalso. destruct Hf as [Hf _]. tauto. +Qed. + +Lemma simp_env_equiv_env Δ: equiv_env (simp_env Δ) Δ. +Proof. +Local Ltac equiv_tac := + repeat rewrite <- list_to_set_disj_rm; + repeat rewrite <- list_to_set_disj_env_add; + repeat (rewrite <- difference_singleton; trivial); + try rewrite <- list_to_set_disj_rm; + try (rewrite union_difference_L by trivial); + try (rewrite union_difference_R by trivial); + try ms. +Local Ltac peapply' th := (erewrite proper_Provable; [| |reflexivity]); [eapply th|equiv_tac]. +revert Δ. apply (well_founded_induction_type wf_env_order). intros Δ Hind. +rewrite simp_env_eq. +case (Δ ⊢? ⊥). +{ intro Hf. apply Provable_dec_of_Prop in Hf. + split; intros φ Hp. + + apply exfalso. assumption. + + simpl. peapply (ExFalso ∅). +} +intro Hbot. +repeat simp_env_tac; (try (eapply equiv_env_trans; [apply Hind; intuition; order_tac|])). +- apply elem_of_list_to_set_disj in Hc. + split; intros φ Hp. + + exhibit Hc 0. apply AndL. peapply' Hp. + + do 2 l_tac'. apply AndL_rev. peapply' Hp. +- destruct Hc as [Hc1 Hc2]. apply elem_of_list_to_set_disj in Hc1, Hc2. + assert(Hc3: Var φ1 ∈ (list_to_set_disj Δ ∖ {[φ1 → φ2]} : env)). + { apply in_difference. intro HF. discriminate HF. assumption. } + split; intros φ Hp. + + exhibit Hc2 0. exhibit Hc3 1. peapply ImpLVar. peapply' Hp. + + l_tac'. peapply' (ImpLVar_rev (list_to_set_disj (rm φ1 (rm (φ1 → φ2) Δ))) φ1 φ2). + peapply' Hp. +- apply elem_of_list_to_set_disj in Hc. + split; intros φ Hp. + + exhibit Hc 0. apply ImpLAnd. peapply' Hp. + + l_tac'. apply ImpLAnd_rev. peapply' Hp. +- apply elem_of_list_to_set_disj in Hc. + split; intros φ Hp. + + exhibit Hc 0. apply ImpLOr. peapply' Hp. + + do 2 l_tac'. apply ImpLOr_rev. peapply' Hp. +- destruct Hc as [Hc Hφ1]. apply elem_of_list_to_set_disj in Hc. + split; intros φ Hp. + + exhibit Hc 0. apply weakening. peapply' Hp. + + apply Provable_dec_of_Prop in Hφ1. + apply additive_cut with φ1. trivial. peapply' Hp. +- apply equiv_env_refl. +Qed. + +Lemma equiv_env_L1 Γ Δ Δ' φ: (equiv_env Δ Δ') -> + Γ ⊎ list_to_set_disj Δ ⊢ φ -> Γ ⊎ list_to_set_disj Δ' ⊢ φ. +Proof. +intros [H1 _] Hp. +revert φ Hp. +induction Γ as [|x Γ] using gmultiset_rec; intros φ Hp. +- peapply H1. peapply Hp. +- peapply (ImpR_rev (Γ ⊎ list_to_set_disj Δ') x). + apply IHΓ, ImpR. peapply Hp. +Qed. + +End Equivalence. + +(* Global Hint Resolve simp_env_L1 : proof. *) + +Infix "≡f" := equiv_form (at level 120). + +Global Infix "≡e" := equiv_env (at level 120). + +Section Variables. + +Local Ltac occ p := simpl; tauto || +match goal with +| Hnin : ∀ φ0 : form, φ0 ∈ ?Γ → ¬ occurs_in p φ0 |- _ => + + let Hin := fresh "Hin" in + try (match goal with |Hocc : ?a ∈ ?Γ |- _ => let Hocc' := fresh "Hocc" in assert (Hocc' := Hnin _ Hocc); simpl in Hocc'; + let Hin' := fresh "Hinx" in assert(Hin' := In_open_boxes _ _ Hocc); simpl in *; + try rewrite open_boxes_remove in * by trivial end); + intro; repeat rewrite env_in_add; repeat rewrite difference_include; simpl; + intro Hin; try tauto; + try (destruct Hin as [Hin|[Hin|Hin]] ||destruct Hin as [Hin|Hin]); + subst; simpl; try tauto; + repeat (apply difference_include in Hin; [|assumption]); + try (now apply Hnin) +end. + +Lemma equiv_env_vars Δ x: + (∃ θ : form, ((θ ∈ simp_env Δ) /\ occurs_in x θ)) -> + ∃ θ : form, ((θ ∈ Δ) /\ occurs_in x θ). +Proof. +revert Δ. refine (well_founded_induction_type wf_env_order _ _). intros Δ Hind. +rewrite (simp_env_eq Δ). +case (Δ ⊢? ⊥). +{ intros _ [θ [Hin Hocc]]. apply elem_of_list_singleton in Hin. subst. contradict Hocc. } +intro Hbot. +repeat simp_env_tac; trivial. +all:(decompose record Hc; + intro Hocc; apply Hind in Hocc; [|order_tac]; destruct Hocc as [θ [Hin Hocc]]; + apply elem_of_list_to_set_disj in Hin; + repeat rewrite <- ?list_to_set_disj_env_add, gmultiset_elem_of_disj_union in Hin; + repeat ((try apply elem_of_list_to_set_disj, elem_of_list_In, in_rm, elem_of_list_In in Hin; + try apply gmultiset_elem_of_singleton in Hin; + subst; try solve[eexists; split; simpl in *; eauto; simpl in *; eauto || tauto]) || destruct Hin as [Hin | Hin])). +Qed. + +End Variables. + +Lemma simp_env_idempotent Δ: simp_env (simp_env Δ) = simp_env Δ. +Proof. +revert Δ. apply (well_founded_induction_type wf_env_order). intros Δ Hind. +rewrite (simp_env_eq Δ). +case (Δ ⊢? ⊥). +{ intro e. rewrite simp_env_eq. case ([⊥] ⊢? ⊥). trivial. intro Hf. contradict Hf. + simpl. peapply (ExFalso ∅). } +intro Hbot. +repeat simp_env_tac; (try (intuition; apply Hind; order_tac)). +rewrite simp_env_eq. +case (Δ ⊢? ⊥); [intros [He _]; tauto| intros _]. +repeat simp_env_tac; try (try (apply Provable_dec_of_Prop in Hc); contradict Hc; intuition; eauto); trivial. +eapply Hf3. eauto. now apply Provable_dec_of_Prop. +Qed.