Stream: math-comp users

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


view this post on Zulip 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?

view this post on Zulip Kenji Maillard (Oct 19 2021 at 12:59):

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

view this post on Zulip Takafumi Saikawa (Oct 19 2021 at 13:01):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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 ;-)

view this post on Zulip 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).

view this post on Zulip Cyril Cohen (Oct 19 2021 at 13:12):

I would rather call it /[conj]

view this post on Zulip Cyril Cohen (Oct 19 2021 at 13:14):

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

view this post on Zulip Enrico Tassi (Oct 19 2021 at 13:16):

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

view this post on Zulip 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...

view this post on Zulip Enrico Tassi (Oct 19 2021 at 13:17):

Damn, you managed to convince me

view this post on Zulip Cyril Cohen (Oct 19 2021 at 13:18):

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

view this post on Zulip Cyril Cohen (Oct 19 2021 at 13:18):

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

view this post on Zulip Enrico Tassi (Oct 19 2021 at 13:18):

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

view this post on Zulip Cyril Cohen (Oct 19 2021 at 13:19):

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

view this post on Zulip 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:

view this post on Zulip Cyril Cohen (Oct 19 2021 at 13:22):

Is there a view that does this?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Oct 19 2021 at 13:23):

Show Proof will tell you

view this post on Zulip Cyril Cohen (Oct 19 2021 at 13:24):

Enrico Tassi said:

Show Proof will tell you

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

view this post on Zulip Cyril Cohen (Oct 19 2021 at 13:24):

:scream:

view this post on Zulip Enrico Tassi (Oct 19 2021 at 13:24):

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

view this post on Zulip 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....

view this post on Zulip Cyril Cohen (Oct 19 2021 at 13:26):

This is terrible...

view this post on Zulip Enrico Tassi (Oct 19 2021 at 13:26):

Maybe /[Pdna] ;-)

view this post on Zulip Cyril Cohen (Oct 19 2021 at 13:26):

Pdna?

view this post on Zulip Enrico Tassi (Oct 19 2021 at 13:27):

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

view this post on Zulip Enrico Tassi (Oct 19 2021 at 13:27):

Time to go back to work ;-)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Oct 19 2021 at 13:35):

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

view this post on Zulip 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

view this post on Zulip 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: Mar 29 2024 at 00:41 UTC