|
Require Import ssreflect ssrfun ssrbool.
(** Test the various idioms that control rewriting in boolean predicate. **)
Definition simpl_P := [pred a | ~~ a].
Definition nosimpl_P : pred bool := [pred a | ~~ a].
Definition coll_P : collective_pred bool := [pred a | ~~ a].
Definition appl_P : applicative_pred bool := [pred a | ~~ a].
Definition can_appl_P : pred bool := [pred a | ~~ a].
Canonical register_can_appl_P := ApplicativePred can_appl_P.
Ltac see_neg := (let x := fresh "x" in set x := {-}(~~ _); clear x).
Lemma test_pred_rewrite (f := false) : True.
Proof.
have _: f \in simpl_P by rewrite inE; see_neg.
have _ a: simpl_P (a && f) by simpl; see_neg; rewrite andbF.
have _ a: simpl_P (a && f) by rewrite inE; see_neg; rewrite andbF.
have _: f \in nosimpl_P by rewrite inE; see_neg.
have _: nosimpl_P f. simpl. Fail see_neg. Fail rewrite inE. done.
have _: f \in coll_P. Fail rewrite inE. by rewrite in_collective; see_neg.
have _: f \in appl_P.
rewrite inE. Fail see_neg. Fail rewrite inE. simpl. Fail see_neg.
Fail rewrite app_predE. done.
have _: f \in can_appl_P.
rewrite inE. Fail see_neg. Fail rewrite inE. simpl. Fail see_neg.
by rewrite app_predE in_simpl; see_neg.
done.
Qed.
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
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.
|
