simp underapplied predicate

Stream: general

[Yury G. Kudryashov]

Is it possible to make simp apply p_iff_q here?

axiom p : Nat → Prop
axiom q : Nat → Prop
axiom p_iff_q : ∀ n, p n ↔ q n

example : p = q := by simp

[Mario Carneiro]

no, you would have to make the underapplied version a simp rule as well if you want this

[Yury G. Kudryashov]

#xy: I define an inductive predicate and generate an iff lemma for it using @[mk_iff]. Later, I want to generate an instance about the predicate by rewriting using the iff lemma (I have an instance for the RHS of the iff).

[Yury G. Kudryashov]

I guess, I'll have to read and understand the code of mk_iff.

[Mario Carneiro]

How would mk_iff generate this kind of thing?

[Mario Carneiro]

Normally it won't just be two equal constants unless your predicate is just a newtype wrapper

[Yury G. Kudryashov]

In practice, it is

@[mk_iff]
structure IsSubsemigroup {M : Type*} [Mul M] (s : Set M) : Prop where
  mul_mem : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s

instance : SomeClass M IsSubsemigroup :=

[Mario Carneiro]

okay, so what's the p = q here?

[Yury G. Kudryashov]

I have a generic instance of SomeClass that generates an instance for the predicate fun s => ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s

[Yury G. Kudryashov]

I want to rewrite using a lemma generated by mk_iff or something similar, then apply this generic instance.

[Yury G. Kudryashov]

It's in branch#YK-bundled-set

[Mario Carneiro]

Hm, I would avoid doing this in general, newtype wrappers are generally not equal (as types) to the things they wrap

[Yury G. Kudryashov]

This is in Prop

[Mario Carneiro]

in this case you can do it, but I'm not sure we want to build much infrastructure for this style of proof

[Mario Carneiro]

why not just rw [show IsSubsemigroup = _ by ext x; simp]?

[Yury G. Kudryashov]

I'm using rw [show IsSubsemigroup = _ from funext (fun s ↦ propext (IsSubsemigroup_iff s))] now

[Mario Carneiro]

does simp not trigger once you have the funext?

[Yury G. Kudryashov]

rw [show IsSubsemigroup = _ from funext fun _ ↦ by simp [IsSubsemigroup_iff]] doesn't work because it fails to close the goal with a metavariable in the RHS by reflexivity.

[Mario Carneiro]

; rfl?

[Yury G. Kudryashov]

Thanks!

[Yury G. Kudryashov]

I'll see what's easier to make work semi-automatically.

[Yury G. Kudryashov]

I want to have this type of proof as a derive handler for BundledSet.InterPred etc from Data/BundledSet/Lattice in that branch.