From 183112fc6a5fbb7d1c6d60b9717cdb8aceda78ca Mon Sep 17 00:00:00 2001 From: Pierre Boutillier Date: Mon, 8 Sep 2014 16:19:39 +0200 Subject: Simpl less (so that cbn will not simpl too much) --- theories/PArith/BinPos.v | 2 +- theories/PArith/BinPosDef.v | 2 +- theories/PArith/Pnat.v | 5 +++-- 3 files changed, 5 insertions(+), 4 deletions(-) (limited to 'theories/PArith') diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index a30c555c1..0f794c513 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -649,7 +649,7 @@ Theorem sub_mask_carry_spec p q : sub_mask_carry p q = pred_mask (sub_mask p q). Proof. revert q. induction p as [p IHp|p IHp| ]; destruct q; simpl; - try reflexivity; try rewrite IHp; + try reflexivity; rewrite ?IHp; destruct (sub_mask p q) as [|[r|r| ]|] || destruct p; auto. Qed. diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index fcc12ab45..44b9e7d03 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -537,7 +537,7 @@ Definition iter_op {A}(op:A->A->A) := end. Definition to_nat (x:positive) : nat := iter_op plus x (S O). - +Arguments to_nat x: simpl never. (** ** From Peano natural numbers to binary positive numbers *) (** A version preserving positive numbers, and sending 0 to 1. *) diff --git a/theories/PArith/Pnat.v b/theories/PArith/Pnat.v index 4336d47af..0f2ecf55a 100644 --- a/theories/PArith/Pnat.v +++ b/theories/PArith/Pnat.v @@ -196,7 +196,8 @@ Theorem inj_iter : Proof. induction p using peano_ind. - trivial. - - intros. rewrite inj_succ, iter_succ. simpl. now f_equal. + - intros. rewrite inj_succ, iter_succ. + simpl. f_equal. apply IHp. Qed. End Pos2Nat. @@ -210,7 +211,7 @@ Module Nat2Pos. Theorem id (n:nat) : n<>0 -> Pos.to_nat (Pos.of_nat n) = n. Proof. induction n as [|n H]; trivial. now destruct 1. - intros _. simpl. destruct n. trivial. + intros _. simpl Pos.of_nat. destruct n. trivial. rewrite Pos2Nat.inj_succ. f_equal. now apply H. Qed. -- cgit v1.2.3