Ssreflect Users Discussion List

[Assia Mahboubi <>]

Hi Ralf,

A variant of Laurent's proposal is to use the ssreflect's take on the 'set'
tactic, which supports pattern selection:

Lemma tt (x : A) n : x +  x *- n = x.
Proof.
set z := (_ *- _).

This:
- finds the first subterm t in the goal which matches pattern (_ *- _)
(according to the documented ssreflect matching algorithm);
- introduces an abbreviation z for t in the context;
- folds to z all the subterms in the goal that are convertible to t
- fails if there is no such t.

As far as I understand, it behaves like:

ssrpattern [_ *- _]; intro selected.

However, you can do things like

Lemma bar (x : A) n : x + x *- n = x *-n.
Proof.
set z := {2}(_ *- _).

(which turns the goal into x + x *-n = z)
that I do not know how to mimic using ssrpattern. But may be is this because I
have never really tried this feature.

assia

Le 24/02/2016 13:50, Laurent Thery a écrit :
> 
> 
> On 02/24/2016 01:35 PM, Ralf Jung wrote:
>> Hi,
>>
>> For our current Coq project, we'd like some of our tactics to support
>> patterns. So, for example,
>>
>>    cancel (_ -* _)
>>
>> should find a magic wand in the goal, and then perform canceling on that
>> hypothesis.
> 
> I am not sure to understand your question but you can always use rewriting 
> to
> single out a subterm with a dummy identity.
> 
> 
> From mathcomp Require Import all_ssreflect all_algebra.
> 
> Import GRing.Theory.
> Open Local Scope ring_scope.
> 
> 
> Set Implicit Arguments.
> Unset Strict Implicit.
> Unset Printing Implicit Defensive.
> 
> Variable A : ringType.
> 
> Definition foo (B : Type) (x : B) := x.
> 
> Lemma fooE (B : Type) (x : B) : x = foo x.
> Proof. by []. Qed.
> 
> Lemma tt (x : A) n : x +  x *- n = x.
> Proof.
> rewrite [_ *- _]fooE.