diff options
Diffstat (limited to 'Tutorial.v')
-rw-r--r-- | Tutorial.v | 33 |
1 files changed, 33 insertions, 0 deletions
@@ -397,3 +397,36 @@ Section Examples. End Examples. +Section Match. + (* The following example is inspired by a question by Francois + Pottier, wokring in the context of separation logic. *) + + Variable T : Type. + Variable star : T -> T -> T. + Hypothesis P : T -> Prop. + + Context (starA : Associative eq star). + Context (starC : Commutative eq star). + + Hypothesis P_hereditary_left : forall a b, P (star a b) -> P a. + Hypothesis P_hereditary_right : forall a b, P (star a b) -> P b. + + Notation "a * b" := (star a b). + + Ltac crush := + match goal with + H: P ?R' |- P ?R => + let h := fresh in + aac_match (fun x => x * R) R' h; + rewrite <- h in H; + try eauto using P_hereditary_right + end. + + Goal forall a b c, P (c * a * c * b) -> P (b * a). + Proof. intros. crush. Qed. + + Goal forall a b c, exists d, P (d * a * c * b) -> P (b * d) /\ b = d. + Proof. intros. eexists. intros. split. crush. reflexivity. Qed. + +End Match. + |