diff options
| author | Cyril Cohen | 2016-10-13 14:20:30 +0200 |
|---|---|---|
| committer | GitHub | 2016-10-13 14:20:30 +0200 |
| commit | 6567e75331b7916bd6c4b61c8da3650926833692 (patch) | |
| tree | 3075e24c206d7e226d3ece566f606a56948a2158 | |
| parent | acf9529aa02b265ffd25e219232a246e92ae5d7f (diff) | |
| parent | 2209e0bce7eeda751f87806a3e77a0c520017a88 (diff) | |
Merge pull request #65 from gares/master
abstract_context utility lemma
| -rw-r--r-- | mathcomp/ssreflect/ssreflect.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/mathcomp/ssreflect/ssreflect.v b/mathcomp/ssreflect/ssreflect.v index 38a8013..cd405fa 100644 --- a/mathcomp/ssreflect/ssreflect.v +++ b/mathcomp/ssreflect/ssreflect.v @@ -422,3 +422,14 @@ 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 *) +(* 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 : + (forall Q, Q = P -> Q x) -> P x. +Proof. by move=> /(_ P); apply. Qed. |