From a3dccb8b00a616d0b1d8e504748b12e55e992d6b Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Thu, 6 Jun 2024 11:39:00 +0200 Subject: [PATCH 01/29] Basic conj and disj simplifications --- theories/iSL/Simp.v | 130 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 130 insertions(+) create mode 100644 theories/iSL/Simp.v diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v new file mode 100644 index 0000000..2b78cb8 --- /dev/null +++ b/theories/iSL/Simp.v @@ -0,0 +1,130 @@ +Require Import ISL.SequentProps. +Require Import ISL.Sequents. +Require Import ISL.Environments. + + +Fixpoint simp φ := match φ with +| φ ∧ ψ => if decide (φ = ⊥) + then ⊥ + else + if decide (ψ = ⊥) + then ⊥ + else (simp φ) ∧ (simp ψ) +| φ ∨ ψ => if decide (φ = ⊥) + then ψ + else + if decide (ψ = ⊥) + then φ + else (simp φ) ∨ (simp ψ) +| _ => φ +end. + +Lemma simpl_equiv_and_L Γ φ ψ : + Γ • φ ⊢ simp φ -> + Γ • ψ ⊢ simp ψ -> + Γ • (φ ∧ ψ) ⊢ simp (φ ∧ ψ). +Proof. + intros IHφ IHψ. + simpl. + apply AndL. + destruct decide. + - rewrite e. + exch 0. apply ExFalso. + - destruct decide. + -- rewrite e. + apply ExFalso. + -- apply AndR. + --- apply weakening. + apply IHφ. + --- exch 0. apply weakening. + apply IHψ. +Qed. + +Lemma simpl_equiv_or_L Γ φ ψ : + Γ • φ ⊢ simp φ -> + Γ • ψ ⊢ simp ψ -> + Γ • (φ ∨ ψ) ⊢ simp (φ ∨ ψ). +Proof. + intros IHφ IHψ. + simpl. + destruct decide. + apply OrL. + - rewrite e. apply ExFalso. + - apply generalised_axiom. + - destruct decide. + -- apply OrL. + --- apply generalised_axiom. + --- rewrite e. + apply ExFalso. + -- apply OrL. + --- apply OrR1. + apply IHφ. + --- apply OrR2. + apply IHψ. +Qed. + + +Theorem simp_equiv_L Γ φ : Γ • φ ⊢ simp φ. +Proof. + induction φ. +- apply generalised_axiom. +- apply generalised_axiom. +- apply (simpl_equiv_and_L Γ φ1 φ2 IHφ1 IHφ2). +- apply (simpl_equiv_or_L Γ φ1 φ2 IHφ1 IHφ2). +- apply generalised_axiom. +- apply generalised_axiom. +Qed. + + +Lemma simpl_equiv_and_R Γ φ ψ : + Γ • (simp φ) ⊢ φ -> + Γ • (simp ψ) ⊢ ψ -> + Γ • (simp (φ ∧ ψ)) ⊢ φ ∧ ψ. +Proof. + intros IHφ IHψ. + simpl. + destruct decide. + - apply ExFalso. + - destruct decide. + -- apply ExFalso. + -- apply AndL. + apply AndR. + --- apply weakening. + apply IHφ. + --- exch 0. apply weakening. + apply IHψ. +Qed. + + +Lemma simpl_equiv_or_R Γ φ ψ : + Γ • (simp φ) ⊢ φ -> + Γ • (simp ψ) ⊢ ψ -> + Γ • (simp (φ ∨ ψ)) ⊢ φ ∨ ψ. +Proof. + intros IHφ IHψ. + simpl. + destruct decide. + - apply OrR2. + apply generalised_axiom. + - destruct decide. + -- apply OrR1. + apply generalised_axiom. + -- apply OrL. + --- apply OrR1. + apply IHφ. + --- apply OrR2. + apply IHψ. +Qed. + + +Theorem simp_equiv_R Γ φ : Γ • (simp φ) ⊢ φ. +Proof. + induction φ. +- apply generalised_axiom. +- apply generalised_axiom. +- apply (simpl_equiv_and_R Γ φ1 φ2 IHφ1 IHφ2). +- apply (simpl_equiv_or_R Γ φ1 φ2 IHφ1 IHφ2). +- apply generalised_axiom. +- apply generalised_axiom. +Qed. + From bc9424c0820a31ea72e72d2e9e428d5b4f22a612 Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Thu, 6 Jun 2024 16:45:27 +0200 Subject: [PATCH 02/29] Induction over weight for the conj and disj lemmas --- theories/iSL/Simp.v | 109 +++++++++++++++++++------------------------- 1 file changed, 48 insertions(+), 61 deletions(-) diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index 2b78cb8..4a4a7ea 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -4,79 +4,66 @@ Require Import ISL.Environments. Fixpoint simp φ := match φ with -| φ ∧ ψ => if decide (φ = ⊥) - then ⊥ - else - if decide (ψ = ⊥) - then ⊥ - else (simp φ) ∧ (simp ψ) -| φ ∨ ψ => if decide (φ = ⊥) - then ψ - else - if decide (ψ = ⊥) - then φ - else (simp φ) ∨ (simp ψ) +(* +| φ1 ∧ (φ2 ∧ φ3) => if decide (φ1 = φ2) + then (simp φ1) ∧ (simp φ3) + else (simp φ1) ∧ (simp φ2) ∧ (simp φ3) +*) +| ⊥ ∧ _ | _ ∧ ⊥ => ⊥ +| φ ∧ ψ => (simp φ) ∧ (simp ψ) +| ⊥ ∨ ψ => simp ψ +| φ ∨ ⊥ => simp φ +| φ ∨ ψ => (simp φ) ∨ (simp ψ) | _ => φ end. -Lemma simpl_equiv_and_L Γ φ ψ : - Γ • φ ⊢ simp φ -> - Γ • ψ ⊢ simp ψ -> + +Lemma simp_equiv_and_L Γ φ ψ : + (forall f, weight f < weight (φ ∧ ψ) -> Γ • f ⊢ simp f) -> Γ • (φ ∧ ψ) ⊢ simp (φ ∧ ψ). Proof. - intros IHφ IHψ. - simpl. - apply AndL. - destruct decide. - - rewrite e. - exch 0. apply ExFalso. - - destruct decide. - -- rewrite e. - apply ExFalso. - -- apply AndR. - --- apply weakening. - apply IHφ. - --- exch 0. apply weakening. - apply IHψ. +intros IH. + +remember (weight φ) as wφ. +assert (Hφ : Γ • φ ⊢ simp φ) by (apply (IH φ); simpl; lia). + +remember (weight ψ) as wψ. +assert (Hψ : Γ • ψ ⊢ simp ψ) by (apply (IH ψ); simpl; lia). + +destruct φ; destruct ψ; simpl; apply AndL; auto 2 with proof; apply AndR; +simpl; auto 2 with proof; exch 0; apply weakening; try apply Hψ. Qed. -Lemma simpl_equiv_or_L Γ φ ψ : - Γ • φ ⊢ simp φ -> - Γ • ψ ⊢ simp ψ -> +Lemma simp_equiv_or_L Γ φ ψ : + (forall f, weight f < weight (φ ∨ ψ) -> Γ • f ⊢ simp f) -> Γ • (φ ∨ ψ) ⊢ simp (φ ∨ ψ). Proof. - intros IHφ IHψ. - simpl. - destruct decide. - apply OrL. - - rewrite e. apply ExFalso. - - apply generalised_axiom. - - destruct decide. - -- apply OrL. - --- apply generalised_axiom. - --- rewrite e. - apply ExFalso. - -- apply OrL. - --- apply OrR1. - apply IHφ. - --- apply OrR2. - apply IHψ. +intros IH. + +remember (weight φ) as wφ. +assert (Hφ : Γ • φ ⊢ simp φ) by (apply (IH φ); simpl; lia). + +remember (weight ψ) as wψ. +assert (Hψ : Γ • ψ ⊢ simp ψ) by (apply (IH ψ); simpl; lia). + +destruct φ; auto 2 with proof; destruct ψ; auto 2 with proof; +simpl; apply OrL; auto 2 with proof. Qed. Theorem simp_equiv_L Γ φ : Γ • φ ⊢ simp φ. Proof. - induction φ. -- apply generalised_axiom. -- apply generalised_axiom. -- apply (simpl_equiv_and_L Γ φ1 φ2 IHφ1 IHφ2). -- apply (simpl_equiv_or_L Γ φ1 φ2 IHφ1 IHφ2). -- apply generalised_axiom. -- apply generalised_axiom. +remember (weight φ) as w. +assert(Hle : weight φ ≤ w) by lia. +clear Heqw. revert φ Hle. +induction w; intros φ Hle; [destruct φ ; simpl in Hle; lia|]. +destruct φ; try apply generalised_axiom; +[eapply (simp_equiv_and_L Γ φ1 φ2)| eapply (simp_equiv_or_L Γ φ1 φ2)]; +intros f H; apply IHw; lia. Qed. - -Lemma simpl_equiv_and_R Γ φ ψ : +(* TODO +Lemma simp_equiv_and_R Γ φ ψ : Γ • (simp φ) ⊢ φ -> Γ • (simp ψ) ⊢ ψ -> Γ • (simp (φ ∧ ψ)) ⊢ φ ∧ ψ. @@ -96,7 +83,7 @@ Proof. Qed. -Lemma simpl_equiv_or_R Γ φ ψ : +Lemma simp_equiv_or_R Γ φ ψ : Γ • (simp φ) ⊢ φ -> Γ • (simp ψ) ⊢ ψ -> Γ • (simp (φ ∨ ψ)) ⊢ φ ∨ ψ. @@ -122,9 +109,9 @@ Proof. induction φ. - apply generalised_axiom. - apply generalised_axiom. -- apply (simpl_equiv_and_R Γ φ1 φ2 IHφ1 IHφ2). -- apply (simpl_equiv_or_R Γ φ1 φ2 IHφ1 IHφ2). +- apply (simp_equiv_and_R Γ φ1 φ2 IHφ1 IHφ2). +- apply (simp_equiv_or_R Γ φ1 φ2 IHφ1 IHφ2). - apply generalised_axiom. - apply generalised_axiom. Qed. - + *) From a6f455c1810cb323681fda5afab7a0b0a5d4785e Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Wed, 12 Jun 2024 18:13:11 +0200 Subject: [PATCH 03/29] define `simp_or` to recursively simplify formulas with or --- theories/iSL/Simp.v | 92 +++++++++++++++++++++++++++++++++++---------- 1 file changed, 73 insertions(+), 19 deletions(-) diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index 4a4a7ea..c5afcfa 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -3,51 +3,104 @@ Require Import ISL.Sequents. Require Import ISL.Environments. +Definition simp_or φ ψ := match φ,ψ with +| ⊥ , ψ => ψ +| φ , ψ => φ ∨ ψ +end. + + +Definition simp_and φ ψ := match φ,ψ with +| ⊥ , _ => ⊥ +| φ , ψ => φ ∧ ψ +end. + Fixpoint simp φ := match φ with (* | φ1 ∧ (φ2 ∧ φ3) => if decide (φ1 = φ2) - then (simp φ1) ∧ (simp φ3) +then (simp φ1) ∧ (simp φ3) else (simp φ1) ∧ (simp φ2) ∧ (simp φ3) *) -| ⊥ ∧ _ | _ ∧ ⊥ => ⊥ -| φ ∧ ψ => (simp φ) ∧ (simp ψ) -| ⊥ ∨ ψ => simp ψ -| φ ∨ ⊥ => simp φ -| φ ∨ ψ => (simp φ) ∨ (simp ψ) +| φ ∨ ψ => simp_or (simp φ) (simp ψ) +| ⊥ ∧ _ | _ ∧ ⊥ => ⊥ +| φ ∧ ψ => (simp φ) ∧ (simp ψ) | _ => φ end. -Lemma simp_equiv_and_L Γ φ ψ : - (forall f, weight f < weight (φ ∧ ψ) -> Γ • f ⊢ simp f) -> - Γ • (φ ∧ ψ) ⊢ simp (φ ∧ ψ). -Proof. -intros IH. -remember (weight φ) as wφ. -assert (Hφ : Γ • φ ⊢ simp φ) by (apply (IH φ); simpl; lia). -remember (weight ψ) as wψ. -assert (Hψ : Γ • ψ ⊢ simp ψ) by (apply (IH ψ); simpl; lia). +Lemma simp_shrink φ : + weight (simp φ) <= weight φ. +Proof. +Admitted. -destruct φ; destruct ψ; simpl; apply AndL; auto 2 with proof; apply AndR; -simpl; auto 2 with proof; exch 0; apply weakening; try apply Hψ. + +Lemma leq_to_le a b : + a < b -> + a <= b. +Proof. + lia. Qed. + + Lemma simp_or_no_bot φ ψ : + φ ≠ ⊥ -> simp_or φ ψ = (φ ∨ ψ). + Admitted. + + + Lemma simp_and_no_bot φ ψ : + φ ≠ ⊥ -> simp_or φ ψ = (φ ∧ ψ). + Admitted. + Lemma simp_equiv_or_L Γ φ ψ : (forall f, weight f < weight (φ ∨ ψ) -> Γ • f ⊢ simp f) -> Γ • (φ ∨ ψ) ⊢ simp (φ ∨ ψ). Proof. intros IH. +assert (Hφ : Γ • φ ⊢ simp φ ) by (apply (IH φ); simpl; lia). +assert (Hψ : Γ • ψ ⊢ simp ψ ) by (apply (IH ψ); simpl; lia). + +destruct φ. +- simpl. auto 3 with proof. +- simpl. auto 2 with proof. +- assert (H: (Γ • φ1 ∧ φ2 ∨ ψ) ⊢ simp_or (simp (φ1 ∧ φ2)) (simp ψ)). + destruct (decide (simp (φ1 ∧ φ2) = ⊥)). + + rewrite e. simpl. apply OrL. + * rewrite e in Hφ. apply exfalso. trivial. + * apply Hψ. + + rewrite simp_or_no_bot. + * auto with proof. + * apply n. + + apply H. +- assert (H: (Γ • (φ1 ∨ φ2) ∨ ψ) ⊢ simp_or (simp (φ1 ∨ φ2)) (simp ψ)). + destruct (decide (simp (φ1 ∨ φ2) = ⊥)). + + rewrite e. simpl. apply OrL. + * rewrite e in Hφ. apply exfalso. trivial. + * apply Hψ. + + rewrite simp_or_no_bot. + * auto with proof. + * apply n. + + apply H. +- simpl. auto 3 with proof. +- simpl. auto 3 with proof. +Qed. + + +Lemma simp_equiv_and_L Γ φ ψ : + (forall f, weight f < weight (φ ∧ ψ) -> Γ • f ⊢ simp f) -> + Γ • (φ ∧ ψ) ⊢ simp (φ ∧ ψ). +Proof. +intros IH. + remember (weight φ) as wφ. assert (Hφ : Γ • φ ⊢ simp φ) by (apply (IH φ); simpl; lia). remember (weight ψ) as wψ. assert (Hψ : Γ • ψ ⊢ simp ψ) by (apply (IH ψ); simpl; lia). -destruct φ; auto 2 with proof; destruct ψ; auto 2 with proof; -simpl; apply OrL; auto 2 with proof. +destruct φ; destruct ψ; simpl; apply AndL; auto 2 with proof; apply AndR; +simpl; auto 2 with proof; exch 0; apply weakening; try apply Hψ. Qed. @@ -115,3 +168,4 @@ Proof. - apply generalised_axiom. Qed. *) + From adce1d4bdf84fc43862d5a0b32e4c77c27e45157 Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Thu, 13 Jun 2024 09:26:18 +0200 Subject: [PATCH 04/29] Prove recursive and simplification --- theories/iSL/Simp.v | 85 +++++++++++++++++++++++++++++++-------------- 1 file changed, 58 insertions(+), 27 deletions(-) diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index c5afcfa..789e762 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -21,36 +21,28 @@ then (simp φ1) ∧ (simp φ3) else (simp φ1) ∧ (simp φ2) ∧ (simp φ3) *) | φ ∨ ψ => simp_or (simp φ) (simp ψ) -| ⊥ ∧ _ | _ ∧ ⊥ => ⊥ -| φ ∧ ψ => (simp φ) ∧ (simp ψ) +| φ ∧ ψ => simp_and (simp φ) (simp ψ) | _ => φ end. - - - -Lemma simp_shrink φ : - weight (simp φ) <= weight φ. -Proof. -Admitted. - - -Lemma leq_to_le a b : - a < b -> - a <= b. -Proof. - lia. -Qed. - - Lemma simp_or_no_bot φ ψ : φ ≠ ⊥ -> simp_or φ ψ = (φ ∨ ψ). - Admitted. +Proof. + intro H. + unfold simp_or. + destruct φ; trivial. + contradict H. reflexivity. +Qed. Lemma simp_and_no_bot φ ψ : - φ ≠ ⊥ -> simp_or φ ψ = (φ ∧ ψ). - Admitted. + φ ≠ ⊥ -> simp_and φ ψ = (φ ∧ ψ). +Proof. + intro H. + unfold simp_and. + destruct φ; trivial. + contradict H. reflexivity. +Qed. Lemma simp_equiv_or_L Γ φ ψ : (forall f, weight f < weight (φ ∨ ψ) -> Γ • f ⊢ simp f) -> @@ -93,14 +85,52 @@ Lemma simp_equiv_and_L Γ φ ψ : Proof. intros IH. -remember (weight φ) as wφ. assert (Hφ : Γ • φ ⊢ simp φ) by (apply (IH φ); simpl; lia). - -remember (weight ψ) as wψ. assert (Hψ : Γ • ψ ⊢ simp ψ) by (apply (IH ψ); simpl; lia). -destruct φ; destruct ψ; simpl; apply AndL; auto 2 with proof; apply AndR; -simpl; auto 2 with proof; exch 0; apply weakening; try apply Hψ. +destruct φ. +- simpl. + apply AndL. + apply AndR. + + exch 0; apply Atom. + + exch 0. apply weakening. apply Hψ. +- simpl. + apply AndL. exch 0. + apply ExFalso. +- assert (H: (Γ • (φ1 ∧ φ2) ∧ ψ) ⊢ simp_and (simp (φ1 ∧ φ2)) (simp ψ)). + destruct (decide (simp (φ1 ∧ φ2) = ⊥)). + + rewrite e. simpl. apply AndL. rewrite e in Hφ. apply weakening. apply exfalso. trivial. + + rewrite simp_and_no_bot. + * apply AndL. + apply AndR. + -- apply weakening. + apply Hφ. + -- exch 0. apply weakening. + apply Hψ. + * apply n. + + apply H. +- assert (H: (Γ • (φ1 ∨ φ2) ∧ ψ) ⊢ simp_and (simp (φ1 ∨ φ2)) (simp ψ)). + destruct (decide (simp (φ1 ∨ φ2) = ⊥)). + + rewrite e. simpl. apply AndL. rewrite e in Hφ. apply weakening. apply exfalso. trivial. + + rewrite simp_and_no_bot. + * apply AndL. + apply AndR. + -- apply weakening. + apply Hφ. + -- exch 0. apply weakening. + apply Hψ. + * apply n. + + apply H. +- simpl. + apply AndL. + apply AndR. + + apply weakening; apply generalised_axiom. + + exch 0. apply weakening. apply Hψ. +- simpl. + apply AndL. + apply AndR. + + apply weakening; apply generalised_axiom. + + exch 0. apply weakening. apply Hψ. Qed. @@ -169,3 +199,4 @@ Proof. Qed. *) + From 622794926f6e60892166bc8f869f69d63797fe98 Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Thu, 13 Jun 2024 14:32:41 +0200 Subject: [PATCH 05/29] Rewrite simp_or and simp_and using if-then-else --- theories/iSL/Simp.v | 206 +++++++++++--------------------------------- 1 file changed, 48 insertions(+), 158 deletions(-) diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index 789e762..01e55b2 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -3,79 +3,50 @@ Require Import ISL.Sequents. Require Import ISL.Environments. -Definition simp_or φ ψ := match φ,ψ with -| ⊥ , ψ => ψ -| φ , ψ => φ ∨ ψ -end. +Definition simp_or φ ψ := + if decide (φ =⊥) then ψ + else if decide (ψ = ⊥) then φ + else φ ∨ ψ. -Definition simp_and φ ψ := match φ,ψ with -| ⊥ , _ => ⊥ -| φ , ψ => φ ∧ ψ -end. +Definition simp_and φ ψ := + if decide (φ =⊥) then ⊥ + else if decide (ψ = ⊥) then ⊥ + else φ ∨ ψ. Fixpoint simp φ := match φ with -(* -| φ1 ∧ (φ2 ∧ φ3) => if decide (φ1 = φ2) -then (simp φ1) ∧ (simp φ3) - else (simp φ1) ∧ (simp φ2) ∧ (simp φ3) -*) | φ ∨ ψ => simp_or (simp φ) (simp ψ) | φ ∧ ψ => simp_and (simp φ) (simp ψ) | _ => φ end. - Lemma simp_or_no_bot φ ψ : - φ ≠ ⊥ -> simp_or φ ψ = (φ ∨ ψ). -Proof. - intro H. - unfold simp_or. - destruct φ; trivial. - contradict H. reflexivity. -Qed. - - - Lemma simp_and_no_bot φ ψ : - φ ≠ ⊥ -> simp_and φ ψ = (φ ∧ ψ). -Proof. - intro H. - unfold simp_and. - destruct φ; trivial. - contradict H. reflexivity. -Qed. - Lemma simp_equiv_or_L Γ φ ψ : (forall f, weight f < weight (φ ∨ ψ) -> Γ • f ⊢ simp f) -> Γ • (φ ∨ ψ) ⊢ simp (φ ∨ ψ). Proof. intros IH. - assert (Hφ : Γ • φ ⊢ simp φ ) by (apply (IH φ); simpl; lia). assert (Hψ : Γ • ψ ⊢ simp ψ ) by (apply (IH ψ); simpl; lia). - -destruct φ. -- simpl. auto 3 with proof. -- simpl. auto 2 with proof. -- assert (H: (Γ • φ1 ∧ φ2 ∨ ψ) ⊢ simp_or (simp (φ1 ∧ φ2)) (simp ψ)). - destruct (decide (simp (φ1 ∧ φ2) = ⊥)). - + rewrite e. simpl. apply OrL. - * rewrite e in Hφ. apply exfalso. trivial. - * apply Hψ. - + rewrite simp_or_no_bot. - * auto with proof. - * apply n. - + apply H. -- assert (H: (Γ • (φ1 ∨ φ2) ∨ ψ) ⊢ simp_or (simp (φ1 ∨ φ2)) (simp ψ)). - destruct (decide (simp (φ1 ∨ φ2) = ⊥)). - + rewrite e. simpl. apply OrL. - * rewrite e in Hφ. apply exfalso. trivial. - * apply Hψ. - + rewrite simp_or_no_bot. - * auto with proof. - * apply n. - + apply H. -- simpl. auto 3 with proof. -- simpl. auto 3 with proof. +simpl. unfold simp_or. +case decide. +- intro Hbot. + apply OrL. + + rewrite Hbot in Hφ. + apply exfalso. trivial. + + apply Hψ. +- intro. + case decide. + + intro Hbot. + apply OrL. + * apply Hφ. + * rewrite Hbot in Hψ. + apply exfalso. trivial. + + intro. + apply OrL. + * apply OrR1. + apply Hφ. + * apply OrR2. + apply Hψ. Qed. @@ -84,53 +55,25 @@ Lemma simp_equiv_and_L Γ φ ψ : Γ • (φ ∧ ψ) ⊢ simp (φ ∧ ψ). Proof. intros IH. - -assert (Hφ : Γ • φ ⊢ simp φ) by (apply (IH φ); simpl; lia). -assert (Hψ : Γ • ψ ⊢ simp ψ) by (apply (IH ψ); simpl; lia). - -destruct φ. -- simpl. - apply AndL. - apply AndR. - + exch 0; apply Atom. - + exch 0. apply weakening. apply Hψ. -- simpl. - apply AndL. exch 0. - apply ExFalso. -- assert (H: (Γ • (φ1 ∧ φ2) ∧ ψ) ⊢ simp_and (simp (φ1 ∧ φ2)) (simp ψ)). - destruct (decide (simp (φ1 ∧ φ2) = ⊥)). - + rewrite e. simpl. apply AndL. rewrite e in Hφ. apply weakening. apply exfalso. trivial. - + rewrite simp_and_no_bot. - * apply AndL. - apply AndR. - -- apply weakening. - apply Hφ. - -- exch 0. apply weakening. - apply Hψ. - * apply n. - + apply H. -- assert (H: (Γ • (φ1 ∨ φ2) ∧ ψ) ⊢ simp_and (simp (φ1 ∨ φ2)) (simp ψ)). - destruct (decide (simp (φ1 ∨ φ2) = ⊥)). - + rewrite e. simpl. apply AndL. rewrite e in Hφ. apply weakening. apply exfalso. trivial. - + rewrite simp_and_no_bot. - * apply AndL. - apply AndR. - -- apply weakening. - apply Hφ. - -- exch 0. apply weakening. - apply Hψ. - * apply n. - + apply H. -- simpl. - apply AndL. - apply AndR. - + apply weakening; apply generalised_axiom. - + exch 0. apply weakening. apply Hψ. -- simpl. - apply AndL. - apply AndR. - + apply weakening; apply generalised_axiom. - + exch 0. apply weakening. apply Hψ. +assert (Hφ : Γ • φ ⊢ simp φ ) by (apply (IH φ); simpl; lia). +assert (Hψ : Γ • ψ ⊢ simp ψ ) by (apply (IH ψ); simpl; lia). +simpl. unfold simp_and. +case decide. +- intro Hbot. + rewrite Hbot in Hφ. + apply AndL. apply weakening. + apply exfalso. trivial. +- intro. + case decide. + + intro Hbot. + rewrite Hbot in Hψ. + apply AndL. exch 0. apply weakening. + apply exfalso. trivial. + + intro. + apply OrR1. + apply AndL. + apply weakening. + apply Hφ. Qed. @@ -145,58 +88,5 @@ destruct φ; try apply generalised_axiom; intros f H; apply IHw; lia. Qed. -(* TODO -Lemma simp_equiv_and_R Γ φ ψ : - Γ • (simp φ) ⊢ φ -> - Γ • (simp ψ) ⊢ ψ -> - Γ • (simp (φ ∧ ψ)) ⊢ φ ∧ ψ. -Proof. - intros IHφ IHψ. - simpl. - destruct decide. - - apply ExFalso. - - destruct decide. - -- apply ExFalso. - -- apply AndL. - apply AndR. - --- apply weakening. - apply IHφ. - --- exch 0. apply weakening. - apply IHψ. -Qed. - - -Lemma simp_equiv_or_R Γ φ ψ : - Γ • (simp φ) ⊢ φ -> - Γ • (simp ψ) ⊢ ψ -> - Γ • (simp (φ ∨ ψ)) ⊢ φ ∨ ψ. -Proof. - intros IHφ IHψ. - simpl. - destruct decide. - - apply OrR2. - apply generalised_axiom. - - destruct decide. - -- apply OrR1. - apply generalised_axiom. - -- apply OrL. - --- apply OrR1. - apply IHφ. - --- apply OrR2. - apply IHψ. -Qed. - - Theorem simp_equiv_R Γ φ : Γ • (simp φ) ⊢ φ. -Proof. - induction φ. -- apply generalised_axiom. -- apply generalised_axiom. -- apply (simp_equiv_and_R Γ φ1 φ2 IHφ1 IHφ2). -- apply (simp_equiv_or_R Γ φ1 φ2 IHφ1 IHφ2). -- apply generalised_axiom. -- apply generalised_axiom. -Qed. - *) - - +Admitted. From cfeb5eb734b5b32a1f7b479b72986def090f7941 Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Thu, 13 Jun 2024 16:50:38 +0200 Subject: [PATCH 06/29] add top simplifications --- theories/iSL/Simp.v | 32 +++++++++++++++++++++++++++----- 1 file changed, 27 insertions(+), 5 deletions(-) diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index 01e55b2..de86c4e 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -6,12 +6,16 @@ Require Import ISL.Environments. Definition simp_or φ ψ := if decide (φ =⊥) then ψ else if decide (ψ = ⊥) then φ + else if decide (φ = ⊤) then ⊤ + else if decide (ψ = ⊤) then ⊤ else φ ∨ ψ. Definition simp_and φ ψ := if decide (φ =⊥) then ⊥ else if decide (ψ = ⊥) then ⊥ + else if decide (φ = ⊤) then ψ + else if decide (ψ = ⊤) then φ else φ ∨ ψ. Fixpoint simp φ := match φ with @@ -20,6 +24,15 @@ Fixpoint simp φ := match φ with | _ => φ end. + +Lemma top_provable Γ φ : + Γ • φ ⊢ ⊤. +Proof. + apply ImpR. + apply ExFalso. +Qed. + + Lemma simp_equiv_or_L Γ φ ψ : (forall f, weight f < weight (φ ∨ ψ) -> Γ • f ⊢ simp f) -> Γ • (φ ∨ ψ) ⊢ simp (φ ∨ ψ). @@ -42,11 +55,19 @@ case decide. * rewrite Hbot in Hψ. apply exfalso. trivial. + intro. - apply OrL. - * apply OrR1. - apply Hφ. - * apply OrR2. - apply Hψ. + case decide. + * intro Htop. + apply top_provable. + * intro. + case decide. + -- intro Htop. + apply top_provable. + -- intro. + apply OrL. + ++ apply OrR1. + apply Hφ. + ++ apply OrR2. + apply Hψ. Qed. @@ -90,3 +111,4 @@ Qed. Theorem simp_equiv_R Γ φ : Γ • (simp φ) ⊢ φ. Admitted. + From 43c25050a8435d5986ad6423a0939d7cbb224958 Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Fri, 14 Jun 2024 09:49:44 +0200 Subject: [PATCH 07/29] Simplify top_provable --- theories/iSL/Simp.v | 24 ++++++++++++++++++------ 1 file changed, 18 insertions(+), 6 deletions(-) diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index de86c4e..0268119 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -25,8 +25,8 @@ Fixpoint simp φ := match φ with end. -Lemma top_provable Γ φ : - Γ • φ ⊢ ⊤. +Lemma top_provable Γ: + Γ ⊢ ⊤. Proof. apply ImpR. apply ExFalso. @@ -91,10 +91,22 @@ case decide. apply AndL. exch 0. apply weakening. apply exfalso. trivial. + intro. - apply OrR1. - apply AndL. - apply weakening. - apply Hφ. + case decide. + * intro. + apply AndL. + exch 0. apply weakening. + apply Hψ. + * intro. + case decide. + -- intro. + apply AndL. + apply weakening. + apply Hφ. + -- intro. + apply OrR1. + apply AndL. + apply weakening. + apply Hφ. Qed. From 2ff8e5e647802a373af23cab193d178b22103296 Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Fri, 14 Jun 2024 09:54:04 +0200 Subject: [PATCH 08/29] Fix simp_and definition --- theories/iSL/Simp.v | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index 0268119..85734ca 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -21,6 +21,7 @@ Definition simp_and φ ψ := Fixpoint simp φ := match φ with | φ ∨ ψ => simp_or (simp φ) (simp ψ) | φ ∧ ψ => simp_and (simp φ) (simp ψ) +| φ → ψ => φ → ψ | _ => φ end. @@ -33,6 +34,13 @@ Proof. Qed. +Lemma self_imp Γ φ : + Γ ⊢ (φ → φ) . +Proof. + apply ImpR. + apply generalised_axiom. +Qed. + Lemma simp_equiv_or_L Γ φ ψ : (forall f, weight f < weight (φ ∨ ψ) -> Γ • f ⊢ simp f) -> Γ • (φ ∨ ψ) ⊢ simp (φ ∨ ψ). From 32280b125f647613e0a4a4efba1cc53e9e6b00dc Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Fri, 14 Jun 2024 10:00:27 +0200 Subject: [PATCH 09/29] Equality simplification on and and or --- theories/iSL/Simp.v | 40 +++++++++++++++++++++------------------- 1 file changed, 21 insertions(+), 19 deletions(-) diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index 85734ca..500cf69 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -8,6 +8,7 @@ Definition simp_or φ ψ := else if decide (ψ = ⊥) then φ else if decide (φ = ⊤) then ⊤ else if decide (ψ = ⊤) then ⊤ + else if decide (φ = ψ) then φ else φ ∨ ψ. @@ -16,16 +17,15 @@ Definition simp_and φ ψ := else if decide (ψ = ⊥) then ⊥ else if decide (φ = ⊤) then ψ else if decide (ψ = ⊤) then φ - else φ ∨ ψ. + else if decide (φ = ψ) then φ + else φ ∧ ψ. Fixpoint simp φ := match φ with | φ ∨ ψ => simp_or (simp φ) (simp ψ) | φ ∧ ψ => simp_and (simp φ) (simp ψ) -| φ → ψ => φ → ψ | _ => φ end. - Lemma top_provable Γ: Γ ⊢ ⊤. Proof. @@ -33,14 +33,6 @@ Proof. apply ExFalso. Qed. - -Lemma self_imp Γ φ : - Γ ⊢ (φ → φ) . -Proof. - apply ImpR. - apply generalised_axiom. -Qed. - Lemma simp_equiv_or_L Γ φ ψ : (forall f, weight f < weight (φ ∨ ψ) -> Γ • f ⊢ simp f) -> Γ • (φ ∨ ψ) ⊢ simp (φ ∨ ψ). @@ -71,11 +63,14 @@ case decide. -- intro Htop. apply top_provable. -- intro. - apply OrL. - ++ apply OrR1. - apply Hφ. - ++ apply OrR2. - apply Hψ. + case decide; [intro Heq | intro ]; apply OrL. + ** apply Hφ. + ** rewrite Heq. + apply Hψ. + ** apply OrR1. + apply Hφ. + ** apply OrR2. + apply Hψ. Qed. @@ -111,10 +106,17 @@ case decide. apply weakening. apply Hφ. -- intro. - apply OrR1. apply AndL. - apply weakening. - apply Hφ. + case decide. + ++ intro. + apply weakening. + apply Hφ. + ++ intro. + apply AndR. + ** apply weakening. + apply Hφ. + ** exch 0. apply weakening. + apply Hψ. Qed. From 912412e068d281548d51b925cb51692f286ba643 Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Fri, 14 Jun 2024 13:29:48 +0200 Subject: [PATCH 10/29] Prove right implication in simplification proofs --- theories/iSL/Simp.v | 118 ++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 115 insertions(+), 3 deletions(-) diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index 500cf69..b89117d 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -1,10 +1,11 @@ Require Import ISL.SequentProps. Require Import ISL.Sequents. Require Import ISL.Environments. +Require Import Coq.Program.Equality. Definition simp_or φ ψ := - if decide (φ =⊥) then ψ + if decide (φ = ⊥) then ψ else if decide (ψ = ⊥) then φ else if decide (φ = ⊤) then ⊤ else if decide (ψ = ⊤) then ⊤ @@ -20,19 +21,32 @@ Definition simp_and φ ψ := else if decide (φ = ψ) then φ else φ ∧ ψ. + +Definition simp_imp φ ψ := + φ → ψ. + Fixpoint simp φ := match φ with | φ ∨ ψ => simp_or (simp φ) (simp ψ) | φ ∧ ψ => simp_and (simp φ) (simp ψ) +| φ → ψ => simp_imp φ ψ | _ => φ end. -Lemma top_provable Γ: + +Lemma top_provable Γ : Γ ⊢ ⊤. Proof. apply ImpR. apply ExFalso. Qed. +Lemma ImpR_idemp Γ φ : + Γ ⊢ (φ → φ). +Proof. + apply ImpR. + apply generalised_axiom. +Qed. + Lemma simp_equiv_or_L Γ φ ψ : (forall f, weight f < weight (φ ∨ ψ) -> Γ • f ⊢ simp f) -> Γ • (φ ∨ ψ) ⊢ simp (φ ∨ ψ). @@ -131,6 +145,104 @@ destruct φ; try apply generalised_axiom; intros f H; apply IHw; lia. Qed. + +Lemma simp_equiv_or_R Γ φ ψ : + (forall f, weight f < weight (φ ∨ ψ) -> Γ • simp f ⊢ f) -> + Γ •simp (φ ∨ ψ) ⊢ (φ ∨ ψ). +Proof. +intros IH. +assert (Hφ : Γ • simp φ ⊢ φ ) by (apply (IH φ); simpl; lia). +assert (Hψ : Γ • simp ψ ⊢ ψ ) by (apply (IH ψ); simpl; lia). +simpl. unfold simp_or. +case decide. +- intro. + apply OrR2. + apply Hψ. +- intro. + case decide. + + intro. + apply OrR1. + apply Hφ. + + intro. + case decide. + * intro Htop. + apply OrR1. + rewrite <- Htop. + apply Hφ. + * intro. + case decide. + -- intro Htop. + apply OrR2. + rewrite <- Htop. + apply Hψ. + -- intro. + case decide. + ++ intro. + apply OrR1. + apply Hφ. + ++ intro. + apply OrL. + ** apply OrR1. + apply Hφ. + ** apply OrR2. + apply Hψ. +Qed. + +Lemma simp_equiv_and_R Γ φ ψ : + (forall f, weight f < weight (φ ∧ ψ) -> Γ • simp f ⊢ f) -> + Γ • simp (φ ∧ ψ) ⊢ φ ∧ ψ. +Proof. +intros IH. +assert (Hφ : Γ • simp φ ⊢ φ ) by (apply (IH φ); simpl; lia). +assert (Hψ : Γ • simp ψ ⊢ ψ ) by (apply (IH ψ); simpl; lia). +simpl. unfold simp_and. +case decide. +- intro. + apply exfalso. apply ExFalso. +- intro. + + case decide. + * intro. + apply exfalso. apply ExFalso. + * intro. + case decide. + -- intro Htop. + apply AndR. + ++ rewrite Htop in Hφ. + apply weakening. + eapply TopL_rev. + apply Hφ. + ++ apply Hψ. + -- intro. + case decide. + ++ intro HTop. + apply AndR. + ** apply Hφ. + ** rewrite HTop in Hψ. + apply weakening. + eapply TopL_rev. + apply Hψ. + ++ intro. + case decide. + ** intro Heq. + apply AndR; [ apply Hφ| rewrite Heq ;apply Hψ]. + ** intro. + apply AndL. + apply AndR. + --- apply weakening. + apply Hφ. + --- exch 0. apply weakening. + apply Hψ. +Qed. + Theorem simp_equiv_R Γ φ : Γ • (simp φ) ⊢ φ. -Admitted. +Proof. +remember (weight φ) as w. +assert(Hle : weight φ ≤ w) by lia. +clear Heqw. revert φ Hle. +induction w; intros φ Hle; [destruct φ ; simpl in Hle; lia|]. +destruct φ; try apply generalised_axiom; +[eapply (simp_equiv_and_R Γ φ1 φ2) | eapply (simp_equiv_or_R Γ φ1 φ2)]; +intros f H; apply IHw; lia. +Qed. + From e8fbf94eb64247b883edcca707e19693fda17e2d Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Fri, 14 Jun 2024 13:40:24 +0200 Subject: [PATCH 11/29] Improve decide intros --- theories/iSL/Simp.v | 168 +++++++++++++++++--------------------------- 1 file changed, 63 insertions(+), 105 deletions(-) diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index b89117d..ad1d307 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -16,8 +16,8 @@ Definition simp_or φ ψ := Definition simp_and φ ψ := if decide (φ =⊥) then ⊥ else if decide (ψ = ⊥) then ⊥ - else if decide (φ = ⊤) then ψ - else if decide (ψ = ⊤) then φ + else if decide (φ = ⊤) then ψ + else if decide (ψ = ⊤) then φ else if decide (φ = ψ) then φ else φ ∧ ψ. @@ -26,14 +26,14 @@ Definition simp_imp φ ψ := φ → ψ. Fixpoint simp φ := match φ with -| φ ∨ ψ => simp_or (simp φ) (simp ψ) -| φ ∧ ψ => simp_and (simp φ) (simp ψ) +| φ ∨ ψ => simp_or (simp φ) (simp ψ) +| φ ∧ ψ => simp_and (simp φ) (simp ψ) | φ → ψ => simp_imp φ ψ | _ => φ end. -Lemma top_provable Γ : +Lemma top_provable Γ : Γ ⊢ ⊤. Proof. apply ImpR. @@ -55,29 +55,21 @@ intros IH. assert (Hφ : Γ • φ ⊢ simp φ ) by (apply (IH φ); simpl; lia). assert (Hψ : Γ • ψ ⊢ simp ψ ) by (apply (IH ψ); simpl; lia). simpl. unfold simp_or. -case decide. -- intro Hbot. - apply OrL. +case decide as [Hbot |]. +- apply OrL. + rewrite Hbot in Hφ. apply exfalso. trivial. + apply Hψ. -- intro. - case decide. - + intro Hbot. - apply OrL. +- case decide as [Hbot |]. + + apply OrL. * apply Hφ. * rewrite Hbot in Hψ. apply exfalso. trivial. - + intro. - case decide. - * intro Htop. - apply top_provable. - * intro. - case decide. - -- intro Htop. - apply top_provable. - -- intro. - case decide; [intro Heq | intro ]; apply OrL. + + case decide as [Htop |]. + * apply top_provable. + * case decide as [Htop |]. + -- apply top_provable. + -- case decide; [intro Heq | intro ]; apply OrL. ** apply Hφ. ** rewrite Heq. apply Hψ. @@ -96,37 +88,27 @@ intros IH. assert (Hφ : Γ • φ ⊢ simp φ ) by (apply (IH φ); simpl; lia). assert (Hψ : Γ • ψ ⊢ simp ψ ) by (apply (IH ψ); simpl; lia). simpl. unfold simp_and. -case decide. -- intro Hbot. - rewrite Hbot in Hφ. +case decide as [Hbot |]. +- rewrite Hbot in Hφ. apply AndL. apply weakening. apply exfalso. trivial. -- intro. - case decide. - + intro Hbot. - rewrite Hbot in Hψ. +- case decide as [Hbot |]. + + rewrite Hbot in Hψ. apply AndL. exch 0. apply weakening. apply exfalso. trivial. - + intro. - case decide. - * intro. - apply AndL. + + case decide as []. + * apply AndL. exch 0. apply weakening. apply Hψ. - * intro. - case decide. - -- intro. - apply AndL. + * case decide as []. + -- apply AndL. apply weakening. apply Hφ. - -- intro. - apply AndL. - case decide. - ++ intro. - apply weakening. + -- apply AndL. + case decide as []. + ++ apply weakening. apply Hφ. - ++ intro. - apply AndR. + ++ apply AndR. ** apply weakening. apply Hφ. ** exch 0. apply weakening. @@ -154,34 +136,24 @@ intros IH. assert (Hφ : Γ • simp φ ⊢ φ ) by (apply (IH φ); simpl; lia). assert (Hψ : Γ • simp ψ ⊢ ψ ) by (apply (IH ψ); simpl; lia). simpl. unfold simp_or. -case decide. -- intro. - apply OrR2. +case decide as []. +- apply OrR2. apply Hψ. -- intro. - case decide. - + intro. - apply OrR1. +- case decide as []. + + apply OrR1. apply Hφ. - + intro. - case decide. - * intro Htop. - apply OrR1. + + case decide as [Htop |]. + * apply OrR1. rewrite <- Htop. apply Hφ. - * intro. - case decide. - -- intro Htop. - apply OrR2. + * case decide as [Htop |]. + -- apply OrR2. rewrite <- Htop. apply Hψ. - -- intro. - case decide. - ++ intro. - apply OrR1. + -- case decide as []. + ++ apply OrR1. apply Hφ. - ++ intro. - apply OrL. + ++ apply OrL. ** apply OrR1. apply Hφ. ** apply OrR2. @@ -192,46 +164,32 @@ Lemma simp_equiv_and_R Γ φ ψ : (forall f, weight f < weight (φ ∧ ψ) -> Γ • simp f ⊢ f) -> Γ • simp (φ ∧ ψ) ⊢ φ ∧ ψ. Proof. -intros IH. -assert (Hφ : Γ • simp φ ⊢ φ ) by (apply (IH φ); simpl; lia). -assert (Hψ : Γ • simp ψ ⊢ ψ ) by (apply (IH ψ); simpl; lia). -simpl. unfold simp_and. -case decide. -- intro. - apply exfalso. apply ExFalso. -- intro. - + case decide. - * intro. - apply exfalso. apply ExFalso. - * intro. - case decide. - -- intro Htop. - apply AndR. - ++ rewrite Htop in Hφ. - apply weakening. - eapply TopL_rev. - apply Hφ. - ++ apply Hψ. - -- intro. - case decide. - ++ intro HTop. - apply AndR. - ** apply Hφ. - ** rewrite HTop in Hψ. - apply weakening. - eapply TopL_rev. - apply Hψ. - ++ intro. - case decide. - ** intro Heq. - apply AndR; [ apply Hφ| rewrite Heq ;apply Hψ]. - ** intro. - apply AndL. - apply AndR. - --- apply weakening. - apply Hφ. - --- exch 0. apply weakening. - apply Hψ. + intros IH. + assert (Hφ : Γ • simp φ ⊢ φ ) by (apply (IH φ); simpl; lia). + assert (Hψ : Γ • simp ψ ⊢ ψ ) by (apply (IH ψ); simpl; lia). + simpl. unfold simp_and. + case decide as []. + - apply exfalso. apply ExFalso. + - case decide as []. + + apply exfalso. apply ExFalso. + + case decide as [Htop |]. + * apply AndR. + -- rewrite Htop in Hφ. + apply weakening. + eapply TopL_rev. + apply Hφ. + -- apply Hψ. + * case decide as [Htop |]. + -- apply AndR. + ++ apply Hφ. + ++ rewrite Htop in Hψ. + apply weakening. + eapply TopL_rev. + apply Hψ. + -- case decide as [ Heq | Hneq]. + ++ apply AndR; [ apply Hφ| rewrite Heq ;apply Hψ]. + ++ apply AndL. + apply AndR; [|exch 0]; apply weakening; [apply Hφ| apply Hψ]. Qed. Theorem simp_equiv_R Γ φ : Γ • (simp φ) ⊢ φ. From 2de5404a543e2a7aca16e5a9b8e0d423fe6c8150 Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Sat, 15 Jun 2024 12:11:05 +0200 Subject: [PATCH 12/29] Prove both simplification entailments at the same time --- theories/iSL/Simp.v | 121 +++++++++++++++++++++----------------------- 1 file changed, 59 insertions(+), 62 deletions(-) diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index ad1d307..540a272 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -1,8 +1,6 @@ Require Import ISL.SequentProps. Require Import ISL.Sequents. Require Import ISL.Environments. -Require Import Coq.Program.Equality. - Definition simp_or φ ψ := if decide (φ = ⊥) then ψ @@ -12,7 +10,6 @@ Definition simp_or φ ψ := else if decide (φ = ψ) then φ else φ ∨ ψ. - Definition simp_and φ ψ := if decide (φ =⊥) then ⊥ else if decide (ψ = ⊥) then ⊥ @@ -40,15 +37,8 @@ Proof. apply ExFalso. Qed. -Lemma ImpR_idemp Γ φ : - Γ ⊢ (φ → φ). -Proof. - apply ImpR. - apply generalised_axiom. -Qed. - Lemma simp_equiv_or_L Γ φ ψ : - (forall f, weight f < weight (φ ∨ ψ) -> Γ • f ⊢ simp f) -> + (forall f, weight f < weight (φ ∨ ψ) -> (Γ • f ⊢ simp f) * (Γ • simp f ⊢ f)) -> Γ • (φ ∨ ψ) ⊢ simp (φ ∨ ψ). Proof. intros IH. @@ -80,8 +70,49 @@ case decide as [Hbot |]. Qed. +Lemma simp_equiv_or_R Γ φ ψ : + (forall f, weight f < weight (φ ∨ ψ) -> (Γ • f ⊢ simp f) * (Γ • simp f ⊢ f)) -> + Γ •simp (φ ∨ ψ) ⊢ (φ ∨ ψ). +Proof. +intros IH. +assert (Hφ : Γ • simp φ ⊢ φ ) by (apply (IH φ); simpl; lia). +assert (Hψ : Γ • simp ψ ⊢ ψ ) by (apply (IH ψ); simpl; lia). +simpl. unfold simp_or. +case decide as []. +- apply OrR2. + apply Hψ. +- case decide as []. + + apply OrR1. + apply Hφ. + + case decide as [Htop |]. + * apply OrR1. + rewrite <- Htop. + apply Hφ. + * case decide as [Htop |]. + -- apply OrR2. + rewrite <- Htop. + apply Hψ. + -- case decide as []. + ++ apply OrR1. + apply Hφ. + ++ apply OrL. + ** apply OrR1. + apply Hφ. + ** apply OrR2. + apply Hψ. +Qed. + + +Lemma simp_equiv_or Γ φ ψ: + (forall f, weight f < weight (φ ∨ ψ) -> (Γ • f ⊢ simp f) * (Γ • simp f ⊢ f)) -> + (Γ • (φ ∨ ψ) ⊢ simp (φ ∨ ψ)) * (Γ • simp (φ ∨ ψ) ⊢(φ ∨ ψ)). +Proof. +intros IH. +split; [ apply simp_equiv_or_L | apply simp_equiv_or_R] ; apply IH. +Qed. + Lemma simp_equiv_and_L Γ φ ψ : - (forall f, weight f < weight (φ ∧ ψ) -> Γ • f ⊢ simp f) -> + (forall f, weight f < weight (φ ∧ ψ) -> (Γ • f ⊢ simp f) * (Γ • simp f ⊢ f)) -> Γ • (φ ∧ ψ) ⊢ simp (φ ∧ ψ). Proof. intros IH. @@ -116,52 +147,8 @@ case decide as [Hbot |]. Qed. -Theorem simp_equiv_L Γ φ : Γ • φ ⊢ simp φ. -Proof. -remember (weight φ) as w. -assert(Hle : weight φ ≤ w) by lia. -clear Heqw. revert φ Hle. -induction w; intros φ Hle; [destruct φ ; simpl in Hle; lia|]. -destruct φ; try apply generalised_axiom; -[eapply (simp_equiv_and_L Γ φ1 φ2)| eapply (simp_equiv_or_L Γ φ1 φ2)]; -intros f H; apply IHw; lia. -Qed. - - -Lemma simp_equiv_or_R Γ φ ψ : - (forall f, weight f < weight (φ ∨ ψ) -> Γ • simp f ⊢ f) -> - Γ •simp (φ ∨ ψ) ⊢ (φ ∨ ψ). -Proof. -intros IH. -assert (Hφ : Γ • simp φ ⊢ φ ) by (apply (IH φ); simpl; lia). -assert (Hψ : Γ • simp ψ ⊢ ψ ) by (apply (IH ψ); simpl; lia). -simpl. unfold simp_or. -case decide as []. -- apply OrR2. - apply Hψ. -- case decide as []. - + apply OrR1. - apply Hφ. - + case decide as [Htop |]. - * apply OrR1. - rewrite <- Htop. - apply Hφ. - * case decide as [Htop |]. - -- apply OrR2. - rewrite <- Htop. - apply Hψ. - -- case decide as []. - ++ apply OrR1. - apply Hφ. - ++ apply OrL. - ** apply OrR1. - apply Hφ. - ** apply OrR2. - apply Hψ. -Qed. - Lemma simp_equiv_and_R Γ φ ψ : - (forall f, weight f < weight (φ ∧ ψ) -> Γ • simp f ⊢ f) -> + (forall f, weight f < weight (φ ∧ ψ) -> (Γ • f ⊢ simp f) * (Γ • simp f ⊢ f)) -> Γ • simp (φ ∧ ψ) ⊢ φ ∧ ψ. Proof. intros IH. @@ -192,15 +179,25 @@ Proof. apply AndR; [|exch 0]; apply weakening; [apply Hφ| apply Hψ]. Qed. -Theorem simp_equiv_R Γ φ : Γ • (simp φ) ⊢ φ. + +Lemma simp_equiv_and Γ φ ψ: + (forall f, weight f < weight (φ ∧ ψ) -> (Γ • f ⊢ simp f) * (Γ • simp f ⊢ f)) -> + (Γ • (φ ∧ ψ) ⊢ simp (φ ∧ ψ)) * (Γ • simp (φ ∧ ψ) ⊢(φ ∧ ψ)). +Proof. +intros IH. +split; [ apply simp_equiv_and_L | apply simp_equiv_and_R] ; apply IH. +Qed. + + + +Theorem simp_equiv Γ φ : (Γ • φ ⊢ simp φ) * (Γ • (simp φ) ⊢ φ). Proof. remember (weight φ) as w. assert(Hle : weight φ ≤ w) by lia. clear Heqw. revert φ Hle. induction w; intros φ Hle; [destruct φ ; simpl in Hle; lia|]. -destruct φ; try apply generalised_axiom; -[eapply (simp_equiv_and_R Γ φ1 φ2) | eapply (simp_equiv_or_R Γ φ1 φ2)]; +destruct φ; simpl; try (split ; apply generalised_axiom); +[eapply (simp_equiv_and Γ φ1 φ2)| + eapply (simp_equiv_or Γ φ1 φ2)]; intros f H; apply IHw; lia. Qed. - - From 34b93600fe6e45ce08f3edfd3aab30f0a78574f2 Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Sat, 15 Jun 2024 12:15:36 +0200 Subject: [PATCH 13/29] Simplify formulas under implication --- theories/iSL/Simp.v | 49 +++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 47 insertions(+), 2 deletions(-) diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index 540a272..38ce072 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -25,7 +25,7 @@ Definition simp_imp φ ψ := Fixpoint simp φ := match φ with | φ ∨ ψ => simp_or (simp φ) (simp ψ) | φ ∧ ψ => simp_and (simp φ) (simp ψ) -| φ → ψ => simp_imp φ ψ +| φ → ψ => simp_imp (simp φ) (simp ψ) | _ => φ end. @@ -189,6 +189,50 @@ split; [ apply simp_equiv_and_L | apply simp_equiv_and_R] ; apply IH. Qed. +Lemma simp_equiv_imp_L Γ φ ψ : + (forall f, weight f < weight (φ → ψ) -> (Γ • f ⊢ simp f) * (Γ • simp f ⊢ f)) -> + Γ • (φ → ψ) ⊢ simp (φ → ψ). +Proof. +intros IH. +assert (HφR : Γ • simp φ ⊢ φ) by (apply (IH φ); simpl; lia). +assert (Hψ : Γ • ψ ⊢ simp ψ) by (apply (IH ψ); simpl; lia). +simpl. unfold simp_imp. +apply ImpR. +exch 0. +apply ImpL. +- apply weakening. apply HφR. +- exch 0. apply weakening. + apply Hψ. +Qed. + +Lemma simp_equiv_imp_R Γ φ ψ : + (forall f, weight f < weight (φ → ψ) -> (Γ • f ⊢ simp f) * (Γ • simp f ⊢ f)) -> + Γ • simp (φ → ψ) ⊢ (φ → ψ). +Proof. + + +intros IH. + +assert (HφL : Γ • φ ⊢ simp φ) by (apply (IH φ); simpl; lia). +assert (HψR : Γ • simp ψ ⊢ ψ) by (apply (IH ψ); simpl; lia). +simpl. unfold simp_imp. +apply ImpR. +exch 0. +apply ImpL. +- apply weakening. apply HφL. +- exch 0. apply weakening. + apply HψR. +Qed. + + +Lemma simp_equiv_imp Γ φ ψ: + (forall f, weight f < weight (φ → ψ) -> (Γ • f ⊢ simp f) * (Γ • simp f ⊢ f)) -> + (Γ • (φ → ψ) ⊢ simp (φ → ψ)) * (Γ • simp (φ → ψ) ⊢(φ → ψ)). +Proof. +intros IH. +split; [ apply simp_equiv_imp_L | apply simp_equiv_imp_R] ; apply IH. +Qed. + Theorem simp_equiv Γ φ : (Γ • φ ⊢ simp φ) * (Γ • (simp φ) ⊢ φ). Proof. @@ -198,6 +242,7 @@ clear Heqw. revert φ Hle. induction w; intros φ Hle; [destruct φ ; simpl in Hle; lia|]. destruct φ; simpl; try (split ; apply generalised_axiom); [eapply (simp_equiv_and Γ φ1 φ2)| - eapply (simp_equiv_or Γ φ1 φ2)]; + eapply (simp_equiv_or Γ φ1 φ2)| + eapply (simp_equiv_imp Γ φ1 φ2)]; intros f H; apply IHw; lia. Qed. From 4b268d56e7a4c196ec5c921d169fd5c7bf3842e4 Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Sat, 15 Jun 2024 13:48:58 +0200 Subject: [PATCH 14/29] Simplify bot and top left of an implication --- theories/iSL/Simp.v | 55 ++++++++++++++++++++++++++++----------------- 1 file changed, 35 insertions(+), 20 deletions(-) diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index 38ce072..3581e16 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -20,7 +20,9 @@ Definition simp_and φ ψ := Definition simp_imp φ ψ := - φ → ψ. + if decide (φ = ⊤) then ψ + else if decide (φ = ⊥) then ⊤ + else φ → ψ. Fixpoint simp φ := match φ with | φ ∨ ψ => simp_or (simp φ) (simp ψ) @@ -33,8 +35,7 @@ end. Lemma top_provable Γ : Γ ⊢ ⊤. Proof. - apply ImpR. - apply ExFalso. + apply ImpR. apply ExFalso. Qed. Lemma simp_equiv_or_L Γ φ ψ : @@ -126,7 +127,7 @@ case decide as [Hbot |]. - case decide as [Hbot |]. + rewrite Hbot in Hψ. apply AndL. exch 0. apply weakening. - apply exfalso. trivial. + apply Hψ. + case decide as []. * apply AndL. exch 0. apply weakening. @@ -195,33 +196,47 @@ Lemma simp_equiv_imp_L Γ φ ψ : Proof. intros IH. assert (HφR : Γ • simp φ ⊢ φ) by (apply (IH φ); simpl; lia). -assert (Hψ : Γ • ψ ⊢ simp ψ) by (apply (IH ψ); simpl; lia). +assert (HφL : Γ • φ ⊢ simp φ) by (apply (IH φ); simpl; lia). +assert (HψL: Γ • ψ ⊢ simp ψ) by (apply (IH ψ); simpl; lia). simpl. unfold simp_imp. -apply ImpR. -exch 0. -apply ImpL. -- apply weakening. apply HφR. -- exch 0. apply weakening. - apply Hψ. +case decide as [Htop |]. +- rewrite Htop in HφR. + apply weak_ImpL. + + eapply TopL_rev. + apply HφR. + + apply HψL. +- case decide as []. + + apply weakening. + apply top_provable. + + apply ImpR. + exch 0. + apply ImpL. + * apply weakening. apply HφR. + * exch 0. apply weakening. + apply HψL. Qed. Lemma simp_equiv_imp_R Γ φ ψ : (forall f, weight f < weight (φ → ψ) -> (Γ • f ⊢ simp f) * (Γ • simp f ⊢ f)) -> Γ • simp (φ → ψ) ⊢ (φ → ψ). Proof. - - intros IH. - assert (HφL : Γ • φ ⊢ simp φ) by (apply (IH φ); simpl; lia). assert (HψR : Γ • simp ψ ⊢ ψ) by (apply (IH ψ); simpl; lia). -simpl. unfold simp_imp. -apply ImpR. -exch 0. -apply ImpL. -- apply weakening. apply HφL. -- exch 0. apply weakening. +simpl. unfold simp_imp. +case decide as [Htop |]. +- apply ImpR. + apply weakening. apply HψR. +- case decide as [Htop |]. + + rewrite Htop in HφL. + auto with proof. + + apply ImpR. + exch 0. + apply ImpL. + * apply weakening. apply HφL. + * exch 0. apply weakening. + apply HψR. Qed. From 0be622f70e85374744330fa63a570c50149a1e37 Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Tue, 18 Jun 2024 11:45:30 +0200 Subject: [PATCH 15/29] Introduce the Lindenbaum Tarski preorder --- theories/iSL/Simp.v | 191 +++++++++++++++++++++++++------------------- 1 file changed, 109 insertions(+), 82 deletions(-) diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index 3581e16..8ea38bf 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -2,6 +2,7 @@ Require Import ISL.SequentProps. Require Import ISL.Sequents. Require Import ISL.Environments. + Definition simp_or φ ψ := if decide (φ = ⊥) then ψ else if decide (ψ = ⊥) then φ @@ -31,6 +32,23 @@ Fixpoint simp φ := match φ with | _ => φ end. +Definition Lindenbaum_Tarski_preorder φ ψ := + ∅ • φ ⊢ ψ. + +Notation "φ ≼ ψ" := (form_order φ ψ) (at level 149). + +Lemma order_to_proof φ ψ: + ∅ • φ ⊢ ψ -> + (φ ≼ ψ). +Admitted. + +Lemma proof_to_order φ ψ: + (φ ≼ ψ) -> + ∅ • φ ⊢ ψ. +Admitted. + +Ltac oeapply th := + apply proof_to_order; apply th. Lemma top_provable Γ : Γ ⊢ ⊤. @@ -38,123 +56,126 @@ Proof. apply ImpR. apply ExFalso. Qed. -Lemma simp_equiv_or_L Γ φ ψ : - (forall f, weight f < weight (φ ∨ ψ) -> (Γ • f ⊢ simp f) * (Γ • simp f ⊢ f)) -> - Γ • (φ ∨ ψ) ⊢ simp (φ ∨ ψ). +Lemma simp_equiv_or_L φ ψ : + (forall f, weight f < weight (φ ∨ ψ) -> (f ≼ simp f) * (simp f ≼ f)) -> + (φ ∨ ψ) ≼ simp (φ ∨ ψ). Proof. intros IH. -assert (Hφ : Γ • φ ⊢ simp φ ) by (apply (IH φ); simpl; lia). -assert (Hψ : Γ • ψ ⊢ simp ψ ) by (apply (IH ψ); simpl; lia). +apply order_to_proof. +assert (Hφ : φ ≼ simp φ ) by (apply (IH φ); simpl; lia). +assert (Hψ : ψ ≼ simp ψ ) by (apply (IH ψ); simpl; lia). simpl. unfold simp_or. case decide as [Hbot |]. - apply OrL. + rewrite Hbot in Hφ. - apply exfalso. trivial. - + apply Hψ. + apply exfalso. oeapply Hφ. + + oeapply Hψ. - case decide as [Hbot |]. + apply OrL. - * apply Hφ. + * oeapply Hφ. * rewrite Hbot in Hψ. - apply exfalso. trivial. + apply exfalso. oeapply Hψ. + case decide as [Htop |]. * apply top_provable. * case decide as [Htop |]. -- apply top_provable. -- case decide; [intro Heq | intro ]; apply OrL. - ** apply Hφ. + ** oeapply Hφ. ** rewrite Heq. - apply Hψ. + oeapply Hψ. ** apply OrR1. - apply Hφ. + oeapply Hφ. ** apply OrR2. - apply Hψ. + oeapply Hψ. Qed. -Lemma simp_equiv_or_R Γ φ ψ : - (forall f, weight f < weight (φ ∨ ψ) -> (Γ • f ⊢ simp f) * (Γ • simp f ⊢ f)) -> - Γ •simp (φ ∨ ψ) ⊢ (φ ∨ ψ). +Lemma simp_equiv_or_R φ ψ : + (forall f, weight f < weight (φ ∨ ψ) -> (f ≼ simp f) * (simp f ≼ f)) -> + simp (φ ∨ ψ) ≼ (φ ∨ ψ). Proof. intros IH. -assert (Hφ : Γ • simp φ ⊢ φ ) by (apply (IH φ); simpl; lia). -assert (Hψ : Γ • simp ψ ⊢ ψ ) by (apply (IH ψ); simpl; lia). +apply order_to_proof. +assert (Hφ : simp φ ≼ φ ) by (apply (IH φ); simpl; lia). +assert (Hψ : simp ψ ≼ ψ ) by (apply (IH ψ); simpl; lia). simpl. unfold simp_or. case decide as []. - apply OrR2. - apply Hψ. + oeapply Hψ. - case decide as []. + apply OrR1. - apply Hφ. + oeapply Hφ. + case decide as [Htop |]. * apply OrR1. rewrite <- Htop. - apply Hφ. + oeapply Hφ. * case decide as [Htop |]. -- apply OrR2. rewrite <- Htop. - apply Hψ. + oeapply Hψ. -- case decide as []. ++ apply OrR1. - apply Hφ. + oeapply Hφ. ++ apply OrL. ** apply OrR1. - apply Hφ. + oeapply Hφ. ** apply OrR2. - apply Hψ. + oeapply Hψ. Qed. - -Lemma simp_equiv_or Γ φ ψ: - (forall f, weight f < weight (φ ∨ ψ) -> (Γ • f ⊢ simp f) * (Γ • simp f ⊢ f)) -> - (Γ • (φ ∨ ψ) ⊢ simp (φ ∨ ψ)) * (Γ • simp (φ ∨ ψ) ⊢(φ ∨ ψ)). +Lemma simp_equiv_or φ ψ: + (forall f, weight f < weight (φ ∨ ψ) -> (f ≼ simp f) * (simp f ≼ f)) -> + ((φ ∨ ψ) ≼ simp (φ ∨ ψ)) * (simp (φ ∨ ψ) ≼ (φ ∨ ψ)). Proof. intros IH. split; [ apply simp_equiv_or_L | apply simp_equiv_or_R] ; apply IH. Qed. -Lemma simp_equiv_and_L Γ φ ψ : - (forall f, weight f < weight (φ ∧ ψ) -> (Γ • f ⊢ simp f) * (Γ • simp f ⊢ f)) -> - Γ • (φ ∧ ψ) ⊢ simp (φ ∧ ψ). +Lemma simp_equiv_and_L φ ψ : + (forall f, weight f < weight (φ ∧ ψ) -> (f ≼ simp f) * (simp f ≼ f)) -> + (φ ∧ ψ) ≼ simp (φ ∧ ψ). Proof. intros IH. -assert (Hφ : Γ • φ ⊢ simp φ ) by (apply (IH φ); simpl; lia). -assert (Hψ : Γ • ψ ⊢ simp ψ ) by (apply (IH ψ); simpl; lia). +apply order_to_proof. +assert (Hφ : φ ≼ simp φ ) by (apply (IH φ); simpl; lia). +assert (Hψ : ψ ≼ simp ψ ) by (apply (IH ψ); simpl; lia). simpl. unfold simp_and. case decide as [Hbot |]. - rewrite Hbot in Hφ. apply AndL. apply weakening. - apply exfalso. trivial. + apply exfalso. oeapply Hφ. - case decide as [Hbot |]. + rewrite Hbot in Hψ. apply AndL. exch 0. apply weakening. - apply Hψ. + oeapply Hψ. + case decide as []. * apply AndL. exch 0. apply weakening. - apply Hψ. + oeapply Hψ. * case decide as []. -- apply AndL. apply weakening. - apply Hφ. + oeapply Hφ. -- apply AndL. case decide as []. ++ apply weakening. - apply Hφ. + oeapply Hφ. ++ apply AndR. ** apply weakening. - apply Hφ. + oeapply Hφ. ** exch 0. apply weakening. - apply Hψ. + oeapply Hψ. Qed. -Lemma simp_equiv_and_R Γ φ ψ : - (forall f, weight f < weight (φ ∧ ψ) -> (Γ • f ⊢ simp f) * (Γ • simp f ⊢ f)) -> - Γ • simp (φ ∧ ψ) ⊢ φ ∧ ψ. +Lemma simp_equiv_and_R φ ψ : + (forall f, weight f < weight (φ ∧ ψ) -> (f ≼ simp f) * (simp f ≼ f)) -> + simp (φ ∧ ψ) ≼ φ ∧ ψ. Proof. intros IH. - assert (Hφ : Γ • simp φ ⊢ φ ) by (apply (IH φ); simpl; lia). - assert (Hψ : Γ • simp ψ ⊢ ψ ) by (apply (IH ψ); simpl; lia). +apply order_to_proof. + assert (Hφ : simp φ ≼ φ ) by (apply (IH φ); simpl; lia). + assert (Hψ : simp ψ ≼ ψ ) by (apply (IH ψ); simpl; lia). simpl. unfold simp_and. case decide as []. - apply exfalso. apply ExFalso. @@ -165,99 +186,105 @@ Proof. -- rewrite Htop in Hφ. apply weakening. eapply TopL_rev. - apply Hφ. - -- apply Hψ. + oeapply Hφ. + -- oeapply Hψ. * case decide as [Htop |]. -- apply AndR. - ++ apply Hφ. + ++ oeapply Hφ. ++ rewrite Htop in Hψ. apply weakening. eapply TopL_rev. - apply Hψ. + oeapply Hψ. -- case decide as [ Heq | Hneq]. - ++ apply AndR; [ apply Hφ| rewrite Heq ;apply Hψ]. + ++ apply AndR; [ oeapply Hφ| rewrite Heq ; oeapply Hψ]. ++ apply AndL. - apply AndR; [|exch 0]; apply weakening; [apply Hφ| apply Hψ]. + apply AndR; [|exch 0]; apply weakening; [oeapply Hφ | oeapply Hψ]. Qed. -Lemma simp_equiv_and Γ φ ψ: - (forall f, weight f < weight (φ ∧ ψ) -> (Γ • f ⊢ simp f) * (Γ • simp f ⊢ f)) -> - (Γ • (φ ∧ ψ) ⊢ simp (φ ∧ ψ)) * (Γ • simp (φ ∧ ψ) ⊢(φ ∧ ψ)). +Lemma simp_equiv_and φ ψ: + (forall f, weight f < weight (φ ∧ ψ) -> (f ≼ simp f) * (simp f ≼ f)) -> + ((φ ∧ ψ) ≼ simp (φ ∧ ψ)) * (simp (φ ∧ ψ) ≼ (φ ∧ ψ)). Proof. intros IH. split; [ apply simp_equiv_and_L | apply simp_equiv_and_R] ; apply IH. Qed. -Lemma simp_equiv_imp_L Γ φ ψ : - (forall f, weight f < weight (φ → ψ) -> (Γ • f ⊢ simp f) * (Γ • simp f ⊢ f)) -> - Γ • (φ → ψ) ⊢ simp (φ → ψ). +Lemma simp_equiv_imp_L φ ψ : + (forall f, weight f < weight (φ → ψ) -> (f ≼ simp f) * (simp f ≼ f)) -> + (φ → ψ) ≼ simp (φ → ψ). Proof. intros IH. -assert (HφR : Γ • simp φ ⊢ φ) by (apply (IH φ); simpl; lia). -assert (HφL : Γ • φ ⊢ simp φ) by (apply (IH φ); simpl; lia). -assert (HψL: Γ • ψ ⊢ simp ψ) by (apply (IH ψ); simpl; lia). +apply order_to_proof. +assert (HφR : simp φ ≼ φ) by (apply (IH φ); simpl; lia). +assert (HφL : φ ≼ simp φ) by (apply (IH φ); simpl; lia). +assert (HψL: ψ ≼ simp ψ) by (apply (IH ψ); simpl; lia). simpl. unfold simp_imp. case decide as [Htop |]. - rewrite Htop in HφR. apply weak_ImpL. + eapply TopL_rev. - apply HφR. - + apply HψL. + oeapply HφR. + + oeapply HψL. - case decide as []. + apply weakening. apply top_provable. + apply ImpR. exch 0. apply ImpL. - * apply weakening. apply HφR. + * apply weakening. oeapply HφR. * exch 0. apply weakening. - apply HψL. + oeapply HψL. Qed. -Lemma simp_equiv_imp_R Γ φ ψ : - (forall f, weight f < weight (φ → ψ) -> (Γ • f ⊢ simp f) * (Γ • simp f ⊢ f)) -> - Γ • simp (φ → ψ) ⊢ (φ → ψ). +Lemma simp_equiv_imp_R φ ψ : + (forall f, weight f < weight (φ → ψ) -> (f ≼ simp f) * ( simp f ≼ f)) -> + simp (φ → ψ) ≼ (φ → ψ). Proof. intros IH. -assert (HφL : Γ • φ ⊢ simp φ) by (apply (IH φ); simpl; lia). -assert (HψR : Γ • simp ψ ⊢ ψ) by (apply (IH ψ); simpl; lia). +apply order_to_proof. +assert (HφL : φ ≼ simp φ) by (apply (IH φ); simpl; lia). +assert (HψR : simp ψ ≼ ψ) by (apply (IH ψ); simpl; lia). simpl. unfold simp_imp. case decide as [Htop |]. - apply ImpR. apply weakening. - apply HψR. + oeapply HψR. - case decide as [Htop |]. + rewrite Htop in HφL. - auto with proof. + apply ImpR. + apply exfalso. + exch 0. apply weakening. + oeapply HφL. + apply ImpR. exch 0. apply ImpL. - * apply weakening. apply HφL. + * apply weakening. oeapply HφL. * exch 0. apply weakening. - apply HψR. + oeapply HψR. Qed. -Lemma simp_equiv_imp Γ φ ψ: - (forall f, weight f < weight (φ → ψ) -> (Γ • f ⊢ simp f) * (Γ • simp f ⊢ f)) -> - (Γ • (φ → ψ) ⊢ simp (φ → ψ)) * (Γ • simp (φ → ψ) ⊢(φ → ψ)). +Lemma simp_equiv_imp φ ψ: + (forall f, weight f < weight (φ → ψ) -> (f ≼ simp f) * (simp f ≼ f)) -> + ((φ → ψ) ≼ simp (φ → ψ)) * (simp (φ → ψ) ≼ (φ → ψ)). Proof. intros IH. split; [ apply simp_equiv_imp_L | apply simp_equiv_imp_R] ; apply IH. Qed. -Theorem simp_equiv Γ φ : (Γ • φ ⊢ simp φ) * (Γ • (simp φ) ⊢ φ). +Theorem simp_equiv φ : + (φ ≼ (simp φ)) * ((simp φ) ≼ φ). Proof. remember (weight φ) as w. assert(Hle : weight φ ≤ w) by lia. clear Heqw. revert φ Hle. induction w; intros φ Hle; [destruct φ ; simpl in Hle; lia|]. -destruct φ; simpl; try (split ; apply generalised_axiom); -[eapply (simp_equiv_and Γ φ1 φ2)| - eapply (simp_equiv_or Γ φ1 φ2)| - eapply (simp_equiv_imp Γ φ1 φ2)]; +destruct φ; simpl; try (split ; apply order_to_proof; apply generalised_axiom); +[eapply (simp_equiv_and φ1 φ2)| + eapply (simp_equiv_or φ1 φ2)| + eapply (simp_equiv_imp φ1 φ2)]; intros f H; apply IHw; lia. Qed. From e6ee4c0da3cfda2aa22a20cb24ca131a03bffd0a Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Tue, 18 Jun 2024 13:56:53 +0200 Subject: [PATCH 16/29] Fix: notation used form_order instead of Lindenbaum_Tarski_preorder. --- theories/iSL/Simp.v | 100 +++++++++++++++++++------------------------- 1 file changed, 43 insertions(+), 57 deletions(-) diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index 8ea38bf..475d80d 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -35,20 +35,7 @@ end. Definition Lindenbaum_Tarski_preorder φ ψ := ∅ • φ ⊢ ψ. -Notation "φ ≼ ψ" := (form_order φ ψ) (at level 149). - -Lemma order_to_proof φ ψ: - ∅ • φ ⊢ ψ -> - (φ ≼ ψ). -Admitted. - -Lemma proof_to_order φ ψ: - (φ ≼ ψ) -> - ∅ • φ ⊢ ψ. -Admitted. - -Ltac oeapply th := - apply proof_to_order; apply th. +Notation "φ ≼ ψ" := (Lindenbaum_Tarski_preorder φ ψ) (at level 149). Lemma top_provable Γ : Γ ⊢ ⊤. @@ -61,32 +48,31 @@ Lemma simp_equiv_or_L φ ψ : (φ ∨ ψ) ≼ simp (φ ∨ ψ). Proof. intros IH. -apply order_to_proof. assert (Hφ : φ ≼ simp φ ) by (apply (IH φ); simpl; lia). assert (Hψ : ψ ≼ simp ψ ) by (apply (IH ψ); simpl; lia). simpl. unfold simp_or. case decide as [Hbot |]. - apply OrL. + rewrite Hbot in Hφ. - apply exfalso. oeapply Hφ. - + oeapply Hψ. + apply exfalso. apply Hφ. + + apply Hψ. - case decide as [Hbot |]. + apply OrL. - * oeapply Hφ. + * apply Hφ. * rewrite Hbot in Hψ. - apply exfalso. oeapply Hψ. + apply exfalso. apply Hψ. + case decide as [Htop |]. * apply top_provable. * case decide as [Htop |]. -- apply top_provable. -- case decide; [intro Heq | intro ]; apply OrL. - ** oeapply Hφ. + ** apply Hφ. ** rewrite Heq. - oeapply Hψ. + apply Hψ. ** apply OrR1. - oeapply Hφ. + apply Hφ. ** apply OrR2. - oeapply Hψ. + apply Hψ. Qed. @@ -95,32 +81,31 @@ Lemma simp_equiv_or_R φ ψ : simp (φ ∨ ψ) ≼ (φ ∨ ψ). Proof. intros IH. -apply order_to_proof. assert (Hφ : simp φ ≼ φ ) by (apply (IH φ); simpl; lia). assert (Hψ : simp ψ ≼ ψ ) by (apply (IH ψ); simpl; lia). simpl. unfold simp_or. case decide as []. - apply OrR2. - oeapply Hψ. + apply Hψ. - case decide as []. + apply OrR1. - oeapply Hφ. + apply Hφ. + case decide as [Htop |]. * apply OrR1. rewrite <- Htop. - oeapply Hφ. + apply Hφ. * case decide as [Htop |]. -- apply OrR2. rewrite <- Htop. - oeapply Hψ. + apply Hψ. -- case decide as []. ++ apply OrR1. - oeapply Hφ. + apply Hφ. ++ apply OrL. ** apply OrR1. - oeapply Hφ. + apply Hφ. ** apply OrR2. - oeapply Hψ. + apply Hψ. Qed. Lemma simp_equiv_or φ ψ: @@ -136,35 +121,34 @@ Lemma simp_equiv_and_L φ ψ : (φ ∧ ψ) ≼ simp (φ ∧ ψ). Proof. intros IH. -apply order_to_proof. assert (Hφ : φ ≼ simp φ ) by (apply (IH φ); simpl; lia). assert (Hψ : ψ ≼ simp ψ ) by (apply (IH ψ); simpl; lia). simpl. unfold simp_and. case decide as [Hbot |]. - rewrite Hbot in Hφ. apply AndL. apply weakening. - apply exfalso. oeapply Hφ. + apply exfalso. apply Hφ. - case decide as [Hbot |]. + rewrite Hbot in Hψ. apply AndL. exch 0. apply weakening. - oeapply Hψ. + apply Hψ. + case decide as []. * apply AndL. exch 0. apply weakening. - oeapply Hψ. + apply Hψ. * case decide as []. -- apply AndL. apply weakening. - oeapply Hφ. + apply Hφ. -- apply AndL. case decide as []. ++ apply weakening. - oeapply Hφ. + apply Hφ. ++ apply AndR. ** apply weakening. - oeapply Hφ. + apply Hφ. ** exch 0. apply weakening. - oeapply Hψ. + apply Hψ. Qed. @@ -173,7 +157,6 @@ Lemma simp_equiv_and_R φ ψ : simp (φ ∧ ψ) ≼ φ ∧ ψ. Proof. intros IH. -apply order_to_proof. assert (Hφ : simp φ ≼ φ ) by (apply (IH φ); simpl; lia). assert (Hψ : simp ψ ≼ ψ ) by (apply (IH ψ); simpl; lia). simpl. unfold simp_and. @@ -186,19 +169,19 @@ apply order_to_proof. -- rewrite Htop in Hφ. apply weakening. eapply TopL_rev. - oeapply Hφ. - -- oeapply Hψ. + apply Hφ. + -- apply Hψ. * case decide as [Htop |]. -- apply AndR. - ++ oeapply Hφ. + ++ apply Hφ. ++ rewrite Htop in Hψ. apply weakening. eapply TopL_rev. - oeapply Hψ. + apply Hψ. -- case decide as [ Heq | Hneq]. - ++ apply AndR; [ oeapply Hφ| rewrite Heq ; oeapply Hψ]. + ++ apply AndR; [ apply Hφ| rewrite Heq ; apply Hψ]. ++ apply AndL. - apply AndR; [|exch 0]; apply weakening; [oeapply Hφ | oeapply Hψ]. + apply AndR; [|exch 0]; apply weakening; [apply Hφ | apply Hψ]. Qed. @@ -216,7 +199,6 @@ Lemma simp_equiv_imp_L φ ψ : (φ → ψ) ≼ simp (φ → ψ). Proof. intros IH. -apply order_to_proof. assert (HφR : simp φ ≼ φ) by (apply (IH φ); simpl; lia). assert (HφL : φ ≼ simp φ) by (apply (IH φ); simpl; lia). assert (HψL: ψ ≼ simp ψ) by (apply (IH ψ); simpl; lia). @@ -225,17 +207,17 @@ case decide as [Htop |]. - rewrite Htop in HφR. apply weak_ImpL. + eapply TopL_rev. - oeapply HφR. - + oeapply HψL. + apply HφR. + + apply HψL. - case decide as []. + apply weakening. apply top_provable. + apply ImpR. exch 0. apply ImpL. - * apply weakening. oeapply HφR. + * apply weakening. apply HφR. * exch 0. apply weakening. - oeapply HψL. + apply HψL. Qed. Lemma simp_equiv_imp_R φ ψ : @@ -243,26 +225,25 @@ Lemma simp_equiv_imp_R φ ψ : simp (φ → ψ) ≼ (φ → ψ). Proof. intros IH. -apply order_to_proof. assert (HφL : φ ≼ simp φ) by (apply (IH φ); simpl; lia). assert (HψR : simp ψ ≼ ψ) by (apply (IH ψ); simpl; lia). simpl. unfold simp_imp. case decide as [Htop |]. - apply ImpR. apply weakening. - oeapply HψR. + apply HψR. - case decide as [Htop |]. + rewrite Htop in HφL. apply ImpR. apply exfalso. exch 0. apply weakening. - oeapply HφL. + apply HφL. + apply ImpR. exch 0. apply ImpL. - * apply weakening. oeapply HφL. + * apply weakening. apply HφL. * exch 0. apply weakening. - oeapply HψR. + apply HψR. Qed. @@ -282,9 +263,14 @@ remember (weight φ) as w. assert(Hle : weight φ ≤ w) by lia. clear Heqw. revert φ Hle. induction w; intros φ Hle; [destruct φ ; simpl in Hle; lia|]. -destruct φ; simpl; try (split ; apply order_to_proof; apply generalised_axiom); +destruct φ; simpl; try (split ; apply generalised_axiom); [eapply (simp_equiv_and φ1 φ2)| eapply (simp_equiv_or φ1 φ2)| eapply (simp_equiv_imp φ1 φ2)]; intros f H; apply IHw; lia. Qed. + +Require Import ISL.PropQuantifiers. + +Definition E_simplified (ψ : form) := Ef (simp ψ). +Definition A_simplified (ψ : form) := Af (simp ψ). From 686bc15bf5538d2f3a72f9b7c4de7bfd1241e221 Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Tue, 18 Jun 2024 14:43:44 +0200 Subject: [PATCH 17/29] relax hypothesis on simplification lemmas --- theories/iSL/Simp.v | 136 +++++++++++++++++++++++--------------------- 1 file changed, 72 insertions(+), 64 deletions(-) diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index 475d80d..07628fb 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -2,7 +2,6 @@ Require Import ISL.SequentProps. Require Import ISL.Sequents. Require Import ISL.Environments. - Definition simp_or φ ψ := if decide (φ = ⊥) then ψ else if decide (ψ = ⊥) then φ @@ -44,12 +43,10 @@ Proof. Qed. Lemma simp_equiv_or_L φ ψ : - (forall f, weight f < weight (φ ∨ ψ) -> (f ≼ simp f) * (simp f ≼ f)) -> + (φ ≼ simp φ) -> (ψ ≼ simp ψ) -> (φ ∨ ψ) ≼ simp (φ ∨ ψ). Proof. -intros IH. -assert (Hφ : φ ≼ simp φ ) by (apply (IH φ); simpl; lia). -assert (Hψ : ψ ≼ simp ψ ) by (apply (IH ψ); simpl; lia). +intros Hφ Hψ. simpl. unfold simp_or. case decide as [Hbot |]. - apply OrL. @@ -75,14 +72,11 @@ case decide as [Hbot |]. apply Hψ. Qed. - Lemma simp_equiv_or_R φ ψ : - (forall f, weight f < weight (φ ∨ ψ) -> (f ≼ simp f) * (simp f ≼ f)) -> + (simp φ ≼ φ) -> (simp ψ ≼ ψ) -> simp (φ ∨ ψ) ≼ (φ ∨ ψ). Proof. -intros IH. -assert (Hφ : simp φ ≼ φ ) by (apply (IH φ); simpl; lia). -assert (Hψ : simp ψ ≼ ψ ) by (apply (IH ψ); simpl; lia). +intros Hφ Hψ. simpl. unfold simp_or. case decide as []. - apply OrR2. @@ -109,20 +103,19 @@ case decide as []. Qed. Lemma simp_equiv_or φ ψ: - (forall f, weight f < weight (φ ∨ ψ) -> (f ≼ simp f) * (simp f ≼ f)) -> + (φ ≼ simp φ) * (simp φ ≼ φ) -> + (ψ ≼ simp ψ) * (simp ψ ≼ ψ) -> ((φ ∨ ψ) ≼ simp (φ ∨ ψ)) * (simp (φ ∨ ψ) ≼ (φ ∨ ψ)). Proof. -intros IH. -split; [ apply simp_equiv_or_L | apply simp_equiv_or_R] ; apply IH. +intros IHφ IHψ. +split; [ apply simp_equiv_or_L | apply simp_equiv_or_R]; try apply IHφ ; try apply IHψ. Qed. Lemma simp_equiv_and_L φ ψ : - (forall f, weight f < weight (φ ∧ ψ) -> (f ≼ simp f) * (simp f ≼ f)) -> + (φ ≼ simp φ) -> (ψ ≼ simp ψ) -> (φ ∧ ψ) ≼ simp (φ ∧ ψ). Proof. -intros IH. -assert (Hφ : φ ≼ simp φ ) by (apply (IH φ); simpl; lia). -assert (Hψ : ψ ≼ simp ψ ) by (apply (IH ψ); simpl; lia). +intros Hφ Hψ. simpl. unfold simp_and. case decide as [Hbot |]. - rewrite Hbot in Hφ. @@ -153,55 +146,52 @@ Qed. Lemma simp_equiv_and_R φ ψ : - (forall f, weight f < weight (φ ∧ ψ) -> (f ≼ simp f) * (simp f ≼ f)) -> + (simp φ ≼ φ) -> (simp ψ ≼ ψ) -> simp (φ ∧ ψ) ≼ φ ∧ ψ. Proof. - intros IH. - assert (Hφ : simp φ ≼ φ ) by (apply (IH φ); simpl; lia). - assert (Hψ : simp ψ ≼ ψ ) by (apply (IH ψ); simpl; lia). - simpl. unfold simp_and. - case decide as []. - - apply exfalso. apply ExFalso. - - case decide as []. - + apply exfalso. apply ExFalso. - + case decide as [Htop |]. - * apply AndR. - -- rewrite Htop in Hφ. - apply weakening. - eapply TopL_rev. - apply Hφ. - -- apply Hψ. - * case decide as [Htop |]. - -- apply AndR. - ++ apply Hφ. - ++ rewrite Htop in Hψ. - apply weakening. - eapply TopL_rev. - apply Hψ. - -- case decide as [ Heq | Hneq]. - ++ apply AndR; [ apply Hφ| rewrite Heq ; apply Hψ]. - ++ apply AndL. - apply AndR; [|exch 0]; apply weakening; [apply Hφ | apply Hψ]. +intros Hφ Hψ. +simpl. unfold simp_and. +case decide as []. +- apply exfalso. apply ExFalso. +- case decide as []. + + apply exfalso. apply ExFalso. + + case decide as [Htop |]. + * apply AndR. + -- rewrite Htop in Hφ. + apply weakening. + eapply TopL_rev. + apply Hφ. + -- apply Hψ. + * case decide as [Htop |]. + -- apply AndR. + ++ apply Hφ. + ++ rewrite Htop in Hψ. + apply weakening. + eapply TopL_rev. + apply Hψ. + -- case decide as [ Heq | Hneq]. + ++ apply AndR; [ apply Hφ| rewrite Heq ; apply Hψ]. + ++ apply AndL. + apply AndR; [|exch 0]; apply weakening; [apply Hφ | apply Hψ]. Qed. Lemma simp_equiv_and φ ψ: - (forall f, weight f < weight (φ ∧ ψ) -> (f ≼ simp f) * (simp f ≼ f)) -> + (φ ≼ simp φ) * (simp φ ≼ φ) -> + (ψ ≼ simp ψ) * (simp ψ ≼ ψ) -> ((φ ∧ ψ) ≼ simp (φ ∧ ψ)) * (simp (φ ∧ ψ) ≼ (φ ∧ ψ)). Proof. -intros IH. -split; [ apply simp_equiv_and_L | apply simp_equiv_and_R] ; apply IH. +intros IHφ IHψ. +split; [ apply simp_equiv_and_L | apply simp_equiv_and_R]; try apply IHφ ; try apply IHψ. Qed. Lemma simp_equiv_imp_L φ ψ : - (forall f, weight f < weight (φ → ψ) -> (f ≼ simp f) * (simp f ≼ f)) -> + (simp φ ≼ φ) -> + (ψ ≼ simp ψ) -> (φ → ψ) ≼ simp (φ → ψ). Proof. -intros IH. -assert (HφR : simp φ ≼ φ) by (apply (IH φ); simpl; lia). -assert (HφL : φ ≼ simp φ) by (apply (IH φ); simpl; lia). -assert (HψL: ψ ≼ simp ψ) by (apply (IH ψ); simpl; lia). +intros HφR HψL. simpl. unfold simp_imp. case decide as [Htop |]. - rewrite Htop in HφR. @@ -221,12 +211,11 @@ case decide as [Htop |]. Qed. Lemma simp_equiv_imp_R φ ψ : - (forall f, weight f < weight (φ → ψ) -> (f ≼ simp f) * ( simp f ≼ f)) -> + (φ ≼ simp φ) -> + (simp ψ ≼ ψ) -> simp (φ → ψ) ≼ (φ → ψ). Proof. -intros IH. -assert (HφL : φ ≼ simp φ) by (apply (IH φ); simpl; lia). -assert (HψR : simp ψ ≼ ψ) by (apply (IH ψ); simpl; lia). +intros HφL HψR. simpl. unfold simp_imp. case decide as [Htop |]. - apply ImpR. @@ -248,13 +237,21 @@ Qed. Lemma simp_equiv_imp φ ψ: - (forall f, weight f < weight (φ → ψ) -> (f ≼ simp f) * (simp f ≼ f)) -> + (φ ≼ simp φ) * (simp φ ≼ φ) -> + (ψ ≼ simp ψ) * (simp ψ ≼ ψ) -> ((φ → ψ) ≼ simp (φ → ψ)) * (simp (φ → ψ) ≼ (φ → ψ)). Proof. -intros IH. -split; [ apply simp_equiv_imp_L | apply simp_equiv_imp_R] ; apply IH. +intros IHφ IHψ. +split; [ apply simp_equiv_imp_L | apply simp_equiv_imp_R]; try apply IHφ ; try apply IHψ. Qed. +Lemma tmp a b c : + c <= S b -> + a < c -> + a <= b. +Proof. + lia. +Qed. Theorem simp_equiv φ : (φ ≼ (simp φ)) * ((simp φ) ≼ φ). @@ -263,14 +260,25 @@ remember (weight φ) as w. assert(Hle : weight φ ≤ w) by lia. clear Heqw. revert φ Hle. induction w; intros φ Hle; [destruct φ ; simpl in Hle; lia|]. -destruct φ; simpl; try (split ; apply generalised_axiom); +destruct φ; simpl; try (split ; apply generalised_axiom); [eapply (simp_equiv_and φ1 φ2)| eapply (simp_equiv_or φ1 φ2)| - eapply (simp_equiv_imp φ1 φ2)]; -intros f H; apply IHw; lia. +eapply (simp_equiv_imp φ1 φ2)]; apply IHw. +- assert (Hφ1w: weight φ1 < weight (φ1 ∧ φ2)) by (simpl; lia). + lia. +- assert (Hφ1w: weight φ2 < weight (φ1 ∧ φ2)) by (simpl; lia). + lia. +- assert (Hφ1w: weight φ1 < weight (φ1 ∨ φ2)) by (simpl; lia). + lia. +- assert (Hφ1w: weight φ2 < weight (φ1 ∨ φ2)) by (simpl; lia). + lia. +- assert (Hφ1w: weight φ1 < weight (φ1 → φ2)) by (simpl; lia). + lia. +- assert (Hφ1w: weight φ2 < weight (φ1 → φ2)) by (simpl; lia). + lia. Qed. Require Import ISL.PropQuantifiers. -Definition E_simplified (ψ : form) := Ef (simp ψ). -Definition A_simplified (ψ : form) := Af (simp ψ). +Definition E_simplified (p:variable) (ψ: form) := simp (Ef p ψ). +Definition A_simplified (p: variable) (ψ: form) := simp (Af p ψ). From 96b8e64db28d60a867df8fd3652a5bc6787e6a36 Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Wed, 19 Jun 2024 16:50:44 +0200 Subject: [PATCH 18/29] admit cut for isl and simplify a -> a to top --- theories/iSL/Simp.v | 52 +++++++++++++++++++++++++++------------------ 1 file changed, 31 insertions(+), 21 deletions(-) diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index 07628fb..ad9736f 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -2,7 +2,9 @@ Require Import ISL.SequentProps. Require Import ISL.Sequents. Require Import ISL.Environments. + Definition simp_or φ ψ := + if decide (φ = ⊥) then ψ else if decide (ψ = ⊥) then φ else if decide (φ = ⊤) then ⊤ @@ -22,6 +24,7 @@ Definition simp_and φ ψ := Definition simp_imp φ ψ := if decide (φ = ⊤) then ψ else if decide (φ = ⊥) then ⊤ + else if decide (φ = ψ) then ⊤ else φ → ψ. Fixpoint simp φ := match φ with @@ -42,6 +45,12 @@ Proof. apply ImpR. apply ExFalso. Qed. + +Theorem cut Γ φ ψ θ: + Γ • φ ⊢ ψ -> Γ • ψ ⊢ θ -> + Γ • φ ⊢ θ. +Admitted. + Lemma simp_equiv_or_L φ ψ : (φ ≼ simp φ) -> (ψ ≼ simp ψ) -> (φ ∨ ψ) ≼ simp (φ ∨ ψ). @@ -202,12 +211,15 @@ case decide as [Htop |]. - case decide as []. + apply weakening. apply top_provable. - + apply ImpR. - exch 0. - apply ImpL. - * apply weakening. apply HφR. - * exch 0. apply weakening. - apply HψL. + + case decide as []. + * apply ImpR. + apply ExFalso. + * apply ImpR. + exch 0. + apply ImpL. + -- apply weakening. apply HφR. + -- exch 0. apply weakening. + apply HψL. Qed. Lemma simp_equiv_imp_R φ ψ : @@ -227,15 +239,21 @@ case decide as [Htop |]. apply exfalso. exch 0. apply weakening. apply HφL. - + apply ImpR. - exch 0. - apply ImpL. - * apply weakening. apply HφL. - * exch 0. apply weakening. - apply HψR. + + case decide as [Heq |]. + * apply ImpR. + exch 0. apply weakening. + rewrite <- Heq in HψR. + eapply cut. + -- apply HφL. + -- apply HψR. + * apply ImpR. + exch 0. + apply ImpL. + -- apply weakening. apply HφL. + -- exch 0. apply weakening. + apply HψR. Qed. - Lemma simp_equiv_imp φ ψ: (φ ≼ simp φ) * (simp φ ≼ φ) -> (ψ ≼ simp ψ) * (simp ψ ≼ ψ) -> @@ -245,14 +263,6 @@ intros IHφ IHψ. split; [ apply simp_equiv_imp_L | apply simp_equiv_imp_R]; try apply IHφ ; try apply IHψ. Qed. -Lemma tmp a b c : - c <= S b -> - a < c -> - a <= b. -Proof. - lia. -Qed. - Theorem simp_equiv φ : (φ ≼ (simp φ)) * ((simp φ) ≼ φ). Proof. From f152239781aa569f5f8e2f1f0e4cba60628cab50 Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Thu, 20 Jun 2024 12:21:47 +0200 Subject: [PATCH 19/29] add simplification benchmarks --- bin/bench.ml | 63 +++++++++++++++++++++++++++ bin/dune | 5 ++- theories/extraction/UIML_extraction.v | 10 ++++- theories/iSL/Simp.v | 1 - 4 files changed, 74 insertions(+), 5 deletions(-) create mode 100644 bin/bench.ml diff --git a/bin/bench.ml b/bin/bench.ml new file mode 100644 index 0000000..e19e987 --- /dev/null +++ b/bin/bench.ml @@ -0,0 +1,63 @@ +open UIML.UIML_extraction +open UIML.Formulas +open Modal_expressions_parser + +let rec weight = function + | Bot -> 1 + | Var _ -> 1 + | And (f1, f2) -> 2 + weight f1 + weight f2 + | Or (f1, f2) -> 3 + weight f1 + weight f2 + | Implies (f1, f2) -> 1 + weight f1 + weight f2 + | Box f -> 1 + weight f + +type bench_info = { name : string; before : int; after : int } + +let percentage_reduction before after = + 100. -. (float_of_int after /. float_of_int before *. 100.) + +let print_results { name; before; after } = + Printf.printf "| %s | %d | %d | %.2f |\n" name before after + (percentage_reduction before after) + +let bench_one fs = + let f = eval fs in + [ + { + name = "A " ^ fs; + before = weight (isl_A [ 'p' ] f); + after = weight (isl_simplified_A [ 'p' ] f); + }; + { + name = "E " ^ fs; + before = weight (isl_E [ 'p' ] f); + after = weight (isl_simplified_E [ 'p' ] f); + }; + ] + +let bench l = + let benches = List.map bench_one l |> List.flatten in + Printf.printf + "| Formula | Before | After | Percentage reduction |\n|--|--|--|--|\n"; + List.iter print_results benches; + print_newline (); + let total, len = + List.fold_left + (fun (total, len) { before; after; _ } -> + (percentage_reduction before after +. total, len + 1)) + (0., 0) benches + in + Printf.printf "Average percentage reduction: %.2f\n" + (total /. float_of_int len) + +let test_cases = + [ + "(q -> p) & (p -> ~r)"; + "(q -> (p -> r)) -> r"; + "((q -> p) -> r) -> r"; + "(a → (q ∧ r)) → s"; + "(a → (q ∧ r)) → ~p"; + "(a → (q ∧ r)) → ~p → k"; + "(q → (q ∧ (k -> p)) -> k)"; + ] + +let _ = bench test_cases diff --git a/bin/dune b/bin/dune index fea33d5..25195d4 100644 --- a/bin/dune +++ b/bin/dune @@ -1,5 +1,6 @@ -(executable - (name uiml_demo) +(executables + (public_names uiml_demo bench) + (names uiml_demo bench) (modes js native) (preprocess (pps js_of_ocaml-ppx)) (libraries js_of_ocaml UIML angstrom)) diff --git a/theories/extraction/UIML_extraction.v b/theories/extraction/UIML_extraction.v index 03727e2..e44ec5d 100644 --- a/theories/extraction/UIML_extraction.v +++ b/theories/extraction/UIML_extraction.v @@ -10,6 +10,8 @@ Require Import K.Interpolation.UIK_braga. Require Import KS_export. Require Import ISL.PropQuantifiers. +Require Import ISL.Simp. + Fixpoint MPropF_of_form (f : Formulas.form) : MPropF := match f with | Formulas.Var n => Var n @@ -32,9 +34,13 @@ end. Definition gl_UI p s := form_of_MPropF (proj1_sig (GL.Interpolation.UIGL_braga.GUI_tot p ([],[MPropF_of_form s]))). Definition k_UI p s := form_of_MPropF(proj1_sig (K.Interpolation.UIK_braga.GUI_tot p ([],[MPropF_of_form s]))). -Definition isl_E v f :=Ef v f. +Definition isl_E v f := Ef v f. Definition isl_A v f := Af v f. -Separate Extraction gl_UI k_UI isl_E isl_A. + +Definition isl_simplified_E v f := E_simplified v f. +Definition isl_simplified_A v f := A_simplified v f. + +Separate Extraction gl_UI k_UI isl_E isl_A isl_simplified_E isl_simplified_A. Cd "..". diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index ad9736f..793c257 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -45,7 +45,6 @@ Proof. apply ImpR. apply ExFalso. Qed. - Theorem cut Γ φ ψ θ: Γ • φ ⊢ ψ -> Γ • ψ ⊢ θ -> Γ • φ ⊢ θ. From 6882e85408853f801c919224b90f809f5a0fd427 Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Thu, 20 Jun 2024 16:41:18 +0200 Subject: [PATCH 20/29] add small set of unit test for simplification --- theories/iSL/Simp.v | 33 +++++++++++++++++++++++++++++++-- 1 file changed, 31 insertions(+), 2 deletions(-) diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index 793c257..397de7e 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -289,5 +289,34 @@ Qed. Require Import ISL.PropQuantifiers. -Definition E_simplified (p:variable) (ψ: form) := simp (Ef p ψ). -Definition A_simplified (p: variable) (ψ: form) := simp (Af p ψ). +Definition E_simplified (p: variable) (ψ: form) := simp (Ef p ψ). +Definition A_simplified (p: variable) (ψ: form) := simp (Af p ψ). + + +Require Import String. + +Local Open Scope string_scope. + +Example ex1: simp (Implies (Var "a") (And (Var "b") (Var "b" ))) = Implies (Var "a") (Var "b"). +Proof. reflexivity. Qed. + + +Example ex2: simp (Implies (Var "a") (Or (Var "b") (Var "b" ))) = Implies (Var "a") (Var "b"). +Proof. reflexivity. Qed. + + +Example ex3: simp (Implies (Var "a") (Var "a")) = Implies Bot Bot. +Proof. reflexivity. Qed. + + +Example ex4: simp (Or (Implies (Var "a") (Var "a")) (Implies (Var "a") (Var "a"))) = Implies Bot Bot. +Proof. reflexivity. Qed. + +Example ex5: simp (And (Implies (Var "a") (Var "a")) (Implies (Var "a") (Var "a"))) = Implies Bot Bot. +Proof. reflexivity. Qed. + + +Example ex6: simp ((Implies (Implies (Implies (Implies (Implies (Var "r") (Var "r")) (Or (And (Var "r") (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (Implies (Var "r") (Var "r")) (Var "r")))) (Var "r")) (Or (And (Implies (Implies (Var "r") (Var "r")) (Or (And (Var "r") (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (Implies (Var "r") (Var "r")) (Var "r")))) (Or (Implies (Var "q") (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "q") (Var "r")))) (Implies (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q"))) (Or (Or (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "q") (Var "r"))) (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q"))) (Var "r")))))) (Implies (And (Implies (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (And (Implies (Var "r") (Var "r")) (Var "q"))) (Or (Or (And (Var "r") (Or (Or (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "q") (Var "r"))) (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q"))) (Var "r")))) (Or (And (Var "r") (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (Implies (Var "r") (Var "r")) (Var "r")))) (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (And (Implies (Var "r") (Var "r")) (Var "q"))) (Var "r")))) (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (And (Implies (Implies (Implies (Var "r") (Var "r")) (Or (And (Var "r") (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (Implies (Var "r") (Var "r")) (Var "r")))) (Var "r")) (Var "q"))) (Or (Or (And (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (And (Implies (Var "r") (Var "r")) (Var "q"))) (Or (Or (And (Var "r") (Or (Or (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "q") (Var "r"))) (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q"))) (Var "r")))) (Or (And (Var "r") (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (Implies (Var "r") (Var "r")) (Var "r")))) (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (And (Implies (Var "r") (Var "r")) (Var "q"))) (Var "r")))) (Or (Or (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "q") (Var "r"))) (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q"))) (Var "r")))) (Or (And (Implies (Implies (Var "r") (Var "r")) (Or (And (Var "r") (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (Implies (Var "r") (Var "r")) (Var "r")))) (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (Implies (Implies (Implies (Var "r") (Var "r")) (Or (And (Var "r") (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (Implies (Var "r") (Var "r")) (Var "r")))) (Var "r")) (Or (And (Implies (Implies (Var "r") (Var "r")) (Or (And (Var "r") (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (Implies (Var "r") (Var "r")) (Var "r")))) (Var "r")) (Var "r"))))) (Implies (And (Implies (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (And (Implies (Var "r") (Var "r")) (Var "q"))) (Or (Or (And (Var "r") (Or (Or (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "q") (Var "r"))) (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q"))) (Var "r")))) (Or (And (Var "r") (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (Implies (Var "r") (Var "r")) (Var "r")))) (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (And (Implies (Var "r") (Var "r")) (Var "q"))) (Var "r")))) (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (And (Implies (Implies (Implies (Var "r") (Var "r")) (Or (And (Var "r") (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (Implies (Var "r") (Var "r")) (Var "r")))) (Var "r")) (Var "q"))) (Or (Or (And (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (And (Implies (Var "r") (Var "r")) (Var "q"))) (Or (Or (And (Var "r") (Or (Or (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "q") (Var "r"))) (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q"))) (Var "r")))) (Or (And (Var "r") (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (Implies (Var "r") (Var "r")) (Var "r")))) (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (And (Implies (Var "r") (Var "r")) (Var "q"))) (Var "r")))) (Var "r")) (Or (And (Implies (Implies (Var "r") (Var "r")) (Or (And (Var "r") (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (Implies (Var "r") (Var "r")) (Var "r")))) (Var "r")) (Var "r"))) (Var "r"))))))) (Var "r"))) + = (Implies (Or (And (Var "r") (Or (Implies (Var "q") (Or (Var "r") (Implies (Var "q") (Var "r")))) (Implies (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q"))) (Implies (Bot) (Bot))))) (Implies (And (Implies (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (Var "q")) (Or (Var "r") (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (Var "q")) (Var "r")))) (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (Var "q")) (Or (Or (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (Var "q")) (Or (Var "r") (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (Var "q")) (Var "r")))) (Var "r")) (Implies (And (Implies (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (Var "q")) (Or (Var "r") (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (Var "q")) (Var "r")))) (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (Var "q")) (Or (Or (And (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (Var "q")) (Or (Var "r") (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (Var "q")) (Var "r")))) (Var "r")) (Var "r")) (Var "r")))))) (Var "r")). +Proof. reflexivity. Qed. + From 1df8ed117510033681f712ab01b5f7c4eb588269 Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Fri, 21 Jun 2024 12:23:31 +0200 Subject: [PATCH 21/29] Prove that simp respects uniform interpolation. A lemma (that the variables of the simplification are a subset of the initial formula) has been admitted for now. --- theories/iSL/Simp.v | 54 +++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 52 insertions(+), 2 deletions(-) diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index 397de7e..1a2c66e 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -2,9 +2,7 @@ Require Import ISL.SequentProps. Require Import ISL.Sequents. Require Import ISL.Environments. - Definition simp_or φ ψ := - if decide (φ = ⊥) then ψ else if decide (ψ = ⊥) then φ else if decide (φ = ⊤) then ⊤ @@ -293,6 +291,58 @@ Definition E_simplified (p: variable) (ψ: form) := simp (Ef p ψ). Definition A_simplified (p: variable) (ψ: form) := simp (Af p ψ). +Lemma vars_incl_simp φ V : + vars_incl φ V -> vars_incl (simp φ) V. +Proof. +Admitted. + +Theorem iSL_uniform_interpolation_simp p V: p ∉ V -> + ∀ φ, vars_incl φ (p :: V) -> + (vars_incl (E_simplified p φ) V) + * (φ ≼ E_simplified p φ) + * (∀ ψ, vars_incl ψ V -> (φ ≼ ψ) -> E_simplified p φ ≼ ψ) + * (vars_incl (A_simplified p φ) V) + * (A_simplified p φ ≼ φ) + * (∀ θ, vars_incl θ V -> (θ ≼ φ) -> (θ ≼ A_simplified p φ)). +Proof. + +intros Hp φ Hvarsφ. +assert (Hislφ : + (vars_incl (Ef p φ) V) + * ({[φ]} ⊢ (Ef p φ)) + * (∀ ψ, vars_incl ψ V -> {[φ]} ⊢ ψ -> {[Ef p φ]} ⊢ ψ) + * (vars_incl (Af p φ) V) + * ({[Af p φ]} ⊢ φ) + * (∀ θ, vars_incl θ V -> {[θ]} ⊢ φ -> {[θ]} ⊢ Af p φ)) by + (apply iSL_uniform_interpolation; [apply Hp | apply Hvarsφ]). +repeat split. + + + intros Hx. + eapply vars_incl_simp. + apply Hislφ. + + eapply cut. + * assert (Hef: ({[φ]} ⊢ Ef p φ)) by apply Hislφ. + peapply Hef. + * apply (simp_equiv (Ef p φ)). + + intros ψ Hψ Hyp. + eapply cut. + * apply (simp_equiv (Ef p φ)). + * assert (Hef: ({[Ef p φ]} ⊢ ψ)) by (apply Hislφ; [apply Hψ | peapply Hyp]). + peapply Hef. + + intros Hx. + eapply vars_incl_simp. + apply Hislφ. + + eapply cut. + * apply (simp_equiv (Af p φ)). + * assert (Hef: ({[Af p φ]} ⊢ φ)) by apply Hislφ. + peapply Hef. + + intros ψ Hψ Hyp. + eapply cut. + * assert (Hef: ({[ψ]} ⊢ Af p φ)) by (apply Hislφ; [apply Hψ | peapply Hyp]). + peapply Hef. + * apply (simp_equiv (Af p φ)). +Qed. + Require Import String. Local Open Scope string_scope. From 8289140d9d424511aa5d3324e3434e69bf65cb69 Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Fri, 21 Jun 2024 14:10:22 +0200 Subject: [PATCH 22/29] Simplify iSL_uniform_interpolation_simp proof --- theories/iSL/Simp.v | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index 1a2c66e..87ebac0 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -293,7 +293,6 @@ Definition A_simplified (p: variable) (ψ: form) := simp (Af p ψ). Lemma vars_incl_simp φ V : vars_incl φ V -> vars_incl (simp φ) V. -Proof. Admitted. Theorem iSL_uniform_interpolation_simp p V: p ∉ V -> @@ -316,7 +315,6 @@ assert (Hislφ : * (∀ θ, vars_incl θ V -> {[θ]} ⊢ φ -> {[θ]} ⊢ Af p φ)) by (apply iSL_uniform_interpolation; [apply Hp | apply Hvarsφ]). repeat split. - + intros Hx. eapply vars_incl_simp. apply Hislφ. @@ -334,8 +332,7 @@ repeat split. apply Hislφ. + eapply cut. * apply (simp_equiv (Af p φ)). - * assert (Hef: ({[Af p φ]} ⊢ φ)) by apply Hislφ. - peapply Hef. + * peapply Hislφ. + intros ψ Hψ Hyp. eapply cut. * assert (Hef: ({[ψ]} ⊢ Af p φ)) by (apply Hislφ; [apply Hψ | peapply Hyp]). From 9d6008db8ac80c2232922085049af57dbd999131 Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Wed, 26 Jun 2024 11:01:21 +0200 Subject: [PATCH 23/29] benchmark computation time --- bin/bench.ml | 101 ++++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 80 insertions(+), 21 deletions(-) diff --git a/bin/bench.ml b/bin/bench.ml index e19e987..5dbe73f 100644 --- a/bin/bench.ml +++ b/bin/bench.ml @@ -10,47 +10,106 @@ let rec weight = function | Implies (f1, f2) -> 1 + weight f1 + weight f2 | Box f -> 1 + weight f -type bench_info = { name : string; before : int; after : int } +type 'a timed_result = { value : 'a; time : float } -let percentage_reduction before after = - 100. -. (float_of_int after /. float_of_int before *. 100.) +type bench_info = { + name : string; + before : int timed_result; + after : int timed_result; +} -let print_results { name; before; after } = - Printf.printf "| %s | %d | %d | %.2f |\n" name before after - (percentage_reduction before after) +let percentage_reduction before after = 100. -. (after /. before *. 100.) +let percentage_increase before after = (after /. before *. 100.) -. 100. + +let time f x = + let attempts = 20 in + let total, value, _ = + List.init attempts (fun _ -> ()) + (* Run the tests `attempts` times *) + |> List.map (fun _ -> + let t = Sys.time () in + let fx = f x in + { value = fx; time = Sys.time () -. t }) + (* Sort them by execution time *) + |> List.sort (fun result1 result2 -> compare result1.time result2.time) + (* Compute the average time removing the slowest and fastest times *) + |> List.fold_left + (fun (total, _, len) { value; time } -> + if len >= 1 && len < attempts - 1 then (total +. time, value, len + 1) + else (total, value, len + 1)) + (0., 0, 0) + in + { value; time = total /. float_of_int (attempts - 2) } + +let print_value_results { name; before; after } = + Printf.printf "| %s | %d | %d | %.2f |\n" name before.value after.value + (percentage_reduction + (float_of_int before.value) + (float_of_int after.value)) + +let print_time_results { name; before; after } = + Printf.printf "| %s | %.4f | %.4f | %.2f |\n" name before.time after.time + (percentage_increase before.time after.time) let bench_one fs = let f = eval fs in [ { name = "A " ^ fs; - before = weight (isl_A [ 'p' ] f); - after = weight (isl_simplified_A [ 'p' ] f); + before = time (fun f -> weight (isl_A [ 'p' ] f)) f; + after = time (fun f -> weight (isl_simplified_A [ 'p' ] f)) f; }; { name = "E " ^ fs; - before = weight (isl_E [ 'p' ] f); - after = weight (isl_simplified_E [ 'p' ] f); + before = time (fun f -> weight (isl_E [ 'p' ] f)) f; + after = time (fun f -> weight (isl_simplified_E [ 'p' ] f)) f; }; ] -let bench l = - let benches = List.map bench_one l |> List.flatten in - Printf.printf - "| Formula | Before | After | Percentage reduction |\n|--|--|--|--|\n"; - List.iter print_results benches; - print_newline (); +let average f l = let total, len = - List.fold_left - (fun (total, len) { before; after; _ } -> - (percentage_reduction before after +. total, len + 1)) - (0., 0) benches + List.fold_left (fun (total, len) e -> (f e +. total, len + 1)) (0., 0) l in + total /. float_of_int len + +let print_bench_value_info benches = + Printf.printf + "| Formula | Interpolant weight | Simplified interpolant weight | \ + Percentage reduction |\n\ + |--|--|--|--|\n"; + List.iter print_value_results benches; + print_newline (); Printf.printf "Average percentage reduction: %.2f\n" - (total /. float_of_int len) + (average + (fun { before; after; _ } -> + percentage_reduction + (float_of_int before.value) + (float_of_int after.value)) + benches) + +let print_bench_time_info benches = + Printf.printf + "| Formula | Interpolant computation time (s) | Simplified interpolant \ + computation time (s) | Percentage increase |\n\ + |--|--|--|--|\n"; + List.iter print_time_results benches; + print_newline (); + Printf.printf "Average percentage increase: %.2f\n" + (average + (fun { before; after; _ } -> percentage_increase before.time after.time) + benches); + Printf.printf "Average absolute time increase (s): %.5f\n" + (average (fun { before; after; _ } -> after.time -. before.time) benches) + +let bench l = + let benches = List.map bench_one l |> List.flatten in + print_bench_value_info benches; + print_newline (); + print_bench_time_info benches let test_cases = [ + "t ∨ q ∨ t"; "(q -> p) & (p -> ~r)"; "(q -> (p -> r)) -> r"; "((q -> p) -> r) -> r"; From d0044f3f8222c7c137e4649e8a69afef71251814 Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Wed, 26 Jun 2024 15:11:06 +0200 Subject: [PATCH 24/29] Benchmark execution time only once and add more tests --- bin/bench.ml | 29 +++++++++++------------------ 1 file changed, 11 insertions(+), 18 deletions(-) diff --git a/bin/bench.ml b/bin/bench.ml index 5dbe73f..61be81e 100644 --- a/bin/bench.ml +++ b/bin/bench.ml @@ -22,24 +22,9 @@ let percentage_reduction before after = 100. -. (after /. before *. 100.) let percentage_increase before after = (after /. before *. 100.) -. 100. let time f x = - let attempts = 20 in - let total, value, _ = - List.init attempts (fun _ -> ()) - (* Run the tests `attempts` times *) - |> List.map (fun _ -> - let t = Sys.time () in - let fx = f x in - { value = fx; time = Sys.time () -. t }) - (* Sort them by execution time *) - |> List.sort (fun result1 result2 -> compare result1.time result2.time) - (* Compute the average time removing the slowest and fastest times *) - |> List.fold_left - (fun (total, _, len) { value; time } -> - if len >= 1 && len < attempts - 1 then (total +. time, value, len + 1) - else (total, value, len + 1)) - (0., 0, 0) - in - { value; time = total /. float_of_int (attempts - 2) } + let t = Sys.time () in + let fx = f x in + { value = fx; time = Sys.time () -. t } let print_value_results { name; before; after } = Printf.printf "| %s | %d | %d | %.2f |\n" name before.value after.value @@ -109,14 +94,22 @@ let bench l = let test_cases = [ + "(p ∧ q) -> ~p"; "t ∨ q ∨ t"; + "~((F & p) -> ~p | F)"; "(q -> p) & (p -> ~r)"; "(q -> (p -> r)) -> r"; "((q -> p) -> r) -> r"; "(a → (q ∧ r)) → s"; "(a → (q ∧ r)) → ~p"; "(a → (q ∧ r)) → ~p → k"; + "(q -> (p -> r)) -> ~t"; + "(q -> (p -> r)) -> ~t"; "(q → (q ∧ (k -> p)) -> k)"; + "(q -> (p ∨ r)) -> ~(t ∨ p)"; + "((q -> (p ∨ r)) ∧ (t -> p)) -> t"; + "((~t -> (q ∧ p)) ∧ (t -> p)) -> t"; + "(~p ∧ q) -> (p ∨ r -> t) -> o"; ] let _ = bench test_cases From ca0db835e17dd86ba0a5cb46a0f3add88ca0eae0 Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Thu, 27 Jun 2024 10:29:29 +0200 Subject: [PATCH 25/29] Progress on the simplification is interpolant proof --- theories/iSL/Simp.v | 118 ++++++++++++++++++++++++++++++++++++++------ 1 file changed, 104 insertions(+), 14 deletions(-) diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index 87ebac0..84806cb 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -270,19 +270,13 @@ induction w; intros φ Hle; [destruct φ ; simpl in Hle; lia|]. destruct φ; simpl; try (split ; apply generalised_axiom); [eapply (simp_equiv_and φ1 φ2)| eapply (simp_equiv_or φ1 φ2)| -eapply (simp_equiv_imp φ1 φ2)]; apply IHw. -- assert (Hφ1w: weight φ1 < weight (φ1 ∧ φ2)) by (simpl; lia). - lia. -- assert (Hφ1w: weight φ2 < weight (φ1 ∧ φ2)) by (simpl; lia). - lia. -- assert (Hφ1w: weight φ1 < weight (φ1 ∨ φ2)) by (simpl; lia). - lia. -- assert (Hφ1w: weight φ2 < weight (φ1 ∨ φ2)) by (simpl; lia). - lia. -- assert (Hφ1w: weight φ1 < weight (φ1 → φ2)) by (simpl; lia). - lia. -- assert (Hφ1w: weight φ2 < weight (φ1 → φ2)) by (simpl; lia). - lia. +eapply (simp_equiv_imp φ1 φ2)]; apply IHw; +[assert (Hφ1w: weight φ1 < weight (φ1 ∧ φ2))| +assert (Hφ1w: weight φ2 < weight (φ1 ∧ φ2))| +assert (Hφ1w: weight φ1 < weight (φ1 ∨ φ2))| +assert (Hφ1w: weight φ2 < weight (φ1 ∨ φ2))| +assert (Hφ1w: weight φ1 < weight (φ1 → φ2))| +assert (Hφ1w: weight φ2 < weight (φ1 → φ2))]; simpl; lia. Qed. Require Import ISL.PropQuantifiers. @@ -290,10 +284,106 @@ Require Import ISL.PropQuantifiers. Definition E_simplified (p: variable) (ψ: form) := simp (Ef p ψ). Definition A_simplified (p: variable) (ψ: form) := simp (Af p ψ). +Lemma bot_vars_incl V: +vars_incl ⊥ V. +Proof. + intros x H. + unfold In. + induction V; auto. +Qed. + + +Lemma top_vars_incl V: +vars_incl ⊤ V. +Proof. + intros x H. + unfold In. + induction V. + - unfold occurs_in in H. + lia. + - auto. +Qed. + +Lemma and_vars_incl_L φ ψ V: + vars_incl (And φ ψ) V -> + vars_incl φ V * vars_incl ψ V. +Proof. + intros H. + split; intros x H1; apply H; simpl; auto. +Qed. + + +Lemma and_vars_incl_R φ ψ V: + vars_incl φ V -> + vars_incl ψ V -> + vars_incl (And φ ψ) V. +Proof. + intros H1 H2. + intros x H. + Admitted. Lemma vars_incl_simp φ V : vars_incl φ V -> vars_incl (simp φ) V. -Admitted. +Proof. +intro H. +induction φ; auto. +- simpl. unfold simp_and. + case decide as []. + + apply bot_vars_incl. + + case decide as []. + * apply bot_vars_incl. + * case decide as []. + -- apply IHφ2. + eapply and_vars_incl_L. + apply H. + -- case decide as []. + ++ apply IHφ1. + apply (and_vars_incl_L _ φ2). + apply H. + ++ case decide as []. + ** apply IHφ1. + apply (and_vars_incl_L _ φ2). + apply H. + ** apply and_vars_incl_R; + [ apply IHφ1; apply (and_vars_incl_L _ φ2)| + apply IHφ2; eapply and_vars_incl_L]; + apply H. +- simpl. unfold simp_or. + case decide as []. + + apply IHφ2. + eapply and_vars_incl_L. + apply H. + + case decide as []. + * apply IHφ1. + apply (and_vars_incl_L _ φ2). + apply H. + * case decide as []. + -- apply top_vars_incl. + -- case decide as []. + ++ apply top_vars_incl. + ++ case decide as []. + ** apply IHφ1. + apply (and_vars_incl_L _ φ2). + apply H. + ** apply and_vars_incl_R; + [ apply IHφ1; apply (and_vars_incl_L _ φ2)| + apply IHφ2; eapply and_vars_incl_L]; + apply H. + +- simpl. unfold simp_imp. + case decide as []. + + apply IHφ2. + eapply and_vars_incl_L. + apply H. + + case decide as []. + * apply top_vars_incl. + * case decide as []. + -- apply top_vars_incl. + -- apply and_vars_incl_R; + [ apply IHφ1; apply (and_vars_incl_L _ φ2)| + apply IHφ2; eapply and_vars_incl_L]; + apply H. +Qed. Theorem iSL_uniform_interpolation_simp p V: p ∉ V -> ∀ φ, vars_incl φ (p :: V) -> From ce7063a0c62f01a0155df821d4de9f8b34662628 Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Fri, 28 Jun 2024 11:15:31 +0200 Subject: [PATCH 26/29] Complete proof of iSL_uniform_interpolation_simp --- theories/iSL/Simp.v | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index 84806cb..3f31234 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -318,9 +318,10 @@ Lemma and_vars_incl_R φ ψ V: vars_incl ψ V -> vars_incl (And φ ψ) V. Proof. - intros H1 H2. - intros x H. - Admitted. + unfold vars_incl. + simpl. + intuition. +Qed. Lemma vars_incl_simp φ V : vars_incl φ V -> vars_incl (simp φ) V. @@ -451,9 +452,3 @@ Proof. reflexivity. Qed. Example ex5: simp (And (Implies (Var "a") (Var "a")) (Implies (Var "a") (Var "a"))) = Implies Bot Bot. Proof. reflexivity. Qed. - - -Example ex6: simp ((Implies (Implies (Implies (Implies (Implies (Var "r") (Var "r")) (Or (And (Var "r") (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (Implies (Var "r") (Var "r")) (Var "r")))) (Var "r")) (Or (And (Implies (Implies (Var "r") (Var "r")) (Or (And (Var "r") (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (Implies (Var "r") (Var "r")) (Var "r")))) (Or (Implies (Var "q") (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "q") (Var "r")))) (Implies (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q"))) (Or (Or (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "q") (Var "r"))) (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q"))) (Var "r")))))) (Implies (And (Implies (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (And (Implies (Var "r") (Var "r")) (Var "q"))) (Or (Or (And (Var "r") (Or (Or (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "q") (Var "r"))) (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q"))) (Var "r")))) (Or (And (Var "r") (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (Implies (Var "r") (Var "r")) (Var "r")))) (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (And (Implies (Var "r") (Var "r")) (Var "q"))) (Var "r")))) (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (And (Implies (Implies (Implies (Var "r") (Var "r")) (Or (And (Var "r") (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (Implies (Var "r") (Var "r")) (Var "r")))) (Var "r")) (Var "q"))) (Or (Or (And (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (And (Implies (Var "r") (Var "r")) (Var "q"))) (Or (Or (And (Var "r") (Or (Or (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "q") (Var "r"))) (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q"))) (Var "r")))) (Or (And (Var "r") (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (Implies (Var "r") (Var "r")) (Var "r")))) (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (And (Implies (Var "r") (Var "r")) (Var "q"))) (Var "r")))) (Or (Or (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "q") (Var "r"))) (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q"))) (Var "r")))) (Or (And (Implies (Implies (Var "r") (Var "r")) (Or (And (Var "r") (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (Implies (Var "r") (Var "r")) (Var "r")))) (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (Implies (Implies (Implies (Var "r") (Var "r")) (Or (And (Var "r") (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (Implies (Var "r") (Var "r")) (Var "r")))) (Var "r")) (Or (And (Implies (Implies (Var "r") (Var "r")) (Or (And (Var "r") (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (Implies (Var "r") (Var "r")) (Var "r")))) (Var "r")) (Var "r"))))) (Implies (And (Implies (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (And (Implies (Var "r") (Var "r")) (Var "q"))) (Or (Or (And (Var "r") (Or (Or (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "q") (Var "r"))) (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q"))) (Var "r")))) (Or (And (Var "r") (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (Implies (Var "r") (Var "r")) (Var "r")))) (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (And (Implies (Var "r") (Var "r")) (Var "q"))) (Var "r")))) (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (And (Implies (Implies (Implies (Var "r") (Var "r")) (Or (And (Var "r") (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (Implies (Var "r") (Var "r")) (Var "r")))) (Var "r")) (Var "q"))) (Or (Or (And (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (And (Implies (Var "r") (Var "r")) (Var "q"))) (Or (Or (And (Var "r") (Or (Or (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "q") (Var "r"))) (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q"))) (Var "r")))) (Or (And (Var "r") (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (Implies (Var "r") (Var "r")) (Var "r")))) (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (And (Implies (Var "r") (Var "r")) (Var "q"))) (Var "r")))) (Var "r")) (Or (And (Implies (Implies (Var "r") (Var "r")) (Or (And (Var "r") (Or (Implies (Implies (Bot) (Bot)) (Var "r")) (Implies (Var "r") (Var "r")))) (Implies (Implies (Var "r") (Var "r")) (Var "r")))) (Var "r")) (Var "r"))) (Var "r"))))))) (Var "r"))) - = (Implies (Or (And (Var "r") (Or (Implies (Var "q") (Or (Var "r") (Implies (Var "q") (Var "r")))) (Implies (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q"))) (Implies (Bot) (Bot))))) (Implies (And (Implies (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (Var "q")) (Or (Var "r") (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (Var "q")) (Var "r")))) (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (Var "q")) (Or (Or (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (Var "q")) (Or (Var "r") (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (Var "q")) (Var "r")))) (Var "r")) (Implies (And (Implies (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (Var "q")) (Or (Var "r") (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (Var "q")) (Var "r")))) (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (Var "q")) (Or (Or (And (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (Var "q")) (Or (Var "r") (Implies (And (Implies (Var "r") (And (And (Var "q") (Var "r")) (And (Var "r") (Var "q")))) (Var "q")) (Var "r")))) (Var "r")) (Var "r")) (Var "r")))))) (Var "r")). -Proof. reflexivity. Qed. - From 32df79028e99f8e21fd788c0ecd1db1e394e9f84 Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Fri, 28 Jun 2024 11:57:54 +0200 Subject: [PATCH 27/29] admit a more general version of cut --- theories/iSL/Simp.v | 50 ++++++++++++++++++++++++++++++++++----------- 1 file changed, 38 insertions(+), 12 deletions(-) diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index 3f31234..b74924d 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -43,11 +43,33 @@ Proof. apply ImpR. apply ExFalso. Qed. -Theorem cut Γ φ ψ θ: - Γ • φ ⊢ ψ -> Γ • ψ ⊢ θ -> - Γ • φ ⊢ θ. +Theorem cut Γ Γ' φ ψ : + Γ ⊢ φ -> Γ' • φ ⊢ ψ -> + Γ ⊎ Γ' ⊢ ψ. Admitted. +Lemma preorder_singleton φ ψ: + {[φ]} ⊢ ψ -> (φ ≼ ψ). +Proof. +intro H. +assert (H3: (φ ≼ ψ) = ({[φ]} ⊢ ψ)) by (apply proper_Provable; ms). +rewrite H3. +apply H. +Qed. + +Corollary cut2 φ ψ θ: + (φ ≼ ψ) -> (ψ ≼ θ) -> + φ ≼ θ. +Proof. + intros H1 H2. + assert ({[φ]} ⊎ ∅ ⊢ θ). { + peapply (cut {[φ]} ∅ ψ θ). + - peapply H1. + - apply H2. + } + apply H. +Qed. + Lemma simp_equiv_or_L φ ψ : (φ ≼ simp φ) -> (ψ ≼ simp ψ) -> (φ ∨ ψ) ≼ simp (φ ∨ ψ). @@ -240,7 +262,7 @@ case decide as [Htop |]. * apply ImpR. exch 0. apply weakening. rewrite <- Heq in HψR. - eapply cut. + eapply cut2. -- apply HφL. -- apply HψR. * apply ImpR. @@ -409,25 +431,29 @@ repeat split. + intros Hx. eapply vars_incl_simp. apply Hislφ. - + eapply cut. + + eapply cut2. * assert (Hef: ({[φ]} ⊢ Ef p φ)) by apply Hislφ. - peapply Hef. + apply preorder_singleton. + apply Hef. * apply (simp_equiv (Ef p φ)). + intros ψ Hψ Hyp. - eapply cut. + eapply cut2. * apply (simp_equiv (Ef p φ)). * assert (Hef: ({[Ef p φ]} ⊢ ψ)) by (apply Hislφ; [apply Hψ | peapply Hyp]). - peapply Hef. + apply preorder_singleton. + apply Hef. + intros Hx. eapply vars_incl_simp. apply Hislφ. - + eapply cut. + + eapply cut2. * apply (simp_equiv (Af p φ)). - * peapply Hislφ. + * apply preorder_singleton. + apply Hislφ. + intros ψ Hψ Hyp. - eapply cut. + eapply cut2. * assert (Hef: ({[ψ]} ⊢ Af p φ)) by (apply Hislφ; [apply Hψ | peapply Hyp]). - peapply Hef. + apply preorder_singleton. + apply Hef. * apply (simp_equiv (Af p φ)). Qed. From 0dc6a6eacf623644c8f2f4ebd82e3e8f83e29eb4 Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Fri, 28 Jun 2024 12:27:00 +0200 Subject: [PATCH 28/29] Use the simplification function for iSL interpolants on the demo --- bin/uiml_demo.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/bin/uiml_demo.ml b/bin/uiml_demo.ml index 4c6e983..119ab38 100644 --- a/bin/uiml_demo.ml +++ b/bin/uiml_demo.ml @@ -50,8 +50,8 @@ there should really at least be a function that checks that iE and iA are given box-free formulas as input.*) method iA s = catch_e (fun () -> s |> eval |> fail_on_modality |> isl_A v |> string_of_formula) method iE s = catch_e (fun () -> s |> eval |> fail_on_modality |> isl_E v |> string_of_formula) - method islA s = catch_e (fun () -> s |> eval |> isl_A v |> string_of_formula) - method islE s = catch_e (fun () -> s |> eval |> isl_E v |> string_of_formula) + method islA s = catch_e (fun () -> s |> eval |> isl_simplified_A v |> string_of_formula) + method islE s = catch_e (fun () -> s |> eval |> isl_simplified_E v |> string_of_formula) method k s = catch_e (fun () -> s |> eval |> isl_E v |> string_of_formula ~classical: true) method gl s = catch_e (fun () -> s |> eval |> isl_E v |> string_of_formula ~classical: true) method parse s = catch_e (fun () -> s |> eval |> string_of_formula) From f9cfc4fb56406d6a86b29cc53a13371a6dd228c7 Mon Sep 17 00:00:00 2001 From: Yago Iglesias Date: Fri, 28 Jun 2024 14:55:07 +0200 Subject: [PATCH 29/29] Rename bin/bench to bin/benchmark --- bin/{bench.ml => benchmark.ml} | 0 bin/dune | 4 ++-- 2 files changed, 2 insertions(+), 2 deletions(-) rename bin/{bench.ml => benchmark.ml} (100%) diff --git a/bin/bench.ml b/bin/benchmark.ml similarity index 100% rename from bin/bench.ml rename to bin/benchmark.ml diff --git a/bin/dune b/bin/dune index 25195d4..157f8cd 100644 --- a/bin/dune +++ b/bin/dune @@ -1,6 +1,6 @@ (executables - (public_names uiml_demo bench) - (names uiml_demo bench) + (public_names uiml_demo benchmark) + (names uiml_demo benchmark) (modes js native) (preprocess (pps js_of_ocaml-ppx)) (libraries js_of_ocaml UIML angstrom))