Quelle simpl_tuning.v Sprache: Coq

(* 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.

Module TestClearSimpl.

Fail Arguments id _ x / : clear simpl.
Fail Arguments id _ ! x : clear simpl.
Fail Arguments id _ : simpl never, clear simpl.
Fail Arguments id _ : simpl nomatch, clear simpl.

Arguments id _ x /.
Lemma foo : id 0 = 0.
simpl.
match goal with |- 0 = 0 => idtac end.
Abort.

Arguments id _ x : clear simpl.
Lemma foo : id 0 = 0.
simpl.
match goal with |- id 0 = 0 => idtac end.
Abort.

End TestClearSimpl.

quality98%

¤ Dauer der Verarbeitung: 0.3 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.