diff options
Diffstat (limited to 'test-suite/success/simpl_tuning.v')
| -rw-r--r-- | test-suite/success/simpl_tuning.v | 149 |
1 files changed, 149 insertions, 0 deletions
diff --git a/test-suite/success/simpl_tuning.v b/test-suite/success/simpl_tuning.v new file mode 100644 index 00000000..d4191b93 --- /dev/null +++ b/test-suite/success/simpl_tuning.v @@ -0,0 +1,149 @@ +(* as it is dynamically inferred by simpl *) +Arguments minus !n / m. + +Lemma foo x y : S (S x) - S y = 0. +simpl. +match goal with |- (match y with O => S x | S _ => _ end = 0) => idtac end. +Abort. + +(* we avoid exposing a match *) +Arguments minus n m : simpl nomatch. + +Lemma foo x : minus 0 x = 0. +simpl. +match goal with |- (0 = 0) => idtac end. +Abort. + +Lemma foo x y : S (S x) - S y = 0. +simpl. +match goal with |- (S x - y = 0) => idtac end. +Abort. + +Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0. +simpl. +match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end. +Abort. + +(* we unfold as soon as we have 1 args, but we avoid exposing a match *) +Arguments minus n / m : simpl nomatch. + +Lemma foo : minus 0 = fun x => 0. +simpl. +match goal with |- minus 0 = _ => idtac end. +Abort. +(* This does not work as one may expect. The point is that simpl is implemented + as "strong (whd_simpl_state)" and after unfolding minus you have + (fun m => match 0 => 0 | S n => ...) that is already in whd and exposes + a match, that of course "strong" would reduce away but at that stage + we don't know, and reducing by hand under the lambda is against whd *) + +(* extra tuning for the usual heuristic *) +Arguments minus !n / m : simpl nomatch. + +Lemma foo x y : S (S x) - S y = 0. +simpl. +match goal with |- (S x - y = 0) => idtac end. +Abort. + +Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0. +simpl. +match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end. +Abort. + +(* full control *) +Arguments minus !n !m /. + +Lemma foo x y : S (S x) - S y = 0. +simpl. +match goal with |- (S x - y = 0) => idtac end. +Abort. + +Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0. +simpl. +match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end. +Abort. + +(* omitting /, that being immediately after the last ! is irrelevant *) +Arguments minus !n !m. + +Lemma foo x y : S (S x) - S y = 0. +simpl. +match goal with |- (S x - y = 0) => idtac end. +Abort. + +Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0. +simpl. +match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end. +Abort. + +Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) := + fun x => (f (fst x), g (snd x)). + +Delimit Scope foo_scope with F. +Notation "@@" := nat (only parsing) : foo_scope. +Notation "@@" := (fun x => x) (only parsing). + +Arguments pf {D1%F C1%type} f [D2 C2] g x : simpl never. + +Lemma foo x : @pf @@ nat @@ nat nat @@ x = pf @@ @@ x. +Abort. + +Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x). + +(* fcomp is unfolded if applied to 6 args *) +Arguments fcomp {A B C}%type f g x /. + +Notation "f \o g" := (fcomp f g) (at level 50). + +Lemma foo (f g h : nat -> nat) x : pf (f \o g) h x = pf f h (g (fst x), snd x). +simpl. +match goal with |- (pf (f \o g) h x = _) => idtac end. +case x; intros x1 x2. +simpl. +match goal with |- (pf (f \o g) h _ = pf f h _) => idtac end. +unfold pf; simpl. +match goal with |- (f (g x1), h x2) = (f (g x1), h x2) => idtac end. +Abort. + +Definition volatile := fun x : nat => x. +Arguments volatile /. + +Lemma foo : volatile = volatile. +simpl. +match goal with |- (fun _ => _) = _ => idtac end. +Abort. + +Set Implicit Arguments. + +Section S1. + +Variable T1 : Type. + +Section S2. + +Variable T2 : Type. + +Fixpoint f (x : T1) (y : T2) n (v : unit) m {struct n} : nat := + match n, m with + | 0,_ => 0 + | S _, 0 => n + | S n', S m' => f x y n' v m' end. + +Global Arguments f x y !n !v !m. + +Lemma foo x y n m : f x y (S n) tt m = f x y (S n) tt (S m). +simpl. +match goal with |- (f _ _ _ _ _ = f _ _ _ _ _) => idtac end. +Abort. + +End S2. + +Lemma foo T x y n m : @f T x y (S n) tt m = @f T x y (S n) tt (S m). +simpl. +match goal with |- (f _ _ _ _ _ = f _ _ _ _ _) => idtac end. +Abort. + +End S1. + +Arguments f : clear implicits and scopes. + |