From 806b05dc5c3a1594231225df0e8e9e28441d8736 Mon Sep 17 00:00:00 2001 From: Enrico Date: Wed, 7 Sep 2016 17:57:19 +0200 Subject: abstract_context utility lemma --- mathcomp/ssreflect/ssreflect.v | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/ssreflect.v b/mathcomp/ssreflect/ssreflect.v index 38a8013..6750142 100644 --- a/mathcomp/ssreflect/ssreflect.v +++ b/mathcomp/ssreflect/ssreflect.v @@ -422,3 +422,13 @@ End ApplyIff. Hint View for move/ iffLRn|2 iffRLn|2 iffLR|2 iffRL|2. Hint View for apply/ iffRLn|2 iffLRn|2 iffRL|2 iffLR|2. +(* To focus non-ssreflect tactics on a subterm, eg vm_compute. *) +(* Usage: *) +(* elim/abstract_context: (pattern) => G defG. *) +(* vm_compute; rewrite {}defG {G}. *) +(* Note that vm_cast are not stored in the proof term, so *) +(* set here := pattern; vm_compute in (value of here) *) +(* blows up at Qed time. *) +Lemma abstract_context T (P : T -> Type) x : + (forall Q, Q = P -> Q x) -> P x. +Proof. by move=> /(_ P); apply. Qed. -- cgit v1.2.3 From 2209e0bce7eeda751f87806a3e77a0c520017a88 Mon Sep 17 00:00:00 2001 From: Enrico Date: Wed, 7 Sep 2016 18:02:09 +0200 Subject: fix comment --- mathcomp/ssreflect/ssreflect.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/ssreflect.v b/mathcomp/ssreflect/ssreflect.v index 6750142..cd405fa 100644 --- a/mathcomp/ssreflect/ssreflect.v +++ b/mathcomp/ssreflect/ssreflect.v @@ -426,7 +426,8 @@ Hint View for apply/ iffRLn|2 iffLRn|2 iffRL|2 iffLR|2. (* Usage: *) (* elim/abstract_context: (pattern) => G defG. *) (* vm_compute; rewrite {}defG {G}. *) -(* Note that vm_cast are not stored in the proof term, so *) +(* Note that vm_cast are not stored in the proof term *) +(* for reductions occuring in the context, hence *) (* set here := pattern; vm_compute in (value of here) *) (* blows up at Qed time. *) Lemma abstract_context T (P : T -> Type) x : -- cgit v1.2.3