diff options
Diffstat (limited to 'Tutorial.v')
-rw-r--r-- | Tutorial.v | 33 |
1 files changed, 0 insertions, 33 deletions
@@ -397,36 +397,3 @@ 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. - |