diff --git a/theories/extraction/UIML_extraction.v b/theories/extraction/UIML_extraction.v index ba82573..d44aae4 100644 --- a/theories/extraction/UIML_extraction.v +++ b/theories/extraction/UIML_extraction.v @@ -5,7 +5,7 @@ Require Import ExtrOcamlBasic ExtrOcamlString. Require Import K.Interpolation.UIK_braga. Require Import KS_export. -Require Import ISL.InvPropQuantifiers ISL.DecisionProcedure ISL.Simp. +Require Import ISL.PropQuantifiers ISL.DecisionProcedure ISL.Simp. Fixpoint MPropF_of_form (f : Formulas.form) : MPropF := diff --git a/theories/iSL/InvPropQuantifiers.v b/theories/iSL/InvPropQuantifiers.v deleted file mode 100644 index 983ad70..0000000 --- a/theories/iSL/InvPropQuantifiers.v +++ /dev/null @@ -1,334 +0,0 @@ -Require Import Coq.Program.Equality. (* for dependent induction *) -Require Import ISL.PropQuantifiers ISL.Sequents ISL.SequentProps. -Require Import ISL.Order ISL.DecisionProcedure. -Require Import Coq.Classes.RelationClasses. -Section UniformInterpolation. - -Definition applicable_AndR φ: {φ1 & {φ2 | φ = (And φ1 φ2)}} + (∀ φ1 φ2, φ ≠ (And φ1 φ2)). -Proof. (destruct φ; eauto). Defined. -(* -Definition applicable_other_var (Γ : list form): {q | p ≠ q /\ Var q ∈ Γ} + (∀ q, p ≠ q -> Var q ∈ Γ -> False). -Proof. - pose (fA := (fun θ => match θ with |Var q => if decide (p = q) then false else true | _ => false end)). - destruct (exists_dec fA Γ) as [(θ & Hin & Hθ) | Hf]. - - left. subst fA. destruct θ. - 1: { case decide in Hθ. auto with *. eexists; split; eauto. apply elem_of_list_In. assumption. } - all: auto with *. - - right. intros ψ1 ψ2 Hψ. rewrite elem_of_list_In in Hψ. apply Hf in Hψ. subst fA. simpl in Hψ. - case decide in Hψ; auto with *. -Defined. -*) - -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_ImpR φ: {φ1 & {φ2 | φ = (Implies φ1 φ2)}} + (∀ φ1 φ2, φ ≠ (Implies φ1 φ2)). -Proof. destruct φ; eauto. Defined. - - -Definition applicable_OrL (Γ : list form): {ψ1 & {ψ2 | (Or ψ1 ψ2) ∈ Γ}} + (∀ ψ1 ψ2, (Or ψ1 ψ2) ∈ Γ -> False). -Proof. - pose (fA := (fun θ => match θ with |Or _ _ => true | _ => false end)). - destruct (exists_dec fA Γ) as [(θ & Hin & Hθ) | Hf]. - - left. subst fA. destruct θ. 4: { 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_ImpL_other_Var (Γ : list form): - {q & {ψ | q ≠ p /\ (Implies (Var q) ψ) ∈ Γ}} + - (∀ q ψ, q ≠ p -> (Implies (Var q) ψ) ∈ Γ -> False). -Proof. - pose (fIp :=λ θ, match θ with | Implies (Var q) _ => if decide (p = q) then false else true | _ => false end). - destruct (exists_dec fIp Γ) as [(θ & Hin & Hθ) | Hf]. - - left. subst fIp. destruct θ; auto with *. - destruct θ1; auto with *. - case decide in Hθ; auto with *. - apply elem_of_list_In in Hin. - do 2 eexists; split; eauto. - - right. intros q ψ Hp Hψ. rewrite elem_of_list_In in Hψ. apply Hf in Hψ. subst fIp. - simpl in Hψ. rewrite decide_False in Hψ; trivial; auto with *. -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_ImpLVar_spec (Γ : list form) q: - {ψ | Var q ∈ Γ /\ (Implies (Var q) ψ) ∈ Γ} + - (∀ ψ, Var q ∈ Γ -> (Implies (Var q) ψ) ∈ Γ -> False). -Proof. - pose (fIp :=λ θ, match θ with | Implies (Var p) _ => if decide (p = q) then true else false | _ => false end). - pose (fp:= (fun θ => match θ with |Var p => if decide (p = q) then if (exists_dec fIp Γ) then true else false else false| _ => false end)). - destruct (exists_dec fp Γ) as [(θ & Hin & Hθ) | Hf]. - - left. subst fp. destruct θ. 2-6: auto with *. - case decide in Hθ; [|auto with *]. subst. - 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. - eexists. split; eauto. - - right. intros ψ Hp Hψ. rewrite elem_of_list_In in Hp, Hψ. apply Hf in Hp. subst fp fIp. - simpl in Hp. rewrite decide_True in Hp by trivial. - 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 applicable_OrR φ: - {φ1 & {φ2 | φ = (Or φ1 φ2)}} + (∀ φ1 φ2, φ = (Or φ1 φ2) -> False). -Proof. destruct φ; eauto with *. Defined. - -Definition applicable_BoxR φ: {φ' | φ = (□ φ')} + (∀ φ', φ = (□ φ') -> False). -Proof. destruct φ; eauto with *. Defined. - -(* -Definition applicable_ImpLImp (Γ : list form): - {φ1 & {φ2 & {φ3 | ((φ1 → φ2) → φ3) ∈ Γ}}} +(forall φ1 φ2 φ3, ((φ1 → φ2) → φ3) ∈ Γ -> False). -Proof. - pose (fII := (fun θ => match θ with |Implies (Implies _ _) _ => true | _ => false end)). - destruct (exists_dec fII Γ) as [(θ & Hin & Hθ) | Hf]. - - left. subst fII. destruct θ. 1-4, 6: auto with *. - destruct θ1. 1-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. -*) - -(* can this be replaced with generalised axiom?*) -Definition applicable_Atom q (Δ : list form) ϕ : - (ϕ = Var q /\ Var q ∈ Δ) + (ϕ ≠ Var q \/ (Var q ∈ Δ -> False)). -Proof. -case (decide (ϕ = Var q)). -case (decide (Var q ∈ Δ)). -all: auto with *. -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). - -(* TODO: plan: - - reuse propquantifiers (esp, don't redefine erule); - - define propquant' as the same fixpoint as propquant, but with a simplification step - - the simplification shold look like the monadic simplifications done here, but more general - - to ensure that' it's still correct, prove that simplified sequents are "equivalent" to the original ones - - show (by induction on the definition of EA and EA') that EA equiv EA' - *) - -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. - -Obligation Tactic := (simpl; intuition order_tac). -Program Fixpoint simp_env (Δ : list form) {wf env_order Δ} : list form := - (* invertible left rules *) - 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. - -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). - -Lemma simp_env_order pe : env_order_refl (simp_env pe) pe. -Proof. -Admitted. - -Variable p : variable. - -Obligation Tactic := solve[simpl; intros; simpl in *; intuition; order_tac] || (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 (* because pattern matchin in lets is not broken *) - 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 p Δ ϕ E A)) - (* A *) - else - ⋁ (in_map Δ (@a_rule_env p Δ ϕ E A)) ⊻ @a_rule_form p Δ ϕ E A. -Next Obligation. intros. subst Δ ϕ. eapply env_order_lt_le_trans; [exact H|]. -order_tac. do 2 apply env_order_eq_add. apply simp_env_order. Qed. -Next Obligation. intros. subst Δ ϕ. eapply env_order_lt_le_trans; [exact H|]. -order_tac. do 2 apply env_order_eq_add. apply simp_env_order. Qed. - -Definition E Δ := EA true (Δ, ⊥). -Definition A := EA false. - -Lemma EA_eq Δ ϕ: let Δ' := simp_env Δ in - (E Δ = ⋀ (in_map Δ' (@e_rule p Δ' ϕ (λ pe _, E pe.1) (λ pe _, A pe)))) /\ - (A (Δ, ϕ) = (⋁ (in_map Δ' (@a_rule_env p Δ' ϕ (λ pe _, E pe.1) (λ pe _, A pe)))) ⊻ - @a_rule_form p Δ' ϕ (λ pe _, E pe.1) (λ pe _, A pe)). -Proof. -simpl. unfold E, A, EA. simpl. -unfold EA_func at 1. -rewrite -> Wf.Fix_eq; simpl. -- split; trivial. - unfold EA_func at 1. rewrite -> Wf.Fix_eq; simpl; trivial. - intros [[|] Δ'] f g Heq; simpl; f_equal. - + apply in_map_ext. intros. trivial. 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. -- intros [[|] Δ'] f g Heq; simpl; f_equal. - + apply in_map_ext. intros. trivial. 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. -Qed. - -Definition Ef (ψ : form) := E [ψ]. -Definition Af (ψ : form) := A ([], ψ). - -End UniformInterpolation. - -Section Equivalence. - -Definition equiv_form φ ψ : Type := (φ ≼ ψ) * (ψ ≼ φ). - -Definition equiv_env Δ Γ: Set := (list_to_set_disj Δ ⊢ ⋀ Γ) * (list_to_set_disj Γ ⊢ ⋀ Δ). - -Lemma symmetric_equiv_env Δ Γ: equiv_env Δ Γ -> equiv_env Γ Δ . -Proof. intros [H1 H2]. split; trivial. Qed. - -Lemma equiv_env_L1 Γ Δ Δ' φ: (equiv_env Δ Δ') -> - Γ ⊎ list_to_set_disj Δ ⊢ φ -> Γ ⊎ list_to_set_disj Δ' ⊢ φ. -Proof. -intros [H1 H2]. -Admitted. - -Lemma equiv_env_L2 Γ Δ Δ' φ: (equiv_env Δ Δ') -> - list_to_set_disj Δ ⊎ Γ ⊢ φ -> list_to_set_disj Δ' ⊎ Γ ⊢ φ. -Proof. -Admitted. - -End Equivalence. - -Infix "≡f" := equiv_form (at level 120). - -Global Infix "≡e" := equiv_env (at level 120). -(* -Section Soundness. - -Variable p : variable. - -Proposition entail_correct_equiv_env Δ Δ' ϕ : (Δ ≡e Δ') -> - (list_to_set_disj Δ ⊢ PropQuantifiers.E p Δ') * - (list_to_set_disj Δ • PropQuantifiers.A p (Δ', ϕ) ⊢ ϕ). -Proof. -intro Heq. split. -- peapply (equiv_env_L1 gmultiset_empty Δ' Δ); eauto. now apply symmetric_equiv_env. - peapply (entail_correct p Δ' ϕ).1 . -- peapply (equiv_env_L2 {[PropQuantifiers.A p (Δ', ϕ)]} Δ' Δ); eauto. now apply symmetric_equiv_env. - peapply (entail_correct p Δ' ϕ).2. -Qed. - -Lemma pq_correct_equiv_env Γ Δ ϕ Δ': - (∀ φ0, φ0 ∈ Γ -> ¬ occurs_in p φ0) -> - (Γ ⊎ list_to_set_disj Δ ⊢ ϕ) -> - (Δ ≡e Δ') -> - (¬ occurs_in p ϕ -> Γ• PropQuantifiers.E p Δ' ⊢ ϕ) * - (Γ• PropQuantifiers.E p Δ' ⊢ PropQuantifiers.A p (Δ', ϕ)). -Proof. -intros Hocc Hp Heq. split. -- intro Hocc'. apply pq_correct; trivial. eapply equiv_env_L1; eauto. -- apply pq_correct; trivial. eapply equiv_env_L1; eauto. -Qed. - - - -End Soundness. -*) \ No newline at end of file diff --git a/theories/iSL/Order.v b/theories/iSL/Order.v index acbf8cb..c52accc 100644 --- a/theories/iSL/Order.v +++ b/theories/iSL/Order.v @@ -36,6 +36,14 @@ Definition env_order_refl Δ Δ' := (env_weight Δ) ≤(env_weight Δ'). 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. intros Γ Δ Heq. unfold env_weight. now rewrite Heq. @@ -396,12 +404,22 @@ Hint Extern 5 (?a ≺· ?b) => order_tac : proof. Lemma pointed_env_order_bot_R pe Δ φ: (pe ≺· (Δ, ⊥)) -> pe ≺· (Δ, φ). Proof. -Admitted. +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. -Admitted. +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 b03fe6c..b86549d 100644 --- a/theories/iSL/PropQuantifiers.v +++ b/theories/iSL/PropQuantifiers.v @@ -74,6 +74,7 @@ match θ with | (□δ1 → δ2) => (□(E((□⁻¹ Δ') • δ2 • □δ1) _ ⇢ A((□⁻¹ Δ') • δ2 • □δ1, δ1) _)) ⇢ E(Δ' • δ2) _ end. + (** The implementation of the rules for defining A is separated into two pieces. 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. *) @@ -448,7 +449,7 @@ split. { (* E *) apply conjunction_R1. intros φ Hin. apply in_in_map in Hin. destruct Hin as (ψ&Hin&Heq). subst φ. -apply (equiv_env_L0 Δ'); [subst Δ'; apply simp_env_equiv_env|]. +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). @@ -479,10 +480,9 @@ destruct ψ; unfold e_rule; exhibit Hi 0; rewrite (proper_Provable _ _ (equiv_di ++ do 2 l_tac. apply HA. order_tac. -- exch 0. l_tac. apply weakening, HE. order_tac. - apply BoxR. apply weakening. box_tac. l_tac. apply HE. order_tac. - } (* A *) -apply (equiv_env_L2 _ Δ'); [subst Δ'; apply simp_env_equiv_env|]. +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. @@ -598,6 +598,7 @@ assert(Ho' : pointed_env_order_refl (elements Γ ++ simp_env Δ, ϕ) (elements 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. +(simp_env_equiv_env Δ).1 Hp assert(Hp' := equiv_env_L1 Γ _ _ _ (symmetric_equiv_env _ _ (simp_env_equiv_env Δ)) Hp). remember (simp_env Δ) as Δ'. clear Hp. rename Hp' into Hp. @@ -792,7 +793,8 @@ end; simpl. 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. @@ -829,7 +831,8 @@ end; simpl. 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. @@ -918,7 +921,7 @@ end; simpl. 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. @@ -934,7 +937,7 @@ end; simpl. 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. diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index 27f6434..0ad4293 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -527,7 +527,7 @@ match goal with end. Qed. -Require Import ISL.InvPropQuantifiers. +Require Import ISL.PropQuantifiers ISL.Simp_env. Definition E_simplified (p: variable) (ψ: form) := simp_form (E p [ψ]). Definition A_simplified (p: variable) (ψ: form) := simp_form (Af p (ψ)). diff --git a/theories/iSL/Simp_env.v b/theories/iSL/Simp_env.v index b69628c..beb196e 100644 --- a/theories/iSL/Simp_env.v +++ b/theories/iSL/Simp_env.v @@ -2,6 +2,7 @@ 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. @@ -125,8 +126,8 @@ Lemma simp_env_eq (Δ : list form): simp_env Δ = applicable_ImpLAnd Δ ? λ δ₁ δ₂ δ₃ _, simp_env ((rm ((δ₁ ∧ δ₂)→ δ₃) Δ • (δ₁ → (δ₂ → δ₃)))) :3 applicable_ImpLOr Δ ? λ δ₁ δ₂ δ₃ _, simp_env (rm ((δ₁ ∨ δ₂)→ δ₃) Δ • (δ₁ → δ₃) • (δ₂ → δ₃)) :3 (* remove redundant assumptions *) - applicable_strong_weakening Δ ? λ φ _, simp_env (rm φ Δ) :1 - Δ. + (applicable_strong_weakening Δ ? λ φ _, simp_env (rm φ Δ) :1 + Δ). Proof. simpl. unfold simp_env. simpl. repeat rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl. split; trivial. @@ -134,6 +135,7 @@ 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 *) @@ -145,6 +147,20 @@ 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. @@ -152,24 +168,27 @@ rewrite simp_env_eq. case (Δ ⊢? ⊥). { intros [Hf _]. destruct Δ as [|φ Δ]. + now apply empty_entails_not_bot in Hf. - + rewrite env_weight_add. - unfold env_order_refl. destruct φ. - * admit. - * destruct Δ as [|φ Δ]. - -- now right. - -- left. unfold env_order, ltof, env_weight. simpl. pose (Order.pow5_gt_0 (weight φ)). lia. - * left. unfold env_order, ltof, env_weight. simpl. - replace 5 with (5 ^ 1) at 1 by trivial. lia. - apply Nat.lt_le_trans with (5 ^ weight φ); [|lia]. - apply Nat.pow_lt_mono_r. lia. destruct φ. simpl. lia. - nia. - pose (Order.pow5_gt_0 (weight φ)). lia. - intro. simpl. auto with proof. - -Admitted. + + 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. @@ -187,57 +206,208 @@ Section Equivalence. Definition equiv_form φ ψ : Type := (φ ≼ ψ) * (ψ ≼ φ). -Definition equiv_env Δ Γ: Set := (list_to_set_disj Δ ⊢ ⋀ Γ) * (list_to_set_disj Γ ⊢ ⋀ Δ). + +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 [H1 H2]. -Admitted. +intros [Hp _] H. peapply (Hp ∅). peapply H. +Qed. +*) +Lemma equiv_env_refl Δ : equiv_env Δ Δ. +Proof. split; trivial. Qed. -Lemma equiv_env_L1 Γ Δ Δ' φ: (equiv_env Δ Δ') -> - Γ ⊎ list_to_set_disj Δ ⊢ φ -> Γ ⊎ list_to_set_disj Δ' ⊢ φ. +Lemma equiv_env_trans Δ Δ' Δ'' : equiv_env Δ Δ' -> equiv_env Δ' Δ'' -> equiv_env Δ Δ''. Proof. -intros [H1 H2]. -Admitted. +intros [H11 H12] [H21 H22]. split; intros; auto. +Qed. + +(* TODO: move *) +Hint Resolve elem_of_list_to_set_disj : proof. -Lemma equiv_env_L2 Γ Δ Δ' φ: (equiv_env Δ Δ') -> - list_to_set_disj Δ ⊎ Γ ⊢ φ -> list_to_set_disj Δ' ⊎ Γ ⊢ φ. + +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. -Admitted. +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. -Admitted. +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 simp_env_L1 Γ Δ φ: - Γ ⊎ list_to_set_disj (simp_env Δ) ⊢ φ -> Γ ⊎ list_to_set_disj Δ ⊢ φ. +Lemma equiv_env_L1 Γ Δ Δ' φ: (equiv_env Δ Δ') -> + Γ ⊎ list_to_set_disj Δ ⊢ φ -> Γ ⊎ list_to_set_disj Δ' ⊢ φ. Proof. -apply equiv_env_L1, simp_env_equiv_env. +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. +(* 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. -intros [θ [Hin Hocc]]. -Admitted. +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. -Admitted. \ No newline at end of file +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.