From 17564e4922acda6b72bf39de7a8c23ed0c0178f6 Mon Sep 17 00:00:00 2001 From: Nicolas Braud-Santoni Date: Sat, 23 Jul 2016 16:21:44 -0400 Subject: Imported Upstream version 8.5.1 --- Tutorial.v | 33 --------------------------------- 1 file changed, 33 deletions(-) (limited to 'Tutorial.v') diff --git a/Tutorial.v b/Tutorial.v index 6356a10..76006ca 100644 --- a/Tutorial.v +++ b/Tutorial.v @@ -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. - -- cgit v1.2.3