1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
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.
|
