Skip to content

Stop using auto with * in intuition #45

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
SkySkimmer wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Stop using auto with * in intuition #45

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions src/bbv/NatLib.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ Section strong.
Hypothesis PH : forall n, (forall m, m < n -> P m) -> P n.

Lemma strong' : forall n m, m <= n -> P m.
induction n; simpl; intuition; apply PH; intuition.
induction n; simpl; intuition auto with zarith; apply PH; intuition.
exfalso; lia.
Qed.

Expand Down Expand Up @@ -98,7 +98,7 @@ Theorem drop_mod2 : forall n k,

do 2 (destruct n; simpl in *; repeat rewrite untimes2 in *; intuition).

destruct k; simpl in *; intuition.
destruct k; simpl in *; intuition lia.

destruct k; simpl; intuition.
rewrite <- plus_n_Sm.
Expand Down Expand Up @@ -374,7 +374,7 @@ Qed.
Theorem Npow2_nat : forall n, nat_of_N (Npow2 n) = pow2 n.
induction n as [|n IHn]; simpl; intuition.
rewrite <- IHn; clear IHn.
case_eq (Npow2 n); intuition; zify; intuition.
case_eq (Npow2 n); intuition lia.
Qed.

Theorem pow2_N : forall n, Npow2 n = N.of_nat (pow2 n).
Expand Down
2 changes: 2 additions & 0 deletions src/bbv/Nomega.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,8 @@ Require Import Coq.ZArith.ZArith.

Local Open Scope N_scope.

Local Ltac Tauto.intuition_solver ::= auto with bool zarith.

Hint Rewrite Nplus_0_r nat_of_Nsucc nat_of_Nplus nat_of_Nminus
N_of_nat_of_N nat_of_N_of_nat
nat_of_P_o_P_of_succ_nat_eq_succ nat_of_P_succ_morphism : N.
Expand Down
8 changes: 4 additions & 4 deletions src/bbv/Word.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -531,15 +531,15 @@ Theorem natToWord_wordToNat : forall sz w, natToWord sz (wordToNat w) = w.
Qed.

Theorem roundTrip_0 : forall sz, wordToNat (natToWord sz 0) = 0.
induction sz; simpl; intuition.
induction sz; simpl; intuition lia.
Qed.

Hint Rewrite roundTrip_0 : wordToNat.

Lemma wordToNat_natToWord' : forall sz w, exists k, wordToNat (natToWord sz w) + k * pow2 sz = w.
induction sz as [|sz IHsz]; simpl; intro w; intuition; repeat rewrite untimes2.

exists w; intuition.
exists w; intuition lia.

case_eq (mod2 w); intro Hmw.

Expand Down Expand Up @@ -573,7 +573,7 @@ Qed.
Theorem wordToNat_natToWord:
forall sz w, exists k, wordToNat (natToWord sz w) = w - k * pow2 sz /\ (k * pow2 sz <= w)%nat.
Proof.
intros sz w; destruct (wordToNat_natToWord' sz w) as [k]; exists k; intuition.
intros sz w; destruct (wordToNat_natToWord' sz w) as [k]; exists k; intuition lia.
Qed.

Lemma wordToNat_natToWord_2: forall sz w : nat,
Expand Down Expand Up @@ -5122,7 +5122,7 @@ Qed.

Lemma ZToWord_plus: forall sz a b, ZToWord sz (a + b) = ZToWord sz a ^+ ZToWord sz b.
Proof.
destruct sz as [|sz]; intros n m; intuition.
destruct sz as [|sz]; intros n m; intuition auto with worder.
rewrite wplus_wplusZ.
unfold wplusZ, wordBinZ.
destruct (wordToZ_ZToWord' (S sz) n) as [k1 D1].
Expand Down