Replace obviously_smaller with the complete decision procedure

hferee · Sep 11, 2024 · 54426f8 · 54426f8
1 parent 352e108
commit 54426f8
Show file tree

Hide file tree

Showing 5 changed files with 104 additions and 153 deletions.
diff --git a/theories/extraction/UIML_extraction.v b/theories/extraction/UIML_extraction.v
@@ -5,7 +5,7 @@ Require Import ExtrOcamlBasic ExtrOcamlString.
 
 Require Import K.Interpolation.UIK_braga.
 Require Import KS_export.
-Require Import ISL.PropQuantifiers ISL.DecisionProcedure ISL.Simp.
+Require Import ISL.PropQuantifiers ISL.DecisionProcedure ISL.Simp ISL.Simp_env.
 
 
 
@@ -34,7 +34,9 @@ Definition k_UI p s := form_of_MPropF(proj1_sig (K.Interpolation.UIK_braga.GUI_t
 Definition isl_E v f := Ef v f.
 Definition isl_A v f := Af v f.
 
-Definition isl_simp f := simp f.
+(* simp_form seems to improve over simp in most cases.
+  Notable exception: (a ∨b) → c *)
+Definition isl_simp f := simp_form f.
 
 Definition isl_simplified_E v f := E_simplified v f.
 Definition isl_simplified_A v f := A_simplified v f.

diff --git a/theories/iSL/DecisionProcedure.v b/theories/iSL/DecisionProcedure.v
@@ -616,3 +616,11 @@ intro Hp. inversion Hp; subst; try eqt; eauto 2.
   + now rw (proper_open_boxes _ _ Heq) 2.
   + now rw Heq 1.
 Defined.
+
+Global Infix "⊢?" := Provable_dec (at level 80).
+
+Lemma Provable_dec_of_Prop Γ φ: (∃ _ : list_to_set_disj Γ ⊢ φ, True) -> (list_to_set_disj Γ ⊢ φ).
+Proof.
+destruct (Proof_tree_dec Γ φ) as [[Hφ1' _] | Hf']. tauto.
+intros Hf. exfalso. destruct Hf as [Hf _]. tauto.
+Qed.