vmurali
commented
6 years ago How about restricting Psatz only to portions that require lia. Or better yet, see if Psatz.lia can be removed and replaced with omega?
On Wed, May 16, 2018 at 8:32 PM, Samuel Gruetter notifications@github.com wrote:
On current master (38fe6a4 https://github.com/mit-plv/bbv/commit/38fe6a40ea26ce738637e340d7f8e9f0eb85fbc3) of bbv, if I do
Print Assumptions roundTrip_0.
I get output like this:
Raxioms.total_order_T : forall r1 r2 : Rdefinitions.R, {Rdefinitions.Rlt r1 r2} + {r1 = r2} + {Rdefinitions.Rgt r1 r2} Raxioms.Rplus_opp_r : forall r : Rdefinitions.R, Rdefinitions.Rplus r (Rdefinitions.Ropp r) = Rdefinitions.IZR 0 Raxioms.Rplus_lt_compat_l : forall r r1 r2 : Rdefinitions.R, Rdefinitions.Rlt r1 r2 -> Rdefinitions.Rlt (Rdefinitions.Rplus r r1) (Rdefinitions.Rplus r r2) Raxioms.Rplus_comm : forall r1 r2 : Rdefinitions.R, Rdefinitions.Rplus r1 r2 = Rdefinitions.Rplus r2 r1 Raxioms.Rplus_assoc : forall r1 r2 r3 : Rdefinitions.R, Rdefinitions.Rplus (Rdefinitions.Rplus r1 r2) r3 = ... truncated because so long ...
This is unacceptable -- I want my theorems based on bbv to be axiom free.
Some time ago, the output was
Closed under the global context
as expected.
Using git bisect, I found that the problem was introduced in 02043b9 https://github.com/mit-plv/bbv/commit/02043b9b599165c2d99817257a6b1dc81fcf3af5 .
This commit imports Psatz, which makes available the hint database called real, which contains axioms about the real numbers. (This can be confirmed by running Print Hint *. before importing Psatz and after importing it and compare the outputs by searching for 'axi').
Moreover, note that the intuition tactic is an alias for intuition auto with *.
Now, the proof of roundTrip_0 uses intuition, and apparently its auto with * uses real number arithmetic to solve some subgoals.
I tried two ways to solve this: Approach 1: Strict hint behavior
Add the following after all imports in Word.v:
( Emulates an import-scoped hint mechanism (what you'd expect), i.e. hints and hint databases are only available if you import their module, but not if they are declared in a transitive dependency of some imported module. ) Set Loose Hint Behavior "Strict".
( these modules contain Rewrite Hints which are actually useful and needed: ) Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop. Import Coq.ZArith.BinInt.Z. Import Coq.NArith.BinNat.N. Import Coq.Arith.PeanoNat.Nat. Import Coq.Logic.Eqdep.EqdepTheory.
However, this requires me to import modules such as Coq.Arith.PeanoNat.Nat to make their hints available, but this redefines things such as eq_refl: It now has the type Reflexive Logic.eq, which is not compatible with normal eq_refl.
I did not succeed in making this approach work. Approach 2: Redefine intuition
Redefine intuition (and firstorder too) to do auto with zarith instead of auto with * (done in this PR).
This works in the sense that Print Assumptions roundTrip_0. now prints Closed under the global context, but it does not really solve the problem that a lot of potentially unwanted hints are still lingering around and might be picked up by other tactics, or might slow down proof search. Questions:
- Will this PR break any projects using bbv?
- Can we make approach 1 (which seems superior to me) work?
You can view, comment on, or merge this pull request online at:
https://github.com/mit-plv/bbv/pull/6 Commit Summary
- redefine intuition so that roundTrip_0 does not depend on real number axioms
File Changes
- M Word.v https://github.com/mit-plv/bbv/pull/6/files#diff-0 (12)
Patch Links:
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/mit-plv/bbv/pull/6, or mute the thread https://github.com/notifications/unsubscribe-auth/AAOaRVCTkh-v5cQfVQrnkE9z_KCGh6Ceks5tzO9egaJpZM4UCW-c .
JasonGross
samuelgruetter
On current master (38fe6a40ea26ce738637e340d7f8e9f0eb85fbc3) of bbv, if I do
I get output like this:
This is unacceptable -- I want my theorems based on bbv to be axiom free.
Some time ago, the output was
as expected.
Using
git bisect, I found that the problem was introduced in 02043b9b599165c2d99817257a6b1dc81fcf3af5.This commit imports
Psatz, which makes available the hint database calledreal, which contains axioms about the real numbers. (This can be confirmed by runningPrint Hint *.before importingPsatzand after importing it and compare the outputs by searching for 'axi').Moreover, note that the
intuitiontactic is an alias forintuition auto with *.Now, the proof of
roundTrip_0usesintuition, and apparently itsauto with *uses real number arithmetic to solve some subgoals.I tried two ways to solve this:
Approach 1: Strict hint behavior
Add the following after all imports in
Word.v:However, this requires me to import modules such as
Coq.Arith.PeanoNat.Natto make their hints available, but this redefines things such aseq_refl: It now has the typeReflexive Logic.eq, which is not compatible with normaleq_refl.I did not succeed in making this approach work.
Approach 2: Redefine intuition
Redefine
intuition(andfirstordertoo) to doauto with zarithinstead ofauto with *(done in this PR).This works in the sense that
Print Assumptions roundTrip_0.now printsClosed under the global context, but it does not really solve the problem that a lot of potentially unwanted hints are still lingering around and might be picked up by other tactics, or might slow down proof search.Questions:
bbv?