diff options
author | Nicolas Braud-Santoni <nicolas@braud-santoni.eu> | 2016-07-23 16:21:44 -0400 |
---|---|---|
committer | Nicolas Braud-Santoni <nicolas@braud-santoni.eu> | 2016-07-23 16:21:44 -0400 |
commit | 17564e4922acda6b72bf39de7a8c23ed0c0178f6 (patch) | |
tree | 9551ca9435f64c019dbef48894f5dd0c64045f1c /Tutorial.v | |
parent | a77bca84565b26aeedec3b210d761240d9d261f4 (diff) |
Imported Upstream version 8.5.1
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. - |