translating `prod.lex_wf` to Lean 4

Stream: lean4

[Arien Malec]

I have (in a termination clause) in Lean 3 :Prod.lex_wf lt_wf lt_wf

My first thought, since we are reasoning on the length of lists, and based on "is something like well founded", is to translate to:

Prod.instWellFoundedRelationProd Nat.lt_wfRel Nat.lt_wfRel, but it doesn't typecheck. I may also be confused about what Lean 4 termination_by' wants...

[Mario Carneiro]

Prod.lex_wf should be a previous definition, and you should be referring to it

[Mario Carneiro]

The lean 4 way of writing this is somewhat different, but if you are sticking to a straight port then those are just previous declarations that have hopefully been #aligned or ported

[Arien Malec]

source diving...

Maybe this does the same work?

instance [ha : WellFoundedRelation α] [hb : WellFoundedRelation β] : WellFoundedRelation (α × β) :=
  lex ha hb

[Arien Malec]

I don't think so. I'm source diving through Init.WF and don't see a theorem tagged the same way as prod.lex.wf

[Arien Malec]

that instWellFoundedRelationProd is the the result of the above instance, right?

[Arien Malec]

I'll go read up on Lean 4 termination proofs.