I want to combine two hypotheses at the stack top like A -> B -> G into A /\ B -> G.

What is the best mathcomp-ish way of doing this?

`move=> a b; move: (conj a b).`

?

Thanks! That's exactly what I did. Can we avoid naming variables?

I've a few ideas, but the need seems weird to me. Do you have a concrete example?

I guess you can prove a lemma saying `forall A B G, (A /\ B -> G) -> (A -> B -> G)`

and apply it, or use the script Kenji just wrote, possibly adding a tac-in-term notation to this operation if you need it in the flow of an intro pattern. Eg `move => x y /[grp] ab z w`

. But again, it looks a weird need.

The concrete situation: I was applying to the stack top a lemma like `eqR_le : x <= y <= x <-> x = y`

and I had two `Rle`

s separately.

What's `/[grp]`

by the way?

(Same as what Enrico says)

```
Require Import ssreflect.
Lemma and_curry (A B C : Prop) : (A /\ B -> C) -> A -> B -> C.
Proof. move=> + a b; exact. Qed.
Lemma coucou (a b : nat) (P : Prop) : a <= b -> b <= a -> P.
Proof.
apply: and_curry.
```

`/[grp]`

would be a "notation" to invoke your little ltac (either `apply: and_curry`

or the script by Kenji), see for example the one for /[dup].

This would make sense if it happens to you all the times and in the middle of an intro pattern. Eg `move=> /[grp]/eqR_le->`

, it depends how much desperate to be concise you are ;-)

if `x`

and `y`

are small you can also rewrite (eqR_le x y) and then kill the side condition by rewriting with the two items (proviso you name them).

I would rather call it `/[conj]`

Note that `move=> /conj/[apply]`

should also do the job.

(now you have to explain it to the zulip stream...)

Cyril Cohen said:

Note that

`move=> /conj/[apply]`

should also do the job.

It does not work :(, I will investigate why...

Damn, you managed to convince me

`move=> ab /(conj ab)`

works though...

(but so should the other line, but the result of `move=> /conj`

is weird...)

Does it have the right implicits? Does `/(@conj _ _)`

work?

Nop... `move=> /(@conj _ _)`

does not work :-(

```
Lemma coucou (a b : nat) (P : Prop) : a <= b -> b <= a -> P.
Proof.
move=> /(@conj _ _).
```

results in

```
(forall P0 : Prop, (a <= b -> P0) -> (P0 -> a <= b) -> P0) -> b <= a -> P
```

~~it looks like it replaced ~~`and`

by its Church encoding :confused:

Is there a view that does this?

I guess move can't see both elements of the stack at the same time

Emilio Jesús Gallego Arias said:

I guess move can't see both elements of the stack at the same time

This is not the problem... tactic in intro pattern have arbitrary access to the goal.

`Show Proof`

will tell you

Enrico Tassi said:

`Show Proof`

will tell you

Thanks!! Indeed the view `iffLR`

was implicitly used ...

:scream:

Anyway, `/[conj]`

could be made to work... why not

Cyril Cohen said:

Enrico Tassi said:

`Show Proof`

will tell youThanks!! Indeed the view

`iffLR`

was implicitly used ...

You know what I suspect: that since `<->`

uses `/\`

internally, it matches `?P /\ ?Q`

with it and creates `_ -> _`

instanciations for `?P`

and `Q`

....

This is terrible...

Maybe `/[Pdna]`

;-)

`Pdna`

?

where `=> /andP[]/[Pdna]`

is the identity :crazy:

Time to go back to work ;-)

```
Notation "[conj]" := (ltac:(let x := fresh "_x" in move=> x /(conj x) {x}))
(only parsing) : ssripat_scope.
```

Cyril Cohen said:

`Notation "[conj]" := (ltac:(let x := fresh "_x" in move=> x /(conj x) {x})) (only parsing) : ssripat_scope.`

It does not interact well with `+`

though...

```
Lemma and_curry (A B C : Prop) : (A /\ B -> C) -> A -> B -> C.
Proof. move=> + a b; exact. Qed.
Notation "[conj]" := (ltac:(apply and_curry)) (only parsing) : ssripat_scope.
```

works better

Hum, I guess `move`

does not nest well...

Thanks, the last version of [conj] works very smoothly!

https://github.com/ieva-itu/robustmean/blob/main/robustmean.v#L491-L503

Thanks for explaining what `iffLR`

did. I've been confused by such `/lemma`

behaviors in the past.

Last updated: Jul 15 2024 at 20:02 UTC