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

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

: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] ;-)

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

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: Oct 13 2024 at 01:02 UTC