1 files changed, 33 insertions, 0 deletions
diff --git a/Tutorial.v b/Tutorial.v
index 76006ca..6356a10 100644
--- a/Tutorial.v
+++ b/Tutorial.v
@@ -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. 
+