problem with the apply tactic

[bodeveix]

The apply has a strange behaviour when the goal is quantified. In the following proof,
apply (λ h, h)
lets the goal unchanged as expected.
However, if we try to explicitly type the parameter h, the tactic apply fails. When looking at the unification problem, it seems that the universal variable x of the goal is discharged before the unification attempt, which makes it fail.

symbol Prop: TYPE;
symbol π: Prop → TYPE;
symbol Set: TYPE;
constant symbol τ: Set → TYPE;

constant symbol ∀ [a] : (τ a → Prop) → Prop;
notation ∀ quantifier;
rule π (∀ $f) ↪ Π x, π ($f x);

symbol T: Set;
symbol P : τ T → Prop;

symbol bug: π (`∀ (x: τ T), P x) ≔
begin
print;
debug +u;
  apply (λ (h : π (`∀ x: τ T, P x)), h ); // error
//  apply (λ h, h); // correct
print;
  admit;
end;

[bodeveix]

It seems the problem can be fixed by modifying line 247 of tactic.ml:

    | Some (_, a) -> count_products c a **- count_products c gt.goal_type**     

[fblanqui]

Hi Jean-Paul. Thanks for your issue, and your suggestion. Note also that in case you have problems with apply, you can always use refine instead. But your tactic call is strange anyway. Your goal is (`∀ x, P x). (λ h, h) cannot be of this type. You can see this if instead you write: refine λ h, h, or perhaps better: refine λ x, x.

[bodeveix]

Hello Frédéric, Thanks for your reply. (λ h, h) was used to make an apply, not a refine. So it should let the goal unchanged. In the original proof, the purpose of the apply was to change the goal into an equivalent one modulo rewriting rules by giving a type to the parameter h. And yes, I plan to replace apply by refine in the proof generator (from Event-B). In fact, after the suggested fix, apply (λ h, h) fails but apply (λ h: \pi (`∀ x, P x), h) succeeds. So discovering the correct number of parameters is not so easy but Coq succeeds to apply both the generic and the instantiated identity... Jean-Paul

…

Le 26 août 2024 à 21:08, Frédéric Blanqui ***@***.***> a écrit : Hi Jean-Paul. Thanks for your issue, and your suggestion. Note also that in case you have problems with apply, you can always use refine instead. But your tactic call is strange anyway. Your goal is (`∀ x, P x). (λ h, h) cannot be of this type. You can see this if instead you write: refine λ h, h, or perhaps better: refine λ x, x. — Reply to this email directly, view it on GitHub <#1131 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AEH7HKFZRR3JJPVY537LB4LZTN4JVAVCNFSM6AAAAABND4QEP2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGMJQHA4DGNJZGY>. You are receiving this because you authored the thread.

[fblanqui]

I still don't understand why you would like to do some apply that does not change the goal.
And this doesn't correspond to the semantics of (apply t), which is defined as (refine t _ ... _), which consists in instantiating the goal metavariable by (t _ ... _).
Trying your suggestion makes other libraries fail, where t is of arity 2 (e.g. ∨ₑ p for some p) and you want (apply t) to be (refine t _ _) whatever the arity of the goal is.
It is not clear to me how to define a better version of apply, but PRs are welcome.

[bodeveix]

I have a definition x <> y := not (x = y) and a goal : \pi (P x y => x <> y) apply (fun (h: \pi (P x y => not (x = y)) => (P x y => x <> y), h) should transform the goal into \pi (P x y => not (x = y)) So even if we apply (an instance of ) the identity fonction, it has a syntactic effect on the goal. It would be possible to use simplify here but the purpose is to obtain exactly what is done by a given Event-B proof step.

…

Le 27 août 2024 à 12:11, Frédéric Blanqui ***@***.***> a écrit : I still don't understand why you would like to do some apply that does not change the goal. And this doesn't correspond to the semantics of (apply t), which is defined as (refine t _ ... _), which consists in instantiating the goal metavariable by (t _ ... _). Trying your suggestion makes other libraries fail, where t is of arity 2 (e.g. ∨ₑ p for some p) and you want (apply t) to be (refine t _ _) whatever the arity of the goal is. It is not clear to me how to define a better version of apply, but PRs are welcome. — Reply to this email directly, view it on GitHub <#1131 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AEH7HKGXJHRYEYJCCZAECJLZTRGERAVCNFSM6AAAAABND4QEP2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGMJSGEYTCOJSG4>. You are receiving this because you authored the thread.

[bodeveix]

Can you send me the failing proof? Thanks.

…

Le 27 août 2024 à 13:57, Jean-Paul Bodeveix ***@***.***> a écrit : I have a definition x <> y := not (x = y) and a goal : \pi (P x y => x <> y) apply (fun (h: \pi (P x y => not (x = y)) => (P x y => x <> y), h) should transform the goal into \pi (P x y => not (x = y)) So even if we apply (an instance of ) the identity fonction, it has a syntactic effect on the goal. It would be possible to use simplify here but the purpose is to obtain exactly what is done by a given Event-B proof step. > Le 27 août 2024 à 12:11, Frédéric Blanqui ***@***.*** ***@***.***>> a écrit : > > > I still don't understand why you would like to do some apply that does not change the goal. > And this doesn't correspond to the semantics of (apply t), which is defined as (refine t _ ... _), which consists in instantiating the goal metavariable by (t _ ... _). > Trying your suggestion makes other libraries fail, where t is of arity 2 (e.g. ∨ₑ p for some p) and you want (apply t) to be (refine t _ _) whatever the arity of the goal is. > It is not clear to me how to define a better version of apply, but PRs are welcome. > > — > Reply to this email directly, view it on GitHub <#1131 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AEH7HKGXJHRYEYJCCZAECJLZTRGERAVCNFSM6AAAAABND4QEP2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGMJSGEYTCOJSG4>. > You are receiving this because you authored the thread. >

[fblanqui]

You'll see it if you do make tests: this is in the stdlib.

[fblanqui]

the purpose of the apply was to change the goal into an equivalent one modulo rewriting rules by giving a type to the parameter h.

Do you mean a type different from the one that is already there but not displayed? To display abstraction domains, use flag "print_domains" on.

apply (λ (h : π (`∀ x: τ T, P x)), h );
apply (λ h:π((Q x y ⇒ not(x = y)) ⇒ (Q x y ⇒ x <> y)), h) (λ z, z)

work with #1279:

symbol Set: TYPE;
constant symbol τ: Set → TYPE;

symbol Prop: TYPE;
symbol π: Prop → TYPE;

constant symbol ∀ [a] : (τ a → Prop) → Prop;
notation ∀ quantifier;
rule π (∀ $f) ↪ Π x, π ($f x);

symbol T: Set;
symbol P : τ T → Prop;

symbol test1: π (`∀ x, P x) ≔
begin
print;
apply λ h, h;
print;
abort;

symbol test2: π (`∀ x, P x) ≔
begin
print;
apply λ h:π(`∀ x:τ T, P x), h;
print;
abort;

symbol not:Prop → Prop;

symbol =: τ T → τ T → Prop;
notation = infix 10;

symbol <> x y ≔ not (x = y);
notation <> infix 10;

symbol ⇒: Prop → Prop → Prop;
notation ⇒ infix 5;
rule π($x ⇒ $y) ↪ π $x → π $y;

symbol Q: τ T → τ T → Prop;

symbol test3 x y: π(Q x y ⇒ x <> y) ≔
begin
assume x y;
print;
apply (λ h:π((Q x y ⇒ not(x = y)) ⇒ (Q x y ⇒ x <> y)), h) (λ z, z);
print;
abort;