hypothesis or implication

Stream: new members

[Patrick Thomas]

Is there a preference between ... (H1 : P) |- Q and ... |- P -> Q?

[Yury G. Kudryashov]

I prefer the former unless the proof is by pattern matching.

[Yury G. Kudryashov]

Because it assigns a readable name to H1 : P right away.

[Patrick Thomas]

I was thinking along the same lines, but was curious if there was a reason to use the other.

[Yury G. Kudryashov]

Consider

def my_id (x : α) : α := x
def my_id2 : α → α := λ x, x

With the latter definition you can dsimp [my_id2] in something like my_id2 = id. With my_id you can only dsimp [my_id] on an applied function.

[Patrick Thomas]

I'm not sure if I understand, maybe because I don't know the details behind simp?

[Patrick Thomas]

Is it just doing replacements?

[Kyle Miller]

#print prefix my_id
/- gives:
my_id.equations._eqn_1 : ∀ {α : Type u_1} (x : α), my_id x = x
-/
#print prefix my_id2
/- gives:
my_id2.equations._eqn_1 : ∀ {α : Type u_1}, my_id2 = λ (x : α), x
-/

These are automatically generated lemmas called "equation lemmas," and they're what dsimp/simp will use if you put my_id or my_id2 into the list of simp lemmas.

[Kyle Miller]

(I'm not sure I've seen a case yet where this matters, but it seems worth knowing that there can be a difference.)

[Patrick Thomas]

So the first can only be used to replace a variable, and the second can only be used to replace a function?

[Kyle Miller]

The second one can replace my_id2 wherever it might appear, but the first can only be used to replace instances of my_id (...), cases where my_id is applied to an argument.

[Patrick Thomas]

Oh, I see. Thank you.

[Kyle Miller]

For example, if you dsimp [my_id2] to the expression my_id2 (y+2), it would first become (λ (x : α), x) (y+2), and then it would be beta reduced to y+2. Or in Yury's example, my_id2 = id would become (λ (x : α), x) = id, but my_id = id would fail to make any progress with dsimp [my_id].

[Patrick Thomas]

Because my_id = id doesn't have something applied to my_id.

[Patrick Thomas]

That makes sense.

[Eric Wieser]

Note that this is only relevant to defs. If you're just proving a lemma, then there are no equations._eqn_n generated.

[Eric Wieser]

Note also that pattern matching behaves like my_id:

def my_id3 : α → α
| x := x

#print prefix my_id3
/- gives:
my_id3.equations._eqn_1 : ∀ {α : Sort u_1} (x : α), my_id3 x = x
-/