Simplifications simplify proof

bin/benchmark.ml

@@ -11,14 +11,6 @@ type bench_info = {
   after : int timed_result;
 }
 
-let rec form_size = function
-  | Var _ -> 1
-  | Bot -> 1
-  | Or (f1, f2) -> 1 + form_size f1 + form_size f2
-  | And (f1, f2) -> 1 + form_size f1 + form_size f2
-  | Implies (f1, f2) -> 1 + form_size f1 + form_size f2
-  | Box f -> 1 + form_size f
-
 let percentage_reduction before after = 100. -. (after /. before *. 100.)
 
 let time f x =
@@ -43,13 +35,13 @@ let bench_one fs =
   [
     {
       name = "A " ^ fs;
-      before = { value = form_size resA.value; time = resA.time };
-      after = { value = form_size simpA.value; time = simpA.time };
+      before = { value = form_size resA.value |> int_of_nat; time = resA.time };
+      after = { value = form_size simpA.value |> int_of_nat; time = simpA.time };
     };
     {
       name = "E " ^ fs;
-      before = { value = form_size resE.value; time = resE.time };
-      after = { value = form_size simpE.value; time = simpE.time };
+      before = { value = form_size resE.value |> int_of_nat; time = resE.time };
+      after = { value = form_size simpE.value |> int_of_nat; time = simpE.time };
     };
   ]
 
@@ -60,15 +52,19 @@ let print_bench_value_info benches =
      computation time (s)|\n\
      |--|--|--|--|--|--|\n";
   List.iter print_value_results benches;
-  print_newline ();
-
-  let sum_before =
-    List.fold_left (fun acc x -> acc + x.before.value) 0 benches
+  let sum_before, sum_after, sum_comp_time, sum_simp_time =
+    List.fold_left
+      (fun (sum_before, sum_after, sum_comp_time, sum_simp_time) bench ->
+        ( sum_before + bench.before.value,
+          sum_after + bench.after.value,
+          bench.before.time +. sum_comp_time,
+          bench.after.time +. sum_simp_time ))
+      (0, 0, 0., 0.) benches
   in
-  let sum_after = List.fold_left (fun acc x -> acc + x.after.value) 0 benches in
-
-  Printf.printf "Average percentage reduction: %.2f\n"
+  Printf.printf "| Total | %d | %d | %.2f | %.4f | %.4f |\n" sum_before
+    sum_after
     (percentage_reduction (float_of_int sum_before) (float_of_int sum_after))
+    sum_comp_time sum_simp_time
 
 let bench l =
   let benches = List.map bench_one l |> List.flatten in

theories/extraction/UIML_extraction.v

@@ -41,5 +41,5 @@ Definition isl_simplified_A v f := A_simplified v f.
 
 Set Extraction Output Directory "extraction".
 
-Separate Extraction gl_UI k_UI isl_E isl_A isl_simplified_E isl_simplified_A Formulas.weight isl_simp.
+Separate Extraction gl_UI k_UI isl_E isl_A isl_simplified_E isl_simplified_A Formulas.weight Formulas.form_size isl_simp.
 

theories/iSL/Formulas.v

@@ -135,3 +135,13 @@ Global Instance irreflexive_form_order : Irreflexive form_order.
 Proof. unfold form_order. intros x y. lia. Qed.
 
 Notation "φ ≺f ψ" := (form_order ψ φ) (at level 149).
+
+
+Fixpoint form_size (φ : form) : nat := match φ with
+| ⊥ => 1
+| Var _ => 1
+| φ ∧ ψ => 1 + form_size φ + form_size ψ
+| φ ∨ ψ => 1 + form_size φ + form_size ψ
+| φ → ψ => 1 + form_size φ + form_size ψ
+| □φ => 1 + form_size φ
+end.

theories/iSL/Simp.v

@@ -46,7 +46,7 @@
 end.
 
 
 Infix "⊻" := simp_or (at level 65).
 
 (* Normalises a large disjunctions flattening them to the right. It assumes
 that there are no disjuctions on the left of any of the input formulas, i.e.
@@ -83,7 +83,7 @@
 end.
 
 
 Infix "⊼" := simp_and (at level 60).
 
 (* Same as `simp_ors` but for large conjunctions. *)
 Fixpoint simp_ands φ ψ :=
@@ -843,7 +843,7 @@
 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)|
  eapply simp_equiv_box];
  apply IHw; 
