show_term

Stream: new members

[Julian Berman]

What kinds of things cause show_term to show terms that don't solve the goal? I take it there's some "hand wavy" reconstruction happening in how it works, but is there anything one should know in general about when this goes wrong? I've seen this a number of times, but as a concrete example, the below from formalising_mathematics produces a term that doesn't close the goal, and also confusingly has id in it --

example {X Y Z : Type} {f : X → Y} {g : Y → Z} (hf : function.injective f) (hg : function.injective g) : function.injective (g ∘ f) :=
begin
  show_term {
    intros x y hxy,
    apply hf,
    apply hg,
    apply hxy,
  }
end

for me produces a term exact id (λ (x y : X) (hxy : (g ∘ f) x = (g ∘ f) y), hf x y (hg (f x) (f y) hxy)) which errors when substituted. (Obviously λ x y hxy, hf (hg hxy) works)

[Kevin Buzzard]

This is a known issue which is to do with the \{{ brackets in the definition of function.injective. I suspect there will be an issue somewhere.

[Julian Berman]

Ah, thanks, I see a couple of open mathlib issues that mention show_term.

[Julian Berman]

And now I've found https://github.com/leanprover-community/lean/issues/394 which I think is the one you pointed out, thank you!