From 701b188b6f17d9f54480654e5959c606a8947c88 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 5 Mar 2019 12:17:49 +0000 Subject: Coq: use setoid rewriting to apply under an existential binder --- lib/coq/Sail2_values.v | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) (limited to 'lib/coq/Sail2_values.v') diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index e6c5e786..ba94a237 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1040,20 +1040,20 @@ Ltac unbool_comparisons := end. Ltac unbool_comparisons_goal := repeat match goal with - | |- context [Z.geb _ _] => rewrite Z.geb_leb - | |- context [Z.gtb _ _] => rewrite Z.gtb_ltb - | |- context [Z.leb _ _ = true] => rewrite Z.leb_le - | |- context [Z.ltb _ _ = true] => rewrite Z.ltb_lt - | |- context [Z.eqb _ _ = true] => rewrite Z.eqb_eq - | |- context [Z.leb _ _ = false] => rewrite Z.leb_gt - | |- context [Z.ltb _ _ = false] => rewrite Z.ltb_ge - | |- context [Z.eqb _ _ = false] => rewrite Z.eqb_neq - | |- context [orb _ _ = true] => rewrite Bool.orb_true_iff - | |- context [orb _ _ = false] => rewrite Bool.orb_false_iff - | |- context [andb _ _ = true] => rewrite Bool.andb_true_iff - | |- context [andb _ _ = false] => rewrite Bool.andb_false_iff - | |- context [negb _ = true] => rewrite Bool.negb_true_iff - | |- context [negb _ = false] => rewrite Bool.negb_false_iff + | |- context [Z.geb _ _] => setoid_rewrite Z.geb_leb + | |- context [Z.gtb _ _] => setoid_rewrite Z.gtb_ltb + | |- context [Z.leb _ _ = true] => setoid_rewrite Z.leb_le + | |- context [Z.ltb _ _ = true] => setoid_rewrite Z.ltb_lt + | |- context [Z.eqb _ _ = true] => setoid_rewrite Z.eqb_eq + | |- context [Z.leb _ _ = false] => setoid_rewrite Z.leb_gt + | |- context [Z.ltb _ _ = false] => setoid_rewrite Z.ltb_ge + | |- context [Z.eqb _ _ = false] => setoid_rewrite Z.eqb_neq + | |- context [orb _ _ = true] => setoid_rewrite Bool.orb_true_iff + | |- context [orb _ _ = false] => setoid_rewrite Bool.orb_false_iff + | |- context [andb _ _ = true] => setoid_rewrite Bool.andb_true_iff + | |- context [andb _ _ = false] => setoid_rewrite Bool.andb_false_iff + | |- context [negb _ = true] => setoid_rewrite Bool.negb_true_iff + | |- context [negb _ = false] => setoid_rewrite Bool.negb_false_iff | |- context [generic_eq _ _ = true] => apply generic_eq_true | |- context [generic_eq _ _ = false] => apply generic_eq_false | |- context [generic_neq _ _ = true] => apply generic_neq_true -- cgit v1.2.3 From 98f447e1ca70999350dac4b7a0d3fbce5c64071b Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 5 Mar 2019 15:13:15 +0000 Subject: Coq: firstorder is better at the boolean goals --- lib/coq/Sail2_values.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'lib/coq/Sail2_values.v') diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index ba94a237..fa40e01a 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1213,8 +1213,9 @@ prepare_for_solver; constructor; intros l r H1 H2; solve [exists l; destruct l; intuition | exists r; destruct l; intuition] end - | match goal with |- context [@eq _ _ _] => - constructor; intuition + | match goal with |- context [@eq bool _ _] => + (* Don't use auto for the fallback to keep runtime down *) + firstorder fail end | constructor; idtac "Unable to solve constraint"; dump_context; fail ]. -- cgit v1.2.3 From e2ba378d45b0072d22ae0e63c0437fd22b25c361 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 7 Mar 2019 11:59:18 +0000 Subject: Coq: apply a little brute force in some boolean goals --- lib/coq/Sail2_values.v | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) (limited to 'lib/coq/Sail2_values.v') diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index fa40e01a..10571412 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1190,6 +1190,13 @@ Ltac fill_in_evar_eq := let y := eval cbn in y in*) idtac "Warning: unknown equality constraint"; constructor; exact (eq_refl _ : x = y) end. +Ltac bruteforce_bool_exists := +match goal with +| |- exists _ : bool,_ => solve [ exists true; bruteforce_bool_exists + | exists false; bruteforce_bool_exists ] +| _ => tauto +end. + Ltac solve_arithfact := (* Attempt a simple proof first to avoid lengthy preparation steps (especially as the large proof terms can upset subsequent proofs). *) @@ -1209,9 +1216,8 @@ prepare_for_solver; (* The datatypes hints give us some list handling, esp In *) | constructor; drop_exists; eauto 3 with datatypes zarith sail (* Booleans - and_boolMP *) - | match goal with |- ArithFact (forall l r:bool, _ -> _ -> exists _, _) => - constructor; intros l r H1 H2; - solve [exists l; destruct l; intuition | exists r; destruct l; intuition] + | match goal with |- ArithFact (forall l r:bool, _ -> _ -> exists _ : bool, _) => + constructor; intros [|] [|] H1 H2; bruteforce_bool_exists end | match goal with |- context [@eq bool _ _] => (* Don't use auto for the fallback to keep runtime down *) -- cgit v1.2.3 From c3d10cdb1787077425e174fa638f1d43de7c797f Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 12 Mar 2019 11:09:33 +0000 Subject: Coq: fix some boolean issues seen in arm Fixes bad precedence issues, removes an out-of-date special case that's not necessary, and solves more goals. --- lib/coq/Sail2_values.v | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'lib/coq/Sail2_values.v') diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 10571412..7db9d5aa 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1037,6 +1037,8 @@ Ltac unbool_comparisons := | H:context [generic_eq _ _ = false] |- _ => apply generic_eq_false in H | H:context [generic_neq _ _ = true] |- _ => apply generic_neq_true in H | H:context [generic_neq _ _ = false] |- _ => apply generic_neq_false in H + | H:context [_ <> true] |- _ => rewrite Bool.not_true_iff_false in H + | H:context [_ <> false] |- _ => rewrite Bool.not_false_iff_true in H end. Ltac unbool_comparisons_goal := repeat match goal with @@ -1058,6 +1060,8 @@ Ltac unbool_comparisons_goal := | |- context [generic_eq _ _ = false] => apply generic_eq_false | |- context [generic_neq _ _ = true] => apply generic_neq_true | |- context [generic_neq _ _ = false] => apply generic_neq_false + | |- context [_ <> true] => rewrite Bool.not_true_iff_false + | |- context [_ <> false] => rewrite Bool.not_false_iff_true end. (* Split up dependent pairs to get at proofs of properties *) @@ -1217,7 +1221,10 @@ prepare_for_solver; | constructor; drop_exists; eauto 3 with datatypes zarith sail (* Booleans - and_boolMP *) | match goal with |- ArithFact (forall l r:bool, _ -> _ -> exists _ : bool, _) => - constructor; intros [|] [|] H1 H2; bruteforce_bool_exists + constructor; intros [|] [|] H1 H2; + repeat match goal with H:?X = ?X -> _ |- _ => specialize (H eq_refl) end; + repeat match goal with H:@ex _ _ |- _ => destruct H end; + bruteforce_bool_exists end | match goal with |- context [@eq bool _ _] => (* Don't use auto for the fallback to keep runtime down *) -- cgit v1.2.3 From 8c56dcf65016c3669b24e2c5828b5588436e078d Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 12 Mar 2019 17:25:15 +0000 Subject: Coq: try non-linear nia solver too --- lib/coq/Sail2_values.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'lib/coq/Sail2_values.v') diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 7db9d5aa..f11e057a 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -10,6 +10,7 @@ Require Export Sumbool. Require Export DecidableClass. Require Import Eqdep_dec. Require Export Zeuclid. +Require Import Psatz. Import ListNotations. Open Scope Z. @@ -1219,6 +1220,7 @@ prepare_for_solver; | constructor; eauto 3 with zarith sail (* The datatypes hints give us some list handling, esp In *) | constructor; drop_exists; eauto 3 with datatypes zarith sail + | match goal with |- context [Z.mul] => constructor; nia end (* Booleans - and_boolMP *) | match goal with |- ArithFact (forall l r:bool, _ -> _ -> exists _ : bool, _) => constructor; intros [|] [|] H1 H2; -- cgit v1.2.3