@@ -1070,6 +1070,81 @@
 
 
 
+Lemma simp_simplifies_conj_disj φ ψ:
+  (form_size (φ ⊼ ψ) ≤  1 + form_size φ + form_size ψ) *
+  (form_size (φ ⊻ ψ) ≤  1 + form_size φ + form_size ψ).
+Proof.
+split;  [unfold simp_and | unfold simp_or]; destruct φ; destruct ψ; 
+repeat match goal with
+  | |- form_size (choose_or _ _) ≤ _ => unfold choose_or
+  | |- form_size (choose_and _ _) ≤ _ => unfold choose_and
+  | |- form_size (match ?x with _ => _ end) ≤  _ => destruct x
+  | _ => simpl; lia
+end.
+Qed.
+
+
+Ltac large_conj_disj_solver :=
+match goal with
+  | |- form_size (?simp_f ?x  (?connector ?φ1 ?φ2)) ≤ _ =>
+    assert (H: form_size (simp_f x (connector φ1 φ2)) ≤ 1 +  (form_size x + (1 + form_size φ1 + form_size φ2))) 
+    by apply simp_simplifies_conj_disj;
+    simpl in H; lia
+
+  | IHφ2 : ∀ ψ : form, form_size (?simp_f_large ?φ2 ψ) ≤ form_size (?connector ?φ2 ψ)
+    |- form_size (?simp_f ?φ1  (?simp_f ?ψ0_1 (?simp_f_large ?φ2 ?ψ0_2))) ≤ _ =>
+    assert (H1: form_size (simp_f φ1  (simp_f ψ0_1  ( simp_f_large φ2 ψ0_2))) ≤ 1 +  form_size φ1 + form_size (simp_f ψ0_1  (simp_f_large φ2 ψ0_2))) 
+    by apply simp_simplifies_conj_disj;
+    assert (H2: form_size ((simp_f ψ0_1 (simp_f_large φ2 ψ0_2))) ≤ 1 +  form_size (ψ0_1) + form_size (simp_f_large φ2 ψ0_2)) 
+    by apply simp_simplifies_conj_disj;
+    assert ( H3: form_size (simp_f_large φ2 ψ0_2) ≤ 1 + form_size φ2 + form_size ψ0_2) by apply IHφ2;
+    lia
+
+  | _ => lia
+end.
+
+Lemma simp_simplifies_ands φ ψ:
+ form_size (simp_ands φ ψ) ≤  form_size (And φ ψ).
+Proof.
+generalize ψ.
+induction φ; intro ψ0; destruct ψ0; try apply simp_simplifies_conj_disj; simpl;
+large_conj_disj_solver.
+Qed.
+
+Lemma simp_simplifies_ors φ ψ:
+ form_size (simp_ors φ ψ) ≤  form_size (Or φ ψ).
+Proof.
+generalize ψ.
+induction φ; intro ψ0; destruct ψ0; try apply simp_simplifies_conj_disj; simpl;
+large_conj_disj_solver.
+Qed.
+
+Lemma simp_simplifies_imp φ ψ:
+ form_size (simp_imp φ ψ) ≤  form_size (Implies φ ψ).
+Proof.
+unfold simp_or.
+destruct φ; destruct ψ; unfold simp_imp;
+repeat match goal with
+  | |- form_size (if decide _ then _ else _) ≤  _=> case decide; intro
+  | _ => simpl; lia
+end.
+Qed.
+
+Theorem simp_simplifies φ:
+  form_size (simp φ) <= form_size φ.
+Proof.
+induction φ; auto; simpl;
+[ assert (H: form_size (simp_ands (simp φ1) (simp φ2)) ≤ S (form_size (simp φ1) + form_size (simp φ2))) 
+    by apply simp_simplifies_ands|
+  assert (H: form_size (simp_ors (simp φ1) (simp φ2)) ≤ S (form_size (simp φ1) + form_size (simp φ2))) 
+    by apply simp_simplifies_ors|
+  assert (H: form_size (simp_imp (simp φ1) (simp φ2)) ≤ S (form_size (simp φ1) + form_size (simp φ2))) 
+    by apply simp_simplifies_imp|
+  idtac
+]; lia.
+Qed.
+
+
 Require Import String.
 Local Open Scope string_scope.