## Stream: math-comp users

### Topic: how to combine two top assumptions with `conj`

#### Takafumi Saikawa (Oct 19 2021 at 12:52):

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?

#### Kenji Maillard (Oct 19 2021 at 12:59):

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

#### Takafumi Saikawa (Oct 19 2021 at 13:01):

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

#### Enrico Tassi (Oct 19 2021 at 13:01):

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.

#### Takafumi Saikawa (Oct 19 2021 at 13:03):

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?

#### Reynald Affeldt (Oct 19 2021 at 13:06):

(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.
``````

#### Enrico Tassi (Oct 19 2021 at 13:07):

`/[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 ;-)

#### Enrico Tassi (Oct 19 2021 at 13:11):

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).

#### Cyril Cohen (Oct 19 2021 at 13:12):

I would rather call it `/[conj]`

#### Cyril Cohen (Oct 19 2021 at 13:14):

Note that `move=> /conj/[apply]` should also do the job.

#### Enrico Tassi (Oct 19 2021 at 13:16):

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

#### Cyril Cohen (Oct 19 2021 at 13:16):

Cyril Cohen said:

Note that `move=> /conj/[apply]` should also do the job.

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

#### Enrico Tassi (Oct 19 2021 at 13:17):

Damn, you managed to convince me

#### Cyril Cohen (Oct 19 2021 at 13:18):

`move=> ab /(conj ab)` works though...

#### Cyril Cohen (Oct 19 2021 at 13:18):

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

#### Enrico Tassi (Oct 19 2021 at 13:18):

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

#### Cyril Cohen (Oct 19 2021 at 13:19):

Nop... `move=> /(@conj _ _)` does not work :-(

#### Cyril Cohen (Oct 19 2021 at 13:20):

``````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:

#### Cyril Cohen (Oct 19 2021 at 13:22):

Is there a view that does this?

#### Emilio Jesús Gallego Arias (Oct 19 2021 at 13:22):

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

#### Cyril Cohen (Oct 19 2021 at 13:23):

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.

#### Enrico Tassi (Oct 19 2021 at 13:23):

`Show Proof` will tell you

#### Cyril Cohen (Oct 19 2021 at 13:24):

Enrico Tassi said:

`Show Proof` will tell you

Thanks!! Indeed the view `iffLR` was implicitly used ...

:scream:

#### Enrico Tassi (Oct 19 2021 at 13:24):

Anyway, `/[conj]` could be made to work... why not

#### Cyril Cohen (Oct 19 2021 at 13:25):

Cyril Cohen said:

Enrico Tassi said:

`Show Proof` will tell you

Thanks!! 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`....

#### Cyril Cohen (Oct 19 2021 at 13:26):

This is terrible...

#### Enrico Tassi (Oct 19 2021 at 13:26):

Maybe `/[Pdna]` ;-)

`Pdna`?

#### Enrico Tassi (Oct 19 2021 at 13:27):

where `=> /andP[]/[Pdna]` is the identity :crazy:

#### Enrico Tassi (Oct 19 2021 at 13:27):

Time to go back to work ;-)

#### Cyril Cohen (Oct 19 2021 at 13:28):

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

#### Cyril Cohen (Oct 19 2021 at 13:32):

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

#### Enrico Tassi (Oct 19 2021 at 13:35):

Hum, I guess `move` does not nest well...

#### Takafumi Saikawa (Oct 19 2021 at 14:34):

Thanks, the last version of [conj] works very smoothly!
https://github.com/ieva-itu/robustmean/blob/main/robustmean.v#L491-L503

#### Paolo Giarrusso (Oct 19 2021 at 21:41):

Thanks for explaining what `iffLR` did. I've been confused by such `/lemma` behaviors in the past.

Last updated: Jan 29 2023 at 18:03 UTC